Merge SetoidList2 into SetoidList.

This file contains low-level stuff for FSets/FMaps. Switching it to
the new version (the one using Equivalence and so on instead of
eq_refl/eq_sym/eq_trans and so on) only leads to a few changes in
FSets/FMaps that are minor and probably invisible to standard users.

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

3 files changed, 46 insertions, 16 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 625f776bf..5b0fb21ef 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -96,6 +96,12 @@ Module KeyDecidableType(D:DecidableType).
   Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
   Hint Immediate eqk_sym eqke_sym.
 
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
@@ -105,7 +111,7 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto; apply eqk_trans; auto.
+   intros; apply InA_eqA with p; auto with *.
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
@@ -128,7 +134,7 @@ Module KeyDecidableType(D:DecidableType).
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index e582db3ea..a8e1ebdd6 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -218,32 +218,32 @@ Notation Sort:=(sort lt).
 Notation NoDup:=(NoDupA eq).
 
 Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
-Proof. exact (InA_eqA eq_sym eq_trans). Qed.
+Proof. exact (InA_eqA eq_equiv). Qed.
 
 Lemma ListIn_In : forall l x, List.In x l -> In x l.
-Proof. exact (In_InA eq_refl). Qed.
+Proof. exact (In_InA eq_equiv). Qed.
 
 Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_ltA lt_trans). Qed.
+Proof. exact (InfA_ltA lt_strorder). Qed.
 
 Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_lt). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
-Proof. exact (SortA_InfA_InA eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
+Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma ListIn_Inf : forall l x, (forall y, List.In y l -> lt x y) -> Inf x l.
 Proof. exact (@In_InfA t lt). Qed.
 
 Lemma In_Inf : forall l x, (forall y, In y l -> lt x y) -> Inf x l.
-Proof. exact (InA_InfA eq_refl (ltA:=lt)). Qed.
+Proof. exact (InA_InfA eq_equiv (ltA:=lt)). Qed.
 
 Lemma Inf_alt :
  forall l x, Sort l -> (Inf x l <-> (forall y, In y l -> lt x y)).
-Proof. exact (InfA_alt eq_refl eq_sym lt_trans lt_eq eq_lt). Qed.
+Proof. exact (InfA_alt eq_equiv lt_strorder lt_compat). Qed.
 
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
-Proof. exact (SortA_NoDupA eq_refl eq_sym lt_trans lt_not_eq lt_eq eq_lt) . Qed.
+Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
@@ -323,6 +323,30 @@ Module KeyOrderedType(O:OrderedType).
   Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
   Hint Immediate eqk_sym eqke_sym.
 
+  Global Instance eqk_equiv : Equivalence eqk.
+  Proof. split; eauto. Qed.
+
+  Global Instance eqke_equiv : Equivalence eqke.
+  Proof. split; eauto. Qed.
+
+  Global Instance ltk_strorder : StrictOrder ltk.
+  Proof.
+   split; eauto.
+   intros (x,e); compute; apply (StrictOrder_Irreflexive x).
+  Qed.
+
+  Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') Hxx' (y,f) (y',f') Hyy'; compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
+  Global Instance ltk_compat' : Proper (eqke==>eqke==>iff) ltk.
+  Proof.
+  intros (x,e) (x',e') (Hxx',_) (y,f) (y',f') (Hyy',_); compute.
+   compute in Hxx'; compute in Hyy'. rewrite Hxx', Hyy'; auto.
+  Qed.
+
   (* Additionnal facts *)
 
   Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'.
@@ -370,7 +394,7 @@ Module KeyOrderedType(O:OrderedType).
 
   Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
   Proof.
-  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *.
   Qed.
 
   Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
@@ -379,10 +403,10 @@ Module KeyOrderedType(O:OrderedType).
   Qed.
 
   Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_eqA eqk_ltk). Qed.
+  Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
 
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
-  Proof. exact (InfA_ltA ltk_trans). Qed.
+  Proof. exact (InfA_ltA ltk_strorder). Qed.
 
   Hint Immediate Inf_eq.
   Hint Resolve Inf_lt.
@@ -390,7 +414,7 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Sort_Inf_In :
       forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof.
-  exact (SortA_InfA_InA eqk_refl eqk_sym ltk_trans ltk_eqk eqk_ltk).
+  exact (SortA_InfA_InA eqk_equiv ltk_strorder ltk_compat).
   Qed.
 
   Lemma Sort_Inf_NotIn :
@@ -405,7 +429,7 @@ Module KeyOrderedType(O:OrderedType).
 
   Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l.
   Proof.
-  exact (SortA_NoDupA eqk_refl eqk_sym ltk_trans ltk_not_eqk ltk_eqk eqk_ltk).
+  exact (SortA_NoDupA eqk_equiv ltk_strorder ltk_compat).
   Qed.
 
   Lemma Sort_In_cons_1 : forall e l e', Sort (e::l) -> InA eqk e' l -> ltk e e'.
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 7258fe52f..fdb1ccc24 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export SetoidList2 DecidableType2 OrderTac.
+Require Export SetoidList DecidableType2 OrderTac.
 Set Implicit Arguments.
 Unset Strict Implicit.