summaryrefslogtreecommitdiff
path: root/theories7/Sets/Multiset.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /theories7/Sets/Multiset.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories7/Sets/Multiset.v')
-rwxr-xr-xtheories7/Sets/Multiset.v186
1 files changed, 0 insertions, 186 deletions
diff --git a/theories7/Sets/Multiset.v b/theories7/Sets/Multiset.v
deleted file mode 100755
index b5d5edf7..00000000
--- a/theories7/Sets/Multiset.v
+++ /dev/null
@@ -1,186 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:39 herbelin Exp $ i*)
-
-(* G. Huet 1-9-95 *)
-
-Require Permut.
-
-Set Implicit Arguments.
-
-Section multiset_defs.
-
-Variable A : Set.
-Variable eqA : A -> A -> Prop.
-Hypothesis Aeq_dec : (x,y:A){(eqA x y)}+{~(eqA x y)}.
-
-Inductive multiset : Set :=
- Bag : (A->nat) -> multiset.
-
-Definition EmptyBag := (Bag [a:A]O).
-Definition SingletonBag := [a:A]
- (Bag [a':A]Cases (Aeq_dec a a') of
- (left _) => (S O)
- | (right _) => O
- end
- ).
-
-Definition multiplicity : multiset -> A -> nat :=
- [m:multiset][a:A]let (f) = m in (f a).
-
-(** multiset equality *)
-Definition meq := [m1,m2:multiset]
- (a:A)(multiplicity m1 a)=(multiplicity m2 a).
-
-Hints Unfold meq multiplicity.
-
-Lemma meq_refl : (x:multiset)(meq x x).
-Proof.
-NewDestruct x; Auto.
-Qed.
-Hints Resolve meq_refl.
-
-Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z).
-Proof.
-Unfold meq.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Rewrite H; Auto.
-Qed.
-
-Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x).
-Proof.
-Unfold meq.
-NewDestruct x; NewDestruct y; Auto.
-Qed.
-Hints Immediate meq_sym.
-
-(** multiset union *)
-Definition munion := [m1,m2:multiset]
- (Bag [a:A](plus (multiplicity m1 a)(multiplicity m2 a))).
-
-Lemma munion_empty_left :
- (x:multiset)(meq x (munion EmptyBag x)).
-Proof.
-Unfold meq; Unfold munion; Simpl; Auto.
-Qed.
-Hints Resolve munion_empty_left.
-
-Lemma munion_empty_right :
- (x:multiset)(meq x (munion x EmptyBag)).
-Proof.
-Unfold meq; Unfold munion; Simpl; Auto.
-Qed.
-
-
-Require Plus. (* comm. and ass. of plus *)
-
-Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)).
-Proof.
-Unfold meq; Unfold multiplicity; Unfold munion.
-NewDestruct x; NewDestruct y; Auto with arith.
-Qed.
-Hints Resolve munion_comm.
-
-Lemma munion_ass :
- (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))).
-Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith.
-Qed.
-Hints Resolve munion_ass.
-
-Lemma meq_left : (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)).
-Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto with arith.
-Qed.
-Hints Resolve meq_left.
-
-Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)).
-Proof.
-Unfold meq; Unfold munion; Unfold multiplicity.
-NewDestruct x; NewDestruct y; NewDestruct z.
-Intros; Elim H; Auto.
-Qed.
-Hints 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 :
- (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 : (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 :
- (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 : (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 : (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 : (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 : (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.
-
-Hints Unfold meq multiplicity : v62 datatypes.
-Hints Resolve munion_empty_right munion_comm munion_ass meq_left meq_right munion_empty_left : v62 datatypes.
-Hints Immediate meq_sym : v62 datatypes.