aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-16 13:46:25 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-16 13:46:25 +0000
commit8d7e3dc633eef34e0e806c4290aebf1b5a8d753d (patch)
tree523f4e6fa138fd95ad8768cdd29ca429c0ac8e9c
parent68dfbbc355bdcab7f7880bacc4be6fe337afa800 (diff)
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
-rw-r--r--theories/Arith/NatOrderedType.v17
-rw-r--r--theories/NArith/NOrderedType.v16
-rw-r--r--theories/NArith/POrderedType.v16
-rw-r--r--theories/Numbers/NatInt/NZAxioms.v114
-rw-r--r--theories/QArith/QOrderedType.v17
-rw-r--r--theories/Reals/ROrderedType.v17
-rw-r--r--theories/Structures/DecidableType2.v276
-rw-r--r--theories/ZArith/ZOrderedType.v15
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 *)