(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "basics/deqsets.ma". include "arithmetics/nat.ma". include "utils.ma". record multiset (A : DeqSet) : Type[0] ≝ { mult : (A → ℕ) }. definition m_eq : ∀A.multiset A → multiset A → Prop ≝ λA,m1,m2.∀a.mult … m1 a = mult … m2 a. lemma m_eq_reflexive : ∀A.reflexive … (m_eq A). // qed. lemma m_eq_symmetric : ∀A.symmetric … (m_eq A). // qed. lemma m_eq_transitive : ∀A.transitive … (m_eq A). // qed. definition empty_multiset : ∀A.multiset A ≝ λA.mk_multiset … (λ_.O). definition singleton : ∀A : DeqSet.A → multiset A ≝ λA,a.mk_multiset … (λx.if x == a then 1 else O). definition multiset_union : ∀A.multiset A → multiset A → multiset A ≝ λA,m1,m2.mk_multiset … (λx.mult … m1 x + mult … m2 x). notation "hvbox(C break ⊔ A)" left associative with precedence 55 for @{ 'm_un \$C \$A }. interpretation "m_union" 'm_un x y = (multiset_union ? x y). notation > "hvbox(C break ⩬ A)" non associative with precedence 45 for @{'m_eq \$C \$A}. interpretation "m_eq" 'm_eq x y = (m_eq ? x y). notation "ⓧ" with precedence 90 for @{'empty_m}. interpretation "empty_mult" 'empty_m = (empty_multiset ?). notation "❨ term 19 C ❩ " with precedence 10 for @{ 'sing \$C}. interpretation "singleton_m" 'sing x = (singleton ? x). lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union ? m1 m2) ⩬ (multiset_union ? m2 m1). normalize // qed. lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ⩬ m1 ⊔ (m2 ⊔ m3). normalize // qed. lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ⩬ m. normalize // qed. lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ⩬ m. normalize // qed. include "basics/lists/list.ma". let rec list_to_multiset (A : DeqSet) (l : list A) on l : multiset A ≝ match l with [ nil ⇒ ⓧ | cons x xs ⇒ ❨ x ❩ ⊔ list_to_multiset … xs ]. lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A. m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2. #A #m #m1 #m2 normalize // qed. lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2. normalize #A #m #m1 #m2 #H #a /2/ qed. lemma list_to_multiset_append : ∀A.∀l1,l2. list_to_multiset A (l1 @ l2) ⩬ list_to_multiset … l1 ⊔ list_to_multiset … l2. #A #l1 elim l1 [ normalize //] #x #xs #IH #l2 change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (??%?); change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (???(??%?)); whd in match (list_to_multiset ??); @m_eq_symmetric @(m_eq_transitive … (m_union_associative …)) @m_eq_union_left_cancellable @m_eq_symmetric @IH qed. lemma is_multiset_mem_neq_zero : ∀A : DeqSet. ∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O. #A #l elim l [ #x *] #x #xs #IH #y * [ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct | #H normalize cases(?==?) normalize [ % #EQ destruct] @IH // ] qed. lemma mem_neq_zero_is_multiset : ∀A : DeqSet. ∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l. #A #l elim l [ #x * #H cases H % ] #x #xs #IH #y normalize inversion(y==x) normalize nodelta #H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption qed. definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝ λA,l1,l2.list_to_multiset … l1 ⩬ list_to_multiset … l2. lemma is_permutation_mem : ∀A :DeqSet. ∀l1,l2 : list A.∀x : A.mem … x l1 → is_permutation A l1 l2 → mem … x l2. #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset (list_to_multiset_append … a) >(list_to_multiset_append … a) >m_union_commutative >m_union_commutative in ⊢ (???%); list_to_multiset_append >m_union_commutative list_to_multiset_append >list_to_multiset_append @m_eq_union_left_cancellable @H qed. lemma is_permutation_append : ∀A.∀l1,l2,l3,l4. is_permutation A l1 l2 → is_permutation A l3 l4 → is_permutation A (l1 @ l3) (l2 @ l4). #A #l1 #l2 #l3 #l4 #H1 #H2 #a >list_to_multiset_append >list_to_multiset_append normalize >H1 >H2 % qed. lemma permute_equal_right : ∀A.∀l1,l2,l. is_permutation A (l1 @ l) (l2 @ l) → is_permutation A l1 l2. #A #l1 #l2 #l normalize #H #a lapply(H a) >list_to_multiset_append >list_to_multiset_append >m_union_commutative >m_union_commutative in ⊢ (???% → ?); normalize // qed. lemma permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) →is_permutation A (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) (((x ::l4 @y ::l3) @l8) @l9)). #A #l1 #l2 #l3 #l4 #l5 #l6 #l7 #l8 #l9 #x #y change with ([x] @ ?) in match ([x] @ ?); change with ([y] @ ?) in match ([y] @ ?); >append_nil #H1 #H2 whd in match (append ???) in ⊢ (???%); change with ([x] @ ?) in match ([x] @ ?) in ⊢ (???%); change with ([y] @ ?) in match ([y] @ ?) in ⊢ (???%); @permute_append_l1 >associative_append in ⊢ (???%); associative_append >associative_append >associative_append >associative_append >associative_append >associative_append >associative_append >associative_append >associative_append @is_permutation_append_left_cancellable associative_append in ⊢ (???%); >associative_append in ⊢ (???%); @is_permutation_append [2: associative_append in H1 : (??%?); #H1 @permute_equal_right [ @(l6@l7) | >associative_append assumption ] ] | associative_append in ⊢ (???%); @is_permutation_append_left_cancellable >associative_append @permute_append_l1 // ] | (\b (refl …)) normalize #EQ destruct ] #x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct >dependent_map_append >dependent_map_append @permute_append_l1 >associative_append whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%); whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?); generalize in ⊢ (? → ???(??(??%)?)); #prf1 #prf2 >(proof_irrelevance_all … g x prf1 prf2) @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%); whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1 @(is_permutation_transitive …(IH … (l3@l4) …) ) [2: assumption |3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //] | @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 // ] >dependent_map_append @is_permutation_append [ >dependent_map_extensional [ @is_permutation_eq | // |] | >dependent_map_extensional [ @is_permutation_eq | // |] ] qed.