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

5 files changed, 86 insertions, 44 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.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 7e3523a8c..898733bd8 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -266,6 +266,17 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
  | Gt => p
  end.
 
+(********************************************************************)
+(** Boolean equality *)
+
+Fixpoint Peqb (x y : positive) : bool :=
+ match x, y with
+ | 1, 1 => true
+ | p~1, q~1 => Peqb p q
+ | p~0, q~0 => Peqb p q
+ | _, _ => false
+ end.
+
 (**********************************************************************)
 (** Decidability of equality on binary positive numbers *)
 
@@ -723,6 +734,29 @@ Proof.
   intros [p|p| ] [q|q| ] H; destr_eq H; auto.
 Qed.
 
+(*********************************************************************)
+(** Properties of boolean equality *)
+
+Theorem Peqb_refl : forall x:positive, Peqb x x = true.
+Proof.
+ induction x; auto.
+Qed.
+
+Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y.
+Proof.
+ induction x; destruct y; simpl; intros; try discriminate.
+ f_equal; auto.
+ f_equal; auto.
+ reflexivity.
+Qed.
+
+Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y.
+Proof.
+ split. apply Peqb_true_eq.
+ intros; subst; apply Peqb_refl.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of comparison on binary positive numbers *)
 
diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index bd701cbea..c47b4b4fe 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -18,10 +18,14 @@ Module N_as_MiniDT <: MiniDecidableType.
  Definition eq_dec := N_eq_dec.
 End N_as_MiniDT.
 
-Module N_as_DT <: UsualDecidableType := Make_UDT N_as_MiniDT.
+Module N_as_DT <: UsualDecidableType.
+ Include Make_UDT N_as_MiniDT.
+ Definition eqb := Neqb.
+ Definition eqb_eq := Neqb_eq.
+End N_as_DT.
 
 (** Note that [N_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig]. *)
+    and a [DecidableTypeOrig] and a [BooleanEqualityType] *)
 
 
 
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index ef381c7f2..d29fb8f38 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -19,73 +19,51 @@ Require Import Ndigits.
 
 (** A boolean equality over [N] *)
 
-Fixpoint Peqb (p1 p2:positive) {struct p2} : bool :=
-  match p1, p2 with
-  | xH, xH => true
-  | xO p'1, xO p'2 => Peqb p'1 p'2
-  | xI p'1, xI p'2 => Peqb p'1 p'2
-  | _, _ => false
-  end.
+Notation Peqb := BinPos.Peqb (only parsing).
+Notation Neqb := BinNat.Neqb (only parsing).
 
-Lemma Peqb_correct : forall p, Peqb p p = true.
-Proof.
-induction p; auto.
-Qed.
+Import BinPos BinNat.
 
-Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq.
+Notation Peqb_correct := Peqb_refl (only parsing).
+
+Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.
 Proof.
- induction p; destruct p'; simpl; intros; try discriminate; auto.
+  intros. now apply (Peqb_eq p p').
 Qed.
 
-Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.
+Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq.
 Proof.
-  intros.
-  apply Pcompare_Eq_eq.
-  apply Peqb_Pcompare; auto.
+  intros. now rewrite Pcompare_eq_iff, <- Peqb_eq.
 Qed.
 
 Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true.
 Proof.
-intros; rewrite <- (Pcompare_Eq_eq _ _ H).
-apply Peqb_correct.
+  intros; now rewrite Peqb_eq, <- Pcompare_eq_iff.
 Qed.
 
-Definition Neqb (a a':N) :=
-  match a, a' with
-  | N0, N0 => true
-  | Npos p, Npos p' => Peqb p p'
-  | _, _ => false
-  end.
-
 Lemma Neqb_correct : forall n, Neqb n n = true.
 Proof.
-  destruct n; trivial.
-  simpl; apply Peqb_correct.
+  intros; now rewrite Neqb_eq.
 Qed.
 
 Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq.
 Proof.
- destruct n; destruct n'; simpl; intros; try discriminate; auto; apply Peqb_Pcompare; auto.
+  intros; now rewrite Ncompare_eq_correct, <- Neqb_eq.
 Qed.
 
 Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true.
 Proof.
-intros; rewrite <- (Ncompare_Eq_eq _ _ H).
-apply Neqb_correct.
+  intros; now rewrite Neqb_eq, <- Ncompare_eq_correct.
 Qed.
 
 Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'.
 Proof.
-  intros.
-  apply Ncompare_Eq_eq.
-  apply Neqb_Ncompare; auto.
+  intros; now rewrite <- Neqb_eq.
 Qed.
 
 Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a.
 Proof.
-  intros; apply bool_1; split; intros.
-  rewrite (Neqb_complete _ _ H); apply Neqb_correct.
-  rewrite (Neqb_complete _ _ H); apply Neqb_correct.
+  intros; apply eq_true_iff_eq. rewrite 2 Neqb_eq; auto with *.
 Qed.
 
 Lemma Nxor_eq_true :
@@ -98,7 +76,8 @@ Lemma Nxor_eq_false :
  forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false.
 Proof.
   intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete a a' H0) in H. rewrite (Nxor_nilpotent a') in H. discriminate H.
+  rewrite (Neqb_complete a a' H0) in H.
+  rewrite (Nxor_nilpotent a') in H. discriminate H.
   trivial.
 Qed.
 
@@ -149,7 +128,8 @@ Lemma Nbit0_neq :
  forall a a',
    Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false.
 Proof.
-  intros. elim (sumbool_of_bool (Neqb a a')). intro H1. rewrite (Neqb_complete _ _ H1) in H.
+  intros. elim (sumbool_of_bool (Neqb a a')). intro H1.
+  rewrite (Neqb_complete _ _ H1) in H.
   rewrite H in H0. discriminate H0.
   trivial.
 Qed.
@@ -166,7 +146,8 @@ Lemma Ndiv2_neq :
    Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false.
 Proof.
   intros. elim (sumbool_of_bool (Neqb a a')). intro H0.
-  rewrite (Neqb_complete _ _ H0) in H. rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H.
+  rewrite (Neqb_complete _ _ H0) in H.
+  rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H.
   trivial.
 Qed.
 
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index a4eeb9b97..b5629eabe 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -18,10 +18,15 @@ Module Positive_as_MiniDT <: MiniDecidableType.
  Definition eq_dec := positive_eq_dec.
 End Positive_as_MiniDT.
 
-Module Positive_as_DT <: UsualDecidableType := Make_UDT Positive_as_MiniDT.
+Module Positive_as_DT <: UsualDecidableType.
+ Include Make_UDT Positive_as_MiniDT.
+ Definition eqb := Peqb.
+ Definition eqb_eq := Peqb_eq.
+End Positive_as_DT.
+
 
 (** Note that [Positive_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig]. *)
+    and a [DecidableTypeOrig] and a [BooleanEqualityType]. *)