diff options
Diffstat (limited to 'theories/Sets/Multiset.v')
| -rw-r--r-- | theories/Sets/Multiset.v | 306 |
1 files changed, 150 insertions, 156 deletions
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index cdc8520c..7084a82d 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Multiset.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Multiset.v 9245 2006-10-17 12:53:34Z notin $ i*) (* G. Huet 1-9-95 *) @@ -16,162 +16,156 @@ 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}. + Variable A : Set. + Variable eqA : A -> A -> Prop. + Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. -Inductive multiset : Set := + 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. + + 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. + + 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 |- *. + destruct x; destruct y; auto. + Qed. + + (** 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. + + Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag). + Proof. + unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto. + Qed. + + + 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 |- *. + destruct x; destruct y; auto with arith. + Qed. + + 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. + + 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. + + 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. + + (** 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). + 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). + Proof. + intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right. + 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 @@ -188,4 +182,4 @@ 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 +Hint Immediate meq_sym: v62 datatypes. |