Imported Upstream version 8.1~gammaupstream/8.1.gamma

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.