Changeset 3552 for LTS/Final.ma
 Timestamp:
 Apr 9, 2015, 11:04:21 PM (5 years ago)
 File:

 1 edited
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
Note: See TracChangeset
for help on using the changeset viewer.