Document CHANGES in setoid rewrite, move DefaultRelation to

SetoidTactics and document it. Cleanup Classes.Equivalence.
Minor fixes to the Program doc.


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

1 files changed, 28 insertions, 75 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 6270fb43b..5e34a4437 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -7,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
+(* Typeclass-based setoids. Definitions on [Equivalence].
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
-   91405 Orsay, France *)
+   91405 Orsay, France *) 
 
 (* $Id$ *)
 
@@ -28,18 +28,29 @@ Unset Strict Implicit.
 
 Open Local Scope signature_scope.
 
-(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
-
-Instance [ Equivalence A R ] => 
-  equivalence_default : DefaultRelation A R | 4.
-
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 Typeclasses unfold @equiv.
 
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+
+Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
+
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
+  
+Open Local Scope equiv_scope.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv [ PER A R ] : relation A := R.
 
+Typeclasses unfold @pequiv.
+
+(** Overloaded notation for partial equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
-(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *)
+(** Shortcuts to make proof search easier. *)
 
 Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv.
 
@@ -57,34 +68,7 @@ Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv.
     transitivity y ; auto.
   Qed.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
-
-(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
-(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
-
-Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
-
-Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-  
-Open Local Scope equiv_scope.
-
-Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
-Proof with auto.
-  intros; intro.
-  assert(z === y) by (symmetry ; auto).
-  assert(x === y) by (transitivity z ; auto).
-  contradiction.
-Qed.
-
-Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
-Proof.
-  intros; intro. 
-  assert(y === x) by (symmetry ; auto).
-  assert(y === z) by (transitivity x ; auto).
-  contradiction.
-Qed.
-
-(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *)
+(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
 Ltac setoid_subst H := 
   match type of H with
@@ -101,6 +85,8 @@ Ltac setoid_subst_nofail :=
 
 Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
 
+(** Simplify the goal w.r.t. equivalence. *)
+
 Ltac equiv_simplify_one :=
   match goal with
     | [ H : ?x === ?x |- _ ] => clear H
@@ -111,6 +97,9 @@ Ltac equiv_simplify_one :=
 
 Ltac equiv_simplify := repeat equiv_simplify_one.
 
+(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
+   for easy recognition in tactics. *)
+
 Ltac equivify_tac :=
   match goal with
     | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
@@ -119,43 +108,6 @@ Ltac equivify_tac :=
 
 Ltac equivify := repeat equivify_tac.
 
-(** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
-
-(* Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *)
-(*   respect := respect. *)
-
-(* (** The partial application too as it is Reflexive. *) *)
-
-(* Instance [ sa : Equivalence A ] (x : A) =>  *)
-(*   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *)
-(*   respect := respect.  *)
-
-(** Instance not exported by default, as comparing types for equivalence may be unintentional. *)
-
-Section Type_Equivalence.
-
-  Definition type_eq : relation Type :=
-    fun x y => x = y.
-  
-  Program Instance type_equivalence : Equivalence Type type_eq.
-  
-  Next Obligation. 
-  Proof. unfold type_eq in *. subst. reflexivity. Qed.
-
-End Type_Equivalence.
-
-(** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *)
-
-Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
-  pequiv_prf :> PER carrier pequiv.
-
-Definition pequiv [ PartialEquivalence A R ] : relation A := R.
-Typeclasses unfold @pequiv.
-
-(** Overloaded notation for partial equiv equivalence. *)
-
-Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
-
 Section Respecting.
 
   (** Here we build an equivalence instance for functions which relates respectful ones only, 
@@ -180,12 +132,13 @@ Section Respecting.
 
 End Respecting.
 
-(** The default equivalence on function spaces. *)
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
 Program Instance [ Equivalence A eqA ] => 
-  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA).
+  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9.
 
   Next Obligation.
   Proof.
     transitivity (y x0) ; auto.
   Qed.
+