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, 44 insertions, 1 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 915a7a944a..851579e125 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