- A little cleanup in Classes/*. Separate standard morphisms on

relf/sym/trans relations from morphisms on prop connectives and
relations.
- Add general order theory on predicates, instantiated for relations.
Derives equivalence, implication, conjunction and disjunction as
liftings from propositional connectives. Can be used for n-ary
homogeneous predicates thanks to a bit of metaprogramming with lists of
types. 
- Rebind Setoid_Theory to use the Equivalence record type instead of
declaring an isomorphic one. One needs to do "red" after constructor to
get the same statements when building objects of type Setoid_Theory, so
scripts break.


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

12 files changed, 488 insertions, 363 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 0ec6c11f9..d7774a2d7 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -35,23 +35,25 @@ Instance [ Equivalence A R ] =>
 
 Definition equiv [ Equivalence A R ] : relation A := R.
 
-(** Shortcuts to make proof search possible (unification won't unfold equiv). *)
+Typeclasses unfold @equiv.
 
-Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
+(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *)
 
-Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
+(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *)
 
-  Next Obligation.
-  Proof.
-    symmetry ; auto.
-  Qed.
+(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *)
 
-Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     symmetry ; auto. *)
+(*   Qed. *)
 
-  Next Obligation.
-  Proof.
-    transitivity y ; auto.
-  Qed.
+(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     transitivity y ; auto. *)
+(*   Qed. *)
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -64,23 +66,6 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
   
 Open Local Scope equiv_scope.
 
-(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
-
-Ltac setoid_subst H := 
-  match type of H with
-    ?x === ?y => substitute H ; clear H x
-  end.
-
-Ltac setoid_subst_nofail :=
-  match goal with
-    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
-    | _ => idtac
-  end.
-  
-(** [subst*] will try its best at substituting every equality in the goal. *)
-
-Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
-
 Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
@@ -97,6 +82,23 @@ Proof.
   contradiction.
 Qed.
 
+(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *)
+
+Ltac setoid_subst H := 
+  match type of H with
+    ?x === ?y => substitute H ; clear H x
+  end.
+
+Ltac setoid_subst_nofail :=
+  match goal with
+    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
+
 Ltac equiv_simplify_one :=
   match goal with
     | [ H : ?x === ?x |- _ ] => clear H
@@ -117,34 +119,28 @@ 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 ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *)
+(*   respect := respect. *)
 
-Instance [ sa : Equivalence A ] (x : A) => 
-  equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
-  respect := respect. 
+(* (** The partial application too as it is Reflexive. *) *)
 
-Definition type_eq : relation Type :=
-  fun x y => x = y.
+(* Instance [ sa : Equivalence A ] (x : A) =>  *)
+(*   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *)
+(*   respect := respect.  *)
 
-Program Instance type_equivalence : Equivalence Type type_eq.
+(** Instance not exported by default, as comparing types for equivalence may be unintentional. *)
 
-  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
+Section Type_Equivalence.
 
-Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
-
-Ltac obligations_tactic ::= morphism_tac.
-
-(** These are morphisms used to rewrite at the top level of a proof, 
-   using [iff_impl_id_morphism] if the proof is in [Prop] and
-   [eq_arrow_id_morphism] if it is in Type. *)
-
-Program Instance iff_impl_id_morphism : 
-  Morphism (iff ++> impl) id.
+  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.
 
-(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
+End Type_Equivalence.
 
 (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *)
 
@@ -152,11 +148,32 @@ 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.
 
-(** Reset the default Program tactic. *)
+Section Respecting.
+
+  (** Here we build an equivalence instance for functions which relates respectful ones only, 
+     we do not export it. *)
+
+  Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+    { morph : A -> B | respectful R R' morph morph }.
+  
+  Program Instance [ Equivalence A R, Equivalence B R' ] => 
+    respecting_equiv : Equivalence respecting
+    (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+
+  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    unfold respecting in *. program_simpl. red in H2,H3,H4. 
+    transitivity (y x0) ; auto.
+    transitivity (y y0) ; auto.
+    symmetry. auto.
+  Qed.
 
-Ltac obligations_tactic ::= program_simpl.
+End Respecting.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index d10cb9724..7cabc836d 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based morphisms with standard instances for equivalence relations.
+(* Typeclass-based morphism definition and standard, minimal instances.
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
@@ -26,7 +26,7 @@ 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. *)
+   These will be used by the [setoid_rewrite] tactic later. *)
 
 (** Respectful morphisms. *)
 
@@ -71,49 +71,6 @@ Class Morphism A (R : relation A) (m : A) : Prop :=
 
 Arguments Scope Morphism [type_scope signature_scope].
 
-(** 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, Equivalence B R' ] => 
-  respecting_equiv : Equivalence respecting
-  (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    destruct x ; simpl.
-    apply r ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    symmetry ; apply H.
-    symmetry ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    transitivity (proj1_sig y y0).
-    apply H ; auto.
-    apply H0. reflexivity.
-  Qed.
-
-(** Can't use the definition [notT] as it gives a universe inconsistency. *)
-
-Ltac obligations_tactic ::= program_simpl ; simpl_relation.
-
-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].
@@ -139,41 +96,41 @@ Proof. firstorder. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m.
+Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
 Proof.
-  intros. apply* H. apply H0.
+  intros. apply sub. apply mor.
 Qed.
 
 Instance morphism_subrelation_morphism : 
   Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
 Proof. reduce. subst. firstorder. Qed.
 
-Inductive done : nat -> Type :=
-  did : forall n : nat, done n.
+(** We use an external tactic to manage the application of subrelation, which is otherwise
+   always applicable. We allow its use only once per branch. *)
+
+Inductive subrelation_done : Prop :=
+  did_subrelation : subrelation_done.
 
 Ltac subrelation_tac := 
   match goal with
-    | [ H : done 1 |- @Morphism _ _ _ ] => fail
+    | [ H : subrelation_done |- _ ] => fail
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did 1) ; eapply @subrelation_morphism
+      set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
 
-(* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *)
-
 Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
-(** Logical implication [impl] is a morphism for logical equivalence. *)
+(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
+Instance iff_impl_subrelation : subrelation iff impl.
+Proof. firstorder. Qed.
 
-(* Typeclasses eauto := debug. *)
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Proof. firstorder. Qed.
 
-Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
-
-  Next Obligation.
-  Proof.
-    split ; apply respect ; [ auto | symmetry ] ; auto.
-  Qed.
+Instance [ subrelation A R R' ] => pointwise_subrelation :
+  subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
+Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
@@ -183,28 +140,26 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] =>
   Next Obligation.
   Proof.
     unfold complement.
-    pose (respect).
-    pose (r x y H).
-    pose (r0 x0 y0 H0).
+    pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
 
 (** The inverse too. *)
 
-Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
+Program Instance [ mor : Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
   inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
 
   Next Obligation.
   Proof.
-    apply respect ; auto.
+    apply mor ; auto.
   Qed.
 
-Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
+Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
   flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
-    apply respect ; auto.
+    apply mor ; auto.
   Qed.
 
 (** Every Transitive relation gives rise to a binary morphism on [impl], 
@@ -229,18 +184,6 @@ Program Instance [ Transitive A R ] =>
     apply* trans_contra_co_morphism ; eauto. eauto.
   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. *)
-
-
 (** Morphism declarations for partial applications. *)
 
 Program Instance [ Transitive A R ] (x : A) =>
@@ -286,18 +229,6 @@ Program Instance [ Equivalence A R ] (x : A) =>
     symmetry...
   Qed.
 
-(** 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 ] =>  *)
-(*   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 [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
@@ -360,57 +291,9 @@ Program Instance 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_inverse_impl_iff_morphism : 
-  Morphism (inverse impl ==> iff ==> inverse impl) and.
-
-Program Instance and_iff_inverse_impl_morphism : 
-  Morphism (iff ==> inverse impl ==> inverse 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_inverse_impl_iff_morphism :
-  Morphism (inverse impl ==> iff ==> inverse impl) or.
-
-Program Instance or_iff_inverse_impl_morphism : 
-  Morphism (iff ==> inverse impl ==> inverse impl) or.
-
-Program Instance or_iff_morphism : 
-  Morphism (iff ==> iff ==> iff) or.
-
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-(* Instance {A B : Type} (m : A -> B) => *)
-(*   any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. *)
-(* Proof. *)
-(*   red ; intros. subst ; reflexivity. *)
-(* Qed. *)
-
-(* Instance {A : Type} (m : A -> Prop) => *)
-(*   any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. *)
-(* Proof. *)
-(*   red ; intros. subst ; split; trivial. *)
-(* Qed. *)
-
 Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
@@ -419,18 +302,13 @@ Instance (A : Type) [ Reflexive B R' ] =>
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
-Instance [ Morphism (A -> B) (inverse R ==> R') m ] =>
-  Morphism (R ==> inverse R') m | 10.
-Proof. firstorder. Qed.
-
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
   Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). 
 Proof.
-  do 2 red ; intros.
-  unfold respectful, relation_equivalence in *.
-  red ; intros.
+  reduce.
+  unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
   split ; intros.
   
     rewrite <- H0.
@@ -452,21 +330,18 @@ Proof.
   split ; intros ; intuition.
 Qed.
 
+
 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.
+  Normalizes subrelation (inverse R ==> inverse R') (inverse (R ==> R')) .
+Proof. simpl_relation. Qed.
 
 Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
   ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
-Proof.
-  red.
-  pose normalizes.
+Proof. red ; intros. 
+  pose normalizes as r.
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
@@ -479,23 +354,23 @@ Program Instance [ Morphism A R m ] =>
 
 Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
 Proof.
-  simpl_relation. 
-  unfold relation_equivalence in H.
+  simpl_relation.
+  reduce in H.
   split ; red ; intros.
   setoid_rewrite <- H.
-  apply respect.
+  apply H0.
   setoid_rewrite H.
-  apply respect.
+  apply H0.
 Qed.
-  
+
 Lemma morphism_releq_morphism 
   [ Normalizes (relation A) relation_equivalence R R',
     Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
-  pose respect.
-  assert(n:=normalizes).
-  setoid_rewrite n.
+  pose respect as r.
+  pose normalizes as norm.
+  setoid_rewrite norm.
   assumption.
 Qed.
 
@@ -510,86 +385,3 @@ Ltac morphism_normalization :=
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
 
-(** Morphisms for relations *)
-
-Instance [ PartialOrder A eqA R ] => 
-   partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R.
-Proof with auto.
-  intros. rewrite partial_order_equivalence.
-  simpl_relation. firstorder.
-    transitivity x... transitivity x0... 
-    transitivity y... transitivity y0...
-Qed.
-
-Instance Morphism (relation_equivalence (A:=A) ==> 
-  relation_equivalence ==> relation_equivalence) relation_conjunction.
-  Proof. firstorder. Qed.
-
-Instance Morphism (relation_equivalence (A:=A) ==> 
-  relation_equivalence ==> relation_equivalence) relation_disjunction.
-  Proof. firstorder. Qed.
-
-
-(** Morphisms for quantifiers *)
-
-Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.     
-    split ; intros.
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H in H₁. assumption.
-    
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H. assumption.
-  Qed.
-
-Program Instance {A : Type} => ex_impl_morphism :
-  Morphism (pointwise_relation impl ==> impl) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.  
-    exists H0. apply H. assumption.
-  Qed.
-
-Program Instance {A : Type} => ex_inverse_impl_morphism : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.  
-    exists H0. apply H. assumption.
-  Qed.
-
-Program Instance {A : Type} => all_iff_morphism : 
-  Morphism (pointwise_relation iff ==> iff) (@all A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Program Instance {A : Type} => all_impl_morphism : 
-  Morphism (pointwise_relation impl ==> impl) (@all A).
-  
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Program Instance {A : Type} => all_inverse_impl_morphism : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
-  
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
-Proof. reflexivity. Qed.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
new file mode 100644
index 000000000..d22ab06cb
--- /dev/null
+++ b/theories/Classes/Morphisms_Prop.v
@@ -0,0 +1,131 @@
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Morphism instances for propositional connectives.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Program.Program.
+
+(** Standard instances for [not], [iff] and [impl]. *)
+
+(** Logical negation. *)
+
+Program Instance not_impl_morphism :
+  Morphism (impl --> impl) not.
+
+Program Instance not_iff_morphism : 
+  Morphism (iff ++> iff) not.
+
+(** Logical conjunction. *)
+
+Program Instance and_impl_iff_morphism :
+  Morphism (impl ==> impl ==> impl) and.
+
+(* 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_inverse_impl_iff_morphism :  *)
+(*   Morphism (inverse impl ==> iff ==> inverse impl) and. *)
+
+(* Program Instance and_iff_inverse_impl_morphism :  *)
+(*   Morphism (iff ==> inverse impl ==> inverse impl) and. *)
+
+Program Instance and_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) and.
+
+(** Logical disjunction. *)
+
+Program Instance or_impl_iff_morphism : 
+  Morphism (impl ==> impl ==> impl) or.
+
+(* 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_inverse_impl_iff_morphism : *)
+(*   Morphism (inverse impl ==> iff ==> inverse impl) or. *)
+
+(* Program Instance or_iff_inverse_impl_morphism :  *)
+(*   Morphism (iff ==> inverse impl ==> inverse impl) or. *)
+
+Program Instance or_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) or.
+
+(** Logical implication [impl] is a morphism for logical equivalence. *)
+
+Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
+
+(** Morphisms for quantifiers *)
+
+Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.     
+    split ; intros.
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H in H₁. assumption.
+    
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_impl_morphism :
+  Morphism (pointwise_relation impl ==> impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => all_iff_morphism : 
+  Morphism (pointwise_relation iff ==> iff) (@all A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_impl_morphism : 
+  Morphism (pointwise_relation impl ==> impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
new file mode 100644
index 000000000..284810e94
--- /dev/null
+++ b/theories/Classes/Morphisms_Relations.v
@@ -0,0 +1,47 @@
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Morphism instances for relations.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(** Morphisms for relations *)
+
+Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_conjunction.
+  Proof. firstorder. Qed.
+
+Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_disjunction.
+  Proof. firstorder. Qed.
+
+(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
+
+Require Import List.
+
+Lemma predicate_equivalence_pointwise (l : list Type) :
+  Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id.
+Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
+
+Lemma predicate_implication_pointwise (l : list Type) :
+  Morphism (@predicate_implication l ==> lift_pointwise l impl) id.
+Proof. do 2 red. unfold predicate_implication. auto. Qed.
+
+(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)
+(*    when [R] and [R'] are in [relation_equivalence]. *)
+
+Instance relation_equivalence_pointwise :
+  Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id.
+Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed.
+
+Instance subrelation_pointwise :
+  Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
+Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f5d3cc1c4..8dfb662b2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -21,9 +21,6 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
 (** Default relation on a given support. *)
 
 Class DefaultRelation A (R : relation A).
@@ -50,6 +47,9 @@ Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+
 Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
@@ -73,6 +73,8 @@ Implicit Arguments Transitive [A].
 
 Hint Resolve @irreflexivity : ord.
 
+Unset Implicit Arguments.
+
 (** We can already dualize all these properties. *)
 
 Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
@@ -115,12 +117,20 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symm
 
 (** * Standard instances. *)
 
+Ltac reduce_hyp H :=
+  match type of H with
+    | context [ _ <-> _ ] => fail 1
+    | _ => red in H ; try reduce_hyp H
+  end.
+
 Ltac reduce_goal :=
   match goal with
     | [ |- _ <-> _ ] => fail 1
     | _ => red ; intros ; try reduce_goal
   end.
 
+Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
+
 Ltac reduce := reduce_goal.
 
 Tactic Notation "apply" "*" constr(t) := 
@@ -203,52 +213,187 @@ Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
 
 Program Instance iff_equivalence : Equivalence Prop iff.
 
-(** The following is not definable. *)
-(*
-Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid : 
-  Equivalence (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
-*)
+(** We now develop a generalization of results on relations for arbitrary predicates.
+   The resulting theory can be applied to homogeneous binary relations but also to
+   arbitrary n-ary predicates. *)
 
+Require Import List.
 
-(** We define the various operations which define the algebra on relations.
-   They are essentially liftings of the logical operations. *)
+(* Notation " [ ] " := nil : list_scope. *)
+(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
 
-Definition relation_equivalence {A : Type} : relation (relation A) :=
-  fun (R R' : relation A) => forall x y, R x y <-> R' x y.
+(* Open Local Scope list_scope. *)
 
-Class subrelation {A:Type} (R R' : relation A) :=
-  is_subrelation : forall x y, R x y -> R' x y.
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
-Implicit Arguments subrelation [[A]].
+Fixpoint arrows (l : list Type) (r : Type) : Type := 
+  match l with 
+    | nil => r
+    | A :: l' => A -> arrows l' r
+  end.
 
+(** We can define abbreviations for operation and relation types based on [arrows]. *)
 
-Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  fun x y => R x y /\ R' x y.
+Definition unary_operation A := arrows (cons A nil) A.
+Definition binary_operation A := arrows (cons A (cons A nil)) A.
+Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
 
-Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  fun x y => R x y \/ R' x y.
+(** We define n-ary [predicate]s as functions into [Prop]. *)
 
-(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *)
-(* Infix "-R>" := subrelation (at level 70) : relation_scope. *)
-(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *)
-(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *)
+Definition predicate (l : list Type) := arrows l Prop.
 
-(* Open Local Scope relation_scope. *)
+(** Unary predicates, or sets. *)
 
-(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+Definition unary_predicate A := predicate (cons A nil).
 
-Program Instance relation_equivalence_equivalence :
-  Equivalence (relation A) relation_equivalence.
+(** Homogenous binary relations, equivalent to [relation A]. *)
+
+Definition binary_relation A := predicate (cons A (cons A nil)).
+
+(** We can close a predicate by universal or existential quantification. *) 
+
+Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => forall x : A, predicate_all tl (f x)
+  end.
+
+Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => exists x : A, predicate_exists tl (f x)
+  end.
+
+(** Pointwise extension of a binary operation on [T] to a binary operation 
+   on functions whose codomain is [T]. *)
+
+Fixpoint pointwise_extension {l : list Type} {T : Type}
+  (op : binary_operation T) : binary_operation (arrows l T) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' => 
+      fun x => pointwise_extension op (R x) (R' x)
+  end.
+
+(** For an operator on [Prop] this lifts the operator to a binary operation. *)
+
+Definition pointwise_relation_extension (l : list Type) (op : binary_relation Prop) : 
+  binary_operation (predicate l) := pointwise_extension op.
+
+(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
+
+Fixpoint lift_pointwise (l : list Type) (op : binary_relation Prop) : binary_relation (predicate l) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' => 
+      forall x, lift_pointwise tl op (R x) (R' x)
+  end.
+
+(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
+
+Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
+  lift_pointwise l iff.
+
+(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
+
+Definition predicate_implication {l : list Type} :=
+  lift_pointwise l impl.
+
+(** Notations for pointwise equivalence and implication of predicates. *)
+
+Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
+Infix "-∙>" := predicate_implication (at level 70) : predicate_scope.
+
+Open Local Scope predicate_scope.
+
+(** The pointwise liftings of conjunction and disjunctions.
+   Note that these are [binary_operation]s, building new relations out of old ones. *)
+
+Definition predicate_intersection {l : list Type} : binary_operation (predicate l) :=
+  pointwise_relation_extension l and.
+
+Definition predicate_union {l : list Type} : binary_operation (predicate l) :=
+  pointwise_relation_extension l or.
+
+Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
+Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.
+
+(** The always [True] and always [False] predicates. *)
+
+Fixpoint true_predicate {l : list Type} : predicate l := 
+  match l with
+    | nil => True
+    | A :: tl => fun _ => @true_predicate tl
+  end.
+
+Fixpoint false_predicate {l : list Type} : predicate l :=
+  match l with
+    | nil => False
+    | A :: tl => fun _ => @false_predicate tl
+  end.
+
+Notation "∙⊤∙" := true_predicate : predicate_scope.
+Notation "∙⊥∙" := false_predicate : predicate_scope.
+
+(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
+
+Program Instance predicate_equivalence_equivalence :
+  Equivalence (predicate l) predicate_equivalence.
 
   Next Obligation.
-  Proof.
-    unfold relation_equivalence in *.
-    apply transitivity with (y x0 y0) ; [ apply H | apply H0 ].
+    induction l ; firstorder.
+  Qed.
+
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  
+  Next Obligation.
+    fold lift_pointwise.
+    induction l. firstorder.
+    intros. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)).
+    firstorder.
+  Qed.
+
+Program Instance predicate_implication_preorder :
+  PreOrder (predicate l) predicate_implication.
+
+  Next Obligation.
+    induction l ; firstorder.
   Qed.
 
-Program Instance subrelation_preorder :
-  PreOrder (relation A) subrelation.
+  Next Obligation.
+    fold lift_pointwise.
+    induction l. firstorder.
+    unfold predicate_implication in *. simpl in *. 
+    intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+  Qed.
+
+(** We define the various operations which define the algebra on binary relations, 
+   from the general ones. *)
+
+Definition relation_equivalence {A : Type} : relation (relation A) :=
+  @predicate_equivalence (cons _ (cons _ nil)).
+
+Class subrelation {A:Type} (R R' : relation A) : Prop :=
+  is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+
+Implicit Arguments subrelation [[A]].
+
+Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_intersection (cons A (cons A nil)) R R'.
+
+Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_union (cons A (cons A nil)) R R'.
+
+(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+
+Instance (A : Type) => relation_equivalence_equivalence :
+  Equivalence (relation A) relation_equivalence.
+Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+
+Instance relation_implication_preorder : PreOrder (relation A) subrelation.
+Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
@@ -256,8 +401,7 @@ Program Instance subrelation_preorder :
    on the carrier. *)
 
 Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
-  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
-
+  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
    for equivalence (see Morphisms).
@@ -265,8 +409,8 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
 
 Instance [ PartialOrder A eqA R ] =>  partial_order_antisym : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose partial_order_equivalence. red in r.
-  apply <- r. firstorder.
+  reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. 
+  apply <- poe. firstorder.
 Qed.
 
 (** The partial order defined by subrelation and relation equivalence. *)
@@ -279,8 +423,6 @@ Program Instance subrelation_partial_order :
     unfold relation_equivalence in *. firstorder.
   Qed.
 
-Instance iff_impl_subrelation : subrelation iff impl.
-Proof. firstorder. Qed.
-
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
-Proof. firstorder. Qed.
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+Proof. reflexivity. Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 38bdc0bc9..9d3648fef 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -17,6 +17,7 @@
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.Equivalence.
 Require Export Coq.Relations.Relation_Definitions.
 
@@ -89,6 +90,7 @@ Ltac reverse_arrows x :=
   end.
 
 Ltac default_add_morphism_tactic :=
+  intros ;
   (try destruct_morphism) ;
   match goal with
     | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6d77a6a0c..617ea6f4f 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -651,7 +651,7 @@ Proof. unfold Equal; congruence. Qed.
 
 Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _).
 Proof. 
-constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
+constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
 Qed.
 
 Add Relation key E.eq 
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 0c19176f8..6afb8fcb7 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -295,12 +295,12 @@ End BoolSpec.
 
 Definition E_ST : Setoid_Theory elt E.eq.
 Proof.
-constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
+constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
 Qed.
 
 Definition Equal_ST : Setoid_Theory t Equal.
 Proof. 
-constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
+constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans].
 Qed.
 
 Add Relation elt E.eq 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 6b30f6351..5ab27cfc7 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -9,7 +9,6 @@
   (*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
-Require Import Coq.Setoids.Setoid.
 
 Set Implicit Arguments.
 
@@ -554,8 +553,7 @@ Section Elts.
     simpl; intros; split; [destruct 1 | apply gt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
     rewrite Heq; intuition. 
-    rewrite <- (IHl x).
-    tauto.
+    pose (IHl x). intuition.
   Qed.
   
   Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a518faa57..6158e88f7 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -44,7 +44,7 @@ Implicit Arguments cons [[A]].
 
 Notation " [] " := nil.
 Notation " [ x ] " := (cons x nil).
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1).
 
 (** n-ary exists ! *)
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 26638893a..2265715b7 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -121,7 +121,7 @@ Defined.
 
 Definition Q_Setoid : Setoid_Theory Q Qeq.
 Proof.
- split; unfold Qeq in |- *; auto; apply Qeq_trans.
+ split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
 Qed.
 
 Add Setoid Q Qeq Q_Setoid as Qsetoid.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 983c651ab..8f59c048f 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -8,22 +8,18 @@
 
 (*i $Id$: i*)
 
-Set Implicit Arguments.
-
 Require Export Coq.Classes.SetoidTactics.
 
 (** For backward compatibility *)
 
-Record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop := 
-  { Seq_refl : forall x:A, Aeq x x;
-    Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
-    Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z }.
-
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
+Definition Setoid_Theory := @Equivalence.  
+Definition Build_Setoid_Theory := @Build_Equivalence.  
+Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x :=
+  Eval compute in reflexivity.
+Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x :=
+  Eval compute in symmetry.
+Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z :=
+  Eval compute in transitivity.
 
 (** Some tactics for manipulating Setoid Theory not officially 
     declared as Setoid. *)