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

 1 edited
Legend:
 Unmodified
 Added
 Removed

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