Backtrack changes on eauto, move specialized version of eauto in

class_tactics for further customizations. Add Equivalence.v for
typeclass definitions on equivalences and clrewrite.v test-suite for
clrewrite. Debugging the tactic I found missing morphisms that are now
in Morphisms.v and removed some that made proof search fail or take too
long, not sure it's complete however.


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

6 files changed, 607 insertions, 155 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6569afc14..4eef08dcc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -33,6 +33,12 @@ open Hiddentac
 open Typeclasses
 open Typeclasses_errors
 
+open Evd
+
+(** Typeclasses instance search tactic / eauto *)
+
+open Auto
+
 let e_give_exact c gl = 
   let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
   if occur_existential t1 or occur_existential t2 then 
@@ -41,6 +47,275 @@ let e_give_exact c gl =
 
 let assumption id = e_give_exact (mkVar id)
 
+let unify_e_resolve  (c,clenv) gls = 
+  let clenv' = connect_clenv gls clenv in
+  let _ = clenv_unique_resolver false clenv' gls in
+  h_simplest_eapply c gls
+
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl = 
+    Eauto.registered_e_assumption ::
+    (tclTHEN Tactics.intro 
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	     (Hint_db.add_list hintl local_db) g'))) ::
+    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+  in 
+  tclFIRST (List.map tclCOMPLETE tacl) goal 
+
+and e_my_find_search db_list local_db hdc concl = 
+  let hdc = head_of_constr_reference hdc in
+  let hintl =
+    if occur_existential concl then 
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+    else 
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+  in 
+  let tac_of_hint = 
+    fun {pri=b; pat = p; code=t} -> 
+      (b, 
+       let tac =
+	 match t with
+	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	   | Give_exact (c) -> e_give_exact c
+	   | Res_pf_THEN_trivial_fail (term,cl) ->
+               tclTHEN (unify_e_resolve (term,cl)) 
+		 (e_trivial_fail_db db_list local_db)
+	   | Unfold_nth c -> unfold_in_concl [[],c]
+	   | Extern tacast -> conclPattern concl 
+	       (Option.get p) tacast
+       in 
+       (tac,fmt_autotactic t))
+  in 
+    List.map tac_of_hint hintl
+
+and e_trivial_resolve db_list local_db gl = 
+  try 
+    Auto.priority 
+      (e_my_find_search db_list local_db 
+	 (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  try List.map snd
+    (e_my_find_search db_list local_db 
+	(List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let find_first_goal gls = 
+  try first_goal gls with UserError _ -> assert false
+
+
+type search_state = { 
+  depth : int; (*r depth of search before failing *)
+  tacres : goal list sigma * validation;
+  last_tactic : std_ppcmds;
+  dblist : Auto.Hint_db.t list;
+  localdb :  Auto.Hint_db.t list }
+    
+module SearchProblem = struct
+    
+  type state = search_state
+
+  let success s = (sig_it (fst s.tacres)) = []
+
+  let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
+    
+  let pr_goals gls =
+    let evars = Evarutil.nf_evars (Refiner.project gls) in
+      prlist (pr_ev evars) (sig_it gls)
+	
+  let filter_tactics (glls,v) l =
+(*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+(*     let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
+    let rec aux = function
+      | [] -> []
+      | (tac,pptac) :: tacl -> 
+	  try 
+	    let (lgls,ptl) = apply_tac_list tac glls in 
+	    let v' p = v (ptl p) in
+(* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+(* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
+	      ((lgls,v'),pptac) :: aux tacl
+	  with e when Logic.catchable_exception e ->
+	    aux tacl
+    in aux l
+
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
+  let compare s s' =
+    let d = s'.depth - s.depth in
+    let nbgoals s = List.length (sig_it (fst s.tacres)) in
+    if d <> 0 then d else nbgoals s - nbgoals s'
+
+  let branching s = 
+    if s.depth = 0 then 
+      []
+    else      
+      let lg = fst s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let assumption_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (List.map 
+	       (fun id -> (Eauto.e_give_exact_constr (mkVar id),
+			   (str "exact" ++ spc () ++ pr_id id)))
+	       (pf_ids_of_hyps g))
+	in
+	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+				    last_tactic = pp; dblist = s.dblist;
+				    localdb = List.tl s.localdb }) l
+      in
+      let intro_tac = 
+	List.map 
+	  (fun ((lgls,_) as res,pp) -> 
+	     let g' = first_goal lgls in 
+	     let hintl = 
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+	       
+             let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in
+	     { depth = s.depth; tacres = res; 
+	       last_tactic = pp; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro,(str "intro")])
+      in
+      let rec_tacs = 
+	let l = 
+	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map 
+	  (fun ((lgls,_) as res, pp) -> 
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; tacres = res; last_tactic = pp;
+		 dblist = s.dblist; localdb = List.tl s.localdb }
+	     else 
+	       { depth = pred s.depth; tacres = res; 
+		 dblist = s.dblist; last_tactic = pp;
+		 localdb = 
+		   list_addn (nbgl'-nbgl) (match s.localdb with [] -> assert false | hd :: _ -> hd) s.localdb })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = 
+    msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
+		  s.last_tactic ++ str "\n"))
+
+end
+
+module Search = Explore.Make(SearchProblem)
+
+let make_initial_state n gls dblist localdbs =
+  { depth = n;
+    tacres = gls;
+    last_tactic = (mt ());
+    dblist = dblist;
+    localdb = localdbs }
+
+let e_depth_search debug p db_list local_dbs gls =
+  try
+    let tac = if debug then Search.debug_depth_first else Search.depth_first in
+    let s = tac (make_initial_state p gls db_list local_dbs) in
+    s.tacres
+  with Not_found -> error "EAuto: depth first search failed"
+
+let e_breadth_search debug n db_list local_dbs gls =
+  try
+    let tac = 
+      if debug then Search.debug_breadth_first else Search.breadth_first 
+    in
+    let s = tac (make_initial_state n gls db_list local_dbs) in
+    s.tacres
+  with Not_found -> error "EAuto: breadth first search failed"
+
+let e_search_auto debug (in_depth,p) lems db_list gls = 
+  let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
+  let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in
+  if in_depth then 
+    e_depth_search debug p db_list local_dbs gls
+  else
+    e_breadth_search debug p db_list local_dbs gls
+
+let full_eauto debug n lems gls = 
+  let dbnames = current_db_names () in
+  let dbnames =  list_subtract dbnames ["v62"] in
+  let db_list = List.map searchtable_map dbnames in
+    e_search_auto debug n lems db_list gls
+
+exception Found of evar_defs
+
+let valid evm p res_sigma l = 
+  let evd' =
+    Evd.fold
+      (fun ev evi (gls, sigma) ->
+	if not (Evd.is_evar evm ev) then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
+		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> ([], sigma)
+	else if not (Evd.is_defined evm ev) && p ev evi then
+	  match gls with
+	      hd :: tl -> 
+		if evi.evar_body = Evar_empty then
+		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
+		    (tl, Evd.evar_define ev cstr sigma)
+		else (tl, sigma)
+	    | [] -> assert(false)
+	else (gls, sigma))
+      !res_sigma (l, Evd.create_evar_defs !res_sigma)
+  in raise (Found (snd evd'))
+    
+let resolve_all_evars_once debug (mode, depth) env p evd =
+  let evm = Evd.evars_of evd in
+  let goals = 
+    Evd.fold
+      (fun ev evi gls ->
+	if evi.evar_body = Evar_empty && p ev evi then
+	  (evi :: gls)
+	else gls)
+      evm []
+  in
+  let gls = { it = List.rev goals; sigma = evm } in
+  let res_sigma = ref evm in
+    res_sigma := Evarutil.nf_evars (sig_sig gls');
+  let gls', valid' = full_eauto debug (mode, depth) [] (gls, valid evm p res_sigma) in
+    try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
+
+exception FoundTerm of constr
+
+let resolve_one_typeclass env gl =
+  let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in
+  let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in
+  let gls', valid' = full_eauto false (true, 15) [] (gls, valid) in
+    try ignore(valid' []); assert false with FoundTerm t -> t
+
+let has_undefined p evd =
+  Evd.fold (fun ev evi has -> has ||
+    (evi.evar_body = Evar_empty && p ev evi))
+    (Evd.evars_of evd) false
+    
+let rec resolve_all_evars debug m env p evd =
+  let rec aux n evd = 
+    if has_undefined p evd && n > 0 then
+      let evd' = resolve_all_evars_once debug m env p evd in
+	aux (pred n) evd'
+    else evd
+  in aux 3 evd
+
+(** Typeclass-based rewriting. *)
+
 let morphism_class = lazy (class_info (id_of_string "Morphism"))
 
 let get_respect cl = 
@@ -147,7 +422,16 @@ let reflexivity_proof env evars carrier relation x =
     (*     with Not_found -> *)
 (*       let meta = Evarutil.new_meta() in *)
 (* 	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *)
-	  
+
+let symmetric_proof env carrier relation =
+  let goal =
+    mkApp (Lazy.force symmetric_type, [| carrier ; relation |])
+  in
+    try 
+      let inst = resolve_one_typeclass env goal in
+	mkApp (Lazy.force symmetric_proof, [| carrier ; relation ; inst |])
+    with e when Logic.catchable_exception e -> raise Not_found
+
 let resolve_morphism env sigma oldt m args args' cstr evars =
   let (morphism_cl, morphism_proj) = Lazy.force morphism_class in
   let morph_instance, proj, sigargs, m', args, args' = 
@@ -270,10 +554,14 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
       | _ -> error "Not a relation"
   in
     if left2right then res
-    else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
+    else
+      try (mkApp (symmetric_proof env car rel, [| x ; y ; c |]), (car, rel, y, x))
+      with Not_found ->
+	(c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
 
 let resolve_all_typeclasses env evd = 
-  Eauto.resolve_all_evars false (true, 15) env (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
+  resolve_all_evars false (true, 15) env
+    (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
     
 (* let _ =  *)
 (*   Typeclasses.solve_instanciation_problem := *)
@@ -372,7 +660,7 @@ let resolve_argument_typeclasses d p env evd onlyargs all =
       (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
   in
     try 
-      Eauto.resolve_all_evars d p env pred evd
+      resolve_all_evars d p env pred evd
     with e -> 
       if all then raise e else evd
 	
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index effebf331..706ba9840 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -226,7 +226,6 @@ let find_first_goal gls =
 
 (*s The following module [SearchProblem] is used to instantiate the generic
     exploration functor [Explore.Make]. *)
-      
 
 type search_state = { 
   depth : int; (*r depth of search before failing *)
@@ -339,13 +338,6 @@ let make_initial_state n gl dblist localdb =
     dblist = dblist;
     localdb = [localdb] }
 
-let make_initial_state_gls n gls dblist localdbs =
-  { depth = n;
-    tacres = gls;
-    last_tactic = (mt ());
-    dblist = dblist;
-    localdb = localdbs }
-
 let debug_depth_first = Search.debug_depth_first
 
 let e_depth_search debug p db_list local_db gl =
@@ -355,13 +347,6 @@ let e_depth_search debug p db_list local_db gl =
     s.tacres
   with Not_found -> error "EAuto: depth first search failed"
 
-let e_depth_search_gls debug p db_list local_dbs gls =
-  try
-    let tac = if debug then Search.debug_depth_first else Search.depth_first in
-    let s = tac (make_initial_state_gls p gls db_list local_dbs) in
-    s.tacres
-  with Not_found -> error "EAuto: depth first search failed"
-
 let e_breadth_search debug n db_list local_db gl =
   try
     let tac = 
@@ -371,15 +356,6 @@ let e_breadth_search debug n db_list local_db gl =
     s.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_breadth_search_gls debug n db_list local_dbs gls =
-  try
-    let tac = 
-      if debug then Search.debug_breadth_first else Search.breadth_first 
-    in
-    let s = tac (make_initial_state_gls n gls db_list local_dbs) in
-    s.tacres
-  with Not_found -> error "EAuto: breadth first search failed"
-
 let e_search_auto debug (in_depth,p) lems db_list gl = 
   let local_db = make_local_hint_db lems gl in 
   if in_depth then 
@@ -389,14 +365,6 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
 
 open Evd
 
-let e_search_auto_gls debug (in_depth,p) lems db_list gls = 
-  let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
-  let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in
-  if in_depth then 
-    e_depth_search_gls debug p db_list local_dbs gls
-  else
-    e_breadth_search_gls debug p db_list local_dbs gls
-
 let eauto debug np lems dbnames =
   let db_list =
     List.map
@@ -413,12 +381,6 @@ let full_eauto debug n lems gl =
   let db_list = List.map searchtable_map dbnames in
   tclTRY (e_search_auto debug n lems db_list) gl
 
-let full_eauto_gls debug n lems gls = 
-  let dbnames = current_db_names () in
-  let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map searchtable_map dbnames in
-    e_search_auto_gls debug n lems db_list gls
-
 let gen_eauto d np lems = function
   | None -> full_eauto d np lems
   | Some l -> eauto d np lems l
@@ -482,60 +444,3 @@ TACTIC EXTEND dfs_eauto
       hintbases(db) ] ->
     [ gen_eauto false (true, make_depth p) lems db ]
 END
-
-open Evd
-
-exception Found of evar_defs
-
-let valid evm p res_sigma l = 
-  let evd' =
-    Evd.fold
-      (fun ev evi (gls, sigma) ->
-	if not (Evd.is_evar evm ev) then
-	  match gls with
-	      hd :: tl -> 
-		if evi.evar_body = Evar_empty then
-		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		    (tl, Evd.evar_define ev cstr sigma)
-		else (tl, sigma)
-	    | [] -> ([], sigma)
-	else if not (Evd.is_defined evm ev) && p ev evi then
-	  match gls with
-	      hd :: tl -> 
-		if evi.evar_body = Evar_empty then
-		  let cstr, obls = Refiner.extract_open_proof !res_sigma hd in
-		    (tl, Evd.evar_define ev cstr sigma)
-		else (tl, sigma)
-	    | [] -> assert(false)
-	else (gls, sigma))
-      !res_sigma (l, Evd.create_evar_defs !res_sigma)
-  in raise (Found (snd evd'))
-    
-let resolve_all_evars_once debug (mode, depth) env p evd =
-  let evm = Evd.evars_of evd in
-  let goals = 
-    Evd.fold
-      (fun ev evi gls ->
-	if evi.evar_body = Evar_empty && p ev evi then
-	  (evi :: gls)
-	else gls)
-      evm []
-  in
-  let gls = { it = List.rev goals; sigma = evm } in
-  let res_sigma = ref evm in
-  let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
-    res_sigma := Evarutil.nf_evars (sig_sig gls');
-    try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
-
-let has_undefined p evd =
-  Evd.fold (fun ev evi has -> has ||
-    (evi.evar_body = Evar_empty && p ev evi))
-    (Evd.evars_of evd) false
-    
-let rec resolve_all_evars debug m env p evd =
-  let rec aux n evd = 
-    if has_undefined p evd && n > 0 then
-      let evd' = resolve_all_evars_once debug m env p evd in
-	aux (pred n) evd'
-    else evd
-  in aux 3 evd
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index a1ff89905..34655b134 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -27,50 +27,5 @@ val registered_e_assumption : tactic
 
 val e_give_exact_constr : constr -> tactic
 
-type search_state = { 
-  depth : int; (*r depth of search before failing *)
-  tacres : goal list sigma * validation;
-  last_tactic : Pp.std_ppcmds;
-  dblist : Auto.Hint_db.t list;
-  localdb :  Auto.Hint_db.t list }
-
-module SearchProblem : sig
-  type state = search_state
-      
-  val filter_tactics :     Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a) ->
-    (Tacmach.tactic * Pp.std_ppcmds) list ->
-    ((Proof_type.goal list Tacmach.sigma * (Proof_type.proof_tree list -> 'a)) *
-     Pp.std_ppcmds)
-    list
-
-  val compare :  search_state -> search_state -> int
-
-  val branching : state -> state list
-  val success : state -> bool
-  val pp : state -> unit
-end
-
-module Search : sig
-  val depth_first : search_state -> search_state
-  val debug_depth_first : search_state -> search_state
-
-  val breadth_first : search_state -> search_state
-  val debug_breadth_first : search_state -> search_state
-end
-
-val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation -> 
-  goal list sigma * validation
-
-val resolve_all_evars_once : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
-  evar_defs
-
-val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
-  evar_defs
-
-val valid :     Evd.evar_map ->
-    (Evd.evar -> Evd.evar_info -> bool) ->
-    Evd.evar_map ref -> Proof_type.proof_tree list -> 'a
-
-
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic
diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v
new file mode 100644
index 000000000..5c56a0daf
--- /dev/null
+++ b/test-suite/typeclasses/clrewrite.v
@@ -0,0 +1,111 @@
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Classes.Equivalence.
+
+Section Equiv.
+  Context [ Equivalence A eqA ].
+
+  Variables x y z w : A.
+
+  Goal eqA x y -> eqA y x.
+    intros H ; clrewrite H.
+    refl.
+  Qed.
+
+  Tactic Notation "simpl" "*" := auto || relation_tac.
+  
+  Goal eqA x y -> eqA y x /\ True.
+    intros H ; clrewrite H.
+    split ; simpl*.
+  Qed.
+
+  Goal eqA x y -> eqA y x /\ eqA x x.
+    intros H ; clrewrite H.
+    split ; simpl*.
+  Qed.
+
+  Goal eqA x y -> eqA y z -> eqA x y.
+    intros H. 
+    clrewrite H.
+    intro. refl.
+  Qed.
+        
+  Goal eqA x y -> eqA z y -> eqA x y.
+    intros H. 
+    clrewrite <- H at 2.
+    clrewrite <- H at 1.
+    intro. refl.
+  Qed.
+
+  Opaque complement.
+
+  Print iff_inverse_impl_binary_morphism.
+
+  Goal eqA x y -> eqA x y -> eqA x y.
+    intros H.
+    clrewrite H.
+    intro. refl.
+  Qed.
+
+  Goal eqA x y -> eqA x y -> eqA x y.
+    intros H.
+    clrewrite <- H.
+    refl.
+  Qed.
+  
+  Goal eqA x y -> True /\ True /\ False /\ eqA x x -> True /\ True /\ False /\ eqA x y.
+  Proof.
+    intros.
+    clrewrite <- H.
+    apply H0.
+  Qed.
+
+End Equiv.
+
+Section Trans.
+  Context [ Transitive A R ].
+
+  Variables x y z w : A.
+
+  Tactic Notation "simpl" "*" := auto || relation_tac.
+  
+(*   Typeclasses eauto := debug. *)
+
+  Goal R x y -> R y x -> R y y -> R x x.
+  Proof with auto.
+    intros H H' H''. 
+
+    clrewrite <- H' at 2.
+    clrewrite H at 1...
+  Qed.
+
+  Goal R x y -> R y z -> R x z.
+    intros H.
+    clrewrite H.
+    refl.
+  Qed.
+        
+  Goal R x y -> R z y -> R x y.
+    intros H. 
+    clrewrite <- H at 2.
+    intro. 
+    clrewrite H at 1.
+  Abort.
+
+  Goal R x y -> True /\ R y z -> True /\ R x z.
+  Proof.
+    intros.
+    clrewrite H.
+    apply H0.
+  Qed.
+
+  Goal R x y -> True /\ True /\ False /\ R y z -> True /\ True /\ False /\ R x z.
+  Proof.
+    intros.
+    clrewrite H.
+    apply H0.
+  Qed.
+
+End Trans.
\ No newline at end of file
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
new file mode 100644
index 000000000..bd525e035
--- /dev/null
+++ b/theories/Classes/Equivalence.v
@@ -0,0 +1,157 @@
+(* -*- 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.
+
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
+
+Definition equiv [ Equivalence A R ] : relation A := R.
+
+(** Shortcuts to make proof search possible (unification won't unfold equiv). *)
+
+Definition equivalence_refl [ sa : Equivalence A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition equivalence_sym [ sa : Equivalence A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition equivalence_trans [ sa : Equivalence A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+(** 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 => clsubstitute 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 [ Equivalence A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Proof with auto.
+  intros; intro.
+  assert(z == y) by relation_sym.
+  assert(x == y) by relation_trans.
+  contradiction.
+Qed.
+
+Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Proof.
+  intros; intro. 
+  assert(y == x) by relation_sym.
+  assert(y == z) by relation_trans.
+  contradiction.
+Qed.
+
+Open Scope type_scope.
+
+Ltac equiv_simplify_one :=
+  match goal with
+    | [ H : ?x == ?x |- _ ] => clear H
+    | [ H : ?x == ?y |- _ ] => clsubst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac equiv_simplify := repeat equiv_simplify_one.
+
+Ltac equivify_tac :=
+  match goal with
+    | [ s : Equivalence ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Equivalence ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac equivify := repeat equivify_tac.
+
+(** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *)
+
+Instance [ sa : Equivalence A ] => equiv_morphism : ? Morphism (equiv ++> equiv ++> iff) equiv :=
+  respect := respect.
+
+(** The partial application too as it is reflexive. *)
+
+Instance [ sa : Equivalence A ] (x : A) => 
+  equiv_partial_app_morphism : ? Morphism (equiv ++> iff) (equiv x) :=
+  respect := respect. 
+
+Definition type_eq : relation Type :=
+  fun x y => x = y.
+
+Program Instance type_equivalence : Equivalence Type type_eq.
+
+  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
+
+Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
+
+Ltac obligations_tactic ::= morphism_tac.
+
+(** These are morphisms used to rewrite at the top level of a proof, 
+   using [iff_impl_id_morphism] if the proof is in [Prop] and
+   [eq_arrow_id_morphism] if it is in Type. *)
+
+Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
+
+(* 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 equivs don't require reflexivity so we can build a partial equiv on the function space. *)
+
+Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
+  pequiv_prf :> PER carrier pequiv.
+
+(** Overloaded notation for partial equiv 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/Morphisms.v b/theories/Classes/Morphisms.v
index 72db276e4..3ba6c1824 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -16,7 +16,6 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
 Require Export Coq.Classes.Relations.
 
 Set Implicit Arguments.
@@ -130,6 +129,10 @@ Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
     destruct respect with x y x0 y0 ; auto.
   Qed.
 
+(** Logical implication [impl] is a morphism for logical equivalence. *)
+
+Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl.
+
 (** The complement of a relation conserves its morphisms. *)
 
 Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
@@ -257,20 +260,20 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** With symmetric relations, variance is no issue ! *)
 
-Program Instance [ Symmetric A R ] B (R' : relation B) 
-  [ Morphism _ (R ++> R') m ] => 
-  sym_contra_morphism : ? Morphism (R --> R') m.
+(* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
+(*   [ Morphism _ (R ++> R') m ] [ Symmetric A R ] =>  *)
+(*   sym_contra_morphism : ? Morphism (R --> R') m. *)
 
-  Next Obligation.
-  Proof with auto.
-    repeat (red ; intros). apply respect.
-    sym...
-  Qed.
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     repeat (red ; intros). apply respect. *)
+(*     sym... *)
+(*   Qed. *)
 
 (** [R] is reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Reflexive A R ] B (R' : relation B)
-  [ ? Morphism (R ++> R') m ] (x : A) =>
+Program Instance (A B : Type) (R : relation A) (R' : relation B)
+  [ ? Morphism (R ++> R') m ] [ Reflexive A R ] (x : A) =>
   reflexive_partial_app_morphism : ? Morphism R' (m x).
 
   Next Obligation.
@@ -280,6 +283,27 @@ Program Instance [ Reflexive A R ] B (R' : relation B)
     refl.
   Qed.
 
+(** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
+   to get an [R y z] goal. *)
+
+Program Instance [ Transitive A R ] => 
+  trans_co_eq_inv_impl_morphism : ? Morphism (R ++> eq ++> inverse impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+    subst x0...
+  Qed.
+
+Program Instance [ Transitive A R ] => 
+  trans_contra_eq_inv_impl_morphism : ? Morphism (R --> eq ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans x...
+    subst x0...
+  Qed.
+
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
 Program Instance [ Transitive A R, Symmetric A R ] => 
@@ -326,6 +350,12 @@ 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. *)
@@ -334,4 +364,10 @@ 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.