MSets: a new generation of FSets

Same global ideas (in particular the use of modules/functors), but:

- frequent use of Type Classes inside interfaces/implementation.
  For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence.
  A class StrictOrder for lt in OrderedType. Extensive use of Proper
  and rewrite.

- now that rewrite is mature, we write specifications of set operators
  via iff instead of many separate requirements based on ->. For instance
   add_spec : In y (add x s) <-> E.eq y x \/ In x s.
  Old-style specs are available in the functor Facts.

- compare is now a pure function (t -> t -> comparison) instead of
  returning a dependent type Compare.

- The "Raw" functors (the ones dealing with e.g. list with no
  sortedness proofs yet, but morally sorted when operating on them)
  are given proper interfaces and a generic functor allows to obtain
  a regular set implementation out of a "raw" one.

The last two points allow to manipulate set objects that are completely free
of proof-parts if one wants to. Later proofs will rely on type-classes
instance search mechanism.

No need to emphasis the fact that this new version is severely incompatible
with the earlier one. I've no precise ideas yet on how allowing an easy
transition (functors ?). For the moment, these new Sets are placed alongside
the old ones, in directory MSets (M for Modular, to constrast with forthcoming
CSets, see below). A few files exist currently in version foo.v and foo2.v,
I'll try to merge them without breaking things. Old FSets will probably move
to a contrib later.

Still to be done:
 - adapt FMap in the same way
 - integrate misc stuff like multisets or the map function
 - CSets, i.e. Sets based on Type Classes : Integration of code contributed by
    S. Lescuyer is on the way.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 122 insertions, 0 deletions

diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v
new file mode 100644
index 000000000..23ae4c85a
--- /dev/null
+++ b/theories/Structures/OrderedTypeAlt.v
@@ -0,0 +1,122 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(* $Id$ *)
+
+Require Import OrderedType.
+
+(** * An alternative (but equivalent) presentation for an Ordered Type
+   inferface. *)
+
+(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt]
+whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ]
+*)
+
+Module Type OrderedTypeAlt.
+
+ Parameter t : Type.
+
+ Parameter compare : t -> t -> comparison.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Parameter compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Parameter compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+
+End OrderedTypeAlt.
+
+(** From this new presentation to the original one. *)
+
+Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
+ Import O.
+
+ Definition t := t.
+
+ Definition eq x y := (x?=y) = Eq.
+ Definition lt x y := (x?=y) = Lt.
+
+ Lemma eq_refl : forall x, eq x x.
+ Proof.
+ intro x.
+ unfold eq.
+ assert (H:=compare_sym x x).
+ destruct (x ?= x); simpl in *; try discriminate; auto.
+ Qed.
+
+ Lemma eq_sym : forall x y, eq x y -> eq y x.
+ Proof.
+ unfold eq; intros.
+ rewrite compare_sym.
+ rewrite H; simpl; auto.
+ Qed.
+
+ Definition eq_trans := (compare_trans Eq).
+
+ Definition lt_trans := (compare_trans Lt).
+
+ Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
+ Proof.
+ unfold eq, lt; intros.
+ rewrite H; discriminate.
+ Qed.
+
+ Definition compare : forall x y, Compare lt eq x y.
+ Proof.
+ intros.
+ case_eq (x ?= y); intros.
+ apply EQ; auto.
+ apply LT; auto.
+ apply GT; red.
+ rewrite compare_sym; rewrite H; auto.
+ Defined.
+
+ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+ Proof.
+ intros; unfold eq.
+ case (x ?= y); [ left | right | right ]; auto; discriminate.
+ Defined.
+
+End OrderedType_from_Alt.
+
+(** From the original presentation to this alternative one. *)
+
+Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
+ Import O.
+ Module MO:=OrderedTypeFacts(O).
+ Import MO.
+
+ Definition t := t.
+
+ Definition compare x y := match compare x y with
+   | LT _ => Lt
+   | EQ _ => Eq
+   | GT _ => Gt
+  end.
+
+ Infix "?=" := compare (at level 70, no associativity).
+
+ Lemma compare_sym :
+   forall x y, (y?=x) = CompOpp (x?=y).
+ Proof.
+ intros x y; unfold compare.
+ destruct O.compare; elim_comp; simpl; auto.
+ Qed.
+
+ Lemma compare_trans :
+   forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+ Proof.
+ intros c x y z.
+ destruct c; unfold compare;
+ do 2 (destruct O.compare; intros; try discriminate);
+ elim_comp; auto.
+ Qed.
+
+End OrderedType_to_Alt.
+
+