12 files changed, 1932 insertions, 0 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
new file mode 100644
index 00000000..debe953a
--- /dev/null
+++ b/theories/Classes/EquivDec.v
@@ -0,0 +1,158 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Decidable equivalences.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: EquivDec.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Export notations. *)
+
+Require Export Coq.Classes.Equivalence.
+
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+   classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Open Scope equiv_scope.
+
+Class [ equiv : Equivalence A ] => DecidableEquivalence :=
+  setoid_decidable : forall x y : A, decidable (x === y).
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
+Class [ equiv : Equivalence A ] => EqDec :=
+  equiv_dec : forall x y : A, { x === y } + { x =/= y }.
+
+(** We define the [==] overloaded notation for deciding equality. It does not take precedence
+   of [==] defined in the type scope, hence we can have both at the same time. *)
+
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
+  match x with
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
+  end.
+
+Require Import Coq.Program.Program.
+
+Open Local Scope program_scope.
+
+(** Invert the branches. *)
+
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
+
+(** Overloaded notation for inequality. *)
+
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
+
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+  if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+  negb (equiv_decb x y).
+
+Infix "==b" := equiv_decb (no associativity, at level 70).
+Infix "<>b" := nequiv_decb (no associativity, at level 70).
+
+(** Decidable leibniz equality instances. *)
+
+Require Import Coq.Arith.Peano_dec.
+
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance nat_eq_eqdec : ! EqDec nat eq :=
+  equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : ! EqDec bool eq :=
+  equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : ! EqDec unit eq :=
+  equiv_dec x y := in_left.
+
+  Next Obligation.
+  Proof.
+    destruct x ; destruct y.
+    reflexivity.
+  Qed.
+
+Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (prod A B) eq :=
+  equiv_dec x y := 
+    let '(x1, x2) := x in 
+    let '(y1, y2) := y in 
+    if x1 == y1 then 
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using unfold complement, equiv ; program_simpl.
+
+Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] :
+  ! EqDec (sum A B) eq :=
+  equiv_dec x y := 
+    match x, y with
+      | inl a, inl b => if a == b then in_left else in_right
+      | inr a, inr b => if a == b then in_left else in_right
+      | inl _, inr _ | inr _, inl _ => in_right
+    end.
+
+  Solve Obligations using unfold complement, equiv ; program_simpl.
+
+(** Objects of function spaces with countable domains like bool have decidable equality. *)
+
+Require Import Coq.Program.FunctionalExtensionality.
+
+Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq :=
+  equiv_dec f g := 
+    if f true == g true then
+      if f false == g false then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+
+  Next Obligation.
+  Proof.
+    extensionality x.
+    destruct x ; auto.
+  Qed.
+
+Require Import List.
+
+Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
+  equiv_dec := 
+    fix aux (x : list A) y { struct x } :=
+    match x, y with
+      | nil, nil => in_left
+      | cons hd tl, cons hd' tl' => 
+        if hd == hd' then
+          if aux tl tl' then in_left else in_right
+          else in_right
+      | _, _ => in_right
+    end.
+
+  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+
+  Next Obligation.
+  Proof. clear aux. red in H0. subst. 
+    destruct y; intuition (discriminate || eauto).
+  Defined.
\ No newline at end of file
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
new file mode 100644
index 00000000..70bf3483
--- /dev/null
+++ b/theories/Classes/Equivalence.v
@@ -0,0 +1,144 @@
+(* -*- 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 setoids. Definitions on [Equivalence].
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+   91405 Orsay, France *) 
+
+(* $Id: Equivalence.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+
+Require Export Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
+Require Import Coq.Classes.RelationClasses.
+Require Export Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Open Local Scope signature_scope.
+
+Definition equiv [ Equivalence A R ] : relation A := R.
+
+Typeclasses unfold equiv.
+
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+
+Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
+
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
+  
+Open Local Scope equiv_scope.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv [ PER A R ] : relation A := R.
+
+Typeclasses unfold pequiv.
+
+(** Overloaded notation for partial equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
+
+(** Shortcuts to make proof search easier. *)
+
+Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
+
+Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
+
+  Next Obligation.
+  Proof.
+    symmetry ; auto.
+  Qed.
+
+Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
+
+  Next Obligation.
+  Proof.
+    transitivity y ; auto.
+  Qed.
+
+(** Use the [substitute] command which substitutes an equivalence 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.
+
+(** Simplify the goal w.r.t. equivalence. *)
+
+Ltac equiv_simplify_one :=
+  match goal with
+    | [ H : ?x === ?x |- _ ] => clear H
+    | [ H : ?x === ?y |- _ ] => setoid_subst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac equiv_simplify := repeat equiv_simplify_one.
+
+(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
+   for easy recognition in tactics. *)
+
+Ltac equivify_tac :=
+  match goal with
+    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac equivify := repeat equivify_tac.
+
+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 respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+    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.
+
+End Respecting.
+
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+
+Program Instance pointwise_equivalence [ Equivalence A eqA ] :
+  Equivalence (B -> A) (pointwise_relation eqA) | 9.
+
+  Next Obligation.
+  Proof.
+    transitivity (y x0) ; auto.
+  Qed.
+
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
new file mode 100644
index 00000000..49fc4f89
--- /dev/null
+++ b/theories/Classes/Functions.v
@@ -0,0 +1,42 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Functional morphisms.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: Functions.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+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 : Prop :=
+  surjective : forall y, exists x : A, RB y (f x).
+
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+  Injective m /\ Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+  monic :> Injective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+  epic :> Surjective m.
+
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+  monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
+
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
new file mode 100644
index 00000000..6ba0c61e
--- /dev/null
+++ b/theories/Classes/Init.v
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Initialization code for typeclasses, setting up the default tactic 
+   for instance search.
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: Init.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+(* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
+
+Tactic Notation "clapply" ident(c) :=
+  eapply @c ; eauto with typeclass_instances.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
new file mode 100644
index 00000000..f21c68a6
--- /dev/null
+++ b/theories/Classes/Morphisms.v
@@ -0,0 +1,467 @@
+(* -*- 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 *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Typeclass-based morphism definition and standard, minimal instances.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: Morphisms.v 11092 2008-06-10 18:28:26Z msozeau $ *)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Import Coq.Relations.Relation_Definitions.
+Require Export Coq.Classes.RelationClasses.
+
+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 [setoid_rewrite] tactic later. *)
+
+(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   for usual morphisms. *)
+
+Class Morphism A (R : relation A) (m : A) : Prop :=
+  respect : R m m.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
+(** Respectful morphisms. *)
+
+(** The fully dependent version, not used yet. *)
+
+Definition respectful_hetero 
+  (A B : Type) 
+  (C : A -> Type) (D : B -> Type) 
+  (R : A -> B -> Prop) 
+  (R' : forall (x : A) (y : B), C x -> D y -> Prop) : 
+    (forall x : A, C x) -> (forall x : B, D x) -> Prop := 
+    fun f g => forall x y, R x y -> R' x y (f x) (g y).
+
+(** The non-dependent version is an instance where we forget dependencies. *)
+
+Definition respectful (A B : Type) 
+  (R : relation A) (R' : relation B) : relation (A -> B) :=
+  Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
+
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+
+Delimit Scope signature_scope with signature.
+Arguments Scope Morphism [type_scope signature_scope].
+
+Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+  (right associativity, at level 55) : signature_scope.
+
+Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
+
+Open Local Scope signature_scope.
+
+(** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
+
+Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
+  PER (A -> B) (R ==> R').
+
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0). 
+    transitivity y0... symmetry...
+    transitivity (y x0)...
+  Qed.
+
+(** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
+
+Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Proof. firstorder. Qed.
+
+(** The subrelation property goes through products as usual. *)
+
+Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
+  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
+Proof. firstorder. Qed.
+
+Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
+  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
+Proof. firstorder. Qed.
+
+(** [Morphism] is itself a covariant morphism for [subrelation]. *)
+
+Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
+Proof.
+  intros. apply sub. apply mor.
+Qed.
+
+Instance morphism_subrelation_morphism : 
+  Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
+Proof. reduce. subst. firstorder. Qed.
+
+(** 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
+    | [ _ : subrelation_done |- _ ] => fail 1
+    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
+      set(H:=did_subrelation) ; eapply @subrelation_morphism
+  end.
+
+Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+
+(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
+
+Instance iff_impl_subrelation : subrelation iff impl.
+Proof. firstorder. Qed.
+
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Proof. firstorder. Qed.
+
+Instance pointwise_subrelation [ sub : subrelation A R R' ] :
+  subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
+Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
+
+(** The complement of a relation conserves its morphisms. *)
+
+Program Instance complement_morphism
+  [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] :
+  Morphism (RA ==> RA ==> iff) (complement R).
+
+  Next Obligation.
+  Proof.
+    unfold complement.
+    pose (mR x y H x0 y0 H0).
+    intuition.
+  Qed.
+
+(** The [inverse] too, actually the [flip] instance is a bit more general. *) 
+
+Program Instance flip_morphism
+  [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] :
+  Morphism (RB ==> RA ==> RC) (flip f).
+
+  Next Obligation.
+  Proof.
+    apply mor ; auto.
+  Qed.
+
+(** Every Transitive relation gives rise to a binary morphism on [impl], 
+   contravariant in the first argument, covariant in the second. *)
+
+Program Instance trans_contra_co_morphism
+  [ Transitive A R ] : Morphism (R --> R ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x...
+    transitivity x0...
+  Qed.
+
+(* (** Dually... *) *)
+
+(* Program Instance [ Transitive A R ] => *)
+(*   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *)
+  
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     apply* trans_contra_co_morphism ; eauto. eauto. *)
+(*   Qed. *)
+
+(** Morphism declarations for partial applications. *)
+
+Program Instance trans_contra_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+Program Instance trans_co_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0...
+  Qed.
+
+Program Instance trans_sym_co_inv_impl_morphism
+  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+Program Instance trans_sym_contra_impl_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0...
+  Qed.
+
+Program Instance equivalence_partial_app_morphism
+  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; transitivity x0...
+    intros.
+    transitivity y...
+    symmetry...
+  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 trans_co_eq_inv_impl_morphism
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+(* Program Instance [ Transitive A R ] =>  *)
+(*   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *)
+
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     transitivity x... *)
+(*   Qed. *)
+
+(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
+
+Program Instance trans_sym_morphism
+  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    transitivity x0... transitivity x...
+  
+    transitivity y... transitivity y0... 
+  Qed.
+
+Program Instance equiv_morphism [ Equivalence A R ] :
+  Morphism (R ==> R ==> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    transitivity x0... transitivity x... symmetry...
+  
+    transitivity y... transitivity y0... symmetry...
+  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.
+  
+(** Coq functions are morphisms for leibniz equality, 
+   applied only if really needed. *)
+
+(* Instance (A : Type) [ Reflexive B R ] => *)
+(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
+(* Proof. simpl_relation. Qed. *)
+
+Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
+  Reflexive (@Logic.eq A ==> R').
+Proof. simpl_relation. Qed.
+
+(** [respectful] is a morphism for relation equivalence. *)
+
+Instance respectful_morphism : 
+  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
+Proof.
+  reduce.
+  unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
+  split ; intros.
+  
+    rewrite <- H0.
+    apply H1.
+    rewrite H.
+    assumption.
+
+    rewrite H0.
+    apply H1.
+    rewrite <- H.
+    assumption.
+Qed.
+
+(** Every element in the carrier of a reflexive relation is a morphism for this relation.
+   We use a proxy class for this case which is used internally to discharge reflexivity constraints.
+   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of 
+   [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
+   to set different priorities in different hint bases and select a particular hint database for
+   resolution of a type class constraint.*) 
+
+Class MorphismProxy A (R : relation A) (m : A) : Prop :=
+  respect_proxy : R m m.
+
+Instance reflexive_morphism_proxy
+  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
+Proof. firstorder. Qed.
+
+Instance morphism_morphism_proxy
+  [ Morphism A R x ] : MorphismProxy A R x | 2.
+Proof. firstorder. Qed.
+
+(* Instance (A : Type) [ Reflexive B R ] => *)
+(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
+(* Proof. simpl_relation. Qed. *)
+
+(** [R] is Reflexive, hence we can build the needed proof. *)
+
+Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
+   Morphism R' (m x).
+Proof. simpl_relation. Qed.
+
+Ltac partial_application_tactic := 
+  let tac x :=
+    match type of x with
+      | Type => fail 1
+      | _ => eapply @Reflexive_partial_app_morphism
+    end
+  in
+  let on_morphism m :=
+    match m with
+      | ?m' ?x => tac x
+      | ?m' _ ?x => tac x
+      | ?m' _ _ ?x => tac x
+      | ?m' _ _ _ ?x => tac x
+      | ?m' _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ _ _ ?x => tac x
+    end
+  in
+  match goal with
+    | [ |- @Morphism _ _ ?m ] => on_morphism m
+  end.
+
+(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *)
+(*   reflexive_partial_app_morphism : Morphism R' (m x). *)
+
+Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
+
+Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
+  relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
+Proof.
+  intros.
+  unfold flip, respectful.
+  split ; intros ; intuition.
+Qed.
+
+(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
+
+Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
+  normalizes : relation_equivalence m m'.
+
+Instance inverse_respectful_norm : 
+  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
+Proof. firstorder. Qed.
+
+(* If not an inverse on the left, do a double inverse. *)
+
+Instance not_inverse_respectful_norm : 
+  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+Proof. firstorder. Qed.
+
+Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
+  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+Proof. red ; intros.  
+  pose normalizes as r.
+  setoid_rewrite r.
+  setoid_rewrite inverse_respectful.
+  reflexivity.
+Qed.
+
+(** Once we have normalized, we will apply this instance to simplify the problem. *)
+
+Program Instance morphism_inverse_morphism
+  [ Morphism A R m ] : Morphism (inverse R) m | 2.
+
+(** Bootstrap !!! *)
+
+Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
+Proof.
+  simpl_relation.
+  reduce in H.
+  split ; red ; intros.
+  setoid_rewrite <- H.
+  apply H0.
+  setoid_rewrite H.
+  apply H0.
+Qed.
+
+Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
+Proof.
+  intros.
+  pose respect as r.
+  pose normalizes as norm.
+  setoid_rewrite norm.
+  assumption.
+Qed.
+
+Inductive normalization_done : Prop := did_normalization.
+
+Ltac morphism_normalization := 
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
+      set(H:=did_normalization) ; eapply @morphism_releq_morphism
+  end.
+
+Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+
+(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
+
+Lemma reflexive_morphism [ Reflexive A R ] (x : A)
+   : Morphism R x.
+Proof. firstorder. Qed.
+
+Ltac morphism_reflexive :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : subrelation_done |- _ ] => fail 1
+    | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
+  end.
+
+Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
new file mode 100644
index 00000000..7dc1f95e
--- /dev/null
+++ b/theories/Classes/Morphisms_Prop.v
@@ -0,0 +1,132 @@
+(* -*- 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.Basics.
+Require Import Coq.Program.Tactics.
+
+(** 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 ex_iff_morphism {A : Type} : 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 ex_impl_morphism {A : Type} :
+  Morphism (pointwise_relation impl ==> impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance ex_inverse_impl_morphism {A : Type} : 
+  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 all_iff_morphism {A : Type} : 
+  Morphism (pointwise_relation iff ==> iff) (@all A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance all_impl_morphism {A : Type} : 
+  Morphism (pointwise_relation impl ==> impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance all_inverse_impl_morphism {A : Type} : 
+  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 00000000..5018fa01
--- /dev/null
+++ b/theories/Classes/Morphisms_Relations.v
@@ -0,0 +1,50 @@
+(* -*- 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 *)
+
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Program.Program.
+
+(** 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 ==> pointwise_lifting iff l) id.
+Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
+
+Lemma predicate_implication_pointwise (l : list Type) :
+  Morphism (@predicate_implication l ==> pointwise_lifting impl l) 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. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed.
+
+Instance subrelation_pointwise :
+  Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
+Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
new file mode 100644
index 00000000..a9a53068
--- /dev/null
+++ b/theories/Classes/RelationClasses.v
@@ -0,0 +1,400 @@
+(* -*- 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 *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* 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
+   91405 Orsay, France *)
+
+(* $Id: RelationClasses.v 11092 2008-06-10 18:28:26Z msozeau $ *)
+
+Require Export Coq.Classes.Init.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Relations.Relation_Definitions.
+
+Notation inverse R := (flip (R:relation _) : relation _).
+
+Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
+
+Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+  fun f g => forall x : A, R (f x) (g x).
+
+(** These are convertible. *)
+
+Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
+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.
+
+Class Irreflexive A (R : relation A) := 
+  irreflexivity :> Reflexive A (complement R).
+
+Class Symmetric A (R : relation A) := 
+  symmetry : forall x y, R x y -> R y x.
+
+Class Asymmetric A (R : relation A) := 
+  asymmetry : forall x y, R x y -> R y x -> False.
+
+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].
+
+Hint Resolve @irreflexivity : ord.
+
+Unset Implicit Arguments.
+
+(** We can already dualize all these properties. *)
+
+Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) :=
+  reflexivity := reflexivity (R:=R).
+
+Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) :=
+  irreflexivity := irreflexivity (R:=R).
+
+Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R).
+
+  Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
+
+Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R).
+  
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
+
+Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R).
+
+  Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
+
+Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ]
+   : Irreflexive (complement R).
+
+  Next Obligation. 
+  Proof. 
+    unfold complement.
+    red. intros H.
+    intros H' ; apply H'.
+    apply (reflexivity H).
+  Qed.
+
+
+Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R).
+
+  Next Obligation.
+  Proof.
+    red ; intros H'.
+    apply (H (symmetry H')).
+  Qed.
+
+(** * 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) := 
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
+Ltac simpl_relation :=
+  unfold flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ intuition ]).
+
+Ltac obligations_tactic ::= simpl_relation.
+
+(** Logical implication. *)
+
+Program Instance impl_Reflexive : Reflexive impl.
+Program Instance impl_Transitive : Transitive impl.
+
+(** Logical equivalence. *)
+
+Program Instance iff_Reflexive : Reflexive iff.
+Program Instance iff_Symmetric : Symmetric iff.
+Program Instance iff_Transitive : Transitive iff.
+
+(** Leibniz equality. *)
+
+Program Instance eq_Reflexive : Reflexive (@eq A).
+Program Instance eq_Symmetric : Symmetric (@eq A).
+Program Instance eq_Transitive : Transitive (@eq A).
+
+(** Various combinations of reflexivity, symmetry and transitivity. *)
+
+(** A [PreOrder] is both Reflexive and Transitive. *)
+
+Class PreOrder A (R : relation A) : Prop :=
+  PreOrder_Reflexive :> Reflexive R ;
+  PreOrder_Transitive :> Transitive R.
+
+(** A partial equivalence relation is Symmetric and Transitive. *)
+
+Class PER (carrier : Type) (pequiv : relation carrier) : Prop :=
+  PER_Symmetric :> Symmetric pequiv ;
+  PER_Transitive :> Transitive pequiv.
+
+(** Equivalence relations. *)
+
+Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
+  Equivalence_Reflexive :> Reflexive equiv ;
+  Equivalence_Symmetric :> Symmetric equiv ;
+  Equivalence_Transitive :> Transitive equiv.
+
+(** An Equivalence is a PER plus reflexivity. *)
+
+Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+  PER_Symmetric := Equivalence_Symmetric ;
+  PER_Transitive := Equivalence_Transitive.
+
+(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
+
+Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
+  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
+
+Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
+  Antisymmetric eq (flip R).
+
+(** Leibinz equality [eq] is an equivalence relation.
+   The instance has low priority as it is always applicable 
+   if only the type is constrained. *)
+
+Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
+
+(** Logical equivalence [iff] is an equivalence relation. *)
+
+Program Instance iff_equivalence : Equivalence Prop iff.
+
+(** 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.
+
+(* Notation " [ ] " := nil : list_scope. *)
+(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
+
+(* Open Local Scope list_scope. *)
+
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
+
+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 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.
+
+(** We define n-ary [predicate]s as functions into [Prop]. *)
+
+Notation predicate l := (arrows l Prop).
+
+(** Unary predicates, or sets. *)
+
+Definition unary_predicate A := predicate (cons A nil).
+
+(** Homogeneous 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].
+   For an operator on [Prop] this lifts the operator to a binary operation. *)
+
+Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
+  (l : list Type) : 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 tl (R x) (R' x)
+  end.
+
+(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
+
+Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' => 
+      forall x, pointwise_lifting op tl (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) :=
+  pointwise_lifting iff l.
+
+(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
+
+Definition predicate_implication {l : list Type} :=
+  pointwise_lifting impl l.
+
+(** 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 := pointwise_extension and.
+Definition predicate_union := pointwise_extension 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.
+    induction l ; firstorder.
+  Qed.
+
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  
+  Next Obligation.
+    fold pointwise_lifting.
+    induction l. firstorder.
+    intros. simpl in *. 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.
+
+  Next Obligation.
+    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 relation_equivalence_equivalence (A : Type) :
+  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.
+   We give an equivalent definition, up-to an equivalence relation 
+   on the carrier. *)
+
+Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
+  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).
+   It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
+
+Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R.
+Proof with auto.
+  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  apply <- poe. firstorder.
+Qed.
+
+(** The partial order defined by subrelation and relation equivalence. *)
+
+Program Instance subrelation_partial_order :
+  ! PartialOrder (relation A) relation_equivalence subrelation.
+
+  Next Obligation.
+  Proof.
+    unfold relation_equivalence in *. 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/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
new file mode 100644
index 00000000..9264b6d2
--- /dev/null
+++ b/theories/Classes/SetoidAxioms.v
@@ -0,0 +1,35 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Extensionality axioms that can be used when reasoning with setoids.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: SetoidAxioms.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.SetoidClass.
+
+(* Application of the extensionality axiom to turn a goal on leibinz equality to 
+   a setoid equivalence. *)
+
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+
+(** Application of the extensionality principle for setoids. *)
+
+Ltac setoid_extensionality :=
+  match goal with
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
+  end.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
new file mode 100644
index 00000000..a9bdaa8f
--- /dev/null
+++ b/theories/Classes/SetoidClass.v
@@ -0,0 +1,181 @@
+(* -*- 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 setoids, tactics and standard instances.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: SetoidClass.v 11065 2008-06-06 22:39:43Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Program.Program.
+
+Require Import Coq.Classes.Init.
+Require Export Coq.Classes.RelationClasses.
+Require Export Coq.Classes.Morphisms.
+Require Import Coq.Classes.Functions.
+
+(** A setoid wraps an equivalence. *)
+
+Class Setoid A :=
+  equiv : relation A ;
+  setoid_equiv :> Equivalence A equiv.
+
+Typeclasses unfold equiv.
+
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(*   equivalence_setoid : Setoid A := *)
+(*   equiv := eqA ; setoid_equiv := eqa. *)
+
+(** Shortcuts to make proof search easier. *)
+
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
+(** Standard setoids. *)
+
+(* Program Instance eq_setoid : Setoid A := *)
+(*   equiv := eq ; setoid_equiv := eq_equivalence. *)
+
+Program Instance iff_setoid : Setoid Prop :=
+  equiv := iff ; setoid_equiv := iff_equivalence.
+
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+
+(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
+(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
+
+Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
+
+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. *)
+
+Ltac clsubst H := 
+  match type of H with
+    ?x == ?y => substitute H ; clear H x
+  end.
+
+Ltac clsubst_nofail :=
+  match goal with
+    | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "clsubst" "*" := clsubst_nofail.
+
+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 (symmetry ; auto).
+  assert(x == y) by (transitivity z ; eauto).
+  contradiction.
+Qed.
+
+Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Proof.
+  intros; intro. 
+  assert(y == x) by (symmetry ; auto).
+  assert(y == z) by (transitivity x ; eauto).
+  contradiction.
+Qed.
+
+Ltac setoid_simplify_one :=
+  match goal with
+    | [ H : (?x == ?x)%type |- _ ] => clear H
+    | [ H : (?x == ?y)%type |- _ ] => clsubst H
+    | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac setoid_simplify := repeat setoid_simplify_one.
+
+Ltac setoidify_tac :=
+  match goal with
+    | [ s : Setoid ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Setoid ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac setoidify := repeat setoidify_tac.
+
+(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
+
+Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
+  trans_sym_morphism.
+
+(** Add this very useful instance in the database. *)
+
+Implicit Arguments setoid_morphism [[!sa]].
+Existing Instance setoid_morphism.
+
+Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
+  Reflexive_partial_app_morphism.
+
+Existing Instance setoid_partial_app_morphism.
+
+Definition type_eq : relation Type :=
+  fun x y => x = y.
+
+Program Instance type_equivalence : Equivalence Type type_eq.
+
+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) Basics.id.
+
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
+
+(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
+
+(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)
+(*   compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
+
+(* Next Obligation. *)
+(* Proof. *)
+(*   apply (respect (m0:=mg)). *)
+(*   apply (respect (m0:=mf)). *)
+(*   assumption. *)
+(* Qed. *)
+
+(** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
+
+Class PartialSetoid (carrier : Type) :=
+  pequiv : relation carrier ;
+  pequiv_prf :> PER carrier pequiv.
+
+(** Overloaded notation for partial setoid equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
+
+(** Reset the default Program tactic. *)
+
+Ltac obligations_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
new file mode 100644
index 00000000..cf3d202d
--- /dev/null
+++ b/theories/Classes/SetoidDec.v
@@ -0,0 +1,126 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Decidable setoid equality theory.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: SetoidDec.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Export notations. *)
+
+Require Export Coq.Classes.SetoidClass.
+
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+   classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Class [ Setoid A ] => DecidableSetoid :=
+  setoid_decidable : forall x y : A, decidable (x == y).
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
+Class [ Setoid A ] => EqDec :=
+  equiv_dec : forall x y : A, { x == y } + { x =/= y }.
+
+(** We define the [==] overloaded notation for deciding equality. It does not take precedence
+   of [==] defined in the type scope, hence we can have both at the same time. *)
+
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
+  match x with
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
+  end.
+
+Require Import Coq.Program.Program.
+
+Open Local Scope program_scope.
+
+(** Invert the branches. *)
+
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+
+(** Overloaded notation for inequality. *)
+
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
+
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+  if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+  negb (equiv_decb x y).
+
+Infix "==b" := equiv_decb (no associativity, at level 70).
+Infix "<>b" := nequiv_decb (no associativity, at level 70).
+
+(** Decidable leibniz equality instances. *)
+
+Require Import Coq.Arith.Arith.
+
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance eq_setoid : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
+
+Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
+  equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
+  equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
+  equiv_dec x y := in_left.
+
+  Next Obligation.
+  Proof.
+    destruct x ; destruct y.
+    reflexivity.
+  Qed.
+
+Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
+  equiv_dec x y := 
+    let '(x1, x2) := x in 
+    let '(y1, y2) := y in 
+    if x1 == y1 then 
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using unfold complement ; program_simpl.
+
+(** Objects of function spaces with countable domains like bool have decidable equality. *)
+
+Require Import Coq.Program.FunctionalExtensionality.
+
+Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
+  equiv_dec f g := 
+    if f true == g true then
+      if f false == g false then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+
+  Next Obligation.
+  Proof.
+    extensionality x.
+    destruct x ; auto.
+  Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
new file mode 100644
index 00000000..b29a52cc
--- /dev/null
+++ b/theories/Classes/SetoidTactics.v
@@ -0,0 +1,176 @@
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Tactics for typeclass-based setoids.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: SetoidTactics.v 10921 2008-05-12 12:27:25Z msozeau $ *)
+
+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.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Default relation on a given support. Can be used by tactics
+   to find a sensible default relation on any carrier. Users can 
+   declare an [Instance A RA] anywhere to declare default relations.
+   This is also done by the [Declare Relation A RA] command with no
+   parameters for backward compatibility. *)
+
+Class DefaultRelation A (R : relation A).
+
+(** To search for the default relation, just call [default_relation]. *)
+
+Definition default_relation [ DefaultRelation A R ] := R.
+
+(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+
+(** The setoid_replace tactics in Ltac, defined in terms of default relations and
+   the setoid_rewrite tactic. *)
+
+Ltac setoidreplace H t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | t ].
+
+Ltac setoidreplacein H H' t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
+
+Ltac setoidreplaceinat H H' t occs :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' at occs ; clear Heq | t ].
+
+Ltac setoidreplaceat H t occs :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq at occs ; clear Heq | t ].
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+  setoidreplace (default_relation x y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceat (default_relation x y) idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) :=
+  setoidreplacein (default_relation x y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceinat (default_relation x y) id idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "by" tactic3(t) :=
+  setoidreplace (default_relation x y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "at" int_or_var_list(o) 
+  "by" tactic3(t) :=
+  setoidreplaceat (default_relation x y) ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) 
+  "by" tactic3(t) :=
+  setoidreplacein (default_relation x y) id ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "in" hyp(id) 
+  "at" int_or_var_list(o) 
+  "by" tactic3(t) :=
+  setoidreplaceinat (default_relation x y) id ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) :=
+  setoidreplace (rel x y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "at" int_or_var_list(o) :=
+  setoidreplaceat (rel x y) idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "by" tactic3(t) :=
+  setoidreplace (rel x y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "at" int_or_var_list(o)  
+  "by" tactic3(t) :=
+  setoidreplaceat (rel x y) ltac:t o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id) :=
+  setoidreplacein (rel x y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id) 
+  "at" int_or_var_list(o) :=
+  setoidreplaceinat (rel x y) id idtac o.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel)
+  "in" hyp(id)
+  "by" tactic3(t) :=
+  setoidreplacein (rel x y) id ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) 
+  "in" hyp(id)
+  "at" int_or_var_list(o)  
+  "by" tactic3(t) :=
+  setoidreplaceinat (rel x y) id ltac:t o.
+
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
+   to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
+   and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+
+Require Import Coq.Program.Tactics.
+
+Open Local Scope signature_scope.
+
+Ltac red_subst_eq_morphism concl :=
+  match concl with
+    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+    | _ => idtac
+  end.
+
+Ltac destruct_morphism :=
+  match goal with
+    | [ |- @Morphism ?A ?R ?m ] => red
+  end.
+
+Ltac reverse_arrows x :=
+  match x with
+    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+    | _ => idtac
+  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)
+  end.
+
+Ltac add_morphism_tactic := default_add_morphism_tactic.