Do another pass on the typeclasses code. Correct globalization of class

names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code. 
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class. 
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].


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

6 files changed, 129 insertions, 181 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 5543f615d..dd9cfbca5 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -35,16 +35,16 @@ Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_refl : reflexive equiv.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_sym : symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+Program Instance [ sa : ! Equivalence A ] => equiv_trans : transitive equiv.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 11c60a3aa..2795e4218 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -22,10 +22,10 @@ Require Export Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
 Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 4fbbe2a40..c752cae86 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -46,7 +46,7 @@ Notation " R --> R' " := (@respectful _ _ (inverse R) R') (right associativity,
    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) :=
+Class Morphism A (R : relation A) (m : A) : Prop :=
   respect : R m m.
 
 (** Here we build an equivalence instance for functions which relates respectful ones only. *)
@@ -54,7 +54,6 @@ Class Morphism A (R : relation A) (m : A) :=
 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, Equivalence B R' ] => 
@@ -63,21 +62,21 @@ Program Instance [ Equivalence A R, Equivalence B R' ] =>
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     destruct x ; simpl.
     apply r ; auto.
   Qed.
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     symmetry ; apply H.
     symmetry ; auto.
   Qed.
 
   Next Obligation.
   Proof.
-    constructor ; intros.
+    red ; intros.
     transitivity (proj1_sig y y0).
     apply H ; auto.
     apply H0. reflexivity.
@@ -116,51 +115,32 @@ Typeclasses unfold relation.
    them up to [impl] in each way. Very important instances as we need [impl]
    morphisms at the top level when we rewrite. *)
 
-Class SubRelation A (R S : relation A) :=
+Class SubRelation A (R S : relation A) : Prop :=
   subrelation :> Morphism (S ==> R) id.
 
 Instance iff_impl_subrelation : SubRelation Prop impl iff.
-Proof.
-  constructor ; red ; intros.
-  tauto.
-Qed.
+Proof. reduce. tauto. Qed.
 
 Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff.
 Proof.
-  constructor ; red ; intros.
-  tauto.
+  reduce. tauto.
 Qed.
 
-Instance [ SubRelation A R₁ R₂ ] =>
+Instance [ sub : SubRelation A R₁ R₂ ] =>
   morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂).
 Proof.
-  constructor ; repeat red. intros x y H x₁ y₁ H₁.
-  destruct subrelation.
-  red in respect0, H ; unfold id in *.
-  apply respect0.
-  apply H.
-  apply H₁.
+  reduce. apply* sub. apply H. assumption.
 Qed.
 
-Instance [ SubRelation A R₂ R₁ ] =>
+Instance [ sub : SubRelation A R₂ R₁ ] =>
   morphisms_subrelation_left : SubRelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
 Proof.
-  constructor ; repeat red ; intros x y H x₁ y₁ H₁.
-  destruct subrelation.
-  red in respect0, H ; unfold id in *.
-  apply H.
-  apply respect0.
-  apply H₁.
+  reduce. apply* H.  apply* sub. assumption.
 Qed.
 
 Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m.
 Proof.
-  intros.
-  destruct subrelation.
-  red in respect0 ; intros.
-  constructor.
-  unfold id in * ; apply respect0.
-  apply respect.
+  intros. apply* H. apply H0.
 Qed.
 
 Inductive done : nat -> Type :=
@@ -183,7 +163,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (* Typeclasses eauto := debug. *)
 
-Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ ! symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m.
 
   Next Obligation.
   Proof.
@@ -192,12 +172,12 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => 
   complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
-    unfold complement ; intros.
+    unfold complement.
     pose (respect).
     pose (r x y H).
     pose (r0 x0 y0 H0).
@@ -211,7 +191,6 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
 
   Next Obligation.
   Proof.
-    unfold inverse ; unfold flip.
     apply respect ; auto.
   Qed.
 
@@ -226,7 +205,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
 (** 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) ] => 
+Program Instance [ ! transitive A (R : relation A) ] => 
   trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
@@ -237,19 +216,15 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Dually... *)
 
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ ! transitive A (R : relation A) ] =>
   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
   
   Next Obligation.
   Proof with auto.
-    intros.
-    destruct (trans_contra_co_morphism (R:=inverse R)).
-    revert respect0.
-    unfold respectful, inverse, flip, impl in * ; intros.
-    eapply respect0 ; eauto.
+    apply* trans_contra_co_morphism ; eauto. eauto.
   Qed.
 
-(* Program Instance [ Transitive A (R : relation A), Symmetric A R ] => *)
+(* 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. *)
@@ -263,7 +238,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ ! transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -271,7 +246,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ ! transitive A R ] (x : A) =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -279,22 +254,20 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity y...
-    symmetry...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ ! transitive A R, symmetric R ] (x : A) =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
-    symmetry...
   Qed.
 
 Program Instance [ Equivalence A R ] (x : A) =>
@@ -311,7 +284,7 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** With symmetric relations, variance is no issue ! *)
 
 (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
-(*   [ Morphism _ (R ==> R') m ] [ Symmetric A R ] =>  *)
+(*   [ Morphism _ (R ==> R') m ] [ symmetric A R ] =>  *)
 (*   sym_contra_morphism : Morphism (R --> R') m. *)
 
 (*   Next Obligation. *)
@@ -323,48 +296,39 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** [R] is reflexive, hence we can build the needed proof. *)
 
 Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+  [ Morphism (R ==> R') m ] [ reflexive R ] (x : A) =>
   reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
-  Next Obligation.
-  Proof with auto.
-    intros.
-    apply (respect (m:=m))...
-    reflexivity.
-  Qed.
-
 (** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ ! transitive A R ] => 
   trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
-    subst x0...
   Qed.
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ ! transitive A R ] => 
   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
   Proof with auto.
     transitivity x...
-    subst x0...
   Qed.
 
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ ! Transitive A R, Symmetric R ] => 
+Program Instance [ ! transitive A R, symmetric R ] => 
   trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
     split ; intros.
-    transitivity x0... transitivity x... symmetry...
+    transitivity x0... transitivity x...
   
-    transitivity y... transitivity y0... symmetry...
+    transitivity y... transitivity y0... 
   Qed.
 
 Program Instance [ Equivalence A R ] => 
@@ -443,12 +407,12 @@ Program Instance or_iff_morphism :
 (*   red ; intros. subst ; split; trivial. *)
 (* Qed. *)
 
-Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
+Instance (A B : Type) [ ! reflexive B R ] (m : A -> B) =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
-Instance (A B : Type) [ ! Reflexive B R' ] => 
-  Reflexive (@Logic.eq A ==> R').
+Instance (A B : Type) [ ! reflexive B R' ] => 
+  reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
 (** [respectful] is a morphism for relation equivalence. *)
@@ -481,12 +445,13 @@ Proof.
   split ; intros ; intuition.
 Qed.
 
-Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) :=
+Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop :=
   normalizes : R m m'.
 
 Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
   Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof.
+  reduce.
   symmetry ; apply inverse_respectful.
 Qed.
 
@@ -494,6 +459,7 @@ Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B)
   [ Normalizes relation_equivalence R' (inverse R'') ] =>
   Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
 Proof.
+  red.
   pose normalizes.
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
@@ -504,19 +470,13 @@ Program Instance (A : Type) (R : relation A)
   [ Morphism R m ] => morphism_inverse_morphism :
   Morphism (inverse R) m | 2.
 
-  Next Obligation.
-  Proof.
-    apply respect.
-  Qed.
-
 (** Bootstrap !!! *)
 
 Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
 Proof.
-  simpl_relation.
-  subst.
+  simpl_relation. 
   unfold relation_equivalence in H.
-  split ; constructor ; intros.
+  split ; red ; intros.
   setoid_rewrite <- H.
   apply respect.
   setoid_rewrite H.
@@ -527,7 +487,7 @@ Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
   [ Normalizes relation_equivalence R R' ]
   [ Morphism R' m ] : Morphism R m.
 Proof.
-  intros. 
+  intros.
   pose respect.
   assert(n:=normalizes).
   setoid_rewrite n.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b053b27f2..53079674f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -50,133 +50,139 @@ Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
-Class Reflexive A (R : relation A) :=
-  reflexive : forall x, R x x.
+Class reflexive A (R : relation A) :=
+  reflexivity : forall x, R x x.
 
-Class Irreflexive A (R : relation A) := 
-  irreflexive : forall x, R x x -> False.
+Class irreflexive A (R : relation A) := 
+  irreflexivity : forall x, R x x -> False.
 
-Class Symmetric A (R : relation A) := 
-  symmetric : forall x y, R x y -> R y x.
+Class symmetric A (R : relation A) := 
+  symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric A (R : relation A) := 
-  asymmetric : forall x y, R x y -> R y x -> False.
+Class asymmetric A (R : relation A) := 
+  asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive A (R : relation A) := 
-  transitive : forall x y z, R x y -> R y z -> R x z.
+Class transitive A (R : relation A) := 
+  transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments Reflexive [A].
-Implicit Arguments Irreflexive [A].
-Implicit Arguments Symmetric [A].
-Implicit Arguments Asymmetric [A].
-Implicit Arguments Transitive [A].
+Implicit Arguments reflexive [A].
+Implicit Arguments irreflexive [A].
+Implicit Arguments symmetric [A].
+Implicit Arguments asymmetric [A].
+Implicit Arguments transitive [A].
 
-Hint Resolve @irreflexive : ord.
+Hint Resolve @irreflexivity : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) :=
-  reflexive := reflexive (R:=R).
+Program Instance [ ! reflexive A R ] => flip_reflexive : reflexive (flip R) :=
+  reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) :=
-  irreflexive := irreflexive (R:=R).
+Program Instance [ ! irreflexive A R ] => flip_irreflexive : irreflexive (flip R) :=
+  irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R).
+Program Instance [ ! symmetric A R ] => flip_symmetric : symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R).
+Program Instance [ ! asymmetric A R ] => flip_asymmetric : asymmetric (flip R).
   
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric.
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R).
+Program Instance [ ! transitive A R ] => flip_transitive : transitive (flip R).
 
-  Solve Obligations using unfold flip ; program_simpl ; clapply transitive.
+  Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) :=
-  reflexive := reflexive (R:=R).
+Program Instance [ ! reflexive A (R : relation A) ] => inverse_reflexive : reflexive (inverse R) :=
+  reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) :=
-  irreflexive := irreflexive (R:=R).
+Program Instance [ ! irreflexive A (R : relation A) ] => inverse_irreflexive : irreflexive (inverse R) :=
+  irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R).
+Program Instance [ ! symmetric A (R : relation A) ] => inverse_symmetric : symmetric (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R).
+Program Instance [ ! asymmetric A (R : relation A) ] => inverse_asymmetric : asymmetric (inverse R).
   
-  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric.
+  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R).
+Program Instance [ ! transitive A (R : relation A) ] => inverse_transitive : transitive (inverse R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ ! Reflexive A (R : relation A) ] => 
-  reflexive_complement_irreflexive : Irreflexive (complement R).
+Program Instance [ ! reflexive A (R : relation A) ] => 
+  reflexive_complement_irreflexive : irreflexive (complement R).
 
-  Next Obligation. 
-  Proof. 
-    apply H.
-    apply reflexive.
-  Qed.
-
-Program Instance [ ! Irreflexive A (R : relation A) ] => 
-  irreflexive_complement_reflexive : Reflexive (complement R).
+Program Instance [ ! irreflexive A (R : relation A) ] => 
+  irreflexive_complement_reflexive : reflexive (complement R).
 
   Next Obligation. 
   Proof. 
     red. intros H.
-    apply (irreflexive H).
+    apply (irreflexivity H).
   Qed.
 
-Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R).
+Program Instance [ ! symmetric A (R : relation A) ] => complement_symmetric : symmetric (complement R).
 
   Next Obligation.
   Proof.
     red ; intros H'.
-    apply (H (symmetric H')).
+    apply (H (symmetry H')).
   Qed.
 
 (** * Standard instances. *)
 
+Ltac reduce_goal :=
+  match goal with
+    | [ |- _ <-> _ ] => fail 1
+    | _ => red ; intros ; try reduce_goal
+  end.
+
+Ltac reduce := reduce_goal.
+
+Tactic Notation "apply" "*" constr(t) := 
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
 Ltac simpl_relation :=
-  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
-    repeat (red ; intros) ; try ( solve [ intuition ]).
+  unfold inverse, flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ intuition ]).
 
 Ltac obligations_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
-Program Instance impl_refl : Reflexive impl.
-Program Instance impl_trans : Transitive impl.
+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.
+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).
+Program Instance eq_refl : reflexive (@eq A).
+Program Instance eq_sym : symmetric (@eq A).
+Program Instance eq_trans : transitive (@eq A).
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
 (** A [PreOrder] is both reflexive and transitive. *)
 
 Class PreOrder A (R : relation A) :=
-  preorder_refl :> Reflexive R ;
-  preorder_trans :> Transitive R.
+  preorder_refl :> reflexive R ;
+  preorder_trans :> transitive R.
 
 (** A partial equivalence relation is symmetric and transitive. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
-  per_sym :> Symmetric pequiv ;
-  per_trans :> Transitive pequiv.
+  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
    codomain. *)
@@ -187,33 +193,28 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 
   Next Obligation.
   Proof with auto.
-    constructor ; intros...
     assert(R x0 x0). 
-    clapply transitive. clapply symmetric.
-    clapply transitive. 
+    transitivity y0... symmetry...
+    transitivity (y x0)...
   Qed.
 
 (** The [Equivalence] typeclass. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) :=
-  equiv_refl :> Reflexive equiv ;
-  equiv_sym :> Symmetric equiv ;
-  equiv_trans :> Transitive equiv.
+  equiv_refl :> reflexive equiv ;
+  equiv_sym :> symmetric equiv ;
+  equiv_trans :> transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
-  antisymmetric : forall x y, R x y -> R y x -> eqA x y.
-
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
-  flip_antisymmetric : Antisymmetric eq (flip R).
-
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
+Class [ Equivalence A eqA ] => antisymmetric (R : relation A) := 
+  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
-  inverse_antisymmetric : Antisymmetric eq (inverse R).
+Program Instance [ eq : Equivalence A eqA, antisymmetric eq R ] => 
+  flip_antisymmetric : antisymmetric eq (flip R).
 
-  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
+Program Instance [ eq : Equivalence A eqA, antisymmetric eq (R : relation A) ] => 
+  inverse_antisymmetric : antisymmetric eq (inverse R).
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
@@ -240,18 +241,6 @@ Program Instance relation_equivalence_equivalence :
 
   Next Obligation.
   Proof.
-    constructor ; red ; intros.
-    apply reflexive.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; red ; intros.
-    apply symmetric ; apply H.
-  Qed.
-  
-  Next Obligation.
-  Proof.
-    constructor ; red ; intros.
-    apply transitive with (y x0 y0) ; [ apply H | apply H0 ].
+    unfold relation_equivalence in *.
+    apply transitivity with (y x0 y0) ; [ apply H | apply H0 ].
   Qed.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5cf33542c..d2ee4f443 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -40,13 +40,13 @@ Typeclasses unfold @equiv.
 
 (** Shortcuts to make proof search easier. *)
 
-Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Definition setoid_refl [ sa : Setoid A ] : reflexive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Definition setoid_sym [ sa : Setoid A ] : symmetric equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Definition setoid_trans [ sa : Setoid A ] : transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
 Existing Instance setoid_refl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 9f6dfab42..ee8c530fa 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -74,7 +74,7 @@ Ltac red_subst_eq_morphism concl :=
 
 Ltac destruct_morphism :=
   match goal with
-    | [ |- @Morphism ?A ?R ?m ] => constructor
+    | [ |- @Morphism ?A ?R ?m ] => red
   end.
 
 Ltac reverse_arrows x :=
@@ -91,4 +91,3 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
-