summaryrefslogtreecommitdiff
path: root/theories/Sets/Multiset.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Sets/Multiset.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Sets/Multiset.v')
-rw-r--r--theories/Sets/Multiset.v306
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.