New algorithm to resolve morphisms, after discussion with Nicolas

Tabareau: 
- first pass: generation of the Morphism constraints with metavariables
  for unspecified relations by one fold over the term. 
  This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
  solution for all the evars at once. 
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.

Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.


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

6 files changed, 420 insertions, 348 deletions

diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index b5352e720..aec260873 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1 +1 @@
-Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto.
+Ltac typeclass_instantiation := eauto with typeclass_instances || eauto.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
new file mode 100644
index 000000000..09a58fa01
--- /dev/null
+++ b/theories/Classes/Morphisms.v
@@ -0,0 +1,350 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Typeclass-based morphisms with standard instances for equivalence relations.
+ 
+   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 $ *)
+
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Init.
+Require Export Coq.Classes.Relations.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Morphisms.
+
+   We now turn to the definition of [Morphism] and declare standard instances. 
+   These will be used by the [clrewrite] tactic later. *)
+
+(** Respectful morphisms. *)
+
+Definition respectful_depT (A : Type) (R : relationT A) 
+  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
+  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
+
+Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
+  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
+
+Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
+  fun f g => forall x y : A, R x y -> R' (f x) (g y).
+
+(** Notations reminiscent of the old syntax for declaring morphisms.
+   We use three + or - for type morphisms, and two for [Prop] ones.
+   *)
+
+Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
+Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+
+Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
+Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
+
+(** 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 : relationT A) (m : A) :=
+  respect : R m m.
+
+(** Here we build an equivalence instance for functions which relates respectful ones only. *)
+
+Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+  { morph : A -> B | respectful R R' morph morph }.
+
+Ltac obligations_tactic ::= program_simpl.
+
+Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
+  respecting_equiv : Equivalence respecting
+  (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    destruct x ; simpl.
+    apply r ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    sym ; apply H.
+    sym ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    trans ((`y) y0).
+    apply H ; auto.
+    apply H0. refl.
+  Qed.
+
+(** Can't use the definition [notT] as it gives a universe inconsistency. *)
+
+Ltac obligations_tactic ::= program_simpl ; simpl_relation.
+
+Program Instance notT_arrow_morphism : 
+  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
+
+Program Instance not_iso_morphism : 
+  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
+
+Program Instance not_impl_morphism :
+  Morphism (Prop -> Prop) (impl --> impl) not.
+
+Program Instance not_iff_morphism : 
+  Morphism (Prop -> Prop) (iff ++> iff) not.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** Leibniz *)
+
+Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)).
+Proof. intros ; constructor ; intros.
+  obligations_tactic.
+  subst.
+  intuition.
+Qed.
+
+(* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *)
+
+(** Any binary morphism respecting some relations up to [iff] respects 
+   them up to [impl] in each way. Very important instances as we need [impl]
+   morphisms at the top level when we rewrite. *)
+
+Program Instance `A` (R : relation A) `B` (R' : relation B)
+  [ ? Morphism (R ++> R' ++> iff) m ] =>
+
+  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+Program Instance `A` (R : relation A) `B` (R' : relation B)
+  [ ? Morphism (R ++> R' ++> iff) m ] =>
+  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+(** The complement of a relation conserves its morphisms. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
+
+  Next Obligation.
+  Proof.
+    unfold complement ; intros.
+    pose (respect).
+    pose (r x y H).
+    pose (r0 x0 y0 H0).
+    intuition.
+  Qed.
+
+(** The inverse too. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
+
+  Next Obligation.
+  Proof.
+    unfold inverse ; unfold flip.
+    apply respect ; auto.
+  Qed.
+
+(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
+(*   fun x y => R x y -> R' (f x) (f y). *)
+
+(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *)
+(*   [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
+(* intros. *)
+(* destruct H. *)
+(* red in respect0. *)
+(* red.  *)
+(* apply respect0. *)
+(* Qed. *)
+
+(* Existing Instance morphism_respectful'. *)
+
+(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
+(*   [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
+(*   intros. *)
+(*   cut (relation A) ; intros R'. *)
+(*   cut ((eqA ++> R') m' m') ; intros. *)
+(*   assert({ R' : relation A & Reflexive R' }). *)
+(*   econstructor. *)
+(*   typeclass_instantiation. *)
+  
+
+(*   assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *)
+(*   eapply ex_intro. *)
+(*   unfold respectful. *)
+(*   typeclass_instantiation. *)
+  
+
+(*   assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *)
+(*   typeclass_instantiation. *)
+(*   Set Printing All. *)
+(*   Show Proof. *)
+  
+  
+(*   apply respect. *)
+
+(** Partial applications are ok when a proof of refl is available. *)
+
+(** A proof of [R x x] is available. *)
+
+(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *)
+(*   [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
+(*   morphism_partial_app_morphism : ? Morphism R' (m x). *)
+
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     apply (respect (m:=m))... *)
+(*     apply respect. *)
+(*   Qed. *)
+
+
+(** Morpshism declarations for partial applications. *)
+
+Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+  trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+  trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans x0...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+  trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+    sym...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+  trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans x0...
+    sym...
+  Qed.
+
+Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
+  equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; trans x0...
+    intros.
+    trans y...
+    sym...
+  Qed.
+
+(** With symmetric relations, variance is no issue ! *)
+
+Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
+  [ Morphism _ (R ++> R') m ] => 
+  sym_contra_morphism : ? Morphism (R --> R') m.
+
+  Next Obligation.
+  Proof with auto.
+    repeat (red ; intros). apply respect.
+    sym...
+  Qed.
+
+(** [R] is reflexive, hence we can build the needed proof. *)
+
+Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
+  [ ? Morphism (R ++> R') m ] (x : A) =>
+  reflexive_partial_app_morphism : ? Morphism R' (m x).
+
+  Next Obligation.
+  Proof with auto.
+    intros.
+    apply (respect (m:=m))...
+    refl.
+  Qed.
+
+(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
+  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    trans x0... trans x... sym...
+  
+    trans y... trans y0... sym...
+  Qed.
+
+Program Instance [ Equivalence A (R : relation A) ] => 
+  equiv_morphism : ? Morphism (R ++> R ++> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    trans x0... trans x... sym...
+  
+    trans y... trans y0... sym...
+  Qed.
+
+(** In case the rewrite happens at top level. *)
+
+Program Instance iff_inverse_impl_id : 
+  ? Morphism (iff ++> inverse impl) id.
+
+Program Instance inverse_iff_inverse_impl_id : 
+  ? Morphism (iff --> inverse impl) id.
+  
+Program Instance iff_impl_id : 
+  ? Morphism (iff ++> impl) id.
+
+Program Instance inverse_iff_impl_id : 
+  ? Morphism (iff --> impl) id.
+  
+(** Standard instances for [iff] and [impl]. *)
+
+(** Logical conjunction. *)
+
+(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *)
+
+(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *)
+
+Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
+
+(** Logical disjunction. *)
+
+(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *)
+
+(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *)
+
+Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index 6ecd4ac3c..694cab59b 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -7,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
-   TODO: explain clrewrite, clsubstitute and so on.
+(* Typeclass-based relations, tactics and standard instances.
+   This is the basic theory needed to formalize morphisms and setoids.
  
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
    91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
@@ -25,14 +25,14 @@ Unset Strict Implicit.
 Definition relationT A := A -> A -> Type.
 Definition relation A := A -> A -> Prop.
 
-Definition inverse A (R : relation A) : relation A := flip R.
+Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
 Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
 
-Definition complementT A (R : relationT A) := fun x y => ! R x y.
+Definition complementT A (R : relationT A) := fun x y => notT (R x y).
 
-Definition complement A (R : relation A) := fun x y => ~ R x y.
+Definition complement A (R : relation A) := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
@@ -112,7 +112,6 @@ Program Instance [ Reflexive A (R : relation A) ] =>
 
   Next Obligation. 
   Proof. 
-    unfold complement in * ; intros.
     apply H.
     apply reflexive.
   Qed.
@@ -122,7 +121,6 @@ Program Instance [ Irreflexive A (R : relation A) ] =>
 
   Next Obligation. 
   Proof. 
-    unfold complement in * ; intros.
     red ; intros.
     apply (irreflexive H).
   Qed.
@@ -131,12 +129,54 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symm
 
   Next Obligation.
   Proof.
-    unfold complement in *.
     red ; intros H'.
     apply (H (symmetric H')).
   Qed.
 
-(** Tactics to solve goals. Each tactic comes in two flavors:
+(** * Standard instances. *)
+
+Ltac simpl_relation :=
+  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
+    repeat (red ; intros) ; try ( solve [ intuition ]).
+
+Ltac obligations_tactic ::= simpl_relation.
+
+(** The arrow is a reflexive and transitive relation on types. *)
+
+Program Instance arrow_refl : ? Reflexive arrow := 
+  reflexive X := id.
+
+Program Instance arrow_trans : ? Transitive arrow := 
+  transitive X Y Z f g := g o f.
+
+(** Isomorphism. *)
+
+Definition iso (A B : Type) := 
+  A -> B * B -> A.
+
+Program Instance iso_refl : ? Reflexive iso.
+Program Instance iso_sym : ? Symmetric iso.
+Program Instance iso_trans : ? Transitive iso.
+
+(** Logical implication. *)
+
+Program Instance impl_refl : ? Reflexive impl.
+Program Instance impl_trans : ? Transitive impl.
+
+(** Logical equivalence. *)
+
+Program Instance iff_refl : ? Reflexive iff.
+Program Instance iff_sym : ? Symmetric iff.
+Program Instance iff_trans : ? Transitive iff.
+
+(** Leibniz equality. *)
+
+Program Instance eq_refl : ? Reflexive (@eq A).
+Program Instance eq_sym : ? Symmetric (@eq A).
+Program Instance eq_trans : ? Transitive (@eq A).
+
+(** ** General tactics to solve goals on relations.
+   Each tactic comes in two flavors:
    - a tactic to immediately solve a goal without user intervention
    - a tactic taking input from the user to make progress on a goal *)
 
@@ -216,6 +256,9 @@ Ltac relation_trans :=
 
     | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => 
       apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
+      apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H')
   end.
 
 Ltac relation_transitive Y := 
@@ -242,254 +285,13 @@ Ltac trans Y := relation_transitive Y.
 
 Ltac relation_tac := relation_refl || relation_sym || relation_trans.
 
-(** * Morphisms.
-
-   We now turn to the definition of [Morphism] and declare standard instances. 
-   These will be used by the [clrewrite] tactic later. *)
-
-(** Respectful morphisms. *)
-
-Definition respectful_depT (A : Type) (R : relationT A) 
-  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
-  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
-
-Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
-  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
-
-Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
-  fun f g => forall x y : A, R x y -> R' (f x) (g y).
-
-(** Notations reminiscent of the old syntax for declaring morphisms.
-   We use three + or - for type morphisms, and two for [Prop] ones.
-   *)
-
-Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
-Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
-
-Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
-Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
-
-(** 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 : relationT A) (m : A) :=
-  respect : R m m.
-
-Ltac simpl_morphism :=
-  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
-    try (red ; intros) ; try ( solve [ intuition ]).
-
-Ltac obligations_tactic ::= simpl_morphism.
-
-(** The arrow is a reflexive and transitive relation on types. *)
-
-Program Instance arrow_refl : ? Reflexive arrow := 
-  reflexive X := id.
-
-Program Instance arrow_trans : ? Transitive arrow := 
-  transitive X Y Z f g := g o f.
-
-(** Can't use the definition [notT] as it gives a to universe inconsistency. *)
-
-Program Instance notT_arrow_morphism : 
-  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
-
-(** Isomorphism. *)
-
-Definition iso (A B : Type) := 
-  A -> B * B -> A.
-
-Program Instance iso_refl : ? Reflexive iso.
-Program Instance iso_sym : ? Symmetric iso.
-Program Instance iso_trans : ? Transitive iso.
-
-Program Instance not_iso_morphism : 
-  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
-
-(** Logical implication. *)
-
-Program Instance impl_refl : ? Reflexive impl.
-Program Instance impl_trans : ? Transitive impl.
-
-Program Instance not_impl_morphism :
-  Morphism (Prop -> Prop) (impl --> impl) not.
-
-(** Logical equivalence. *)
-
-Program Instance iff_refl : ? Reflexive iff.
-Program Instance iff_sym : ? Symmetric iff.
-Program Instance iff_trans : ? Transitive iff.
-
-Program Instance not_iff_morphism : 
-  Morphism (Prop -> Prop) (iff ++> iff) not.
-
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
-
-(** If you have a morphism from [RA] to [RB] you have a contravariant morphism 
-   from [RA] to [inverse RB]. *)
-
-Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] =>
-  morph_impl_co_contra_inverse :
-  ? Morphism (RA --> inverse RB) m.
-
-  Next Obligation.
-  Proof.
-    apply respect.
-    apply H.
-  Qed.
-
-(** Every transitive relation gives rise to a binary morphism on [impl], 
-   contravariant in the first argument, covariant in the second. *)
-
-Program Instance [ Transitive A (R : relation A) ] => 
-  trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R.
-
-  Next Obligation.
-  Proof with auto.
-    trans x...
-    trans x0...
-  Qed.
-
-(** Dually... *)
-
-Program Instance [ Transitive A (R : relation A) ] =>
-  trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R.
-
-  Obligations Tactic := idtac.
-  
-  Next Obligation.
-  Proof with auto.
-    intros.
-    destruct (trans_contra_co_morphism (R:=inverse R)).
-    revert respect0.
-    unfold respectful, inverse, flip in * ; intros.
-    apply respect0 ; auto.
-  Qed.
-
-Obligations Tactic := simpl_morphism.
-
-(** With symmetric relations, variance is no issue ! *)
-
-Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
-  [ Morphism _ (R ++> R') m ] => 
-  sym_contra_morphism : ? Morphism (R --> R') m.
-
-  Next Obligation.
-  Proof with auto.
-    apply respect.
-    sym...
-  Qed.
-
-(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
-
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
-  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    trans x0... trans x... sym...
-  
-    trans y... trans y0... sym...
-  Qed.
-
-(** The complement of a relation conserves its morphisms. *)
-
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
-
-  Next Obligation.
-  Proof.
-    red ; unfold complement ; intros.
-    pose (respect).
-    pose (r x y H).
-    pose (r0 x0 y0 H0).
-    intuition.
-  Qed.
-
-(** The inverse too. *)
-
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
-
-  Next Obligation.
-  Proof.
-    unfold inverse ; unfold flip.
-    apply respect ; auto.
-  Qed.
-
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
-  trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R.
-
-  Next Obligation.
-  Proof with auto.
-    trans y...
-    sym...
-    trans y0...
-    sym...
-  Qed.
-
-(** Any binary morphism respecting some relations up to [iff] respects 
-   them up to [impl] in each way. Very important instances as we need [impl]
-   morphisms at the top level when we rewrite. *)
-
-Program Instance `A` (R : relation A) `B` (R' : relation B) 
-  [ ? Morphism (R ++> R' ++> iff) m ] => 
-  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
-
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
-
-Program Instance `A` (R : relation A) `B` (R' : relation B)
-  [ ? Morphism (R ++> R' ++> iff) m ] => 
-  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
-
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
-
-(** Standard instances for [iff] and [impl]. *)
-
-(** Logical conjunction. *)
-
-Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
-
-Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
-
-Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
-
-(** Logical disjunction. *)
-
-Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
-
-Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
-
-Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
-
-(** Leibniz equality. *)
-
-Program Instance eq_refl : ? Reflexive (@eq A).
-Program Instance eq_sym : ? Symmetric (@eq A).
-Program Instance eq_trans : ? Transitive (@eq A).
-
-Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) :=
-  trans_sym_morphism.
-
-Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m.
-
 (** The [PER] typeclass. *)
 
 Class PER (carrier : Type) (pequiv : relationT carrier) :=
   per_sym :> Symmetric pequiv ;
   per_trans :> Transitive pequiv.
 
-(** We can build a PER on the coq function space if we have PERs on the domain and
+(** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
 Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => 
@@ -520,38 +322,10 @@ Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] =>
 
   Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto.
 
-(** Here we build an equivalence instance for functions which relates respectful ones only. *)
-
-Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
-  { morph : A -> B | respectful R R' morph morph }.
-
-Ltac obligations_tactic ::= program_simpl.
-
-Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
-  respecting_equiv : Equivalence respecting
-  (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
+Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => 
+  inverse_antisymmetric : ? Antisymmetric eq (inverse R).
 
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    destruct x ; simpl.
-    apply r ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    sym ; apply H.
-    sym ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    trans ((`y) y0).
-    apply H ; auto.
-    apply H0. refl.
-  Qed.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply antisymmetric ; eauto.
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 78e53aa01..5e18ef2af 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -23,6 +23,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
@@ -30,6 +31,10 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence A equiv.
 
+Program Instance [ eqa : Equivalence A (eqA : relation A) ] => 
+  equivalence_setoid : Setoid A :=
+  equiv := eqA ; setoid_equiv := eqa.
+
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
@@ -43,8 +48,8 @@ Proof. eauto with typeclass_instances. Qed.
 
 (** Standard setoids. *)
 
-Program Instance eq_setoid : Setoid A :=
-  equiv := eq ; setoid_equiv := eq_equivalence.
+(* Program Instance eq_setoid : Setoid A := *)
+(*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
 Program Instance iff_setoid : Setoid Prop :=
   equiv := iff ; setoid_equiv := iff_equivalence.
@@ -56,14 +61,7 @@ Program Instance iff_setoid : Setoid Prop :=
 
 Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
-
-Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
-Proof with auto.
-  intros ; red ; intros.
-  apply H.
-  sym...
-Qed.
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -82,15 +80,15 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
-Proof.
-  intros; intro. 
+Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Proof with auto.
+  intros; intro.
   assert(z == y) by relation_sym.
   assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y == x) by relation_sym.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 39809865c..fb7f8827b 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -39,51 +39,3 @@ Ltac setoideq_ext :=
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
   end.
 
-Ltac setoid_tactic :=
-  match goal with
-    | [ H : ?eq ?x ?y |- ?eq ?y ?x ] => sym ; apply H
-    | [ |- ?eq ?x ?x ] => refl
-    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-      
-    | [ H : ?eq ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
-    | [ |- @equiv _ _ _ ?x ?x ] => refl
-    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-
-    | [ H : @equiv ?A ?R ?s ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
-    | [ |- @equiv _ _ _ ?x ?x ] => refl
-    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-
-    | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tactic
-  end.
-(** Need to fix fresh to not fail if some arguments are not identifiers. *)
-(* Ltac setoid_sat ::= *)
-(*   match goal with *)
-(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
-(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
-(*   end. *)
-
-Ltac setoid_sat :=
-  match goal with
-    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
-    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
-  end.
-Ltac setoid_saturate := repeat setoid_sat.
-
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index e5bc98dee..014ff3a01 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -139,5 +139,3 @@ Tactic Notation "exist" constr(x) := exists x.
 Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
 Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
 Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
-
-Notation " ! A " := (notT A) (at level 200, A at level 100) : type_scope.