Changeset 3552

Timestamp:

Apr 9, 2015, 11:04:21 PM (6 years ago)

Author:

piccolo

Message:

closed all daemons

Location:

LTS

Files:

• Final.ma (modified) (2 diffs)
• Permutation.ma (modified) (6 diffs)
• Vm.ma (modified) (1 diff)

LTS/Final.ma

@@ -86 +86 @@
 qed.
 
-lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
-∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
-#A #l elim l [ #x *] #x #xs #IH #y *
-[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
-| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
-]
-qed.
-
-lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
-∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
-#A #l elim l [ #x * #H cases H % ]
-#x #xs #IH #y normalize inversion(y==x) normalize nodelta
-#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
-qed.
-
-lemma is_permutation_mem : ∀A :DeqSet.
-∀l1,l2 : list A.∀x : A.mem … x l1 →
-is_permutation A l1 l2 → mem … x l2.
-#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
-qed.
-
-lemma mem_list : ∀A : Type[0].
-∀l : list A.∀x : A.mem … x l → 
-∃l1,l2.l=l1 @ [x] @ l2.
-#A #l elim l
-[ #x *]
-#x #xs #IH #y *
-[ #EQ destruct %{[]} %{xs} %
-| #H cases(IH … H) #l1 * #l2 #EQ destruct
-  %{(x :: l1)} %{l2} %
-]
-qed.
-
-lemma is_permutation_case : ∀A : DeqSet.
-∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l → 
-∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
-#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
-#l1 * #l2 #EQ destruct %{l1} %{l2} % //
-@(permute_equal_right … [x]) @permute_append_all
-@(is_permutation_transitive … H) 
-/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
-qed.
 
 lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) → 
@@ -139 +97 @@
 >big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
 >is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
-qed.
-
-definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝ 
-λA,B,l,f,x,prf.f x prf.
-
-lemma proof_irrelevance_temp :  ∀A,B : Type[0].∀l : list A.
-∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
-applica … f x prf1 = applica … f x prf2.
-//
-qed.
-
-lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.
-∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
-f x prf1 = f x prf2.
-#A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp
-qed.
-
-lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.
-∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) → 
-dependent_map … l f = dependent_map … l g.
-#A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);
-@eq_f2 // @IH //
-qed.
-
-lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
-∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
-∀perm : is_permutation A l1 l2.
-(∀a : A.
- ∀prf : mem … a l1.f a prf = g a ?) → 
-is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
-[2: @(is_permutation_mem … perm) //]
-#A #B #l1 elim l1 -l1
-[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
-#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
->dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
-whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
-whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
-generalize in ⊢ (? → ???(??(??%)?));
-#prf1 #prf2
->(proof_irrelevance_all … g x prf1 prf2)
-@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
-whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
-@(is_permutation_transitive …(IH … (l3@l4) …) ) 
-[2: assumption
-|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
-| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
-]
->dependent_map_append @is_permutation_append 
-[ >dependent_map_extensional [ @is_permutation_eq | // |]
-| >dependent_map_extensional [ @is_permutation_eq | // |]
-]
 qed.
 

LTS/Permutation.ma

@@ -15 +15 @@
 include "basics/deqsets.ma".
 include "arithmetics/nat.ma".
+include "utils.ma".
 
 record multiset (A : DeqSet) : Type[0] ≝ 
@@ -42 +43 @@
 interpretation "m_union" 'm_un x y = (multiset_union ? x y).
 
-notation > "hvbox(C break ≅ A)" non associative with precedence 45 for @{'m_eq $C $A}.
+notation > "hvbox(C break ⩬ A)" non associative with precedence 45 for @{'m_eq $C $A}.
 interpretation "m_eq" 'm_eq x y = (m_eq ? x y).
 
@@ -51 +52 @@
 interpretation "singleton_m" 'sing x = (singleton ? x).
 
-lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union … m1 m2) ≅ (multiset_union … m2 m1).
-normalize //
-qed.
-
-lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ≅ m1 ⊔ (m2 ⊔ m3).
-normalize //
-qed.
-
-lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ≅ m.
-normalize //
-qed.
-
-lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ≅ m.
+lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union ? m1 m2) ⩬ (multiset_union ? m2 m1).
+normalize //
+qed.
+
+lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ⩬ m1 ⊔ (m2 ⊔ m3).
+normalize //
+qed.
+
+lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ⩬ m.
+normalize //
+qed.
+
+lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ⩬ m.
 normalize //
 qed.
@@ -76 +77 @@
 
 lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A.
-m1 ≅ m2 → m ⊔ m1 ≅ m ⊔ m2.
+m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2.
 #A #m #m1 #m2 normalize //
 qed.
 
-lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ≅ m ⊔ m2 → m1 ≅ m2.
+lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2.
 normalize #A #m #m1 #m2 #H #a /2/
 qed.
 
 lemma list_to_multiset_append : ∀A.∀l1,l2.
-list_to_multiset A (l1 @ l2) ≅ list_to_multiset … l1 ⊔ list_to_multiset … l2.
+list_to_multiset A (l1 @ l2) ⩬ list_to_multiset … l1 ⊔ list_to_multiset … l2.
 #A #l1 elim l1
 [ normalize //]
@@ -95 +96 @@
 qed.
 
+lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
+∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
+#A #l elim l [ #x *] #x #xs #IH #y *
+[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
+| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
+]
+qed.
+
+lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
+∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
+#A #l elim l [ #x * #H cases H % ]
+#x #xs #IH #y normalize inversion(y==x) normalize nodelta
+#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
+qed.
 
 definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝ 
-λA,l1,l2.list_to_multiset … l1 ≅ list_to_multiset … l2.
+λA,l1,l2.list_to_multiset … l1 ⩬ list_to_multiset … l2.
+
+lemma is_permutation_mem : ∀A :DeqSet.
+∀l1,l2 : list A.∀x : A.mem … x l1 →
+is_permutation A l1 l2 → mem … x l2.
+#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
+qed.
 
 lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l.
@@ -193 +214 @@
 ]
 qed.
+
+lemma is_permutation_case : ∀A : DeqSet.
+∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l → 
+∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
+#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
+#l1 * #l2 #EQ destruct %{l1} %{l2} % //
+@(permute_equal_right … [x]) @permute_append_all
+@(is_permutation_transitive … H) 
+/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
+qed.
+
+lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
+∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
+∀perm : is_permutation A l1 l2.
+(∀a : A.
+ ∀prf : mem … a l1.f a prf = g a ?) → 
+is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
+[2: @(is_permutation_mem … perm) //]
+#A #B #l1 elim l1 -l1
+[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
+#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
+>dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
+whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
+whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
+generalize in ⊢ (? → ???(??(??%)?));
+#prf1 #prf2
+>(proof_irrelevance_all … g x prf1 prf2)
+@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
+whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
+@(is_permutation_transitive …(IH … (l3@l4) …) ) 
+[2: assumption
+|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
+| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
+]
+>dependent_map_append @is_permutation_append 
+[ >dependent_map_extensional [ @is_permutation_eq | // |]
+| >dependent_map_extensional [ @is_permutation_eq | // |]
+]
+qed.

LTS/Vm.ma

@@ -821 +821 @@
   |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH
 ]
-qed.
-
-let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ 
-(match l return λx.l=x → ? with
-[ nil ⇒ λ_.nil ?
-| cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)
-])(refl …).
-[ >prf %% | >prf %2 assumption]
-qed.
-
-lemma dependent_map_append : ∀A,B,l1,l2,f.
-dependent_map A B (l1 @ l2) (λa,prf.f a prf) = 
-(dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).
-[2: @hide_prf /2/ | 3: @hide_prf /2/]
-#A #B #l1 elim l1 normalize /2/
-qed.
-
-lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.
-        ∀EQ:l1 = l2.
-         dependent_map A B l1 (λa,prf.f a prf) =
-         dependent_map A B l2 (λa,prf.f a ?).
-[2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]
 qed.