From e121b1de13ed893a37a73c852e4e9de933eef32a Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 10 Jun 2008 18:28:26 +0000
Subject: - Correct handling of DependentMorphism error, using tclFAIL instead
 of   letting the exception go uncatched. - Reorder definitions in Morphisms,
 move the PER on (R ==> R') in   Morphisms where it can be declared properly.
 Add an instance for   Equivalence => Per. - Change bug#1604 test file to the
 new semantics of [setoid_rewrite at] - More unicode characters parsed by
 coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/Morphisms.v       | 40 +++++++++++++++++++++++++-------------
 theories/Classes/RelationClasses.v | 21 +++++++-------------
 2 files changed, 33 insertions(+), 28 deletions(-)

(limited to 'theories')

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 6885d0b29..0d464b84e 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -28,6 +28,21 @@ Unset Strict Implicit.
    We now turn to the definition of [Morphism] and declare standard instances. 
    These will be used by the [setoid_rewrite] tactic later. *)
 
+(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   for usual morphisms. *)
+
+Class Morphism A (R : relation A) (m : A) : Prop :=
+  respect : R m m.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -49,6 +64,7 @@ Definition respectful (A B : Type)
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
 Delimit Scope signature_scope with signature.
+Arguments Scope Morphism [type_scope signature_scope].
 
 Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
   (right associativity, at level 55) : signature_scope.
@@ -63,22 +79,18 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
-(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
-   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
-   for usual morphisms. *)
-
-Class Morphism A (R : relation A) (m : A) : Prop :=
-  respect : R m m.
-
-Arguments Scope Morphism [type_scope signature_scope].
-
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
+(** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
+Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
+  PER (A -> B) (R ==> R').
 
-Typeclasses unfold relation.
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0). 
+    transitivity y0... symmetry...
+    transitivity (y x0)...
+  Qed.
 
 (** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 17a645c8f..044195f19 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -162,26 +162,19 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
   PER_Symmetric :> Symmetric pequiv ;
   PER_Transitive :> Transitive pequiv.
 
-(** We can build a PER on the Coq function space if we have PERs on the domain and
-   codomain. *)
-
-Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B)
-  (fun f g => forall (x y : A), R x y -> R' (f x) (g y)).
-
-  Next Obligation.
-  Proof with auto.
-    assert(R x0 x0). 
-    transitivity y0... symmetry...
-    transitivity (y x0)...
-  Qed.
-
-(** The [Equivalence] typeclass. *)
+(** Equivalence relations. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
   Equivalence_Reflexive :> Reflexive equiv ;
   Equivalence_Symmetric :> Symmetric equiv ;
   Equivalence_Transitive :> Transitive equiv.
 
+(** An Equivalence is a PER plus reflexivity. *)
+
+Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+  PER_Symmetric := Equivalence_Symmetric ;
+  PER_Transitive := Equivalence_Transitive.
+
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
-- 
cgit v1.2.3