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

1 files changed, 18 insertions, 0 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 8d589f053..f0ec2ad64 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -106,6 +106,15 @@ Definition Nmult n m :=
 
 Infix "*" := Nmult : N_scope.
 
+(** Boolean Equality *)
+
+Definition Neqb n m :=
+ match n, m with
+  | N0, N0 => true
+  | Npos n, Npos m => Peqb n m
+  | _,_ => false
+ end.
+
 (** Order *)
 
 Definition Ncompare n m :=
@@ -364,6 +373,15 @@ destruct n; destruct m; reflexivity || (try discriminate H).
 injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity.
 Qed.
 
+(** Properties of boolean order. *)
+
+Lemma Neqb_eq : forall n m, Neqb n m = true <-> n=m.
+Proof.
+destruct n as [|n], m as [|m]; simpl; split; auto; try discriminate.
+intros; f_equal. apply (Peqb_eq n m); auto.
+intros. apply (Peqb_eq n m). congruence.
+Qed.
+
 (** Properties of comparison *)
 
 Lemma Ncompare_refl : forall n, (n ?= n) = Eq.