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, 243 insertions, 0 deletions

diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
new file mode 100644
index 000000000..a39f336a5
--- /dev/null
+++ b/theories/Structures/OrderedTypeEx.v
@@ -0,0 +1,243 @@
+(***********************************************************************)
+(*  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.
+Require Import ZArith.
+Require Import Omega.
+Require Import NArith Ndec.
+Require Import Compare_dec.
+
+(** * Examples of Ordered Type structures. *)
+
+(** First, a particular case of [OrderedType] where
+    the equality is the usual one of Coq. *)
+
+Module Type UsualOrderedType.
+ Parameter Inline t : Type.
+ Definition eq := @eq t.
+ Parameter Inline lt : t -> t -> Prop.
+ Definition eq_refl := @refl_equal t.
+ Definition eq_sym := @sym_eq t.
+ Definition eq_trans := @trans_eq t.
+ Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ Parameter compare : forall x y : t, Compare lt eq x y.
+ Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+End UsualOrderedType.
+
+(** a [UsualOrderedType] is in particular an [OrderedType]. *)
+
+Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U.
+
+(** [nat] is an ordered type with respect to the usual order on natural numbers. *)
+
+Module Nat_as_OT <: UsualOrderedType.
+
+  Definition t := nat.
+
+  Definition eq := @eq nat.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt := lt.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof. unfold lt; intros; apply lt_trans with y; auto. Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof. unfold lt, eq; intros; omega. Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+    intros x y; destruct (nat_compare x y) as [ | | ]_eqn.
+    apply EQ. apply nat_compare_eq; assumption.
+    apply LT. apply nat_compare_Lt_lt; assumption.
+    apply GT. apply nat_compare_Gt_gt; assumption.
+  Defined.
+
+  Definition eq_dec := eq_nat_dec.
+
+End Nat_as_OT.
+
+
+(** [Z] is an ordered type with respect to the usual order on integers. *)
+
+Open Local Scope Z_scope.
+
+Module Z_as_OT <: UsualOrderedType.
+
+  Definition t := Z.
+  Definition eq := @eq Z.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt (x y:Z) := (x<y).
+
+  Lemma lt_trans : forall x y z, x<y -> y<z -> x<z.
+  Proof. intros; omega. Qed.
+
+  Lemma lt_not_eq : forall x y, x<y -> ~ x=y.
+  Proof. intros; omega. Qed.
+
+  Definition compare : forall x y, Compare lt eq x y.
+  Proof.
+    intros x y; destruct (x ?= y) as [ | | ]_eqn.
+    apply EQ; apply Zcompare_Eq_eq; assumption.
+    apply LT; assumption.
+    apply GT; apply Zgt_lt; assumption.
+  Defined.
+
+  Definition eq_dec := Z_eq_dec.
+
+End Z_as_OT.
+
+(** [positive] is an ordered type with respect to the usual order on natural numbers. *)
+
+Open Local Scope positive_scope.
+
+Module Positive_as_OT <: UsualOrderedType.
+  Definition t:=positive.
+  Definition eq:=@eq positive.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt p q:= (p ?= q) Eq = Lt.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof.
+  unfold lt; intros x y z.
+  change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z).
+  omega.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof.
+  intros; intro.
+  rewrite H0 in H.
+  unfold lt in H.
+  rewrite Pcompare_refl in H; discriminate.
+  Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  intros x y. destruct ((x ?= y) Eq) as [ | | ]_eqn.
+  apply EQ; apply Pcompare_Eq_eq; assumption.
+  apply LT; assumption.
+  apply GT; apply ZC1; assumption.
+  Defined.
+
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+   intros; unfold eq; decide equality.
+  Defined.
+
+End Positive_as_OT.
+
+
+(** [N] is an ordered type with respect to the usual order on natural numbers. *)
+
+Open Local Scope positive_scope.
+
+Module N_as_OT <: UsualOrderedType.
+  Definition t:=N.
+  Definition eq:=@eq N.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Definition lt:=Nlt.
+  Definition lt_trans := Nlt_trans.
+  Definition lt_not_eq := Nlt_not_eq.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  intros x y. destruct (x ?= y)%N as [ | | ]_eqn.
+  apply EQ; apply Ncompare_Eq_eq; assumption.
+  apply LT; assumption.
+  apply GT. apply Ngt_Nlt; assumption.
+  Defined.
+
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+   intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec.
+  Defined.
+
+End N_as_OT.
+
+
+(** From two ordered types, we can build a new OrderedType
+   over their cartesian product, using the lexicographic order. *)
+
+Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
+ Module MO1:=OrderedTypeFacts(O1).
+ Module MO2:=OrderedTypeFacts(O2).
+
+ Definition t := prod O1.t O2.t.
+
+ Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y).
+
+ Definition lt x y :=
+    O1.lt (fst x) (fst y) \/
+    (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)).
+
+ Lemma eq_refl : forall x : t, eq x x.
+ Proof.
+ intros (x1,x2); red; simpl; auto.
+ Qed.
+
+ Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq; simpl; intuition.
+ Qed.
+
+ Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+ Proof.
+ intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto.
+ Qed.
+
+ Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+ Proof.
+ intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition.
+ left; eauto.
+ left; eapply MO1.lt_eq; eauto.
+ left; eapply MO1.eq_lt; eauto.
+ right; split; eauto.
+ Qed.
+
+ Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+ Proof.
+ intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition.
+ apply (O1.lt_not_eq H0 H1).
+ apply (O2.lt_not_eq H3 H2).
+ Qed.
+
+ Definition compare : forall x y : t, Compare lt eq x y.
+ intros (x1,x2) (y1,y2).
+ destruct (O1.compare x1 y1).
+ apply LT; unfold lt; auto.
+ destruct (O2.compare x2 y2).
+ apply LT; unfold lt; auto.
+ apply EQ; unfold eq; auto.
+ apply GT; unfold lt; auto.
+ apply GT; unfold lt; auto.
+ Defined.
+
+ Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
+ Proof.
+ intros; elim (compare x y); intro H; [ right | left | right ]; auto.
+ auto using lt_not_eq.
+ assert (~ eq y x); auto using lt_not_eq, eq_sym.
+ Defined.
+
+End PairOrderedType.
+