Add new files theories/Program/Basics.v and theories/Classes/Relations.v

for basic functional programming and relation
definitions respectively. 
Classes.Relations also includes the definition of Morphism
and instances for the standard morphisms and relations (eq, iff, impl,
inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
has been reimplemented on top of these definitions, hence it doesn't
require a setoid implementation anymore. It also generates obligations
for missing reflexivity proofs, like the current setoid_rewrite. It has
not been tested on large examples but it should handle directions and
occurences. Works with in if no obligations are generated at this time.
What's missing is being able to rewrite by a lemma instead of a simple
hypothesis with no premises.


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

9 files changed, 1008 insertions, 376 deletions

diff --git a/Makefile.common b/Makefile.common
index 0e6c3925c6..4a60b251a2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -708,8 +708,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo \
-	theories/Classes/SetoidDec.vo
+CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \
+	 theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
@@ -766,7 +766,7 @@ DPVO:=contrib/dp/Dp.vo
 
 SUBTACVO:=theories/Program/Tactics.vo theories/Program/Equality.vo theories/Program/Subset.vo \
 	theories/Program/Utils.vo theories/Program/Wf.vo theories/Program/Program.vo \
-	theories/Program/FunctionalExtensionality.vo
+	theories/Program/FunctionalExtensionality.vo theories/Program/Basics.vo
 
 RTAUTOVO:= \
  contrib/rtauto/Bintree.vo contrib/rtauto/Rtauto.vo
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4a2dad8cab..a58125dc09 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1608,7 +1608,7 @@ defined in the same file:
 
 \begin{Variants}
 \item {\tt dependent induction {\ident} generalizing {\ident$_1$} \dots
-    {\ident$_n$}}\tacindex{dependent induction ... generalizing}
+    {\ident$_n$}}\tacindex{dependent induction \dots\ generalizing}
   
   Does dependent induction on the hypothesis {\ident} but first
   generalizes the goal by the given variables so that they are
@@ -1616,9 +1616,9 @@ defined in the same file:
   to do with the variables that are inside some constructors in the
   induction hypothesis. The other ones need not be further generalized.
 
-\item {\tt dependent destruction}\tacindex{dependent destruction}
+\item {\tt dependent destruction {\ident}}\tacindex{dependent destruction}
   
-  Does the generalization of the instance but uses {\tt destruct}
+  Does the generalization of the instance {\ident} but uses {\tt destruct}
   instead of {\tt induction} on the generalized hypothesis. This gives
   results equivalent to {\tt inversion} or {\tt dependent inversion} if
   the hypothesis is dependent.
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 66324158dd..dcc3ffbd24 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -42,22 +42,45 @@ let e_give_exact c gl =
 let assumption id = e_give_exact (mkVar id)
 
 let morphism_class = lazy (class_info (id_of_string "Morphism"))
-let morphism2_class = lazy (class_info (id_of_string "BinaryMorphism"))
-let morphism3_class = lazy (class_info (id_of_string "TernaryMorphism"))
 
 let get_respect cl = 
   Option.get (List.hd (Recordops.lookup_projections cl.cl_impl))
 
 let respect_proj = lazy (get_respect (Lazy.force morphism_class))
-let respect2_proj = lazy (get_respect (Lazy.force morphism2_class))
-let respect3_proj = lazy (get_respect (Lazy.force morphism3_class))
 
 let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s
 let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
 let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
 let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
+let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
+let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
+
+let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive")
+let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive")
+
+let symmetric_type = lazy (gen_constant ["Classes"; "Relations"] "Symmetric")
+let symmetric_proof = lazy (gen_constant ["Classes"; "Relations"] "symmetric")
+
+let transitive_type = lazy (gen_constant ["Classes"; "Relations"] "Transitive")
+let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive")
+
+let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse")
+
+let respectful_dep = lazy (gen_constant ["Classes"; "Relations"] "respectful_dep")
+let respectful = lazy (gen_constant ["Classes"; "Relations"] "respectful")
+
+let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
+let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
+
+(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
+let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
+
+let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
 
 let iff_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "iff_setoid")
+let eq_setoid = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_setoid")
+
 let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv")
 let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism")
 let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
@@ -70,12 +93,10 @@ let arrow_morphism a b =
 let setoid_refl pars x = 
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
       
-let class_one = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
-let class_two = lazy (Lazy.force morphism2_class, Lazy.force respect2_proj)
-let class_three = lazy (Lazy.force morphism3_class, Lazy.force respect3_proj)
+let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
 
-exception Found of (constr * constant * constr list * constr * constr array *
-		       (constr * (constr * constr * constr * constr * constr)) option array)
+exception Found of (constr * constr * (types * types) list * constr * constr array *
+		       (constr * (constr * constr * constr * constr)) option array)
 
 let resolve_morphism_evd env evd app = 
   let ev = Evarutil.e_new_evar evd env app in
@@ -88,79 +109,123 @@ let resolve_morphism_evd env evd app =
 let is_equiv env sigma t = 
   isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
 
-let resolve_morphism env sigma direction oldt m args args' = 
-  let evars = ref (Evd.create_evar_defs Evd.empty) in
-  let morph_instance, proj, subst, m', args, args' = 
-    if is_equiv env sigma m then 
-      let params, rest = array_chop 3 args in
-      let a, r, s = params.(0), params.(1), params.(2) in
-      let params', rest' = array_chop 3 args' in
-      let inst = mkApp (Lazy.force setoid_morphism, params) in
-	(* Equiv gives a binary morphism *)
-      let (cl, proj) = Lazy.force class_two in
-      let ctxargs = [ a; r; s; a; r; s; mkProp; Lazy.force iff; Lazy.force iff_setoid; ] in
-      let m' = mkApp (m, [| a; r; s |]) in
-	inst, proj, ctxargs, m', rest, rest'
-    else
-      let cls =
+let split_head = function
+    hd :: tl -> hd, tl
+  | [] -> assert(false)
+
+let build_signature isevars env m cstrs finalcstr =
+  let new_evar isevars env t =
+    Evarutil.e_new_evar isevars env
+      (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
+  in
+  let mk_relty ty obj =
+    let relty = mkApp (Lazy.force coq_relation, [| ty |]) in
+      match obj with
+	| None -> new_evar isevars env relty
+	| Some (p, (a, r, oldt, newt)) -> r
+  in
+  let rec aux t l =
+    let t = Reductionops.whd_betadelta env (Evd.evars_of !isevars) t in
+    match kind_of_term t, l with
+      | Prod (na, ty, b), obj :: cstrs -> 
+	  let (arg, evars) = aux b cstrs in
+	  let relty = mk_relty ty obj in
+	  let arg' = mkApp (Lazy.force respectful, [| ty ; relty ; b ; arg |]) in
+	    arg', (ty, relty) :: evars
+      | _, _ -> 
+	  (match finalcstr with
+	      None -> 
+		let rel = mk_relty t None in 
+		  rel, [t, rel]
+	    | Some (t, rel) -> rel, [t, rel])
+      | _, _ -> assert false
+  in aux m cstrs
+
+let reflexivity_proof env carrier relation x =
+  let goal = 
+    mkApp (Lazy.force reflexive_type, [| carrier ; relation |])
+  in
+    try let inst = resolve_one_typeclass env goal in
+	  mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
+    with Not_found ->
+      let meta = Evarutil.new_meta() in
+	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |]))
+	  
+let resolve_morphism env sigma direction oldt m args args' cstr = 
+  let (morphism_cl, morphism_proj) = Lazy.force morphism_class in
+  let morph_instance, proj, sigargs, m', args, args' = 
+(*     if is_equiv env sigma m then  *)
+(*       let params, rest = array_chop 3 args in *)
+(*       let a, r, s = params.(0), params.(1), params.(2) in *)
+(*       let params', rest' = array_chop 3 args' in *)
+(*       let inst = mkApp (Lazy.force setoid_morphism, params) in *)
+(* 	(* Equiv gives a binary morphism *) *)
+(*       let (cl, proj) = Lazy.force class_two in *)
+(*       let ctxargs = [ a; r; s; a; r; s; mkProp; Lazy.force iff; Lazy.force iff_setoid; ] in *)
+(*       let m' = mkApp (m, [| a; r; s |]) in *)
+(* 	inst, proj, ctxargs, m', rest, rest' *)
+(*     else *)
+    let evars = ref (Evd.create_evar_defs Evd.empty) in
+    let pars =
 	match Array.length args with
-	    1 -> [Lazy.force class_one, 1]
-	  | 2 -> [Lazy.force class_two, 2; Lazy.force class_one, 1]
-	  | n -> [Lazy.force class_three, 3; Lazy.force class_two, 2; Lazy.force class_one, 1]
+	    1 -> [1]
+	  | 2 -> [2;1]
+	  | 3 -> [3;2;1]
+	  | _ -> [4;3;2;1]
       in
 	try 
-	  List.iter (fun ((cl, proj), n) ->
+	  List.iter (fun n ->
 	    evars := Evd.create_evar_defs Evd.empty;
-	    let cl_param, cl_context = match cl.cl_context with hd :: tl -> hd, tl | [] -> assert false in
-	    let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] (List.map snd cl_context) in
 	    let morphargs, morphobjs = array_chop (Array.length args - n) args in
 	    let morphargs', morphobjs' = array_chop (Array.length args - n) args' in
-	    let args = List.rev_map (fun (_, c) -> c) ctxevs in
 	    let appm = mkApp(m, morphargs) in
 	    let appmtype = Typing.type_of env sigma appm in
-	    let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in
-	    let mtype = replace_vars ctxevs (pi3 (snd cl_param)) in
+	    let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
+	    let cl_args = [| appmtype ; signature ; appm |] in
+	    let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
 	      try 
-		evars := Evarconv.the_conv_x env appmtype mtype !evars;
-		evars := Evarutil.nf_evar_defs !evars;
-		let app = Evarutil.nf_isevar !evars app in
-		  raise (Found (resolve_morphism_evd env evars app, proj, args, appm, morphobjs, morphobjs'))
+		let morph = resolve_morphism_evd env evars app in
+		let evm = Evd.evars_of !evars in
+		let sigargs = List.map 
+		  (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y) 
+		  sigargs 
+		in
+		let appm = Reductionops.nf_evar evm appm in
+		let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in
+		let proj = 
+		  mkApp (mkConst morphism_proj, 
+			Array.append cl_args [|morph|])
+		in
+		  raise (Found (morph, proj, sigargs, appm, morphobjs, morphobjs'))
 	      with Not_found -> ()
 		| Reduction.NotConvertible -> ()
 		| Stdpp.Exc_located (_, Pretype_errors.PretypeError _) 
 		| Pretype_errors.PretypeError _ -> ())
-	    cls; 
+	    pars;
 	  raise Not_found
 	with Found x -> x
   in 
-  evars := Evarutil.nf_evar_defs !evars;
-  let evm = Evd.evars_of !evars in
-  let ctxargs = List.map (Reductionops.nf_evar evm) subst in
-  let m' = Reductionops.nf_evar evm m' in
-  let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in
   let projargs, respars, typeargs = 
     array_fold_left2 
-      (fun (acc, ctxargs, typeargs') x y -> 
-	let par, ctx = list_chop 3 ctxargs in
+      (fun (acc, sigargs, typeargs') x y -> 
+	let (carrier, relation), sigargs = split_head sigargs in
 	  match y with
 	      None ->
-		let refl_proof = setoid_refl par x in
-		  [ refl_proof ; x ; x ] @ acc, ctx, x :: typeargs'
-	    | Some (p, (_, _, _, _, t')) ->
-		if direction then
-		  [ p ; t'; x ] @ acc, ctx, t' :: typeargs'
-		else [ p ; x; t' ] @ acc, ctx, t' :: typeargs')
-      ([], ctxargs, []) args args'
+		let refl_proof = reflexivity_proof env carrier relation x in
+		  [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs'
+	    | Some (p, (_, _, _, t')) ->
+		[ p ; t'; x ] @ acc, sigargs, t' :: typeargs')
+      ([], sigargs, []) args args'
   in
-  let proof = applistc appproj (List.rev projargs) in
+  let proof = applistc proj (List.rev projargs) in
   let newt = applistc m' (List.rev typeargs) in
     match respars with
-	[ a ; r ; s ] -> (proof, (a, r, s, oldt, newt))
+	[ a, r ] -> (proof, (a, r, oldt, newt))
       | _ -> assert(false)
-      
-let build_new gl env setoid direction occs origt newt hyp hypinfo concl =
+
+let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr =
   let is_occ occ = occs = [] || List.mem occ occs in
-  let rec aux t occ = 
+  let rec aux t occ cstr =
     match kind_of_term t with
       | _ when eq_constr t origt -> 
 	  if is_occ occ then
@@ -170,70 +235,82 @@ let build_new gl env setoid direction occs origt newt hyp hypinfo concl =
       | App (m, args) ->
 	  let args', occ = 
 	    Array.fold_left 
-	      (fun (acc, occ) arg -> let res, occ = aux arg occ in (res :: acc, occ))
+	      (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ))
 	      ([], occ) args
 	  in
-	  let res = 
+	  let res =
 	    if List.for_all (fun x -> x = None) args' then None
 	    else 
 	      let args' = Array.of_list (List.rev args') in
-		(try Some (resolve_morphism env (project gl) direction t m args args')
+		(try Some (resolve_morphism env sigma direction t m args args' cstr)
 		  with Not_found -> None)
 	  in res, occ
 
       | Prod (_, x, b) -> 
-	  let x', occ = aux x occ in
-	  let b', occ = aux b occ in
+	  let x', occ = aux x occ None in
+	  let b', occ = aux b occ None in
 	  let res = 
 	    if x' = None && b' = None then None
 	    else 
-	      (try Some (resolve_morphism env (project gl) direction t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |])
+	      (try Some (resolve_morphism env sigma direction t
+			    (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |]
+			    cstr)
 		with Not_found -> None)
 	  in res, occ
 
       | _ -> None, occ
-  in aux concl 1
-
-let decompose_setoid_eqhyp env sigma c dir t = 
-  match kind_of_term t with
-    | App (equiv, [| a; r; s; x; y |]) ->
-	if dir then (c, (a, r, s, x, y))
-	else (c, (a, r, s, y, x))
-    | App (r, args) when Array.length args >= 2 -> 
-	(try 
-	    let (p, (a, r, s, _, _)) = resolve_morphism env sigma dir t r args (Array.map (fun _ -> None) args) in
-	    let _, args = array_chop (Array.length args - 2) args in
-	      if dir then (c, (a, r, s, args.(0), args.(1)))
-	      else (c, (a, r, s, args.(1), args.(0)))
-	  with Not_found -> error "Not a (declared) setoid equality")
-    | _ -> error "Not a setoid equality"
+  in aux concl 1 cstr
+
+let decompose_setoid_eqhyp gl env sigma c left2right t = 
+  let (c, (car, rel, x, y) as res) =
+    match kind_of_term t with
+	(*     | App (equiv, [| a; r; s; x; y |]) -> *)
+	(* 	if dir then (c, (a, r, s, x, y)) *)
+	(* 	else (c, (a, r, s, y, x)) *)
+      | App (r, args) when Array.length args >= 2 -> 
+	  let relargs, args = array_chop (Array.length args - 2) args in
+	  let rel = mkApp (r, relargs) in
+	  let typ = pf_type_of gl rel in
+	    (match kind_of_term typ with
+	      | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation) 
+		    || eq_constr relation (Lazy.force coq_relationT) ->
+		  (c, (carrier, rel, args.(0), args.(1)))
+	      | _ when isArity typ ->
+		  let (ctx, ar) = destArity typ in
+		    (match ctx with
+			[ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
+			  (c, (sx, rel, args.(0), args.(1)))
+		      | _ -> error "Only binary relations are supported")
+	      | _ -> error "Not a relation")
+      | _ -> error "Not a relation"
+  in
+    if left2right then res
+    else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
 
 let cl_rewrite_clause c left2right occs clause gl =
   let env = pf_env gl in
   let sigma = project gl in
   let hyp = pf_type_of gl c in
-  let hypt, (typ, rel, setoid, origt, newt as hypinfo) = decompose_setoid_eqhyp env sigma c left2right hyp in
+  let hypt, (typ, rel, origt, newt as hypinfo) = decompose_setoid_eqhyp gl env sigma c left2right hyp in
   let concl, is_hyp = 
     match clause with
 	Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
       | None -> pf_concl gl, None
   in
-  let eq, _ = build_new gl env setoid left2right occs origt newt hypt hypinfo concl in
+  let cstr = 
+    match is_hyp with
+	None -> (mkProp, mkApp (Lazy.force inverse, [| mkProp; Lazy.force impl |]))
+      | Some _ -> (mkProp, Lazy.force impl)
+  in
+  let eq, _ = build_new gl env sigma left2right occs origt newt hypt hypinfo concl (Some cstr) in
     match eq with  
-	Some (p, (_, _, _, _, t)) -> 
-	  let proj = 
-	    if left2right then 
-	      let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
-	    else 
-	      let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in
-		applistc (Lazy.force proj)
-		  [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
-	  in
-	    (match is_hyp with
-	      | Some id -> Tactics.apply_in true id [proj,NoBindings]
-	      | None -> Tactics.apply proj) gl
+	Some (p, (_, _, oldt, newt)) -> 
+	  (match is_hyp with
+	    | Some id -> Tactics.apply_in true id [p,NoBindings]
+	    | None -> 
+		let meta = Evarutil.new_meta() in
+		let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in
+		  refine term) gl
       | None -> tclIDTAC gl
 	  
 open Extraargs
@@ -258,3 +335,17 @@ let clsubstitute o c =
 TACTIC EXTEND map_tac
 | [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
 END
+
+
+(* 
+	  let proj = 
+	    if left2right then 
+	      let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in
+		applistc (Lazy.force proj)
+		  [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
+	    else 
+	      let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in
+		applistc (Lazy.force proj)
+		  [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
+	  in
+*)
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
new file mode 100644
index 0000000000..6ecd4ac3c7
--- /dev/null
+++ b/theories/Classes/Relations.v
@@ -0,0 +1,569 @@
+(* -*- 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.
+   TODO: explain clrewrite, clsubstitute and so on.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Init.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Definition relationT A := A -> A -> Type.
+Definition relation A := A -> A -> Prop.
+
+Definition inverse A (R : relation A) : relation A := flip R.
+
+Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
+Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
+
+Definition complementT A (R : relationT A) := fun x y => ! R x y.
+
+Definition complement A (R : relation A) := fun x y => ~ R x y.
+
+(** These are convertible. *)
+
+Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R).
+Proof. reflexivity. Qed.
+
+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. *)
+
+Class Reflexive A (R : relationT A) :=
+  reflexive : forall x, R x x.
+
+Class Irreflexive A (R : relationT A) := 
+  irreflexive : forall x, R x x -> False.
+
+Class Symmetric A (R : relationT A) := 
+  symmetric : forall x y, R x y -> R y x.
+
+Class Asymmetric A (R : relationT A) := 
+  asymmetric : forall x y, R x y -> R y x -> False.
+
+Class Transitive A (R : relationT A) := 
+  transitive : 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 @irreflexive : ord.
+
+(** We can already dualize all these properties. *)
+
+Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) :=
+  reflexive := reflexive (R:=R).
+
+Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) :=
+  irreflexive := irreflexive (R:=R).
+
+Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R).
+
+  Solve Obligations using unfold flip ; program_simpl ; eapply symmetric ; eauto.
+
+Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R).
+  
+  Solve Obligations using program_simpl ; unfold flip in * ; intros ; eapply asymmetric ; eauto.
+
+Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R).
+
+  Solve Obligations using unfold flip ; program_simpl ; eapply transitive ; eauto.
+
+(** Have to do it again for Prop. *)
+
+Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) :=
+  reflexive := reflexive (R:=R).
+
+Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) :=
+  irreflexive := irreflexive (R:=R).
+
+Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R).
+
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply symmetric ; eauto.
+
+Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R).
+  
+  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; eapply asymmetric ; eauto.
+
+Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R).
+
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply transitive ; eauto.
+
+Program Instance [ Reflexive A (R : relation A) ] => 
+  reflexive_complement_irreflexive : Irreflexive A (complement R).
+
+  Next Obligation. 
+  Proof. 
+    unfold complement in * ; intros.
+    apply H.
+    apply reflexive.
+  Qed.
+
+Program Instance [ Irreflexive A (R : relation A) ] => 
+  irreflexive_complement_reflexive : Reflexive A (complement R).
+
+  Next Obligation. 
+  Proof. 
+    unfold complement in * ; intros.
+    red ; intros.
+    apply (irreflexive H).
+  Qed.
+
+Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R).
+
+  Next Obligation.
+  Proof.
+    unfold complement in *.
+    red ; intros H'.
+    apply (H (symmetric H')).
+  Qed.
+
+(** Tactics to solve goals. Each tactic comes in two flavors:
+   - a tactic to immediately solve a goal without user intervention
+   - a tactic taking input from the user to make progress on a goal *)
+
+Definition relate A (R : relationT A) : relationT A := R.
+
+Ltac relationify_relation R R' :=
+  match goal with
+    | [ H : context [ R ?x ?y ] |- _ ] => change (R x y) with (R' x y) in H
+    | [ |- context [ R ?x ?y ] ] => change (R x y) with (R' x y)
+  end.
+
+Ltac relationify R :=
+  set (R' := relate R) ; progress (repeat (relationify_relation R R')).
+
+Ltac relation_refl :=
+  match goal with
+    | [ |- ?R ?X ?X ] => apply (reflexive (R:=R) X)
+    | [ H : ?R ?X ?X |- _ ] => apply (irreflexive (R:=R) H)
+
+    | [ |- ?R ?A ?X ?X ] => apply (reflexive (R:=R A) X)
+    | [ H : ?R ?A ?X ?X |- _ ] => apply (irreflexive (R:=R A) H)
+
+    | [ |- ?R ?A ?B ?X ?X ] => apply (reflexive (R:=R A B) X)
+    | [ H : ?R ?A ?B ?X ?X |- _ ] => apply (irreflexive (R:=R A B) H)
+
+    | [ |- ?R ?A ?B ?C ?X ?X ] => apply (reflexive (R:=R A B C) X)
+    | [ H : ?R ?A ?B ?C ?X ?X |- _ ] => apply (irreflexive (R:=R A B C) H)
+
+    | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X)
+    | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H)
+  end.
+
+Ltac refl := relation_refl.
+
+Ltac relation_sym := 
+  match goal with
+    | [ H : ?R ?X ?Y |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y) H)
+
+    | [ H : ?R ?A ?X ?Y |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y) H)
+
+    | [ H : ?R ?A ?B ?X ?Y |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y) H)
+
+    | [ H : ?R ?A ?B ?C ?X ?Y |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y) H)
+
+    | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H)
+
+  end.
+
+Ltac relation_symmetric := 
+  match goal with
+    | [ |- ?R ?Y ?X ] => apply (symmetric (R:=R) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?Y ?X ] => apply (symmetric (R:=R A) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?B ?Y ?X ] => apply (symmetric (R:=R A B) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y))
+
+    | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y))
+  end.
+
+Ltac sym := relation_symmetric.
+
+Ltac relation_trans := 
+  match goal with
+    | [ H : ?R ?X ?Y, H' : ?R ?Y ?Z |- ?R ?X ?Z ] => 
+      apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?X ?Y, H' : ?R ?A ?Y ?Z |- ?R ?A ?X ?Z ] => 
+      apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?X ?Y, H' : ?R ?A ?B ?Y ?Z |- ?R ?A ?B ?X ?Z ] => 
+      apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?C ?X ?Y, H' : ?R ?A ?B ?C ?Y ?Z |- ?R ?A ?B ?C ?X ?Z ] => 
+      apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => 
+      apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H')
+  end.
+
+Ltac relation_transitive Y := 
+  match goal with
+    | [ |- ?R ?X ?Z ] => 
+      apply (transitive (R:=R) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?X ?Z ] => 
+      apply (transitive (R:=R A) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?B ?X ?Z ] => 
+      apply (transitive (R:=R A B) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?B ?C ?X ?Z ] => 
+      apply (transitive (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
+
+    | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => 
+      apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z))
+  end.
+
+Ltac trans Y := relation_transitive Y.
+
+(** To immediatly solve a goal on setoid equality. *)
+
+Ltac relation_tac := relation_refl || relation_sym || relation_trans.
+
+(** * Morphisms.
+
+   We now turn to the definition of [Morphism] and declare standard instances. 
+   These will be used by the [clrewrite] tactic later. *)
+
+(** Respectful morphisms. *)
+
+Definition respectful_depT (A : Type) (R : relationT A) 
+  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
+  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
+
+Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
+  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
+
+Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
+  fun f g => forall x y : A, R x y -> R' (f x) (g y).
+
+(** Notations reminiscent of the old syntax for declaring morphisms.
+   We use three + or - for type morphisms, and two for [Prop] ones.
+   *)
+
+Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
+Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+
+Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
+Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
+
+(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   for usual morphisms. *)
+
+Class Morphism A (R : relationT A) (m : A) :=
+  respect : R m m.
+
+Ltac simpl_morphism :=
+  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
+    try (red ; intros) ; try ( solve [ intuition ]).
+
+Ltac obligations_tactic ::= simpl_morphism.
+
+(** The arrow is a reflexive and transitive relation on types. *)
+
+Program Instance arrow_refl : ? Reflexive arrow := 
+  reflexive X := id.
+
+Program Instance arrow_trans : ? Transitive arrow := 
+  transitive X Y Z f g := g o f.
+
+(** Can't use the definition [notT] as it gives a to universe inconsistency. *)
+
+Program Instance notT_arrow_morphism : 
+  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
+
+(** Isomorphism. *)
+
+Definition iso (A B : Type) := 
+  A -> B * B -> A.
+
+Program Instance iso_refl : ? Reflexive iso.
+Program Instance iso_sym : ? Symmetric iso.
+Program Instance iso_trans : ? Transitive iso.
+
+Program Instance not_iso_morphism : 
+  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
+
+(** Logical implication. *)
+
+Program Instance impl_refl : ? Reflexive impl.
+Program Instance impl_trans : ? Transitive impl.
+
+Program Instance not_impl_morphism :
+  Morphism (Prop -> Prop) (impl --> impl) not.
+
+(** Logical equivalence. *)
+
+Program Instance iff_refl : ? Reflexive iff.
+Program Instance iff_sym : ? Symmetric iff.
+Program Instance iff_trans : ? Transitive iff.
+
+Program Instance not_iff_morphism : 
+  Morphism (Prop -> Prop) (iff ++> iff) not.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** If you have a morphism from [RA] to [RB] you have a contravariant morphism 
+   from [RA] to [inverse RB]. *)
+
+Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] =>
+  morph_impl_co_contra_inverse :
+  ? Morphism (RA --> inverse RB) m.
+
+  Next Obligation.
+  Proof.
+    apply respect.
+    apply H.
+  Qed.
+
+(** Every transitive relation gives rise to a binary morphism on [impl], 
+   contravariant in the first argument, covariant in the second. *)
+
+Program Instance [ Transitive A (R : relation A) ] => 
+  trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans x...
+    trans x0...
+  Qed.
+
+(** Dually... *)
+
+Program Instance [ Transitive A (R : relation A) ] =>
+  trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R.
+
+  Obligations Tactic := idtac.
+  
+  Next Obligation.
+  Proof with auto.
+    intros.
+    destruct (trans_contra_co_morphism (R:=inverse R)).
+    revert respect0.
+    unfold respectful, inverse, flip in * ; intros.
+    apply respect0 ; auto.
+  Qed.
+
+Obligations Tactic := simpl_morphism.
+
+(** With symmetric relations, variance is no issue ! *)
+
+Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
+  [ Morphism _ (R ++> R') m ] => 
+  sym_contra_morphism : ? Morphism (R --> R') m.
+
+  Next Obligation.
+  Proof with auto.
+    apply respect.
+    sym...
+  Qed.
+
+(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
+  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    trans x0... trans x... sym...
+  
+    trans y... trans y0... sym...
+  Qed.
+
+(** The complement of a relation conserves its morphisms. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
+
+  Next Obligation.
+  Proof.
+    red ; unfold complement ; intros.
+    pose (respect).
+    pose (r x y H).
+    pose (r0 x0 y0 H0).
+    intuition.
+  Qed.
+
+(** The inverse too. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
+
+  Next Obligation.
+  Proof.
+    unfold inverse ; unfold flip.
+    apply respect ; auto.
+  Qed.
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
+  trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+    sym...
+    trans y0...
+    sym...
+  Qed.
+
+(** Any binary morphism respecting some relations up to [iff] respects 
+   them up to [impl] in each way. Very important instances as we need [impl]
+   morphisms at the top level when we rewrite. *)
+
+Program Instance `A` (R : relation A) `B` (R' : relation B) 
+  [ ? Morphism (R ++> R' ++> iff) m ] => 
+  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+Program Instance `A` (R : relation A) `B` (R' : relation B)
+  [ ? Morphism (R ++> R' ++> iff) m ] => 
+  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+(** Standard instances for [iff] and [impl]. *)
+
+(** Logical conjunction. *)
+
+Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
+
+Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
+
+Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
+
+(** Logical disjunction. *)
+
+Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
+
+Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
+
+Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
+
+(** Leibniz equality. *)
+
+Program Instance eq_refl : ? Reflexive (@eq A).
+Program Instance eq_sym : ? Symmetric (@eq A).
+Program Instance eq_trans : ? Transitive (@eq A).
+
+Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) :=
+  trans_sym_morphism.
+
+Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m.
+
+(** The [PER] typeclass. *)
+
+Class PER (carrier : Type) (pequiv : relationT carrier) :=
+  per_sym :> Symmetric pequiv ;
+  per_trans :> Transitive pequiv.
+
+(** We can build a PER on the coq function space if we have PERs on the domain and
+   codomain. *)
+
+Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => 
+  arrow_per : PER (A -> B)
+  (fun f g => forall (x y : A), R x y -> R' (f x) (g y)).
+
+  Next Obligation.
+  Proof with auto.
+    constructor ; intros...
+    assert(R x0 x0) by (trans y0 ; [ auto | sym ; auto ]).
+    trans (y x0)...
+  Qed.
+
+(** The [Equivalence] typeclass. *)
+
+Class Equivalence (carrier : Type) (equiv : relationT carrier) :=
+  equiv_refl :> Reflexive equiv ;
+  equiv_sym :> Symmetric equiv ;
+  equiv_trans :> Transitive equiv.
+
+(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
+
+Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) := 
+  antisymmetric : forall x y, R x y -> R y x -> eqA x y.
+
+Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => 
+  flip_antisymmetric : ? Antisymmetric eq (flip R).
+
+  Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto.
+
+(** Here we build an equivalence instance for functions which relates respectful ones only. *)
+
+Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+  { morph : A -> B | respectful R R' morph morph }.
+
+Ltac obligations_tactic ::= program_simpl.
+
+Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
+  respecting_equiv : Equivalence respecting
+  (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    destruct x ; simpl.
+    apply r ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    sym ; apply H.
+    sym ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    trans ((`y) y0).
+    apply H ; auto.
+    apply H0. refl.
+  Qed.
+
+(** Leibinz equality [eq] is an equivalence relation. *)
+
+Program Instance eq_equivalence : Equivalence A eq.
+
+(** Logical equivalence [iff] is an equivalence relation. *)
+
+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)).
+*)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f61b4a4159..78e53aa012 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -22,72 +22,48 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** We first define setoids on a carrier, it amounts to an equivalence relation. 
-   Now [equiv] is overloaded for every [Setoid].
-*)
+Require Export Coq.Classes.Relations.
 
-Require Export Coq.Relations.Relations.
+(** A setoid wraps an equivalence. *)
 
-Class Setoid (carrier : Type) (equiv : relation carrier) :=
-  equiv_prf : equivalence carrier equiv.
+Class Setoid A :=
+  equiv : relation A ;
+  setoid_equiv :> Equivalence A equiv.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+(** Shortcuts to make proof search easier. *)
 
-Definition equiv [ Setoid A R ] : _ := R.
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(* 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.
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
+(** Standard setoids. *)
 
-Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
-Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
-Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
+Program Instance eq_setoid : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
 
-Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =/= y -> y =/= x.
-Proof.
-  intros ; red ; intros.
-  apply equiv_sym in H0...
-  apply (H H0).
-Qed.
-
-(** Tactics to do some progress on the goal, called by the user. *)
-
-Ltac do_setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
-    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
-    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
-    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
-  end.
+Program Instance iff_setoid : Setoid Prop :=
+  equiv := iff ; setoid_equiv := iff_equivalence.
 
-Ltac refl := do_setoid_refl.
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
-Ltac do_setoid_sym := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- not (@equiv ?A ?R ?s ?X ?Y) ] => apply (nequiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
-  end.
+(** 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. *)
 
-Ltac sym := do_setoid_sym.
+Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Ltac do_setoid_trans Y := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
-  end.
+Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
 
-Ltac trans y := do_setoid_trans y.
+Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
+Proof with auto.
+  intros ; red ; intros.
+  apply H.
+  sym...
+Qed.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -106,66 +82,24 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-(** Tactics to immediately solve the goal without user help. *)
-
-Ltac setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ H : ?X =/= ?X |- _ ] => elim H ; setoid_refl
-  end.
-
-Ltac setoid_sym := 
-  match goal with
-    | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H)
-    | [ H : ?X =/= ?Y |- ?Y =/= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
-  end.
-
-Ltac setoid_trans := 
-  match goal with
-    | [ H : ?X == ?Y, H' : ?Y == ?Z |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z) H H')
-  end.
-
-(** To immediatly solve a goal on setoid equality. *)
-
-Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans.
-
 Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(z == y) by setoid_sym.
-  assert(x == y) by setoid_trans.
+  assert(z == y) by relation_sym.
+  assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
 Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y == x) by setoid_sym.
-  assert(y == z) by setoid_trans.
+  assert(y == x) by relation_sym.
+  assert(y == z) by relation_trans.
   contradiction.
 Qed.
 
 Open Scope type_scope.
 
-(** Need to fix fresh to not fail if some arguments are not identifiers. *)
-(* Ltac setoid_sat ::= *)
-(*   match goal with *)
-(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
-(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
-(*   end. *)
-
-Ltac setoid_sat :=
-  match goal with
-    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
-    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
-  end.
-
 Ltac setoid_simplify_one :=
   match goal with
     | [ H : ?x == ?x |- _ ] => clear H
@@ -175,192 +109,68 @@ Ltac setoid_simplify_one :=
 
 Ltac setoid_simplify := repeat setoid_simplify_one.
 
-Ltac setoid_saturate := repeat setoid_sat.
-
 Ltac setoidify_tac :=
   match goal with
-    | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Setoid ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+    | [ 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.
 
-Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] 
-  (m : a -> b) : Prop :=
-  forall x y, eqa x y -> eqb (m x) (m y).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => 
-  Morphism (m : a -> b) :=
-  respect : respectful m.
-
-(** Here we build a setoid instance for functions which relates respectful ones only. *)
-
-Definition respecting [ Setoid a R, Setoid b R' ] : Type := 
-  { morph : a -> b | respectful morph }.
-
-Ltac obligations_tactic ::= try red ; program_simpl ; try tauto.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => 
-  arrow_setoid : 
-  Setoid ({ morph : a -> b | respectful morph })
-
-  (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-
-  Next Obligation.
-  Proof.
-    trans (y x0) ; eauto.
-    apply H.
-    refl.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    sym ; apply H.
-    sym ; auto.
-  Qed.
-
-(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
-   some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
-
-Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ]
-  (m : a -> b -> c) : Prop :=
-  forall x y, eqa x y -> 
-    forall z w, eqb z w -> eqc (m x z) (m y w).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => 
-  BinaryMorphism (m : a -> b -> c) :=
-  respect2 : binary_respectful m.
-
-Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ]
-  (m : a -> b -> c -> d) : Prop :=
-  forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => 
-  TernaryMorphism (m : a -> b -> c -> d) :=
-  respect3 : ternary_respectful m.
-
-(** Definition of the usual morphisms in [Prop]. *)
-
-Program Instance iff_setoid : Setoid Prop iff :=
-  equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
-
-Program Instance not_morphism : Morphism Prop iff Prop iff not.
-
-Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
-
-(* We make the setoids implicit, they're always [iff] *)
-
-Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]].
-
-Program Instance or_morphism : ? BinaryMorphism or.
-
-Definition impl (A B : Prop) := A -> B.
-
-Program Instance impl_morphism : ? BinaryMorphism impl.
-
-Next Obligation.
-Proof.
-  unfold impl. tauto.
-Qed.
-
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
-Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R.
+Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
+  trans_sym_morphism.
 
-Next Obligation.
-Proof with auto.
-  split ; intros.
-  trans x. sym... trans z...
-  trans y... trans w... sym...
-Qed.
-  
-Definition iff_morphism : BinaryMorphism iff := setoid_morphism.
+(** Add this very useful instance in the database. *)
 
-Existing Instance iff_morphism.
+Implicit Arguments setoid_morphism [[!sa]].
+Existing Instance setoid_morphism.
 
-Implicit Arguments eq [[A]].
+Definition type_eq : relation Type :=
+  fun x y => x = y.
 
-Program Instance eq_setoid : Setoid A eq :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+Program Instance type_equivalence : Equivalence Type type_eq.
 
-Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq.
+  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
 
-Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m.
+Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Implicit Arguments arrow_morphism [[A] [B] [C]].
+Ltac obligations_tactic ::= morphism_tac.
 
-Program Instance type_setoid : Setoid Type (fun x y => x = y) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+(** 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. *)
 
-Lemma setoid_subst : forall (x y : Type), x == y -> x -> y.
-Proof.
-  intros.
-  rewrite <- H.
-  apply X.
-Qed.
+Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y.
-Proof.
-  intros.
-  clrewrite <- H.
-  apply H0.
-Qed.
+Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
 
-Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
-  mg : ? Morphism sb sc g, mf : ? Morphism sa sb f ] => 
-  compose_morphism : ? Morphism sa sc (fun x => g (f x)).
+(* 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. *)
+    
 
-Next Obligation.
-Proof.
-  apply (respect (m0:=mg)).
-  apply (respect (m0:=mf)).
-  assumption.
-Qed.
+(* 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) (equiv : relation carrier) :=
-  pequiv_prf : PER carrier equiv.
+Class PartialSetoid (carrier : Type) :=
+  pequiv : relation carrier ;
+  pequiv_prf :> PER carrier pequiv.
 
 (** Overloaded notation for partial setoid equivalence. *)
 
-Definition pequiv [ PartialSetoid A R ] : _ := R.
-
 Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
-Definition pequiv_sym [ s : PartialSetoid A R ] : forall x y : A, R x y -> R y x := per_sym _ _ pequiv_prf.
-Definition pequiv_trans [ s : PartialSetoid A R ] : forall x y z : A, R x y -> R y z -> R x z := per_trans _ _ pequiv_prf.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_partial_setoid : 
-  PartialSetoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  pequiv_prf := Build_PER _ _ _ _.
-
-Next Obligation.
-Proof.
-  sym.
-  apply H.
-  sym ; assumption.
-Qed.
-
-Next Obligation.
-Proof.
-  trans (y x0).
-  apply H ; auto.
-  trans y0 ; auto.
-  sym ; auto.
-  apply H0 ; auto.
-Qed.
-
-(** The following is not definable. *)
-(*
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
-  Setoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-*)
-
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index f68a7d3a4b..0a86233166 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class [ Setoid A R ] => DecidableSetoid :=
+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 R ] => EqDec :=
+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
@@ -44,15 +44,15 @@ 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 
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
   end.
 
 Require Import Coq.Program.Program.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A R ] (x y : A) : bool :=
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A R ] (x y : A) : bool :=
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -71,19 +71,19 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 (** Decidable leibniz equality instances. *)
 
-Implicit Arguments eq [[A]].
-
 Require Import Coq.Arith.Arith.
 
-Program Instance nat_eqdec : EqDec nat eq :=
+(** 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 (@eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : EqDec bool eq :=
+Program Instance bool_eqdec : ? EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : EqDec unit eq :=
+Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) :=
   equiv_dec x y := left.
 
   Next Obligation.
@@ -92,7 +92,8 @@ Program Instance unit_eqdec : EqDec unit eq :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq :=
+Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => 
+  prod_eqdec : ? EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
@@ -101,13 +102,11 @@ Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq
       else right
     else right.
 
-  Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates.
-
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
+Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then left
@@ -118,7 +117,6 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
 
   Next Obligation.
   Proof.
-    red.
     extensionality x.
     destruct x ; auto.
   Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 540ac184e6..39809865cd 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -25,12 +25,12 @@ Require Export Coq.Classes.SetoidClass.
 (* Application of the extensionality axiom to turn a goal on leibinz equality to 
    a setoid equivalence. *)
 
-Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y.
+Lemma setoideq_eq [ sa : Setoid a ] : forall x y : a, x == y -> x = y.
 Proof.
   admit.
 Qed.
 
-Implicit Arguments setoideq_eq [[a] [eqa] [sa]].
+Implicit Arguments setoideq_eq [[a] [sa]].
 
 (** Application of the extensionality principle for setoids. *)
 
@@ -65,5 +65,25 @@ Ltac setoid_tactic :=
     | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl
     | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H
     | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tac
+    | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tactic
   end.
+(** Need to fix fresh to not fail if some arguments are not identifiers. *)
+(* Ltac setoid_sat ::= *)
+(*   match goal with *)
+(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
+(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
+(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
+(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
+(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
+(*   end. *)
+
+Ltac setoid_sat :=
+  match goal with
+    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
+    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
+    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
+    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
+    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
+  end.
+Ltac setoid_saturate := repeat setoid_sat.
+
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
new file mode 100644
index 0000000000..e5bc98dee3
--- /dev/null
+++ b/theories/Program/Basics.v
@@ -0,0 +1,143 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Standard functions and proofs about them.
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Program.FunctionalExtensionality.
+
+Definition compose `A B C` (g : B -> C) (f : A -> B) := fun x : A => g (f x).
+
+Definition arrow (A B : Type) := A -> B.
+
+Definition impl (A B : Prop) : Prop := A -> B.
+
+Definition id `A` := fun x : A => x.
+
+Hint Unfold compose.
+
+Notation " g 'o' f " := (compose g f)  (at level 50, left associativity) : program_scope.
+
+Open Scope program_scope.
+
+Lemma compose_id_left : forall A B (f : A -> B), id o f = f.
+Proof.
+  intros.
+  unfold id, compose.
+  symmetry ; apply eta_expansion.
+Qed.
+
+Lemma compose_id_right : forall A B (f : A -> B), f o id = f.
+Proof.
+  intros.
+  unfold id, compose.
+  symmetry ; apply eta_expansion.
+Qed.
+
+Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
+  h o (g o f) = h o g o f.
+Proof.
+  reflexivity.
+Qed.
+
+Hint Rewrite @compose_id_left @compose_id_right @compose_assoc : core.
+
+Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing).
+
+Definition const `A B` (a : A) := fun x : B => a.
+
+Definition flip `A B C` (f : A -> B -> C) x y := f y x.
+
+Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f.
+Proof.
+  unfold flip.
+  intros.
+  extensionality x ; extensionality y.
+  reflexivity.
+Qed.
+
+Definition apply `A B` (f : A -> B) (x : A) := f x.
+
+(** Notations for the unit type and value. *)
+
+Notation " () " := Datatypes.unit : type_scope.
+Notation " () " := tt.
+
+(** Set maximally inserted implicit arguments for standard definitions. *)
+
+Implicit Arguments eq [[A]].
+
+Implicit Arguments Some [[A]].
+Implicit Arguments None [[A]].
+
+Implicit Arguments inl [[A] [B]].
+Implicit Arguments inr [[A] [B]].
+
+Implicit Arguments left [[A] [B]].
+Implicit Arguments right [[A] [B]].
+
+(** Curryfication. *)
+
+Definition curry `a b c` (f : a -> b -> c) (p : prod a b) : c :=
+  let (x, y) := p in f x y.
+
+Definition uncurry `a b c` (f : prod a b -> c) (x : a) (y : b) : c :=
+  f (x, y).
+
+Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f.
+Proof.
+  simpl ; intros.
+  unfold uncurry, curry.
+  extensionality x ; extensionality y.
+  reflexivity.
+Qed.
+
+Lemma curry_uncurry : forall a b c (f : prod a b -> c), curry (uncurry f) = f.
+Proof.
+  simpl ; intros.
+  unfold uncurry, curry.
+  extensionality x. 
+  destruct x ; simpl ; reflexivity.
+Qed.
+
+(** Useful implicits and notations for lists. *)
+
+Require Export Coq.Lists.List.
+
+Implicit Arguments nil [[A]].
+Implicit Arguments cons [[A]].
+
+Notation " [] " := nil.
+Notation " [ x ] " := (cons x nil).
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
+
+(** n-ary exists ! *)
+
+Notation "'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
+  (at level 200, x ident, y ident, right associativity) : type_scope.
+
+Notation "'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
+  (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
+
+Notation "'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
+  (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
+
+Tactic Notation "exist" constr(x) := exists x.
+Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
+Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
+Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+
+Notation " ! A " := (notT A) (at level 200, A at level 100) : type_scope.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index fb172db845..4d92be3c5d 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -2,3 +2,4 @@ Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
 Require Export Coq.Program.Subset.
+Require Export Coq.Program.Basics.
\ No newline at end of file