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

2 files changed, 140 insertions, 1 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 915a7a944..851579e12 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -33,7 +33,7 @@ Class Setoid (carrier : Type) (equiv : relation carrier) :=
 
 Definition equiv [ Setoid A R ] : _ := R.
 
-Infix "==" := equiv (at level 70, no associativity).
+Infix "==" := equiv (at level 70, no associativity) : type_scope.
 
 Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
 Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
@@ -190,3 +190,46 @@ Proof.
   apply (respect (m0:=m0)).
   assumption.
 Qed.
+
+(** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
+
+Class PartialSetoid (carrier : Type) (equiv : relation carrier) :=
+  pequiv_prf : PER carrier equiv.
+
+(** Overloaded notation for partial setoid equivalence. *)
+
+Definition pequiv [ PartialSetoid A R ] : _ := R.
+
+Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
+
+Definition pequiv_sym [ s : PartialSetoid A R ] : forall x y : A, R x y -> R y x := per_sym _ _ pequiv_prf.
+Definition pequiv_trans [ s : PartialSetoid A R ] : forall x y z : A, R x y -> R y z -> R x z := per_trans _ _ pequiv_prf.
+
+Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_partial_setoid : 
+  PartialSetoid (a -> b)
+  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
+  pequiv_prf := Build_PER _ _ _ _.
+
+Next Obligation.
+Proof.
+  sym.
+  apply H.
+  sym ; assumption.
+Qed.
+
+Next Obligation.
+Proof.
+  trans (y x0).
+  apply H ; auto.
+  trans y0 ; auto.
+  sym ; auto.
+  apply H0 ; auto.
+Qed.
+
+(** The following is not definable. *)
+(*
+Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
+  Setoid (a -> b)
+  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+*)
\ No newline at end of file
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.