1 files changed, 126 insertions, 0 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
new file mode 100644
index 00000000..cf3d202d
--- /dev/null
+++ b/theories/Classes/SetoidDec.v
@@ -0,0 +1,126 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Decidable setoid equality theory.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: SetoidDec.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Export notations. *)
+
+Require Export Coq.Classes.SetoidClass.
+
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+   classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Class [ Setoid A ] => DecidableSetoid :=
+  setoid_decidable : forall x y : A, decidable (x == y).
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
+Class [ Setoid A ] => EqDec :=
+  equiv_dec : forall x y : A, { x == y } + { x =/= y }.
+
+(** We define the [==] overloaded notation for deciding equality. It does not take precedence
+   of [==] defined in the type scope, hence we can have both at the same time. *)
+
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
+  match x with
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
+  end.
+
+Require Import Coq.Program.Program.
+
+Open Local Scope program_scope.
+
+(** Invert the branches. *)
+
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+
+(** Overloaded notation for inequality. *)
+
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
+
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+  if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+  negb (equiv_decb x y).
+
+Infix "==b" := equiv_decb (no associativity, at level 70).
+Infix "<>b" := nequiv_decb (no associativity, at level 70).
+
+(** Decidable leibniz equality instances. *)
+
+Require Import Coq.Arith.Arith.
+
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance eq_setoid : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
+
+Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
+  equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
+  equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
+  equiv_dec x y := in_left.
+
+  Next Obligation.
+  Proof.
+    destruct x ; destruct y.
+    reflexivity.
+  Qed.
+
+Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
+  equiv_dec x y := 
+    let '(x1, x2) := x in 
+    let '(y1, y2) := y in 
+    if x1 == y1 then 
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using unfold complement ; program_simpl.
+
+(** Objects of function spaces with countable domains like bool have decidable equality. *)
+
+Require Import Coq.Program.FunctionalExtensionality.
+
+Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
+  equiv_dec f g := 
+    if f true == g true then
+      if f false == g false then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+
+  Next Obligation.
+  Proof.
+    extensionality x.
+    destruct x ; auto.
+  Qed.