FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType

 After lots of hesitations, OrderedType now requires this "eq_dec" field, which
 is redundant (can be deduced from "compare"), but allows the subtyping relation
 DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
 extensions of weak sets. Of course this change introduces a last-minute
 incompatibility, but:

  - There is a clear gain in term of functionnality / simplicity.
  - FSets 8.2 already needs some adaptations when compared with 8.1, so it's
    the right time to push such incompatible changes.
  - Transition shouldn't be too hard: the old OrderedType still exists under
    the name MiniOrderedType, and functor MOT_to_OT allows to convert from
    one to the other.

 Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
 (resp. OrderedType), an eq_dec on sets is now required in these interfaces
 and in the implementations. In pratice, it is really easy to build from
 equal and equal_1 and equal_2.

 Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
 while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
 Idem with WDecide, WProperties and WEqProperties.

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

1 files changed, 22 insertions, 0 deletions

diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index dbc72e0e7a..8f82fe93dc 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -34,6 +34,7 @@ Module Type UsualOrderedType.
  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]. *)
@@ -68,6 +69,8 @@ Module Nat_as_OT <: UsualOrderedType.
     intro; constructor 3; auto.
   Defined.
 
+  Definition eq_dec := eq_nat_dec.
+
 End Nat_as_OT.
 
 
@@ -99,6 +102,8 @@ Module Z_as_OT <: UsualOrderedType.
     apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto.
   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. *) 
@@ -140,6 +145,11 @@ Module Positive_as_OT <: UsualOrderedType.
   rewrite <- Pcompare_antisym; rewrite H; auto.
   Defined.
 
+  Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }.
+  Proof.
+   intros; unfold eq; decide equality.
+  Defined.
+
 End Positive_as_OT.
 
 
@@ -183,6 +193,11 @@ Module N_as_OT <: UsualOrderedType.
    destruct (Nleb x y); intuition.
   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.
 
 
@@ -243,5 +258,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
  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.