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, 49 insertions, 3 deletions

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 7b329dd5e..6a05d9683 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 5a5caaab8..988122b0b 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 *)