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

13 files changed, 188 insertions, 57 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 4ddae93726..312b76e97e 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 dda2fca6ca..01e84a5254 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]. *)
 
 
 
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 8d589f053b..f0ec2ad64c 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 7e3523a8c7..898733bd87 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 bd701cbeaf..c47b4b4fe5 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 ef381c7f26..d29fb8f388 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 a4eeb9b97d..b5629eabec 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]. *)
 
 
 
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index f6f457f654..f383491d9d 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -20,10 +20,14 @@ Module Q_as_DT <: DecidableType.
  Definition eq_dec := Qeq_dec.
 
  (** The next fields are not mandatory, but allow [Q_as_DT] to be
-     also a [DecidableTypeOrig]. *)
+     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.
+
 End Q_as_DT.
 
 
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 61f49810a8..ec229abd9c 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -18,13 +18,23 @@ Proof.
     intuition eauto 3.
 Qed.
 
+Definition Reqb r1 r2 := if Req_dec r1 r2 then true else false.
+Lemma Reqb_eq : forall r1 r2, Reqb r1 r2 = true <-> r1=r2.
+Proof.
+ intros; unfold Reqb; destruct Req_dec as [EQ|NEQ]; auto with *.
+ split; try discriminate. intro EQ; elim NEQ; auto.
+Qed.
 
 Module R_as_MiniDT <: MiniDecidableType.
  Definition t := R.
  Definition eq_dec := Req_dec.
 End R_as_MiniDT.
 
-Module R_as_DT <: UsualDecidableType := Make_UDT R_as_MiniDT.
+Module R_as_DT <: UsualDecidableType.
+ Include Make_UDT R_as_MiniDT.
+ Definition eqb := Reqb.
+ Definition eqb_eq := Reqb_eq.
+End R_as_DT.
 
 (** Note that [R_as_DT] can also be seen as a [DecidableType]
     and a [DecidableTypeOrig]. *)
@@ -79,6 +89,6 @@ Ltac r_order :=
  change (@eq R) with ROrder.OrderElts.eq in *;
  ROrder.order.
 
-(** Note that [z_order] is domain-agnostic: it will not prove
+(** Note that [r_order] is domain-agnostic: it will not prove
     [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
 
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 7b329dd5e6..6a05d9683d 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -13,7 +13,7 @@ Require Export RelationClasses.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Types with Equalities, and nothing more (for subtyping purpose) *)
+(** * Types with Equality, and nothing more (for subtyping purpose) *)
 
 Module Type EqualityType.
   Parameter Inline t : Type.
@@ -25,7 +25,7 @@ Module Type EqualityType.
   Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
 End EqualityType.
 
-(** * Types with decidable Equalities (but no ordering) *)
+(** * Types with decidable Equality (but no ordering) *)
 
 Module Type DecidableType.
   Include Type EqualityType.
@@ -82,6 +82,7 @@ Module Update_DT (E:DecidableTypeOrig) <: DecidableType.
  Definition eq_dec := E.eq_dec.
 End Update_DT.
 
+
 (** * UsualDecidableType
 
    A particular case of [DecidableType] where the equality is
@@ -117,3 +118,35 @@ Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType.
 End Make_UDT.
 
 
+(** * 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.
\ No newline at end of file
diff --git a/theories/Structures/DecidableType2Facts.v b/theories/Structures/DecidableType2Facts.v
index 5a5caaab8b..988122b0b5 100644
--- a/theories/Structures/DecidableType2Facts.v
+++ b/theories/Structures/DecidableType2Facts.v
@@ -6,7 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import DecidableType2 SetoidList.
+Require Import DecidableType2 Bool SetoidList.
+
+(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType).
+
+Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
+Proof.
+intros x x' Exx' y y' Eyy'.
+apply eq_true_iff_eq.
+rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
+Qed.
+
+End BoolEqualityFacts.
 
 
 (** * Keys and datas used in FMap *)
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 06ba2eb89b..d976b01c6b 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -226,6 +226,11 @@ Qed.
 
 (** ** Properties of opposite on binary integer numbers *)
 
+Theorem Zopp_0 : Zopp Z0 = Z0.
+Proof.
+  reflexivity.
+Qed.
+
 Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
 Proof.
   reflexivity.
diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
index 34456dcf9c..b5ba8290c8 100644
--- a/theories/ZArith/ZOrderedType.v
+++ b/theories/ZArith/ZOrderedType.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinInt Zcompare Zorder ZArith_dec
+Require Import BinInt Zcompare Zorder Zbool ZArith_dec
  DecidableType2 OrderedType2 OrderedType2Facts.
 
 Local Open Scope Z_scope.
@@ -18,10 +18,14 @@ Module Z_as_MiniDT <: MiniDecidableType.
  Definition eq_dec := Z_eq_dec.
 End Z_as_MiniDT.
 
-Module Z_as_DT <: UsualDecidableType := Make_UDT Z_as_MiniDT.
+Module Z_as_DT <: UsualDecidableType.
+ Include Make_UDT Z_as_MiniDT.
+ Definition eqb := Zeq_bool.
+ Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
+End Z_as_DT.
 
 (** Note that [Z_as_DT] can also be seen as a [DecidableType]
-    and a [DecidableTypeOrig]. *)
+    and a [DecidableTypeOrig] and a [BooleanEqualityType] *)