summaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/setoid_replace.ml')
-rw-r--r--tactics/setoid_replace.ml686
1 files changed, 686 insertions, 0 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
new file mode 100644
index 00000000..74b062e0
--- /dev/null
+++ b/tactics/setoid_replace.ml
@@ -0,0 +1,686 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(* $Id: setoid_replace.ml,v 1.31.2.1 2004/07/16 19:30:55 herbelin Exp $ *)
+
+open Tacmach
+open Proof_type
+open Libobject
+open Reductionops
+open Term
+open Termops
+open Names
+open Entries
+open Libnames
+open Nameops
+open Util
+open Pp
+open Printer
+open Environ
+open Tactics
+open Tacticals
+open Vernacexpr
+open Safe_typing
+open Nametab
+open Decl_kinds
+open Constrintern
+
+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 = Constrintern.interp_constr Evd.empty (Global.env()) c
+
+let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
+
+let global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s
+
+let current_constant id =
+ try
+ global_reference id
+ with Not_found ->
+ anomaly ("Setoid: cannot find "^(string_of_id id))
+
+(* Setoid_theory *)
+
+let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory")
+
+let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl")
+let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym")
+let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans")
+
+let coq_fleche = lazy(constant ["Setoid"] "fleche")
+
+(* Coq constants *)
+
+let coqeq = lazy(global_constant ["Logic"] "eq")
+
+let coqconj = lazy(global_constant ["Logic"] "conj")
+let coqand = lazy(global_constant ["Logic"] "and")
+let coqproj1 = lazy(global_constant ["Logic"] "proj1")
+let coqproj2 = lazy(global_constant ["Logic"] "proj2")
+
+(************************* 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 subst_setoid subst setoid =
+ let set_a' = subst_mps subst setoid.set_a in
+ let set_aeq' = subst_mps subst setoid.set_aeq in
+ let set_th' = subst_mps subst setoid.set_th in
+ if set_a' == setoid.set_a
+ && set_aeq' == setoid.set_aeq
+ && set_th' == setoid.set_th
+ then
+ setoid
+ else
+ { set_a = set_a' ;
+ set_aeq = set_aeq' ;
+ set_th = set_th' ;
+ }
+
+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_module = false;
+ 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 subst_set (_,subst,(s,th as obj)) =
+ let s' = subst_mps subst s in
+ let th' = subst_setoid subst th in
+ if s' == s && th' == th then obj else
+ (s',th')
+ and export_set x = Some x
+ in
+ declare_object {(default_object "setoid-theory") with
+ cache_function = cache_set;
+ open_function = (fun i o -> if i=1 then cache_set o);
+ subst_function = subst_set;
+ classify_function = (fun (_,x) -> Substitute x);
+ 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 subst_morph subst morph =
+ let lem' = subst_mps subst morph.lem in
+ let arg_types' = list_smartmap (subst_mps subst) morph.arg_types in
+ let lem2' = option_smartmap (subst_mps subst) morph.lem2 in
+ if lem' == morph.lem
+ && arg_types' == morph.arg_types
+ && lem2' == morph.lem2
+ then
+ morph
+ else
+ { lem = lem' ;
+ profil = morph.profil ;
+ arg_types = arg_types' ;
+ lem2 = lem2' ;
+ }
+
+
+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_module = false;
+ 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 subst_set (_,subst,(m,c as obj)) =
+ let m' = subst_mps subst m in
+ let c' = subst_morph subst c in
+ if m' == m && c' == c then obj else
+ (m',c')
+ and export_set x = Some x
+ in
+ declare_object {(default_object "morphism-definition") with
+ cache_function = cache_set;
+ open_function = (fun i o -> if i=1 then cache_set o);
+ subst_function = subst_set;
+ classify_function = (fun (_,x) -> Substitute x);
+ 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_common_sign env a eq =
+ let na = named_hd env a Anonymous in
+ let ne = named_hd env eq Anonymous in
+ [(ne,None,mkApp (eq, [|(mkRel 3);(mkRel 2)|]));
+ (ne,None,mkApp (eq, [|(mkRel 4);(mkRel 3)|]));
+ (na,None,a);(na,None,a);(na,None,a);(na,None,a)]
+
+(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *)
+let eq_lem_proof env a eq sym trans =
+ let sign = eq_lem_common_sign env a eq in
+ let ne = named_hd env eq Anonymous in
+ let sign = (ne,None,mkApp (eq, [|(mkRel 6);(mkRel 4)|]))::sign in
+ let ccl = mkApp (eq, [|(mkRel 6);(mkRel 4)|]) in
+ let body =
+ 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)|]))|]) in
+ let p = it_mkLambda_or_LetIn body sign in
+ let t = it_mkProd_or_LetIn ccl sign in
+ (p,t)
+
+(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *)
+let eq_lem2_proof env a eq sym trans =
+ let sign = eq_lem_common_sign env a eq in
+ let ccl1 =
+ mkArrow
+ (mkApp (eq, [|(mkRel 6);(mkRel 4)|]))
+ (mkApp (eq, [|(mkRel 6);(mkRel 4)|])) in
+ let ccl2 =
+ mkArrow
+ (mkApp (eq, [|(mkRel 5);(mkRel 3)|]))
+ (mkApp (eq, [|(mkRel 7);(mkRel 5)|])) in
+ let ccl = mkApp (Lazy.force coqand, [|ccl1;ccl2|]) in
+ let body =
+ mkApp ((Lazy.force coqconj),
+ [|ccl1;ccl2;
+ 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)|]))|]))|])))|])
+ in
+ let p = it_mkLambda_or_LetIn body sign in
+ let t = it_mkProd_or_LetIn ccl sign in
+ (p,t)
+
+let gen_eq_lem_name =
+ let i = ref 0 in
+ function () ->
+ incr i;
+ make_ident "setoid_eq_ext" (Some !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_morph_typ) = eq_lem_proof env a aeq sym trans in
+ let (eq_morph2, eq_morph2_typ) = 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
+ ((DefinitionEntry {const_entry_body = eq_morph;
+ const_entry_type = Some eq_morph_typ;
+ const_entry_opaque = true}),
+ IsProof Lemma) in
+ let _ = Declare.declare_constant eq_ext_name2
+ ((DefinitionEntry {const_entry_body = eq_morph2;
+ const_entry_type = Some eq_morph2_typ;
+ const_entry_opaque = true}),
+ IsProof Lemma) 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 add_setoid a aeq th =
+ add_setoid (constr_of a) (constr_of aeq) (constr_of th)
+
+(***************** 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
+ | Var id -> add_suffix id "_ext"
+ | Const kn -> add_suffix (id_of_label (label kn)) "_ext"
+ | Ind (kn, i) -> add_suffix (id_of_label (label kn)) ((string_of_int i)^"_ext")
+ | Construct ((kn,i),j) -> add_suffix
+ (id_of_label (label kn)) ((string_of_int i)^(string_of_int j)^"_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 hook =
+ 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
+ new_edited id m poss;
+ Pfedit.start_proof id (IsGlobal (Proof Lemma))
+ (Declare.clear_proofs (Global.named_context ()))
+ lem hook;
+ (Options.if_verbose msg (Pfedit.pr_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 = add_suffix lem_name "2" in
+ let _ = Declare.declare_constant lem2_name
+ ((DefinitionEntry {const_entry_body = lem_2;
+ const_entry_type = None;
+ const_entry_opaque = true}),
+ IsProof Lemma) 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 morphism_hook stre ref =
+ let pf_id = id_of_global ref in
+ if (is_edited pf_id)
+ then
+ (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id)
+
+let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook
+
+(****************************** 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
+ | App (c,al) ->
+ let a = Array.map (mark_occur t) al
+ in if (get_mark a) then (MApp a) else Tokeep
+ | Prod (_, 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
+ | ((App (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"))
+ | ((Prod (_,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 = destConst fleche_constr 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 None 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) ->
+ if is_r
+ then (match hyp with
+ | None -> errorlabstrm "Setoid_replace"
+ (str "You should use the tactic Replace here")
+ | Some h ->
+ let hypt = pf_type_of glll h in
+ let (heq, hargs) = decompose_app hypt in
+ let rec get_last_two = function
+ | [c1;c2] -> (c1, c2)
+ | x::y::z -> get_last_two (y::z)
+ | _ -> assert false in
+ let (hc1,hc2) = get_last_two hargs in
+ if c1 = hc1
+ then
+ apply (mkApp (Lazy.force coqproj2,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
+ else
+ apply (mkApp (Lazy.force coqproj1,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
+ )
+ else (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) = decompose_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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 01:51:49 +0000