Changeset 3540 for LTS/Final.ma
 Timestamp:
 Mar 17, 2015, 7:33:34 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Final.ma
r3535 r3540 83 83 @(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map 84 84 [2: <EQcostlabs in ⊢ (??%?); %  // ] 85 qed. 85 qed. 86 87 lemma is_multiset_mem_neq_zero : ∀A : DeqSet. 88 ∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O. 89 #A #l elim l [ #x *] #x #xs #IH #y * 90 [ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct 91  #H normalize cases(?==?) normalize [ % #EQ destruct] @IH // 92 ] 93 qed. 94 95 lemma mem_neq_zero_is_multiset : ∀A : DeqSet. 96 ∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l. 97 #A #l elim l [ #x * #H cases H % ] 98 #x #xs #IH #y normalize inversion(y==x) normalize nodelta 99 #H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption 100 qed. 86 101 87 102 lemma is_permutation_mem : ∀A :DeqSet. 88 103 ∀l1,l2 : list A.∀x : A.mem … x l1 → 89 104 is_permutation A l1 l2 → mem … x l2. 90 cases daemon105 #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption 91 106 qed. 92 107 93 108 definition is_abelian ≝ λM : monoid. 94 109 ∀x,y : M.op … M x y = op … M y x. 110 111 lemma mem_list : ∀A : Type[0]. 112 ∀l : list A.∀x : A.mem … x l → 113 ∃l1,l2.l=l1 @ [x] @ l2. 114 #A #l elim l 115 [ #x *] 116 #x #xs #IH #y * 117 [ #EQ destruct %{[]} %{xs} % 118  #H cases(IH … H) #l1 * #l2 #EQ destruct 119 %{(x :: l1)} %{l2} % 120 ] 121 qed. 122 123 lemma is_permutation_case : ∀A : DeqSet. 124 ∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l → 125 ∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2. 126 #A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%] 127 #l1 * #l2 #EQ destruct %{l1} %{l2} % // 128 @(permute_equal_right … [x]) @permute_append_all 129 @(is_permutation_transitive … H) 130 /4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/ 131 qed. 95 132 96 133 lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) → 97 134 ∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 → 98 135 (〚l1〛 a) = (〚l2〛 a). 99 cases daemon 136 #M #Hab #l1 elim l1 l1 137 [ * // #x #xs #a #H lapply(H x) normalize >(\b (refl …)) normalize #EQ destruct] 138 #x #xs #IH #l #a #H cases(is_permutation_case … H) #l1 * #l2 * #H1 #H2 destruct 139 change with ([?]@?) in match (?::?); >big_op_associative >act_op >(IH … H1) 140 <associative_append 141 >big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1) 142 >is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); % 143 qed. 144 145 definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝ 146 λA,B,l,f,x,prf.f x prf. 147 148 lemma proof_irrelevance_temp : ∀A,B : Type[0].∀l : list A. 149 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. 150 applica … f x prf1 = applica … f x prf2. 151 // 152 qed. 153 154 lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A. 155 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. 156 f x prf1 = f x prf2. 157 #A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp 158 qed. 159 160 lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A. 161 ∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) → 162 dependent_map … l f = dependent_map … l g. 163 #A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%); 164 @eq_f2 // @IH // 100 165 qed. 101 166 … … 105 170 (∀a : A. 106 171 ∀prf : mem … a l1.f a prf = g a ?) → 107 is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).172 is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)). 108 173 [2: @(is_permutation_mem … perm) //] 109 cases daemon 174 #A #B #l1 elim l1 l1 175 [ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ] 176 #x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct 177 >dependent_map_append >dependent_map_append @permute_append_l1 >associative_append 178 whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%); 179 whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?); 180 generalize in ⊢ (? → ???(??(??%)?)); 181 #prf1 #prf2 182 >(proof_irrelevance_all … g x prf1 prf2) 183 @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%); 184 whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1 185 @(is_permutation_transitive …(IH … (l3@l4) …) ) 186 [2: assumption 187 3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/  #H6 @mem_append_l2 @mem_append_l2 //] 188  @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 // 189 ] 190 >dependent_map_append @is_permutation_append 191 [ >dependent_map_extensional [ @is_permutation_eq  // ] 192  >dependent_map_extensional [ @is_permutation_eq  // ] 193 ] 110 194 qed. 111 195
Note: See TracChangeset
for help on using the changeset viewer.