diff options
Diffstat (limited to 'theories/Sets/Multiset.v')
| -rwxr-xr-x | theories/Sets/Multiset.v | 191 |
1 files changed, 191 insertions, 0 deletions
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v new file mode 100755 index 00000000..a308282b --- /dev/null +++ b/theories/Sets/Multiset.v @@ -0,0 +1,191 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Multiset.v,v 1.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*) + +(* G. Huet 1-9-95 *) + +Require Import Permut. + +Set Implicit Arguments. + +Section multiset_defs. + +Variable A : Set. +Variable eqA : A -> A -> Prop. +Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. + +Inductive multiset : Set := + 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 + | left _ => 1 + | right _ => 0 + 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. + +Hint Unfold meq multiplicity. + +Lemma meq_refl : forall x:multiset, meq x x. +Proof. +destruct x; auto. +Qed. +Hint Resolve meq_refl. + +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 |- *. +destruct x; destruct y; auto. +Qed. +Hint Immediate meq_sym. + +(** multiset union *) +Definition munion (m1 m2:multiset) := + Bag (fun a:A => multiplicity m1 a + multiplicity m2 a). + +Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x). +Proof. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. +Qed. +Hint Resolve munion_empty_left. + +Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). +Proof. +unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. +Qed. + + +Require Import 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 |- *. +destruct x; destruct y; auto with arith. +Qed. +Hint Resolve munion_comm. + +Lemma munion_ass : + forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z; auto with arith. +Qed. +Hint Resolve munion_ass. + +Lemma meq_left : + forall x y z:multiset, meq x y -> meq (munion x z) (munion y z). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto with arith. +Qed. +Hint Resolve meq_left. + +Lemma meq_right : + forall x y z:multiset, meq x y -> meq (munion z x) (munion z y). +Proof. +unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *. +destruct x; destruct y; destruct z. +intros; elim H; auto. +Qed. +Hint Resolve meq_right. + + +(** Here we should make multiset an abstract datatype, by hiding [Bag], + [munion], [multiplicity]; all further properties are proved abstractly *) + +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); auto. +exact meq_trans. +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. +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. +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). +Proof. +intros; apply (twist multiset munion meq); auto. +exact meq_trans. +Qed. + +Lemma multiset_twist2 : + forall x y z t:multiset, + meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t). +Proof. +intros; apply meq_trans with (munion (munion x (munion y z)) t). +apply meq_sym; apply munion_ass. +apply meq_left; apply munion_perm_left. +Qed. + +(** specific for treesort *) + +Lemma treesort_twist1 : + forall x y z t u:multiset, + meq u (munion y z) -> + meq (munion x (munion u t)) (munion (munion y (munion x t)) z). +Proof. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +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) -> + meq (munion x (munion u t)) (munion (munion y (munion x z)) t). +Proof. +intros; apply meq_trans with (munion x (munion (munion y z) t)). +apply meq_right; apply meq_left; trivial. +apply multiset_twist2. +Qed. + + +(*i theory of minter to do similarly +Require Min. +(* multiset intersection *) +Definition minter := [m1,m2:multiset] + (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))). +i*) + +End multiset_defs. + +Unset Implicit Arguments. + +Hint Unfold meq multiplicity: v62 datatypes. +Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right + munion_empty_left: v62 datatypes. +Hint Immediate meq_sym: v62 datatypes.
\ No newline at end of file |