Added a typeclass-based system to reason on decidable propositions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14887 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 90 insertions, 0 deletions

diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
new file mode 100644
index 000000000..40543ac62
--- /dev/null
+++ b/theories/Classes/DecidableClass.v
@@ -0,0 +1,89 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * A typeclass to ease the handling of decidable properties. *)
+
+(** A proposition is decidable whenever it is reflected by a boolean. *)
+
+Class Decidable (P : Prop) := {
+  Decidable_witness : bool;
+  Decidable_spec : Decidable_witness = true <-> P
+}.
+
+(** Alternative ways of specifying the reflection property. *)
+
+Lemma Decidable_sound : forall P (H : Decidable P),
+  Decidable_witness = true -> P.
+Proof.
+intros P H Hp; apply -> Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+  P -> Decidable_witness = true.
+Proof.
+intros P H Hp; apply <- Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+   ~ P -> Decidable_witness = false.
+Proof.
+intros P [wit spec] Hd; simpl; destruct wit; tauto.
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+  Decidable_witness = false -> ~ P.
+Proof.
+intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
+Qed.
+
+(** The generic function that should be used to program, together with some
+  useful tactics. *)
+
+Definition decide P {H : Decidable P} := @Decidable_witness P H.
+
+Ltac _decide_ P H :=
+  let b := fresh "b" in
+  set (b := decide P) in *;
+  assert (H : decide P = b) by reflexivity;
+  clearbody b;
+  destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H].
+
+Tactic Notation "decide" constr(P) "as" ident(H) :=
+  _decide_ P H.
+
+Tactic Notation "decide" constr(P) :=
+  let H := fresh "H" in _decide_ P H.
+
+(** Some usual instances. *)
+
+Require Import Bool Arith ZArith.
+
+Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
+  Decidable_witness := eqb x y
+}.
+Next Obligation.
+split.
+  now apply eqb_prop.
+  now destruct 1; apply eqb_reflx.
+Qed.
+
+Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
+  Decidable_witness := beq_nat x y
+}.
+Next Obligation.
+split.
+  now intros H; symmetry in H; apply beq_nat_eq in H; auto.
+  now destruct 1; symmetry; apply beq_nat_refl.
+Qed.
+
+Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
+  Decidable_witness := Zeq_bool x y
+}.
+Next Obligation.
+split; apply Zeq_is_eq_bool.
+Qed.
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
index 9daf133b4..a4b5d664e 100644
--- a/theories/Classes/vo.itarget
+++ b/theories/Classes/vo.itarget
@@ -1,3 +1,4 @@
+DecidableClass.v
 Equivalence.vo
 EquivDec.vo
 Init.vo