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, 15 insertions, 0 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.