Ajout du .ml pour la tactique Setoid_replace

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

2 files changed, 703 insertions, 0 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
new file mode 100644
index 0000000000..dd35bc58f4
--- /dev/null
+++ b/tactics/setoid_replace.ml
@@ -0,0 +1,681 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Tacmach
+open Proof_type
+open Libobject
+open Reduction
+open Term
+open Names
+open Util
+open Pp
+open Printer
+open Vernacinterp
+open Environ
+open Termast
+open Command
+open Tactics 
+
+type setoid =
+    { set_a : constr;
+      set_aeq : constr;
+      set_th : constr
+    }
+
+type morphism =
+    { lem : constr;
+      profil : bool list;
+      arg_types : constr list;
+      lem2 : constr option
+    }
+
+let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c
+
+let constant dir s =
+  let dir = "Coq"::"Setoid"::dir in
+  let id = id_of_string s in
+    try 
+      Declare.global_reference_in_absolute_module dir id
+  with Not_found ->
+    anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+
+let global_constant dir s =
+  let dir = "Coq"::"Init"::dir in
+  let id = id_of_string s in
+    try 
+      Declare.global_reference_in_absolute_module dir id
+  with Not_found ->
+    anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id)))
+
+let current_constant id =
+  try
+    Declare.global_reference CCI id
+  with Not_found ->
+    anomaly ("Setoid: cannot find "^(string_of_id id))
+
+(* Setoid_theory *)
+
+let coq_Setoid_Theory = lazy(constant ["Setoid_replace"] "Setoid_Theory")
+
+let coq_seq_refl = lazy(constant ["Setoid_replace"] "Seq_refl")
+let coq_seq_sym = lazy(constant ["Setoid_replace"] "Seq_sym")
+let coq_seq_trans = lazy(constant ["Setoid_replace"] "Seq_trans")
+
+let coq_fleche = lazy(constant ["Setoid_replace"] "fleche")
+
+(* Coq constants *)
+
+let coqeq = lazy(global_constant ["Logic"] "eq")
+
+let coqconj = lazy(global_constant ["Logic"] "conj")
+
+(************************* Table of declared setoids **********************)
+
+
+(* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
+
+module Cmap = Map.Make(struct type t = constr let compare = compare end)
+
+let setoid_table = ref Gmap.empty
+
+let setoid_table_add (s,th) = setoid_table := Gmap.add s th !setoid_table
+let setoid_table_find s = Gmap.find s !setoid_table
+let setoid_table_mem s = Gmap.mem s !setoid_table
+
+let equiv_list () = List.map (fun x -> x.set_aeq) (Gmap.rng !setoid_table)
+
+let _ = 
+  Summary.declare_summary "setoid-table"
+    { Summary.freeze_function = (fun () -> !setoid_table);
+      Summary.unfreeze_function = (fun t -> setoid_table := t);
+      Summary.init_function = (fun () -> setoid_table := Gmap .empty);
+      Summary.survive_section = false }
+
+(* Declare a new type of object in the environment : "setoid-theory". *)
+
+let (setoid_to_obj, obj_to_setoid)=
+  let cache_set (_,(s, th)) = setoid_table_add (s,th)
+  and export_set x = Some x 
+  in 
+    declare_object ("setoid-theory",
+		    { cache_function = cache_set;
+		      load_function = (fun _ -> ());
+		      open_function = cache_set;
+		      export_function = export_set})
+
+(******************************* Table of declared morphisms ********************)
+
+(* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
+
+let morphism_table = ref Gmap.empty
+
+let morphism_table_add (m,c) = morphism_table := Gmap.add m c !morphism_table
+let morphism_table_find m = Gmap.find m !morphism_table
+let morphism_table_mem m = Gmap.mem m !morphism_table
+
+let _ = 
+  Summary.declare_summary "morphism-table"
+    { Summary.freeze_function = (fun () -> !morphism_table);
+      Summary.unfreeze_function = (fun t -> morphism_table := t);
+      Summary.init_function = (fun () -> morphism_table := Gmap .empty);
+      Summary.survive_section = false }
+
+(* Declare a new type of object in the environment : "morphism-definition". *)
+
+let (morphism_to_obj, obj_to_morphism)=
+  let cache_set (_,(m, c)) = morphism_table_add (m, c)
+  and export_set x = Some x 
+  in 
+    declare_object ("morphism-definition",
+		    { cache_function = cache_set;
+		      load_function = (fun _ -> ());
+		      open_function = cache_set;
+		      export_function = export_set})
+
+(************************** Adding a setoid to the database *********************)
+
+(* Find the setoid theory associated with a given type A.
+This implies that only one setoid theory can be declared for
+a given type A. *)
+
+let find_theory a =
+  try 
+    setoid_table_find a 
+  with Not_found ->
+    errorlabstrm "Setoid" 
+      [< 'sTR "No Declared Setoid Theory for ";
+	 prterm a; 'fNL;
+	 'sTR "Use Add Setoid to declare it">]
+    
+(* Add a Setoid to the database after a type verification. *)
+
+let eq_lem_proof env a eq sym trans = 
+  lambda_create env
+    (a, lambda_create env
+       (a, lambda_create env
+	  (a, lambda_create env 
+	     (a, lambda_create env 
+		((mkApp (eq, [|(mkRel 4);(mkRel 3)|])), lambda_create env
+		   ((mkApp (eq, [|(mkRel 3);(mkRel 2)|])), lambda_create env
+		      ((mkApp (eq, [|(mkRel 6);(mkRel 4)|])),
+		       (mkApp (trans,
+			       [|(mkRel 6);(mkRel 7);(mkRel 4);
+				 (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
+				 (mkApp (trans,
+					 [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]
+			      )))))))))
+
+let eq_lem2_proof env a eq sym trans = 
+  lambda_create env
+    (a, lambda_create env
+       (a, lambda_create env
+	  (a, lambda_create env 
+	     (a, lambda_create env 
+		((mkApp (eq, [|(mkRel 4);(mkRel 3)|])), lambda_create env
+		   ((mkApp (eq, [|(mkRel 3);(mkRel 2)|])),
+		    (mkApp ((Lazy.force coqconj),
+			    [|(mkArrow 
+				 (mkApp (eq, [|(mkRel 6);(mkRel 4)|]))
+				 (mkApp (eq, [|(mkRel 6);(mkRel 4)|])));
+			      (mkArrow
+				 (mkApp (eq, [|(mkRel 5);(mkRel 3)|]))
+				 (mkApp (eq, [|(mkRel 7);(mkRel 5)|])));
+			      (lambda_create env
+				 ((mkApp (eq, [|(mkRel 6);(mkRel 4)|])),
+				  (mkApp (trans,
+					  [|(mkRel 6);(mkRel 7);(mkRel 4);
+					    (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
+					    (mkApp (trans,
+						    [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]))));
+			      (lambda_create env
+				 ((mkApp (eq, [|(mkRel 5);(mkRel 3)|])),
+				  (mkApp (trans,
+					  [|(mkRel 7);(mkRel 6);(mkRel 5);(mkRel 3);
+					    (mkApp (trans,
+						    [|(mkRel 6);(mkRel 4);(mkRel 5);(mkRel 1);
+						      (mkApp (sym, [|(mkRel 5);(mkRel 4);(mkRel 2)|]))|]))|]))))|]))))))))
+
+let gen_eq_lem_name =
+  let i = ref 0 in
+    function () -> 
+      incr i;
+      id_of_string ("setoid_eq_ext"^(string_of_int !i))
+
+let add_setoid a aeq th =
+  if setoid_table_mem a 
+  then errorlabstrm "Add Setoid"
+    [< 'sTR "A Setoid Theory is already declared for "; prterm a >]
+  else let env = Global.env () in
+    if (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
+	  (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |])))
+    then (Lib.add_anonymous_leaf 
+	    (setoid_to_obj 
+	       (a, { set_a = a;
+		     set_aeq = aeq;
+		     set_th = th}));
+	  let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in
+	  let trans = mkApp ((Lazy.force coq_seq_trans), [|a; aeq; th|]) in
+	  let eq_morph = eq_lem_proof env a aeq sym trans in
+	  let eq_morph2 = eq_lem2_proof env a aeq sym trans in
+	    Options.if_verbose pPNL [< prterm a;'sTR " is registered as a setoid">];
+	    let eq_ext_name = gen_eq_lem_name () in 
+	    let eq_ext_name2 = gen_eq_lem_name () in 
+	    let _ = Declare.declare_constant eq_ext_name
+		      ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph; 
+					       Declarations.const_entry_type = None}),
+		       Declare.NeverDischarge,true) in
+	    let _ = Declare.declare_constant eq_ext_name2
+		      ((Declare.ConstantEntry {Declarations.const_entry_body = eq_morph2; 
+					       Declarations.const_entry_type = None}),
+		       Declare.NeverDischarge,true) in
+	    let eqmorph = (current_constant eq_ext_name) in
+	    let eqmorph2 = (current_constant eq_ext_name2) in
+	      (Lib.add_anonymous_leaf
+		 (morphism_to_obj (aeq, 
+				   { lem = eqmorph;
+				     profil = [true; true];
+				     arg_types = [a;a];
+				     lem2 = (Some eqmorph2)})));
+	      Options.if_verbose pPNL [< prterm aeq;'sTR " is registered as a morphism">])
+    else errorlabstrm "Add Setoid" [< 'sTR "Not a valid setoid theory" >]
+
+(* The vernac command "Add Setoid" *)
+
+let constr_of_comarg = function 
+  | VARG_CONSTR c -> constr_of c
+  | _ -> anomaly "Add Setoid"
+
+let _ = 
+  vinterp_add "AddSetoid"
+    (function 
+       | [(VARG_CONSTR a); (VARG_CONSTR aeq); (VARG_CONSTR th)] -> 
+	   (fun () -> (add_setoid 
+			 (constr_of a)
+			 (constr_of aeq)
+			 (constr_of th)))
+       | _ -> anomaly "AddSetoid")
+ 
+(***************** Adding a morphism to the database ****************************)
+
+(* We maintain a table of the currently edited proofs of morphism lemma
+   in order to add them in the morphism_table when the user does Save *)
+
+let edited = ref Gmap.empty
+
+let new_edited id m profil = 
+  edited := Gmap.add id (m,profil)  !edited
+
+let is_edited id =
+  Gmap.mem id !edited
+
+let no_more_edited id =
+  edited := Gmap.remove id !edited
+
+let what_edited id =
+  Gmap.find id !edited
+
+let check_is_dependent t n =
+  let rec aux t i n =
+    if (i<n)
+    then (dependent (mkRel i) t) || (aux t (i+1) n)
+    else false
+  in aux t 0 n
+
+let gen_lem_name m = match kind_of_term m with 
+  | IsVar id -> id_of_string ((string_of_id id)^"_ext")
+  | IsConst (sp, _) -> id_of_string ((string_of_id(basename sp))^"_ext")
+  | IsMutInd ((sp, i), _) -> id_of_string ((string_of_id(basename sp))^(string_of_int i)^"_ext")
+  | IsMutConstruct (((sp,i),j), _) -> id_of_string 
+      ((string_of_id(basename sp))^(string_of_int i)^(string_of_int i)^"_ext")
+  | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">]
+
+let gen_lemma_tail m lisset body n =
+  let l = (List.length lisset) in
+  let a1 = Array.create l (mkRel 0) in
+  let a2 = Array.create l (mkRel 0) in
+  let rec aux i n = function
+    | true::q -> 
+	a1.(i) <- (mkRel n);
+	a2.(i) <- (mkRel (n-1));
+	aux (i+1) (n-2) q
+    | false::q ->
+	a1.(i) <- (mkRel n);
+	a2.(i) <- (mkRel n);
+	aux (i+1) (n-1) q
+    | [] -> () in 
+    aux 0 n lisset;
+    if (eq_constr body mkProp)
+    then mkArrow (mkApp (m,a1)) (lift 1 (mkApp (m, a2)))
+    else if (setoid_table_mem body)
+    then mkApp ((setoid_table_find body).set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|])
+    else mkApp ((Lazy.force coqeq), [|body; (mkApp (m, a1)); (mkApp (m, a2))|])
+
+let gen_lemma_middle m larg lisset body n =
+  let rec aux la li i n = match (la, li) with
+    | ([], []) -> gen_lemma_tail m lisset body n
+    | (t::q, true::lq) -> 
+	mkArrow (mkApp ((setoid_table_find t).set_aeq, 
+			[|(mkRel i); (mkRel (i-1))|])) (aux q lq (i-1) (n+1))
+    | (t::q, false::lq) -> aux q lq (i-1) n
+    | _ -> assert false
+  in aux larg lisset n n
+
+let gen_compat_lemma env m body larg lisset = 
+  let rec aux la li n = match (la, li) with
+    | (t::q, true::lq) -> 
+	prod_create env (t,(prod_create env (t, (aux q lq (n+2)))))
+    | (t::q, false::lq) -> 
+	prod_create env (t, (aux q lq (n+1)))
+    | ([],[]) -> gen_lemma_middle m larg lisset body n
+    | _ -> assert false
+  in aux larg lisset 0
+
+let new_morphism m id =
+  if morphism_table_mem m
+  then errorlabstrm "New Morphism"
+    [< 'sTR "The term "; prterm m; 'sTR " is already declared as a morphism">]
+  else 
+    let env = Global.env() in
+    let typeofm = (Typing.type_of env Evd.empty m) in
+    let typ = (nf_betaiota typeofm) in  (* nf_bdi avant, mais bug *)
+    let (argsrev, body) = (decompose_prod typ) in
+    let args = (List.rev argsrev) in
+      if (args=[])
+      then errorlabstrm "New Morphism"
+	[< 'sTR "The term "; prterm m; 'sTR " is not a product">]
+      else if (check_is_dependent typ (List.length args))
+      then  errorlabstrm "New Morphism"
+	[< 'sTR "The term "; prterm m; 'sTR " should not be a dependent product">]
+      else (
+	let args_t = (List.map snd args) in
+	let poss = (List.map setoid_table_mem args_t) in
+	let lem = (gen_compat_lemma env m body args_t poss) in
+	let lemast = (ast_of_constr true env lem) in
+	  new_edited id m poss;
+	  start_proof_com (Some id) Declare.NeverDischarge lemast;
+	  (Options.if_verbose Vernacentries.show_open_subgoals ()))
+
+let rec sub_bool l1 n = function
+  | [] -> []
+  | true::q -> ((List.hd l1), n)::(sub_bool (List.tl l1) (n-2) q)
+  | false::q -> (sub_bool (List.tl l1) (n-1) q)
+
+let gen_lemma_iff_tail m mext larg lisset n k =
+  let a1 = Array.create k (mkRel 0) in
+  let a2 = Array.create k (mkRel 0) in
+  let nb = List.length lisset in
+  let b1 = Array.create nb (mkRel 0) in
+  let b2 = Array.create nb (mkRel 0) in
+  let rec aux i j = function
+    |[] -> ()
+    |true::q ->
+       (a1.(i) <- (mkRel j);
+	a1.(i+1) <- (mkRel (j-1));
+	a2.(i) <- (mkRel (j-1));
+	a2.(i+1) <- (mkRel j);
+	aux (i+2) (j-2) q)
+    |false::q ->
+       (a1.(i) <- (mkRel j);
+	a2.(i) <- (mkRel j);
+	aux (i+1) (j-1) q) in
+  let rec aux2 i j = function
+    | (t,p)::q -> 
+	let th = (setoid_table_find t).set_th
+	and equiv = (setoid_table_find t).set_aeq in
+	  a1.(i) <- (mkRel j);
+	  a2.(i) <- mkApp ((Lazy.force coq_seq_sym),
+			   [|t; equiv; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]);
+	  aux2 (i+1) (j-1) q
+    | [] -> () in
+  let rec aux3 i j = function
+    | true::q -> 
+	b1.(i) <- (mkRel j);
+	b2.(i) <- (mkRel (j-1));
+	aux3 (i+1) (j-2) q
+    | false::q ->
+	b1.(i) <- (mkRel j);
+	b2.(i) <- (mkRel j);
+	aux3 (i+1) (j-1) q
+    | [] -> () in 
+    aux 0 k lisset;
+    aux2 n (k-n) (sub_bool larg k lisset);
+    aux3 0 k lisset;
+    mkApp ((Lazy.force coqconj),
+	   [|(mkArrow (mkApp (m,b1)) (lift 1 (mkApp (m, b2))));
+	     (mkArrow (mkApp (m,b2)) (lift 1 (mkApp (m, b1))));
+	     (mkApp (mext, a1));(mkApp (mext, a2))|])
+
+let gen_lemma_iff_middle env m mext larg lisset n =
+  let rec aux la li i k = match (la, li) with
+    | ([], []) -> gen_lemma_iff_tail m mext larg lisset n k
+    | (t::q, true::lq) -> 
+	lambda_create env ((mkApp ((setoid_table_find t).set_aeq, [|(mkRel i); (mkRel (i-1))|])),
+			   (aux q lq (i-1) (k+1)))
+    | (t::q, false::lq) -> aux q lq (i-1) k
+    | _ -> assert false
+  in aux larg lisset n n
+
+let gen_lem_iff env m mext larg lisset =
+  let rec aux la li n = match (la, li) with
+    | (t::q, true::lq) -> 
+	lambda_create env (t,(lambda_create env (t, (aux q lq (n+2)))))
+    | (t::q, false::lq) -> 
+	lambda_create env (t, (aux q lq (n+1)))
+    | ([],[]) -> gen_lemma_iff_middle env m mext larg lisset n
+    | _ -> assert false
+  in aux larg lisset 0
+
+let add_morphism lem_name (m,profil) =
+  if morphism_table_mem m
+  then errorlabstrm "New Morphism"
+    [< 'sTR "The term "; prterm m; 'sTR " is already declared as a morpism">]
+  else 
+    let env = Global.env() in
+    let mext = (current_constant lem_name) in
+    let typeofm = (Typing.type_of env Evd.empty m) in
+    let typ = (nf_betaiota typeofm) in
+    let (argsrev, body) = (decompose_prod typ) in
+    let args = List.rev argsrev in
+    let args_t = (List.map snd args) in
+    let poss = (List.map setoid_table_mem args_t) in
+    let _ = assert (poss=profil) in
+      (if (eq_constr body mkProp)
+       then
+	 (let lem_2 = gen_lem_iff env m mext args_t poss in
+	  let lem2_name = (id_of_string ((string_of_id lem_name)^"2")) in
+	  let _ = Declare.declare_constant lem2_name
+		    ((Declare.ConstantEntry {Declarations.const_entry_body = lem_2; 
+					     Declarations.const_entry_type = None}),
+		     Declare.NeverDischarge,true) in
+	  let lem2 = (current_constant lem2_name) in
+	    (Lib.add_anonymous_leaf
+	       (morphism_to_obj (m, 
+				 { lem = mext;
+				   profil = poss;
+				   arg_types = args_t;
+				   lem2 = (Some lem2)})));
+	    Options.if_verbose message ((string_of_id lem2_name) ^ " is defined"))
+       else
+	 (Lib.add_anonymous_leaf
+	    (morphism_to_obj (m, 
+			      { lem = mext;
+				profil = poss;
+				arg_types = args_t;
+				lem2 = None}))));
+      Options.if_verbose pPNL [< prterm m;'sTR " is registered as a morphism">]   
+    
+let _ = 
+  let current_save = vinterp_map "SaveNamed" in
+    overwriting_vinterp_add "SaveNamed"
+      (function 
+	 |[] -> (fun () -> 
+		   let pf_id = Pfedit.get_current_proof_name () in
+		     current_save [] ();
+		     if (is_edited pf_id)
+		     then 
+		       (add_morphism pf_id (what_edited pf_id);
+			no_more_edited pf_id))
+	 | _ -> assert false)
+
+let _ = 
+  let current_defined = vinterp_map "DefinedNamed" in
+    overwriting_vinterp_add "DefinedNamed"
+      (function 
+	 |[] -> (fun () -> let pf_id = Pfedit.get_current_proof_name () in
+			 current_defined [] ();
+			 if (is_edited pf_id)
+			 then 
+			   (add_morphism pf_id (what_edited pf_id);
+			   no_more_edited pf_id))
+	 | _ -> assert false)
+
+(*
+let _ = 
+  vinterp_add "NewMorphism"
+    (function 
+       | [(VARG_IDENTIFIER s)] ->
+	   (fun () -> 
+	      try 
+		(let m = Declare.global_reference CCI s in
+		   new_morphism m (gen_lem_name m))
+	      with 
+		  Not_found -> 
+		    errorlabstrm "New Morphism" 
+		      [< 'sTR "The term "; 'sTR(string_of_id s); 'sTR" is not a known name">])
+       | _ -> anomaly "NewMorphism")
+*)
+  
+let _ = 
+  vinterp_add "NamedNewMorphism"
+    (function 
+       | [(VARG_IDENTIFIER s);(VARG_CONSTR m)] ->
+	   (fun () -> new_morphism (constr_of m) s)
+       | _ -> anomaly "NewMorphism")
+
+(****************************** The tactic itself *******************************)
+
+type constr_with_marks =
+  | MApp of constr_with_marks array 
+  | Toreplace
+  | Tokeep
+  | Mimp of constr_with_marks * constr_with_marks
+
+let is_to_replace = function
+  | Tokeep -> false
+  | Toreplace -> true
+  | MApp _ -> true
+  | Mimp _ -> true
+
+let get_mark a = 
+  Array.fold_left (||) false (Array.map is_to_replace a)
+
+let rec mark_occur t in_c =
+  if (eq_constr t in_c) then Toreplace else
+    match kind_of_term in_c with
+      | IsApp (c,al) -> 
+	  let a = Array.map (mark_occur t) al
+	  in if (get_mark a) then (MApp a) else Tokeep
+      | IsProd (_, c1, c2) -> 
+	  if (dependent (mkRel 1) c2)
+	  then Tokeep
+	  else 
+	    let c1m = mark_occur t c1 in
+	    let c2m = mark_occur t c2 in
+	      if ((is_to_replace c1m)||(is_to_replace c2m))
+	      then (Mimp (c1m, c2m))
+	      else Tokeep
+      | _ -> Tokeep
+
+let create_args ca ma bl c1 c2 = 
+  let rec aux i = function
+    | [] -> []
+    | true::q -> 
+	if (is_to_replace ma.(i)) 
+	then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) q)
+	else ca.(i)::ca.(i)::(aux (i+1) q)
+    | false::q -> ca.(i)::(aux (i+1) q)
+  in
+    aux 0 bl
+
+
+let res_tac c a hyp =
+  let sa = setoid_table_find a in
+  let fin = match hyp with
+    | None -> Auto.full_trivial
+    | Some h -> 
+	tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0)) 
+	  (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0))
+	     Auto.full_trivial) in
+    tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0))
+      (tclORELSE assumption
+	 (tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption)
+	    fin))
+
+let id_res_tac c a = 
+  let sa = setoid_table_find a in
+    (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th; c|]))))
+
+(* An exception to catchs errors *)
+
+exception Nothing_found of constr;;
+
+let rec create_tac_list i a al c1 c2 hyp args_t = function
+  | [] -> []
+  | false::q -> create_tac_list (i+1) a al c1 c2 hyp args_t q
+  | true::q -> 
+      if (is_to_replace a.(i))
+      then (zapply false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
+      else (id_res_tac al.(i) (List.nth args_t i))::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
+(*      else tclIDTAC::(create_tac_list (i+1) a al c1 c2 hyp q) *)
+
+and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
+  | ((IsApp (c,al)),(MApp a)) -> (
+      try 
+	let m = morphism_table_find c in
+	let args = Array.of_list (create_args al a m.profil c1 c2) in
+	  if is_r
+	  then tclTHENS (apply (mkApp (m.lem, args)))
+	    ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])
+ 	  else (match m.lem2 with
+		  | None -> 
+		      tclTHENS (apply (mkApp (m.lem, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)
+		  | Some xom -> 
+		      tclTHENS (apply (mkApp (xom, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil))
+      with Not_found -> errorlabstrm "Setoid_replace" 
+	  [< 'sTR "The term "; prterm c; 'sTR " has not been declared as a morphism">])
+  | ((IsProd (_,hh, cc)),(Mimp (hhm, ccm))) ->
+      let al = [|hh; cc|] in
+      let a = [|hhm; ccm|] in
+      let fleche_constr = (Lazy.force coq_fleche) in
+      let fleche_cp = (match (kind_of_term fleche_constr) with
+			 | (IsConst (cp,_)) -> cp 
+			 | _ -> assert false) in
+      let new_concl = (mkApp (fleche_constr, al)) in
+	if is_r 
+	then
+	  let m = morphism_table_find fleche_constr in
+	  let args = Array.of_list (create_args al a m.profil c1 c2) in  
+	    tclTHEN (change_in_concl new_concl)
+	      (tclTHENS (apply (mkApp (m.lem, args)))
+		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
+(*		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
+	else (zapply is_r new_concl (MApp a) c1 c2 hyp)
+(*      let args = Array.of_list (create_args [|hh; cc|] [|hhm; ccm|] [true;true] c1 c2) in
+	if is_r
+	then tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext), args)))
+	  ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
+	else tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext2), args)))
+	  ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
+*)
+  | (_, Toreplace) -> (res_tac gl (pf_type_of glll gl) hyp) (* tclORELSE Auto.full_trivial tclIDTAC *)
+  | (_, Tokeep) -> (match hyp with 
+		      | None -> errorlabstrm "Setoid_replace"
+			  [< 'sTR "No replacable occurence of "; prterm c1; 'sTR " found">]
+		      | Some _ ->errorlabstrm "Setoid_replace"
+			  [< 'sTR "No rewritable occurence of "; prterm c1; 'sTR " found">])
+  | _ -> anomaly ("Bug in Setoid_replace")) glll
+
+let setoid_replace c1 c2 hyp gl =
+  let but = (pf_concl gl) in
+    (zapply true but (mark_occur c1 but) c1 c2 hyp) gl
+
+let general_s_rewrite lft2rgt c gl =
+  let ctype = pf_type_of gl c in
+  let (equiv, args) = decomp_app ctype in
+  let rec get_last_two = function
+    | [c1;c2] -> (c1, c2)
+    | x::y::z -> get_last_two (y::z)
+    | _ -> error "The term provided is not an equivalence" in 
+  let (c1,c2) = get_last_two args in
+    if lft2rgt
+    then setoid_replace c1 c2 (Some c) gl
+    else setoid_replace c2 c1 (Some c) gl
+
+let setoid_rewriteLR = general_s_rewrite true
+
+let setoid_rewriteRL = general_s_rewrite false
+
+let dyn_setoid_replace = function
+  | [(Constr c1);(Constr c2)] -> (fun gl -> setoid_replace c1 c2 None gl)
+  | _ -> invalid_arg "Setoid_replace : Bad arguments"
+      
+let h_setoid_replace = hide_tactic "Setoid_replace" dyn_setoid_replace
+
+let dyn_setoid_rewriteLR = function
+  | [(Constr c)] -> setoid_rewriteLR c
+  | _ -> invalid_arg "Setoid_rewrite : Bad arguments"
+
+let h_setoid_rewriteLR = hide_tactic "Setoid_rewriteLR" dyn_setoid_rewriteLR
+
+let dyn_setoid_rewriteRL = function
+  | [(Constr c)] -> setoid_rewriteRL c
+  | _ -> invalid_arg "Setoid_rewrite : Bad arguments"
+
+let h_setoid_rewriteRL = hide_tactic "Setoid_rewriteRL" dyn_setoid_rewriteRL
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
new file mode 100644
index 0000000000..c280bb269f
--- /dev/null
+++ b/tactics/setoid_replace.mli
@@ -0,0 +1,22 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Proof_type
+
+val equiv_list : unit -> constr list
+
+val setoid_replace : constr -> constr -> constr option -> tactic
+
+val setoid_rewriteLR : constr -> tactic
+
+val setoid_rewriteRL : constr -> tactic
+
+val general_s_rewrite : bool -> constr -> tactic