diff options
Diffstat (limited to 'theories/Sets/Multiset.v')
| -rw-r--r-- | theories/Sets/Multiset.v | 40 |
1 files changed, 25 insertions, 15 deletions
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index d2bff488..7216ae33 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Multiset.v 10616 2008-03-04 17:33:35Z letouzey $ i*) +(*i $Id$ i*) (* G. Huet 1-9-95 *) -Require Import Permut. +Require Import Permut Setoid. Set Implicit Arguments. @@ -18,11 +18,12 @@ Section multiset_defs. Variable A : Type. Variable eqA : A -> A -> Prop. + Hypothesis eqA_equiv : Equivalence eqA. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. Inductive multiset : Type := Bag : (A -> nat) -> multiset. - + Definition EmptyBag := Bag (fun a:A => 0). Definition SingletonBag (a:A) := Bag (fun a':A => match Aeq_dec a a' with @@ -31,23 +32,23 @@ Section multiset_defs. end). Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a. - + (** multiset equality *) Definition meq (m1 m2:multiset) := forall a:A, multiplicity m1 a = multiplicity m2 a. - + Lemma meq_refl : forall x:multiset, meq x x. Proof. destruct x; unfold meq; reflexivity. Qed. - + Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z. Proof. unfold meq in |- *. destruct x; destruct y; destruct z. intros; rewrite H; auto. Qed. - + Lemma meq_sym : forall x y:multiset, meq x y -> meq y x. Proof. unfold meq in |- *. @@ -62,7 +63,7 @@ Section multiset_defs. Proof. unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. Qed. - + Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). Proof. unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. @@ -70,7 +71,7 @@ Section multiset_defs. Require Plus. (* comm. and ass. of plus *) - + Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *. @@ -106,28 +107,28 @@ Section multiset_defs. Lemma munion_rotate : forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)). Proof. - intros; apply (op_rotate multiset munion meq). + intros; apply (op_rotate multiset munion meq). apply munion_comm. apply munion_ass. exact meq_trans. exact meq_sym. trivial. Qed. - + Lemma meq_congr : forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t). Proof. intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right. exact meq_trans. Qed. - + Lemma munion_perm_left : forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)). Proof. intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym. exact meq_trans. Qed. - + Lemma multiset_twist1 : forall x y z t:multiset, meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z). @@ -156,7 +157,7 @@ Section multiset_defs. apply meq_right; apply meq_left; trivial. apply multiset_twist1. Qed. - + Lemma treesort_twist2 : forall x y z t u:multiset, meq u (munion y z) -> @@ -167,8 +168,17 @@ Section multiset_defs. apply multiset_twist2. Qed. + (** SingletonBag *) + + Lemma meq_singleton : forall a a', + eqA a a' -> meq (SingletonBag a) (SingletonBag a'). + Proof. + intros; red; simpl; intro a0. + destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha; + decide (Aeq_dec a' a0) with Ha; reflexivity. + Qed. -(*i theory of minter to do similarly +(*i theory of minter to do similarly Require Min. (* multiset intersection *) Definition minter := [m1,m2:multiset] |