Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms

 We can now have a diamond-like approch to extentions of signatures,
 instead of a linear-only chains as earlier...

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

8 files changed, 322 insertions, 166 deletions

diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index 01e84a525..287d0c955 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -12,20 +12,17 @@ Require Import Lt Peano_dec Compare_dec EqNat
 
 (** * DecidableType structure for Peano numbers *)
 
-Module Nat_as_MiniDT <: MiniDecidableType.
+Module Nat_as_UBE <: UsualBoolEq.
  Definition t := nat.
- Definition eq_dec := eq_nat_dec.
-End Nat_as_MiniDT.
-
-Module Nat_as_DT <: UsualDecidableType.
- Include Make_UDT Nat_as_MiniDT.
- (** The next fields aren't mandatory but allow more subtyping. *)
+ Definition eq := @eq nat.
  Definition eqb := beq_nat.
  Definition eqb_eq := beq_nat_true_iff.
-End Nat_as_DT.
+End Nat_as_UBE.
+
+Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE.
 
-(** Note that [Nat_as_DT] can also be seen as a [DecidableType],
-    or a [DecidableTypeOrig] or a [BooleanEqualityType]. *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
 
 
 
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index c47b4b4fe..08391d33f 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -13,19 +13,17 @@ Local Open Scope N_scope.
 
 (** * DecidableType structure for [N] binary natural numbers *)
 
-Module N_as_MiniDT <: MiniDecidableType.
+Module N_as_UBE <: UsualBoolEq.
  Definition t := N.
- Definition eq_dec := N_eq_dec.
-End N_as_MiniDT.
-
-Module N_as_DT <: UsualDecidableType.
- Include Make_UDT N_as_MiniDT.
+ Definition eq := @eq N.
  Definition eqb := Neqb.
  Definition eqb_eq := Neqb_eq.
-End N_as_DT.
+End N_as_UBE.
+
+Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE.
 
-(** Note that [N_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig] and a [BooleanEqualityType] *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
 
 
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index b5629eabe..85667e29a 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -13,20 +13,18 @@ Local Open Scope positive_scope.
 
 (** * DecidableType structure for [positive] numbers *)
 
-Module Positive_as_MiniDT <: MiniDecidableType.
+Module Positive_as_UBE <: UsualBoolEq.
  Definition t := positive.
- Definition eq_dec := positive_eq_dec.
-End Positive_as_MiniDT.
-
-Module Positive_as_DT <: UsualDecidableType.
- Include Make_UDT Positive_as_MiniDT.
+ Definition eq := @eq positive.
  Definition eqb := Peqb.
  Definition eqb_eq := Peqb_eq.
-End Positive_as_DT.
+End Positive_as_UBE.
 
+Module Positive_as_DT <: UsualDecidableTypeFull
+ := Make_UDTF Positive_as_UBE.
 
-(** Note that [Positive_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig] and a [BooleanEqualityType]. *)
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
 
 
 
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 9dd6eaf05..c85e84b04 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -10,40 +10,36 @@
 
 (*i $Id$ i*)
 
+Require Import DecidableType2 OrderedType2.
 Require Export NumPrelude.
 
-Module Type NZAxiomsSig.
-
-Parameter Inline t : Type.
-Parameter Inline eq : t -> t -> Prop.
-Parameter Inline zero : t.
-Parameter Inline succ : t -> t.
-Parameter Inline pred : t -> t.
-Parameter Inline add : t -> t -> t.
-Parameter Inline sub : t -> t -> t.
-Parameter Inline mul : t -> t -> t.
+Delimit Scope NumScope with Num.
+Local Open Scope NumScope.
 
-(* Unary subtraction (opp) is not defined on natural numbers, so we have
-   it for integers only *)
+(** Axiomatization of a domain with zero, successor, predecessor,
+    and a bi-directional induction principle. We require [P (S n) = n]
+    but not the other way around, since this domain is meant
+    to be either N or Z. In fact it can be a few other things,
+    for instance [Z/nZ] (See file [NZDomain for a study of that).
+*)
 
-Instance eq_equiv : Equivalence eq.
-Instance succ_wd : Proper (eq ==> eq) succ.
-Instance pred_wd : Proper (eq ==> eq) pred.
-Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+Module Type NZDomain_fun (Import E : EqualityType).
+ (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *)
 
-Delimit Scope NumScope with Num.
-Local Open Scope NumScope.
 Notation "x == y"  := (eq x y) (at level 70) : NumScope.
 Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope.
+
+Parameter Inline zero : t.
+Parameter Inline succ : t -> t.
+Parameter Inline pred : t -> t.
+
 Notation "0" := zero : NumScope.
 Notation S := succ.
 Notation P := pred.
 Notation "1" := (S 0) : NumScope.
-Notation "x + y" := (add x y) : NumScope.
-Notation "x - y" := (sub x y) : NumScope.
-Notation "x * y" := (mul x y) : NumScope.
+
+Instance succ_wd : Proper (eq ==> eq) S.
+Instance pred_wd : Proper (eq ==> eq) P.
 
 Axiom pred_succ : forall n, P (S n) == n.
 
@@ -51,7 +47,35 @@ Axiom bi_induction :
   forall A : t -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 
-Axiom add_0_l : forall n, 0 + n == n.
+End NZDomain_fun.
+
+Module Type NZDomainSig.
+ Include Type EqualityType.
+ Include Self Type NZDomain_fun.
+End NZDomainSig.
+
+Module Type NZDecDomainSig.
+ Include Type DecidableType.
+ Include Self Type NZDomain_fun.
+End NZDecDomainSig.
+
+(** Axiomatization of basic operations : [+] [-] [*] *)
+
+Module Type NZBasicFuns_fun (Import NZ : NZDomainSig).
+
+Parameter Inline add : t -> t -> t.
+Parameter Inline sub : t -> t -> t.
+Parameter Inline mul : t -> t -> t.
+
+Notation "x + y" := (add x y) : NumScope.
+Notation "x - y" := (sub x y) : NumScope.
+Notation "x * y" := (mul x y) : NumScope.
+
+Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+
+Axiom add_0_l : forall n, (0 + n) == n.
 Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
 
 Axiom sub_0_r : forall n, n - 0 == n.
@@ -60,11 +84,21 @@ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
 Axiom mul_0_l : forall n, 0 * n == 0.
 Axiom mul_succ_l : forall n m, S n * m == n * m + m.
 
-End NZAxiomsSig.
+End NZBasicFuns_fun.
 
-Module Type NZOrdAxiomsSig.
-Include Type NZAxiomsSig.
-Local Open Scope NumScope.
+Module Type NZBasicFunsSig.
+ Include Type NZDomainSig.
+ Include Self Type NZBasicFuns_fun.
+End NZBasicFunsSig.
+
+(** Old name for the same interface: *)
+
+Module Type NZAxiomsSig := NZBasicFunsSig.
+
+
+(** Axiomatization of order *)
+
+Module Type NZOrd_fun (Import NZ : NZDomainSig).
 
 Parameter Inline lt : t -> t -> Prop.
 Parameter Inline le : t -> t -> Prop.
@@ -75,18 +109,40 @@ Notation "x > y" := (lt y x) (only parsing) : NumScope.
 Notation "x >= y" := (le y x) (only parsing) : NumScope.
 
 Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
-(** Compatibility of [le] can be proved later from [lt_wd] and [lt_eq_cases] *)
+(** Compatibility of [le] can be proved later from [lt_wd]
+    and [lt_eq_cases] *)
 
 Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Axiom lt_irrefl : forall n, ~ (n < n).
 Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
 
+End NZOrd_fun.
+
+Module Type NZOrdSig.
+ Include Type NZDomainSig.
+ Include Self Type NZOrd_fun.
+End NZOrdSig.
+
+
+(** Axiomatization of minimum and maximum *)
+
+Module Type NZMinMax_fun (Import NZ : NZOrdSig).
+
 Parameter Inline min : t -> t -> t.
 Parameter Inline max : t -> t -> t.
+
 (** Compatibility of [min] and [max] can be proved later *)
+
 Axiom min_l : forall n m, n <= m -> min n m == n.
 Axiom min_r : forall n m, m <= n -> min n m == m.
 Axiom max_l : forall n m, m <= n -> max n m == n.
 Axiom max_r : forall n m, n <= m -> max n m == m.
 
+End NZMinMax_fun.
+
+Module Type NZOrdAxiomsSig.
+ Include Type NZDomainSig.
+ Include Self Type NZBasicFuns_fun.
+ Include Self Type NZOrd_fun.
+ Include Self Type NZMinMax_fun.
 End NZOrdAxiomsSig.
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index f383491d9..cad77b4eb 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -13,23 +13,22 @@ Local Open Scope Q_scope.
 
 (** * DecidableType structure for rational numbers *)
 
-Module Q_as_DT <: DecidableType.
+Module Q_as_DT <: DecidableTypeFull.
  Definition t := Q.
  Definition eq := Qeq.
  Instance eq_equiv : Equivalence Qeq.
- Definition eq_dec := Qeq_dec.
-
- (** The next fields are not mandatory, but allow [Q_as_DT] to be
-     also a [DecidableTypeOrig] (resp. a [BooleanEqualityType]). *)
- Definition eq_refl := Qeq_refl.
- Definition eq_sym := Qeq_sym.
- Definition eq_trans := eq_trans.
-
  Definition eqb := Qeq_bool.
  Definition eqb_eq := Qeq_bool_iff.
 
+ Include Self Backport_ET_fun. (** eq_refl, eq_sym, eq_trans *)
+ Include Self Bool2Dec_fun. (** eq_dec *)
+
 End Q_as_DT.
 
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
+
+
 
 (** * OrderedType structure for rational numbers *)
 
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index ec229abd9..4ef8d7bcc 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -25,16 +25,19 @@ Proof.
  split; try discriminate. intro EQ; elim NEQ; auto.
 Qed.
 
-Module R_as_MiniDT <: MiniDecidableType.
+Module R_as_UBE <: UsualBoolEq.
  Definition t := R.
- Definition eq_dec := Req_dec.
-End R_as_MiniDT.
-
-Module R_as_DT <: UsualDecidableType.
- Include Make_UDT R_as_MiniDT.
+ Definition eq := @eq R.
  Definition eqb := Reqb.
  Definition eqb_eq := Reqb_eq.
-End R_as_DT.
+End R_as_UBE.
+
+Module R_as_DT <: UsualDecidableTypeFull := Make_UDTF R_as_UBE.
+
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
+
+
 
 (** Note that [R_as_DT] can also be seen as a [DecidableType]
     and a [DecidableTypeOrig]. *)
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 102572b5b..7cae4358b 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -15,138 +15,246 @@ Unset Strict Implicit.
 
 (** * Types with Equality, and nothing more (for subtyping purpose) *)
 
-Module Type EqualityType.
+Module Type BareEquality.
   Parameter Inline t : Type.
   Parameter Inline eq : t -> t -> Prop.
-  Instance eq_equiv : Equivalence eq.
+End BareEquality.
+
+(** * Specification of the equality by the Type Classe [Equivalence] *)
 
+Module Type Equality_fun (Import E:BareEquality).
+  Instance eq_equiv : Equivalence eq.
   Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
-End EqualityType.
+End Equality_fun.
 
-(** * Types with decidable Equality (but no ordering) *)
-
-Module Type DecidableType.
-  Include Type EqualityType.
-  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
-End DecidableType.
-
-(** * Old versions of [DecidableType], with reflexivity, symmetry,
-  transitivity as three separate axioms. *)
-
-Module Type EqualityTypeOrig.
-  Parameter Inline t : Type.
-  Parameter Inline eq : t -> t -> Prop.
+(** * Earlier specification of equality by three separate lemmas. *)
 
+Module Type EqualityOrig_fun(Import E:BareEquality).
   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.
-
   Hint Immediate eq_sym.
   Hint Resolve eq_refl eq_trans.
-End EqualityTypeOrig.
+End EqualityOrig_fun.
 
-Module Type DecidableTypeOrig.
-  Include Type EqualityTypeOrig.
+(** * Types with decidable equality *)
+
+Module Type Decidable_fun (Import E:BareEquality).
   Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+End Decidable_fun.
+
+(** * Boolean Equality *)
+
+(** Having [eq_dec] is the same as having a boolean equality plus
+    a correctness proof. *)
+
+Module Type BoolEq_fun (Import E:BareEquality).
+  Parameter Inline eqb : t -> t -> bool.
+  Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
+End BoolEq_fun.
+
+(** From these basic blocks, we can build many combinations
+    of static standalone module types. *)
+
+Module Type EqualityType.
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+End EqualityType.
+
+Module Type EqualityTypeOrig.
+  Include Type BareEquality.
+  Include Self Type EqualityOrig_fun.
+End EqualityTypeOrig.
+
+Module Type EqualityTypeBoth. (* <: EqualityType <: EqualityTypeOrig *)
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+  Include Self Type EqualityOrig_fun.
+End EqualityTypeBoth.
+
+Module Type DecidableType. (* <: EqualityType *)
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+  Include Self Type Decidable_fun.
+End DecidableType.
+
+Module Type DecidableTypeOrig. (* <: EqualityTypeOrig *)
+  Include Type BareEquality.
+  Include Self Type EqualityOrig_fun.
+  Include Self Type Decidable_fun.
 End DecidableTypeOrig.
 
-(** * Compatibility wrapper from/to the old version of [DecidableType] *)
+Module Type DecidableTypeBoth. (* <: DecidableType <: DecidableTypeOrig *)
+  Include Type EqualityTypeBoth.
+  Include Self Type Decidable_fun.
+End DecidableTypeBoth.
 
-(** Interestingly, a module can be at the same time a [DecidableType]
-    and a [DecidableTypeOrig]. For the sake of compatibility,
-    this will be the case of all [DecidableType] modules provided here.
-*)
+Module Type BooleanEqualityType. (* <: EqualityType *)
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+  Include Self Type BoolEq_fun.
+End BooleanEqualityType.
 
-Module Backport_ET (E:EqualityType) <: EqualityTypeOrig.
+Module Type BooleanDecidableType. (* <: DecidableType <: BooleanEqualityType *)
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+  Include Self Type Decidable_fun.
+  Include Self Type BoolEq_fun.
+End BooleanDecidableType.
+
+Module Type DecidableTypeFull. (* <: all previous interfaces *)
+  Include Type BareEquality.
+  Include Self Type Equality_fun.
+  Include Self Type EqualityOrig_fun.
+  Include Self Type Decidable_fun.
+  Include Self Type BoolEq_fun.
+End DecidableTypeFull.
+
+
+(** * Compatibility wrapper from/to the old version of
+      [EqualityType] and [DecidableType] *)
+
+Module Backport_ET_fun (E:BareEquality)(F:Equality_fun E) <: EqualityOrig_fun E.
+ Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+End Backport_ET_fun.
+
+Module Update_ET_fun (E:BareEquality)(F:EqualityOrig_fun E) <: Equality_fun E.
+ Instance eq_equiv : Equivalence E.eq.
+ Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+End Update_ET_fun.
+
+Module Backport_ET (E:EqualityType) <: EqualityTypeBoth.
  Include E.
- Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+ Include Backport_ET_fun E E.
 End Backport_ET.
 
-Module Update_ET (E:EqualityTypeOrig) <: EqualityType.
+Module Update_ET (E:EqualityTypeOrig) <: EqualityTypeBoth.
  Include E.
- Instance eq_equiv : Equivalence eq.
- Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed.
+ Include Update_ET_fun E E.
 End Update_ET.
 
-Module Backport_DT (E:DecidableType) <: DecidableTypeOrig.
- Include Backport_ET E.
- Definition eq_dec := E.eq_dec.
+Module Backport_DT (E:DecidableType) <: DecidableTypeBoth.
+ Include E.
+ Include Backport_ET_fun E E.
 End Backport_DT.
 
-Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
- Include Update_ET E.
- Definition eq_dec := E.eq_dec.
+Module Update_DT (E:DecidableTypeOrig) <: DecidableTypeBoth.
+ Include E.
+ Include Update_ET_fun E E.
 End Update_DT.
 
 
+(** * Having [eq_dec] is equivalent to having [eqb] and its spec. *)
+
+Module Dec2Bool_fun (E:BareEquality)(F:Decidable_fun E) <: BoolEq_fun E.
+ Definition eqb x y := if F.eq_dec x y then true else false.
+ Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
+ Proof.
+  intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ].
+  auto with *.
+  split. discriminate. intro EQ; elim NEQ; auto.
+ Qed.
+End Dec2Bool_fun.
+
+Module Bool2Dec_fun (E:BareEquality)(F:BoolEq_fun E) <: Decidable_fun E.
+ Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
+ Proof.
+  intros x y. assert (H:=F.eqb_eq x y).
+  destruct (F.eqb x y); [left|right].
+  apply -> H; auto.
+  intro EQ. apply H in EQ. discriminate.
+ Defined.
+End Bool2Dec_fun.
+
+Module Dec2Bool (E:DecidableType) <: BooleanDecidableType.
+ Include E.
+ Include Dec2Bool_fun E E.
+End Dec2Bool.
+
+Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType.
+ Include E.
+ Include Bool2Dec_fun E E.
+End Bool2Dec.
+
+
+
 (** * UsualDecidableType
 
    A particular case of [DecidableType] where the equality is
    the usual one of Coq. *)
 
-Module Type UsualDecidableType.
+Module Type UsualBareEquality. (* <: BareEquality *)
  Parameter Inline t : Type.
  Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
- Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
+End UsualBareEquality.
+
+Module UsualEquality_fun (E:UsualBareEquality) <: Equality_fun E.
+ Program Instance eq_equiv : Equivalence E.eq.
+End UsualEquality_fun.
+
+Module UsualEqualityOrig_fun (E:UsualBareEquality) <: EqualityOrig_fun E.
+ Definition eq_refl := @eq_refl E.t.
+ Definition eq_sym := @eq_sym E.t.
+ Definition eq_trans := @eq_trans E.t.
+End UsualEqualityOrig_fun.
+
+Module Type UsualEqualityType. (* <: EqualityType *)
+ Include Type UsualBareEquality.
+ Include Self Type Equality_fun.
+End UsualEqualityType.
+
+Module Type UsualDecidableType. (* <: DecidableType *)
+ Include Type UsualBareEquality.
+ Include Self Type Equality_fun.
+ Include Self Type Decidable_fun.
 End UsualDecidableType.
 
+Module Type UsualDecidableTypeBoth. (* <: DecidableTypeBoth *)
+ Include Type UsualBareEquality.
+ Include Self Type Equality_fun.
+ Include Self Type EqualityOrig_fun.
+ Include Self Type Decidable_fun.
+End UsualDecidableTypeBoth.
+
+Module Type UsualBoolEq.
+ Include Type UsualBareEquality.
+ Include Self Type BoolEq_fun.
+End UsualBoolEq.
+
+Module Type UsualDecidableTypeFull. (* <: DecidableTypeFull *)
+ Include Type UsualBareEquality.
+ Include Self Type Equality_fun.
+ Include Self Type EqualityOrig_fun.
+ Include Self Type Decidable_fun.
+ Include Self Type BoolEq_fun.
+End UsualDecidableTypeFull.
+
 (** a [UsualDecidableType] is in particular an [DecidableType]. *)
 
 Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
 
-(** an shortcut for easily building a UsualDecidableType *)
+(** Some shortcuts for easily building a UsualDecidableType *)
 
 Module Type MiniDecidableType.
- Parameter Inline t : Type.
- Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }.
+ Parameter t : Type.
+ Parameter eq_dec : forall x y : t, {eq x y}+{~eq x y}.
 End MiniDecidableType.
 
-Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
- Definition t:=M.t.
+Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth.
+ Include M.
  Definition eq := @eq M.t.
- Program Instance eq_equiv : Equivalence eq.
- Definition eq_dec := M.eq_dec.
- (* For building DecidableTypeOrig at the same time: *)
- Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+ Include Self UsualEquality_fun.
+ Include Self UsualEqualityOrig_fun.
 End Make_UDT.
 
+Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull.
+ Include M. (* t, eq, eqb, eqb_eq *)
+ Include UsualEquality_fun M.
+ Include UsualEqualityOrig_fun M.
+ Include Bool2Dec_fun M M.
+End Make_UDTF.
 
-(** * Boolean Equality *)
-
-(** Having [eq_dec] is the same as having a boolean equality plus
-    a correctness proof. *)
-
-Module Type BooleanEqualityType.
- Include Type EqualityType.
- Parameter Inline eqb : t -> t -> bool.
- Parameter eqb_eq : forall x y, eqb x y = true <-> eq x y.
-End BooleanEqualityType.
-
-Module Bool_to_Dec (E:BooleanEqualityType) <: DecidableType.
- Include E.
- Lemma eq_dec : forall x y, {eq x y}+{~eq x y}.
- Proof.
-  intros x y. assert (H:=eqb_eq x y).
-  destruct (eqb x y); [left|right].
-  apply -> H; auto.
-  intro EQ. apply H in EQ. discriminate.
- Defined.
-End Bool_to_Dec.
-
-Module Dec_to_Bool (E:DecidableType) <: BooleanEqualityType.
- Include E.
- Definition eqb x y := if eq_dec x y then true else false.
- Lemma eqb_eq : forall x y, eqb x y = true <-> eq x y.
- Proof.
-  intros x y. unfold eqb. destruct eq_dec as [EQ|NEQ].
-  auto with *.
-  split. discriminate. intro EQ; elim NEQ; auto.
- Qed.
-End Dec_to_Bool.
diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
index b5ba8290c..c717284fd 100644
--- a/theories/ZArith/ZOrderedType.v
+++ b/theories/ZArith/ZOrderedType.v
@@ -13,20 +13,17 @@ Local Open Scope Z_scope.
 
 (** * DecidableType structure for binary integers *)
 
-Module Z_as_MiniDT <: MiniDecidableType.
+Module Z_as_UBE <: UsualBoolEq.
  Definition t := Z.
- Definition eq_dec := Z_eq_dec.
-End Z_as_MiniDT.
-
-Module Z_as_DT <: UsualDecidableType.
- Include Make_UDT Z_as_MiniDT.
+ Definition eq := @eq Z.
  Definition eqb := Zeq_bool.
  Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
-End Z_as_DT.
+End Z_as_UBE.
 
-(** Note that [Z_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig] and a [BooleanEqualityType] *)
+Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE.
 
+(** Note that the last module fulfills by subtyping many other
+    interfaces, such as [DecidableType] or [EqualityType]. *)
 
 
 (** * OrderedType structure for binary integers *)