FSetCompat: a compatibility wrapper between FSets and MSets

 Thanks to the functors in FSetCompat, the three implementations
 of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few
 lines adapting the corresponding MSets implementation to the old
 interface.

 This approach breaks FSetFullAVL. Since this file is of little use
 for stdlib users, we migrate it into contrib Orsay/FSets.

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

3 files changed, 68 insertions, 106 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index c6d16a6c5..61fd743dc 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -9,6 +9,8 @@
 (* $Id$ *)
 
 Require Export SetoidList.
+Require DecidableType. (* No Import here, this is on purpose *)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -31,6 +33,24 @@ Module Type DecidableType.
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
 End DecidableType.
 
+(** * Compatibility wrapper from/to the old version of [DecidableType] *)
+
+Module Type DecidableTypeOrig := DecidableType.DecidableType.
+
+Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
+ Include E.
+ Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+End Backport_DT.
+
+Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
+ Include E.
+ Instance eq_equiv : Equivalence eq.
+ Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed.
+End Update_DT.
+
+
 (** * Additional notions about keys and datas used in FMap *)
 
 Module KeyDecidableType(D:DecidableType).
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index c2990f283..31c9324f8 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -44,16 +44,17 @@ End OrderTacSig.
 
 (** An abstract vision of the predicates. This allows a one-line
     statement for interesting transitivity properties: for instance
-    [trans_ord LE LE = LE] will imply later [le x y -> le y z -> le x z].
- *)
+    [trans_ord OLE OLE = OLE] will imply later
+    [le x y -> le y z -> le x z].
+*)
 
-Inductive ord := EQ | LT | LE.
+Inductive ord := OEQ | OLT | OLE.
 Definition trans_ord o o' :=
  match o, o' with
- | EQ, _ => o'
- | _, EQ => o
- | LE, LE => LE
- | _, _ => LT
+ | OEQ, _ => o'
+ | _, OEQ => o
+ | OLE, OLE => OLE
+ | _, _ => OLT
  end.
 Infix "+" := trans_ord : order.
 
@@ -103,7 +104,7 @@ Ltac subst_eqns :=
  end.
 
 Definition interp_ord o :=
- match o with EQ => eq | LT => lt | LE => le end.
+ match o with OEQ => eq | OLT => lt | OLE => le end.
 Notation "#" := interp_ord : order.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
@@ -112,15 +113,15 @@ destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
  subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
 
-Definition eq_trans x y z : x==y -> y==z -> x==z := trans EQ EQ x y z.
-Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans LE LE x y z.
-Definition lt_trans x y z : x<y -> y<z -> x<z := trans LT LT x y z.
-Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans LE LT x y z.
-Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans LT LE x y z.
-Definition eq_lt x y z : x==y -> y<z -> x<z := trans EQ LT x y z.
-Definition lt_eq x y z : x<y -> y==z -> x<z := trans LT EQ x y z.
-Definition eq_le x y z : x==y -> y<=z -> x<=z := trans EQ LE x y z.
-Definition le_eq x y z : x<=y -> y==z -> x<=z := trans LE EQ x y z.
+Definition eq_trans x y z : x==y -> y==z -> x==z := trans OEQ OEQ x y z.
+Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans OLE OLE x y z.
+Definition lt_trans x y z : x<y -> y<z -> x<z := trans OLT OLT x y z.
+Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans OLE OLT x y z.
+Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans OLT OLE x y z.
+Definition eq_lt x y z : x==y -> y<z -> x<z := trans OEQ OLT x y z.
+Definition lt_eq x y z : x<y -> y==z -> x<z := trans OLT OEQ x y z.
+Definition eq_le x y z : x==y -> y<=z -> x<=z := trans OEQ OLE x y z.
+Definition le_eq x y z : x<=y -> y==z -> x<=z := trans OLE OEQ x y z.
 
 Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
 Proof. eauto using eq_trans, eq_sym. Qed.
@@ -176,7 +177,7 @@ end.
 Ltac order_eq x y eqn :=
  match x with
  | y => clear eqn
- | _ => change (#EQ x y) in eqn; order_rewr x eqn
+ | _ => change (#OEQ x y) in eqn; order_rewr x eqn
  end.
 
 (** Goal preparation : We turn all negative hyps into positive ones
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
index 43b3d05f8..6c2fb0d3f 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrderedType2Alt.v
@@ -13,42 +13,15 @@
 
 (* $Id$ *)
 
-Require Import OrderedType2.
+Require Import OrderedType OrderedType2.
 Set Implicit Arguments.
 
-(** NB: Instead of [comparison], defined in [Datatypes.v] which is [Eq|Lt|Gt],
-  we used historically the dependent type [compare] which is
-  [EQ _ | LT _ | GT _ ]
-*)
-
-Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type :=
-  | LT : lt x y -> Compare lt eq x y
-  | EQ : eq x y -> Compare lt eq x y
-  | GT : lt y x -> Compare lt eq x y.
-
 (** * Some alternative (but equivalent) presentations for an Ordered Type
    inferface. *)
 
 (** ** The original interface *)
 
-Module Type OrderedTypeOrig.
-  Parameter Inline t : Type.
-
-  Parameter Inline eq : t -> t -> Prop.
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
-  Parameter Inline lt : t -> t -> Prop.
-  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.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
-
-End OrderedTypeOrig.
+Module Type OrderedTypeOrig := OrderedType.OrderedType.
 
 (** ** An interface based on compare *)
 
@@ -69,43 +42,31 @@ End OrderedTypeAlt.
 
 (** ** From OrderedTypeOrig to OrderedType. *)
 
-Module OrderedType_from_Orig (O:OrderedTypeOrig) <: OrderedType.
+Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
 
- Import O.
- Definition t := O.t.
- Definition eq := O.eq.
- Instance eq_equiv : Equivalence eq.
- Proof.
-  split; red; [ apply eq_refl | apply eq_sym | eapply eq_trans ].
- Qed.
+ Include Update_DT O.  (* Provides : t eq eq_equiv eq_dec *)
 
  Definition lt := O.lt.
- Instance lt_strorder : StrictOrder lt.
- Proof.
-  split; repeat red; intros.
-  eapply lt_not_eq; eauto.
-  eapply lt_trans; eauto.
- Qed.
 
- Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
- Proof.
-  intros; destruct (compare x z); auto.
-  elim (@lt_not_eq x y); eauto.
-  elim (@lt_not_eq z y); eauto using lt_trans.
- Qed.
-
- Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z.
+ Instance lt_strorder : StrictOrder lt.
  Proof.
-  intros; destruct (compare x z); auto.
-  elim (@lt_not_eq y z); eauto.
-  elim (@lt_not_eq y x); eauto using lt_trans.
+  split.
+  intros x Hx. apply (O.lt_not_eq Hx); auto with *.
+  exact O.lt_trans.
  Qed.
 
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
  Proof.
   apply proper_sym_impl_iff_2; auto with *.
-  repeat red; intros.
-  eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto.
+  intros x x' Hx y y' Hy H.
+  assert (H0 : lt x' y).
+   destruct (O.compare x' y) as [H'|H'|H']; auto.
+   elim (O.lt_not_eq H). transitivity x'; auto with *.
+   elim (O.lt_not_eq (O.lt_trans H H')); auto.
+  destruct (O.compare x' y') as [H'|H'|H']; auto.
+  elim (O.lt_not_eq H).
+   transitivity x'; auto with *. transitivity y'; auto with *.
+  elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *.
  Qed.
 
  Definition compare x y :=
@@ -120,31 +81,15 @@ Module OrderedType_from_Orig (O:OrderedTypeOrig) <: OrderedType.
   intros; unfold compare; destruct O.compare; auto.
  Qed.
 
- Definition eq_dec : forall x y, { eq x y } + { ~eq x y }.
- Proof.
-  intros; destruct (O.compare x y).
-  right. apply lt_not_eq; auto.
-  left; auto.
-  right. intro. apply (@lt_not_eq y x); auto.
- Defined.
-
-End OrderedType_from_Orig.
+End Update_OT.
 
 (** ** From OrderedType to OrderedTypeOrig. *)
 
-Module OrderedType_to_Orig (O:OrderedType) <: OrderedTypeOrig.
+Module Backport_OT (O:OrderedType) <: OrderedTypeOrig.
 
- Import O.
- Definition t := t.
- Definition eq := eq.
- Definition lt := lt.
+ Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *)
 
- Lemma eq_refl : Reflexive eq.
- Proof. auto. Qed.
- Lemma eq_sym : Symmetric eq.
- Proof. apply eq_equiv. Qed.
- Lemma eq_trans : Transitive eq.
- Proof. apply eq_equiv. Qed.
+ Definition lt := O.lt.
 
  Lemma lt_not_eq : forall x y, lt x y -> ~eq x y.
  Proof.
@@ -152,23 +97,20 @@ Module OrderedType_to_Orig (O:OrderedType) <: OrderedTypeOrig.
  Qed.
 
  Lemma lt_trans : Transitive lt.
- Proof. apply lt_strorder. Qed.
+ Proof. apply O.lt_strorder. Qed.
 
  Definition compare : forall x y, Compare lt eq x y.
  Proof.
-  intros. generalize (compare_spec x y); unfold Cmp, flip.
-  destruct (compare x y); [apply EQ|apply LT|apply GT]; auto.
+  intros. generalize (O.compare_spec x y); unfold Cmp, flip.
+  destruct (O.compare x y); [apply EQ|apply LT|apply GT]; auto.
  Defined.
 
- Definition eq_dec := eq_dec.
-
-End OrderedType_to_Orig.
+End Backport_OT.
 
 
 (** ** From OrderedTypeAlt to OrderedType. *)
 
-Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
- Import O.
+Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
 
  Definition t := t.
 
@@ -239,12 +181,11 @@ Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType.
  case (x ?= y); [ left | right | right ]; auto; discriminate.
  Defined.
 
-End OrderedType_from_Alt.
+End OT_from_Alt.
 
 (** From the original presentation to this alternative one. *)
 
-Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
- Import O.
+Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt.
 
  Definition t := t.
  Definition compare := compare.
@@ -294,4 +235,4 @@ Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt.
  intros; apply StrictOrder_Transitive with y; auto.
  Qed.
 
-End OrderedType_to_Alt.
+End OT_to_Alt.