Changeset 3552
Legend:
- Unmodified
- Added
- Removed
-
LTS/Final.ma
r3549 r3552 86 86 qed. 87 87 88 lemma is_multiset_mem_neq_zero : ∀A : DeqSet.89 ∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.90 #A #l elim l [ #x *] #x #xs #IH #y *91 [ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct92 | #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //93 ]94 qed.95 96 lemma mem_neq_zero_is_multiset : ∀A : DeqSet.97 ∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.98 #A #l elim l [ #x * #H cases H % ]99 #x #xs #IH #y normalize inversion(y==x) normalize nodelta100 #H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption101 qed.102 103 lemma is_permutation_mem : ∀A :DeqSet.104 ∀l1,l2 : list A.∀x : A.mem … x l1 →105 is_permutation A l1 l2 → mem … x l2.106 #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption107 qed.108 109 lemma mem_list : ∀A : Type[0].110 ∀l : list A.∀x : A.mem … x l →111 ∃l1,l2.l=l1 @ [x] @ l2.112 #A #l elim l113 [ #x *]114 #x #xs #IH #y *115 [ #EQ destruct %{[]} %{xs} %116 | #H cases(IH … H) #l1 * #l2 #EQ destruct117 %{(x :: l1)} %{l2} %118 ]119 qed.120 121 lemma is_permutation_case : ∀A : DeqSet.122 ∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →123 ∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.124 #A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]125 #l1 * #l2 #EQ destruct %{l1} %{l2} % //126 @(permute_equal_right … [x]) @permute_append_all127 @(is_permutation_transitive … H)128 /4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/129 qed.130 88 131 89 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) 140 98 >is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); % 141 qed.142 143 definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝144 λA,B,l,f,x,prf.f x prf.145 146 lemma proof_irrelevance_temp : ∀A,B : Type[0].∀l : list A.147 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.148 applica … f x prf1 = applica … f x prf2.149 //150 qed.151 152 lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.153 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.154 f x prf1 = f x prf2.155 #A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp156 qed.157 158 lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.159 ∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) →160 dependent_map … l f = dependent_map … l g.161 #A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);162 @eq_f2 // @IH //163 qed.164 165 lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.166 ∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).167 ∀perm : is_permutation A l1 l2.168 (∀a : A.169 ∀prf : mem … a l1.f a prf = g a ?) →170 is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).171 [2: @(is_permutation_mem … perm) //]172 #A #B #l1 elim l1 -l1173 [ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]174 #x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct175 >dependent_map_append >dependent_map_append @permute_append_l1 >associative_append176 whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);177 whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);178 generalize in ⊢ (? → ???(??(??%)?));179 #prf1 #prf2180 >(proof_irrelevance_all … g x prf1 prf2)181 @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);182 whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1183 @(is_permutation_transitive …(IH … (l3@l4) …) )184 [2: assumption185 |3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]186 | @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //187 ]188 >dependent_map_append @is_permutation_append189 [ >dependent_map_extensional [ @is_permutation_eq | // |]190 | >dependent_map_extensional [ @is_permutation_eq | // |]191 ]192 99 qed. 193 100 -
LTS/Permutation.ma
r3527 r3552 15 15 include "basics/deqsets.ma". 16 16 include "arithmetics/nat.ma". 17 include "utils.ma". 17 18 18 19 record multiset (A : DeqSet) : Type[0] ≝ … … 42 43 interpretation "m_union" 'm_un x y = (multiset_union ? x y). 43 44 44 notation > "hvbox(C break ≅A)" non associative with precedence 45 for @{'m_eq $C $A}.45 notation > "hvbox(C break ⩬ A)" non associative with precedence 45 for @{'m_eq $C $A}. 45 46 interpretation "m_eq" 'm_eq x y = (m_eq ? x y). 46 47 … … 51 52 interpretation "singleton_m" 'sing x = (singleton ? x). 52 53 53 lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union … m1 m2) ≅ (multiset_union …m2 m1).54 normalize // 55 qed. 56 57 lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ≅m1 ⊔ (m2 ⊔ m3).58 normalize // 59 qed. 60 61 lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ≅m.62 normalize // 63 qed. 64 65 lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ≅m.54 lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union ? m1 m2) ⩬ (multiset_union ? m2 m1). 55 normalize // 56 qed. 57 58 lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ⩬ m1 ⊔ (m2 ⊔ m3). 59 normalize // 60 qed. 61 62 lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ⩬ m. 63 normalize // 64 qed. 65 66 lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ⩬ m. 66 67 normalize // 67 68 qed. … … 76 77 77 78 lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A. 78 m1 ≅ m2 → m ⊔ m1 ≅m ⊔ m2.79 m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2. 79 80 #A #m #m1 #m2 normalize // 80 81 qed. 81 82 82 lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ≅ m ⊔ m2 → m1 ≅m2.83 lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2. 83 84 normalize #A #m #m1 #m2 #H #a /2/ 84 85 qed. 85 86 86 87 lemma list_to_multiset_append : ∀A.∀l1,l2. 87 list_to_multiset A (l1 @ l2) ≅list_to_multiset … l1 ⊔ list_to_multiset … l2.88 list_to_multiset A (l1 @ l2) ⩬ list_to_multiset … l1 ⊔ list_to_multiset … l2. 88 89 #A #l1 elim l1 89 90 [ normalize //] … … 95 96 qed. 96 97 98 lemma is_multiset_mem_neq_zero : ∀A : DeqSet. 99 ∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O. 100 #A #l elim l [ #x *] #x #xs #IH #y * 101 [ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct 102 | #H normalize cases(?==?) normalize [ % #EQ destruct] @IH // 103 ] 104 qed. 105 106 lemma mem_neq_zero_is_multiset : ∀A : DeqSet. 107 ∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l. 108 #A #l elim l [ #x * #H cases H % ] 109 #x #xs #IH #y normalize inversion(y==x) normalize nodelta 110 #H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption 111 qed. 97 112 98 113 definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝ 99 λA,l1,l2.list_to_multiset … l1 ≅ list_to_multiset … l2. 114 λA,l1,l2.list_to_multiset … l1 ⩬ list_to_multiset … l2. 115 116 lemma is_permutation_mem : ∀A :DeqSet. 117 ∀l1,l2 : list A.∀x : A.mem … x l1 → 118 is_permutation A l1 l2 → mem … x l2. 119 #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption 120 qed. 100 121 101 122 lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l. … … 193 214 ] 194 215 qed. 216 217 lemma is_permutation_case : ∀A : DeqSet. 218 ∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l → 219 ∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2. 220 #A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%] 221 #l1 * #l2 #EQ destruct %{l1} %{l2} % // 222 @(permute_equal_right … [x]) @permute_append_all 223 @(is_permutation_transitive … H) 224 /4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/ 225 qed. 226 227 lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A. 228 ∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B). 229 ∀perm : is_permutation A l1 l2. 230 (∀a : A. 231 ∀prf : mem … a l1.f a prf = g a ?) → 232 is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)). 233 [2: @(is_permutation_mem … perm) //] 234 #A #B #l1 elim l1 -l1 235 [ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ] 236 #x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct 237 >dependent_map_append >dependent_map_append @permute_append_l1 >associative_append 238 whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%); 239 whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?); 240 generalize in ⊢ (? → ???(??(??%)?)); 241 #prf1 #prf2 242 >(proof_irrelevance_all … g x prf1 prf2) 243 @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%); 244 whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1 245 @(is_permutation_transitive …(IH … (l3@l4) …) ) 246 [2: assumption 247 |3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //] 248 | @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 // 249 ] 250 >dependent_map_append @is_permutation_append 251 [ >dependent_map_extensional [ @is_permutation_eq | // |] 252 | >dependent_map_extensional [ @is_permutation_eq | // |] 253 ] 254 qed. -
LTS/Vm.ma
r3549 r3552 821 821 |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH 822 822 ] 823 qed.824 825 let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝826 (match l return λx.l=x → ? with827 [ nil ⇒ λ_.nil ?828 | cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?)829 ])(refl …).830 [ >prf %% | >prf %2 assumption]831 qed.832 833 lemma dependent_map_append : ∀A,B,l1,l2,f.834 dependent_map A B (l1 @ l2) (λa,prf.f a prf) =835 (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)).836 [2: @hide_prf /2/ | 3: @hide_prf /2/]837 #A #B #l1 elim l1 normalize /2/838 qed.839 840 lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f.841 ∀EQ:l1 = l2.842 dependent_map A B l1 (λa,prf.f a prf) =843 dependent_map A B l2 (λa,prf.f a ?).844 [2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ]845 823 qed. 846 824
Note: See TracChangeset
for help on using the changeset viewer.