DecidableType: A specification via boolean equality as an alternative to eq_dec

 + adaptation of {Nat,N,P,Z,Q,R}_as_DT for them to provide both eq_dec and eqb

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

2 files changed, 24 insertions, 4 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 4ddae9372..312b76e97 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -99,3 +99,18 @@ Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
 Proof.
  induction x; destruct y; simpl; auto; intros; discriminate.
 Qed.
+
+Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y.
+Proof.
+ split. apply beq_nat_true.
+ intros; subst; symmetry; apply beq_nat_refl.
+Qed.
+
+Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y.
+Proof.
+ intros x y.
+ split. apply beq_nat_false.
+ generalize (beq_nat_true_iff x y).
+ destruct beq_nat; auto.
+ intros IFF NEQ. elim NEQ. apply IFF; auto.
+Qed.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index dda2fca6c..01e84a525 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Lt Peano_dec Compare_dec
+Require Import Lt Peano_dec Compare_dec EqNat
  DecidableType2 OrderedType2 OrderedType2Facts.
 
 
@@ -17,10 +17,15 @@ Module Nat_as_MiniDT <: MiniDecidableType.
  Definition eq_dec := eq_nat_dec.
 End Nat_as_MiniDT.
 
-Module Nat_as_DT <: UsualDecidableType := Make_UDT 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 eqb := beq_nat.
+ Definition eqb_eq := beq_nat_true_iff.
+End Nat_as_DT.
 
-(** Note that [Nat_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig]. *)
+(** Note that [Nat_as_DT] can also be seen as a [DecidableType],
+    or a [DecidableTypeOrig] or a [BooleanEqualityType]. *)