Add partial setoids in theories/Classes, add SetoidDec class for setoids with a decidable equality. Fix name capture bug, again.

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

1 files changed, 96 insertions, 0 deletions

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
new file mode 100644
index 000000000..aa151772d
--- /dev/null
+++ b/theories/Classes/SetoidDec.v
@@ -0,0 +1,96 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Classes.SetoidClass.
+
+Class [ Setoid A R ] => EqDec :=
+  equiv_dec : forall x y : A, { R x y } + { ~ R x y }.
+
+Infix "==" := equiv_dec (no associativity, at level 70).
+
+Require Import Coq.Program.Program.
+
+Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { ~ R x y } + { R x y } :=
+  if x == y then right else left.
+
+Infix "<>" := nequiv_dec (no associativity, at level 70).
+
+Definition equiv_decb [ EqDec A R ] (x y : A) : bool :=
+  if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A R ] (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. *)
+
+Implicit Arguments eq [[A]].
+
+Require Import Coq.Arith.Arith.
+
+Program Instance nat_eqdec : EqDec nat eq :=
+  equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : EqDec bool eq :=
+  equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : EqDec unit eq :=
+  equiv_dec x y := left.
+
+Next Obligation.
+Proof.
+  destruct x ; destruct y.
+  reflexivity.
+Qed.
+
+Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq :=
+  equiv_dec x y := 
+    dest x as (x1, x2) in 
+    dest y as (y1, y2) in 
+    if x1 == y1 then 
+      if x2 == y2 then left
+      else right
+    else right.
+
+Solve Obligations using program_simpl ; red ; intro ; autoinjections ; discriminates.
+
+Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
+  equiv_dec f g := 
+    if f true == g true then
+      if f false == g false then left
+      else right
+    else right.
+
+Require Import Coq.Program.FunctionalExtensionality.
+
+Next Obligation.
+Proof.
+  extensionality x.
+  destruct x ; auto.
+Qed.
+
+Next Obligation.
+Proof.
+  red ; intro ; subst.
+  discriminates.
+Qed.