| 1 | (**************************************************************************) |
|---|
| 2 | (* ___ *) |
|---|
| 3 | (* ||M|| *) |
|---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
|---|
| 5 | (* ||T|| *) |
|---|
| 6 | (* ||I|| Developers: *) |
|---|
| 7 | (* ||T|| The HELM team. *) |
|---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
|---|
| 9 | (* \ / *) |
|---|
| 10 | (* \ / This file is distributed under the terms of the *) |
|---|
| 11 | (* v GNU General Public License Version 2 *) |
|---|
| 12 | (* *) |
|---|
| 13 | (**************************************************************************) |
|---|
| 14 | |
|---|
| 15 | include "basics/deqsets.ma". |
|---|
| 16 | include "arithmetics/nat.ma". |
|---|
| 17 | include "utils.ma". |
|---|
| 18 | |
|---|
| 19 | record multiset (A : DeqSet) : Type[0] ≝ |
|---|
| 20 | { mult : (A → ℕ) }. |
|---|
| 21 | |
|---|
| 22 | definition m_eq : ∀A.multiset A → multiset A → Prop ≝ |
|---|
| 23 | λA,m1,m2.∀a.mult … m1 a = mult … m2 a. |
|---|
| 24 | |
|---|
| 25 | lemma m_eq_reflexive : ∀A.reflexive … (m_eq A). |
|---|
| 26 | // |
|---|
| 27 | qed. |
|---|
| 28 | |
|---|
| 29 | lemma m_eq_symmetric : ∀A.symmetric … (m_eq A). |
|---|
| 30 | // |
|---|
| 31 | qed. |
|---|
| 32 | |
|---|
| 33 | lemma m_eq_transitive : ∀A.transitive … (m_eq A). |
|---|
| 34 | // |
|---|
| 35 | qed. |
|---|
| 36 | |
|---|
| 37 | definition empty_multiset : ∀A.multiset A ≝ λA.mk_multiset … (λ_.O). |
|---|
| 38 | definition singleton : ∀A : DeqSet.A → multiset A ≝ λA,a.mk_multiset … (λx.if x == a then 1 else O). |
|---|
| 39 | definition multiset_union : ∀A.multiset A → multiset A → multiset A ≝ |
|---|
| 40 | λA,m1,m2.mk_multiset … (λx.mult … m1 x + mult … m2 x). |
|---|
| 41 | |
|---|
| 42 | notation "hvbox(C break ⊔ A)" left associative with precedence 55 for @{ 'm_un $C $A }. |
|---|
| 43 | interpretation "m_union" 'm_un x y = (multiset_union ? x y). |
|---|
| 44 | |
|---|
| 45 | notation > "hvbox(C break ⩬ A)" non associative with precedence 45 for @{'m_eq $C $A}. |
|---|
| 46 | interpretation "m_eq" 'm_eq x y = (m_eq ? x y). |
|---|
| 47 | |
|---|
| 48 | notation "ⓧ" with precedence 90 for @{'empty_m}. |
|---|
| 49 | interpretation "empty_mult" 'empty_m = (empty_multiset ?). |
|---|
| 50 | |
|---|
| 51 | notation "❨ term 19 C ❩ " with precedence 10 for @{ 'sing $C}. |
|---|
| 52 | interpretation "singleton_m" 'sing x = (singleton ? x). |
|---|
| 53 | |
|---|
| 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. |
|---|
| 67 | normalize // |
|---|
| 68 | qed. |
|---|
| 69 | |
|---|
| 70 | include "basics/lists/list.ma". |
|---|
| 71 | |
|---|
| 72 | let rec list_to_multiset (A : DeqSet) (l : list A) on l : multiset A ≝ |
|---|
| 73 | match l with |
|---|
| 74 | [ nil ⇒ ⓧ |
|---|
| 75 | | cons x xs ⇒ ❨ x ❩ ⊔ list_to_multiset … xs |
|---|
| 76 | ]. |
|---|
| 77 | |
|---|
| 78 | lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A. |
|---|
| 79 | m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2. |
|---|
| 80 | #A #m #m1 #m2 normalize // |
|---|
| 81 | qed. |
|---|
| 82 | |
|---|
| 83 | lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2. |
|---|
| 84 | normalize #A #m #m1 #m2 #H #a /2/ |
|---|
| 85 | qed. |
|---|
| 86 | |
|---|
| 87 | lemma list_to_multiset_append : ∀A.∀l1,l2. |
|---|
| 88 | list_to_multiset A (l1 @ l2) ⩬ list_to_multiset … l1 ⊔ list_to_multiset … l2. |
|---|
| 89 | #A #l1 elim l1 |
|---|
| 90 | [ normalize //] |
|---|
| 91 | #x #xs #IH #l2 change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (??%?); |
|---|
| 92 | change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (???(??%?)); |
|---|
| 93 | whd in match (list_to_multiset ??); @m_eq_symmetric |
|---|
| 94 | @(m_eq_transitive … (m_union_associative …)) |
|---|
| 95 | @m_eq_union_left_cancellable @m_eq_symmetric @IH |
|---|
| 96 | qed. |
|---|
| 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. |
|---|
| 112 | |
|---|
| 113 | definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝ |
|---|
| 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. |
|---|
| 121 | |
|---|
| 122 | lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l. |
|---|
| 123 | // |
|---|
| 124 | qed. |
|---|
| 125 | |
|---|
| 126 | lemma is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 → |
|---|
| 127 | is_permutation A (x :: l1) (x :: l2). |
|---|
| 128 | normalize // |
|---|
| 129 | qed. |
|---|
| 130 | |
|---|
| 131 | lemma permute_append_all : ∀A.∀l1,l2,l3,l4.is_permutation A (l1@l2) (l3@l4) → |
|---|
| 132 | is_permutation A (l2 @l1) (l4@l3). |
|---|
| 133 | #A #l1 #l2 #l3 #l4 normalize #H #a >(list_to_multiset_append … a) |
|---|
| 134 | >(list_to_multiset_append … a) >m_union_commutative |
|---|
| 135 | >m_union_commutative in ⊢ (???%); <list_to_multiset_append <list_to_multiset_append @H |
|---|
| 136 | qed. |
|---|
| 137 | |
|---|
| 138 | lemma permute_append_l1 : ∀A.∀l1,l2,l3.is_permutation A l1 (l2 @ l3) → |
|---|
| 139 | is_permutation A l1 (l3 @ l2). |
|---|
| 140 | #A #l1 #l2 #l3 #H #a >list_to_multiset_append >m_union_commutative <list_to_multiset_append @H |
|---|
| 141 | qed. |
|---|
| 142 | |
|---|
| 143 | lemma is_permutation_commutative : ∀A.symmetric … (is_permutation A). |
|---|
| 144 | // |
|---|
| 145 | qed. |
|---|
| 146 | |
|---|
| 147 | lemma is_permutation_transitive : ∀A.transitive … (is_permutation A). |
|---|
| 148 | // |
|---|
| 149 | qed. |
|---|
| 150 | |
|---|
| 151 | lemma is_permutation_append_left_cancellable : ∀A.∀l,l1,l2.is_permutation A l1 l2 → |
|---|
| 152 | is_permutation A (l @ l1) (l @ l2). |
|---|
| 153 | #A #l #l1 #l2 #H #a >list_to_multiset_append >list_to_multiset_append |
|---|
| 154 | @m_eq_union_left_cancellable @H |
|---|
| 155 | qed. |
|---|
| 156 | |
|---|
| 157 | lemma is_permutation_append : ∀A.∀l1,l2,l3,l4. |
|---|
| 158 | is_permutation A l1 l2 → is_permutation A l3 l4 → |
|---|
| 159 | is_permutation A (l1 @ l3) (l2 @ l4). |
|---|
| 160 | #A #l1 #l2 #l3 #l4 #H1 #H2 #a >list_to_multiset_append |
|---|
| 161 | >list_to_multiset_append normalize >H1 >H2 % |
|---|
| 162 | qed. |
|---|
| 163 | |
|---|
| 164 | lemma permute_equal_right : ∀A.∀l1,l2,l. |
|---|
| 165 | is_permutation A (l1 @ l) (l2 @ l) → is_permutation A l1 l2. |
|---|
| 166 | #A #l1 #l2 #l normalize #H #a lapply(H a) >list_to_multiset_append >list_to_multiset_append |
|---|
| 167 | >m_union_commutative >m_union_commutative in ⊢ (???% → ?); |
|---|
| 168 | normalize // |
|---|
| 169 | qed. |
|---|
| 170 | |
|---|
| 171 | lemma permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. |
|---|
| 172 | (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) |
|---|
| 173 | →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) |
|---|
| 174 | →is_permutation A |
|---|
| 175 | (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) |
|---|
| 176 | (((x ::l4 @y ::l3) @l8) @l9)). |
|---|
| 177 | #A #l1 #l2 #l3 #l4 #l5 #l6 #l7 #l8 #l9 #x #y |
|---|
| 178 | change with ([x] @ ?) in match ([x] @ ?); |
|---|
| 179 | change with ([y] @ ?) in match ([y] @ ?); |
|---|
| 180 | >append_nil #H1 #H2 whd in match (append ???) in ⊢ (???%); |
|---|
| 181 | change with ([x] @ ?) in match ([x] @ ?) in ⊢ (???%); |
|---|
| 182 | change with ([y] @ ?) in match ([y] @ ?) in ⊢ (???%); |
|---|
| 183 | @permute_append_l1 >associative_append in ⊢ (???%); |
|---|
| 184 | <associative_append in ⊢ (???%); <associative_append in ⊢ (???%); |
|---|
| 185 | <associative_append <associative_append <associative_append |
|---|
| 186 | @(is_permutation_transitive … ((((([y]@l4)@l3)@l8)@l9)@[x])) |
|---|
| 187 | [ >associative_append >associative_append >associative_append |
|---|
| 188 | >associative_append >associative_append >associative_append |
|---|
| 189 | >associative_append >associative_append >associative_append |
|---|
| 190 | @is_permutation_append_left_cancellable |
|---|
| 191 | <associative_append in ⊢ (???%); <associative_append in ⊢ (???%); <associative_append in ⊢ (???%); |
|---|
| 192 | @permute_append_l1 |
|---|
| 193 | @(is_permutation_transitive … ([x]@l6@l5@l1@l2@l7)) |
|---|
| 194 | [2: @is_permutation_append_left_cancellable |
|---|
| 195 | @(is_permutation_transitive … ((l5 @ l1) @ ((l6@l2)@l7))) |
|---|
| 196 | [2: >associative_append in ⊢ (???%); >associative_append in ⊢ (???%); |
|---|
| 197 | @is_permutation_append |
|---|
| 198 | [2: <associative_append in ⊢ (???%); assumption |
|---|
| 199 | | >associative_append in H1 : (??%?); #H1 @permute_equal_right |
|---|
| 200 | [ @(l6@l7) | >associative_append assumption ] |
|---|
| 201 | ] |
|---|
| 202 | | <associative_append in ⊢ (??(???%)?); @is_permutation_commutative |
|---|
| 203 | @permute_append_l1 >associative_append in ⊢ (???%); @is_permutation_append_left_cancellable |
|---|
| 204 | >associative_append @permute_append_l1 // |
|---|
| 205 | ] |
|---|
| 206 | | <associative_append <associative_append <associative_append in ⊢ (???%); |
|---|
| 207 | <associative_append in ⊢ (???%); @permute_append_all @is_permutation_append_left_cancellable |
|---|
| 208 | @permute_append_all @is_permutation_append_left_cancellable @permute_append_l1 // |
|---|
| 209 | ] |
|---|
| 210 | | @permute_append_all @is_permutation_append_left_cancellable @permute_append_all |
|---|
| 211 | @is_permutation_append_left_cancellable @permute_append_all |
|---|
| 212 | @is_permutation_append_left_cancellable @permute_append_all |
|---|
| 213 | @is_permutation_append_left_cancellable @permute_append_l1 // |
|---|
| 214 | ] |
|---|
| 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. |
|---|
