diff options
Diffstat (limited to 'tactics/setoid_replace.ml')
-rw-r--r-- | tactics/setoid_replace.ml | 2023 |
1 files changed, 0 insertions, 2023 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml deleted file mode 100644 index 95d56f11..00000000 --- a/tactics/setoid_replace.ml +++ /dev/null @@ -1,2023 +0,0 @@ -(************************************************************************) -(* 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 11094 2008-06-10 19:35:23Z herbelin $ *) - -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 Clenv -open Unification -open Tactics -open Tacticals -open Vernacexpr -open Safe_typing -open Nametab -open Decl_kinds -open Constrintern -open Mod_subst - -let replace = ref (fun _ _ _ -> assert false) -let register_replace f = replace := f - -let general_rewrite = ref (fun _ _ -> assert false) -let register_general_rewrite f = general_rewrite := f - -(* util function; it should be in util.mli *) -let prlist_with_sepi sep elem = - let rec aux n = - function - | [] -> mt () - | [h] -> elem n h - | h::t -> - let e = elem n h and s = sep() and r = aux (n+1) t in - e ++ s ++ r - in - aux 1 - -type relation = - { rel_a: constr ; - rel_aeq: constr; - rel_refl: constr option; - rel_sym: constr option; - rel_trans : constr option; - rel_quantifiers_no: int (* it helps unification *); - rel_X_relation_class: constr; - rel_Xreflexive_relation_class: constr - } - -type 'a relation_class = - Relation of 'a (* the rel_aeq of the relation or the relation *) - | Leibniz of constr option (* the carrier (if eq is partially instantiated) *) - -type 'a morphism = - { args : (bool option * 'a relation_class) list; - output : 'a relation_class; - lem : constr; - morphism_theory : constr - } - -type funct = - { f_args : constr list; - f_output : constr - } - -type morphism_class = - ACMorphism of relation morphism - | ACFunction of funct - -let subst_mps_in_relation_class subst = - function - Relation t -> Relation (subst_mps subst t) - | Leibniz t -> Leibniz (Option.map (subst_mps subst) t) - -let subst_mps_in_argument_class subst (variance,rel) = - variance, subst_mps_in_relation_class subst rel - -let constr_relation_class_of_relation_relation_class = - function - Relation relation -> Relation relation.rel_aeq - | Leibniz t -> Leibniz t - - -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 gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s -let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s -let eval_reference dir s = EvalConstRef (destConst (constant dir s)) -let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s)) - -let current_constant id = - try - global_reference id - with Not_found -> - anomalylabstrm "" - (str "Setoid: cannot find " ++ pr_id id ++ - str "(if loading Setoid.v under coqtop, use option \"-top Coq.Setoids.Setoid_tac\")") - -(* From Setoid.v *) - -let coq_reflexive = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "reflexive") -let coq_symmetric = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "symmetric") -let coq_transitive = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "transitive") -let coq_relation = - lazy(gen_constant ["Relations"; "Relation_Definitions"] "relation") - -let coq_Relation_Class = lazy(constant ["Setoid_tac"] "Relation_Class") -let coq_Argument_Class = lazy(constant ["Setoid_tac"] "Argument_Class") -let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory") -let coq_Morphism_Theory = lazy(constant ["Setoid_tac"] "Morphism_Theory") -let coq_Build_Morphism_Theory= lazy(constant ["Setoid_tac"] "Build_Morphism_Theory") -let coq_Compat = lazy(constant ["Setoid_tac"] "Compat") - -let coq_AsymmetricReflexive = lazy(constant ["Setoid_tac"] "AsymmetricReflexive") -let coq_SymmetricReflexive = lazy(constant ["Setoid_tac"] "SymmetricReflexive") -let coq_SymmetricAreflexive = lazy(constant ["Setoid_tac"] "SymmetricAreflexive") -let coq_AsymmetricAreflexive = lazy(constant ["Setoid_tac"] "AsymmetricAreflexive") -let coq_Leibniz = lazy(constant ["Setoid_tac"] "Leibniz") - -let coq_RAsymmetric = lazy(constant ["Setoid_tac"] "RAsymmetric") -let coq_RSymmetric = lazy(constant ["Setoid_tac"] "RSymmetric") -let coq_RLeibniz = lazy(constant ["Setoid_tac"] "RLeibniz") - -let coq_ASymmetric = lazy(constant ["Setoid_tac"] "ASymmetric") -let coq_AAsymmetric = lazy(constant ["Setoid_tac"] "AAsymmetric") - -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_variance = lazy(constant ["Setoid_tac"] "variance") -let coq_Covariant = lazy(constant ["Setoid_tac"] "Covariant") -let coq_Contravariant = lazy(constant ["Setoid_tac"] "Contravariant") -let coq_Left2Right = lazy(constant ["Setoid_tac"] "Left2Right") -let coq_Right2Left = lazy(constant ["Setoid_tac"] "Right2Left") -let coq_MSNone = lazy(constant ["Setoid_tac"] "MSNone") -let coq_MSCovariant = lazy(constant ["Setoid_tac"] "MSCovariant") -let coq_MSContravariant = lazy(constant ["Setoid_tac"] "MSContravariant") - -let coq_singl = lazy(constant ["Setoid_tac"] "singl") -let coq_cons = lazy(constant ["Setoid_tac"] "necons") - -let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_asymmetric_areflexive_transitive_relation") -let coq_equality_morphism_of_symmetric_areflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_symmetric_areflexive_transitive_relation") -let coq_equality_morphism_of_asymmetric_reflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_asymmetric_reflexive_transitive_relation") -let coq_equality_morphism_of_symmetric_reflexive_transitive_relation = - lazy(constant ["Setoid_tac"] - "equality_morphism_of_symmetric_reflexive_transitive_relation") -let coq_make_compatibility_goal = - lazy(constant ["Setoid_tac"] "make_compatibility_goal") -let coq_make_compatibility_goal_eval_ref = - lazy(eval_reference ["Setoid_tac"] "make_compatibility_goal") -let coq_make_compatibility_goal_aux_eval_ref = - lazy(eval_reference ["Setoid_tac"] "make_compatibility_goal_aux") - -let coq_App = lazy(constant ["Setoid_tac"] "App") -let coq_ToReplace = lazy(constant ["Setoid_tac"] "ToReplace") -let coq_ToKeep = lazy(constant ["Setoid_tac"] "ToKeep") -let coq_ProperElementToKeep = lazy(constant ["Setoid_tac"] "ProperElementToKeep") -let coq_fcl_singl = lazy(constant ["Setoid_tac"] "fcl_singl") -let coq_fcl_cons = lazy(constant ["Setoid_tac"] "fcl_cons") - -let coq_setoid_rewrite = lazy(constant ["Setoid_tac"] "setoid_rewrite") -let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") -let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") -let coq_unit = lazy(gen_constant ["Init"; "Datatypes"] "unit") -let coq_tt = lazy(gen_constant ["Init"; "Datatypes"] "tt") -let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq") - -let coq_morphism_theory_of_function = - lazy(constant ["Setoid_tac"] "morphism_theory_of_function") -let coq_morphism_theory_of_predicate = - lazy(constant ["Setoid_tac"] "morphism_theory_of_predicate") -let coq_relation_of_relation_class = - lazy(eval_reference ["Setoid_tac"] "relation_of_relation_class") -let coq_directed_relation_of_relation_class = - lazy(eval_reference ["Setoid_tac"] "directed_relation_of_relation_class") -let coq_interp = lazy(eval_reference ["Setoid_tac"] "interp") -let coq_Morphism_Context_rect2 = - lazy(eval_reference ["Setoid_tac"] "Morphism_Context_rect2") -let coq_iff = lazy(gen_constant ["Init";"Logic"] "iff") -let coq_impl = lazy(constant ["Setoid_tac"] "impl") - - -(************************* Table of declared relations **********************) - - -(* Relations are stored in a table which is synchronised with the - Reset mechanism. The table maps the term denoting the relation to - the data of type relation that characterises the relation *) - -let relation_table = ref Gmap.empty - -let relation_table_add (s,th) = relation_table := Gmap.add s th !relation_table -let relation_table_find s = Gmap.find s !relation_table -let relation_table_mem s = Gmap.mem s !relation_table - -let prrelation s = - str "(" ++ pr_lconstr s.rel_a ++ str "," ++ pr_lconstr s.rel_aeq ++ str ")" - -let prrelation_class = - function - Relation eq -> - (try prrelation (relation_table_find eq) - with Not_found -> - str "[[ Error: " ++ pr_lconstr eq ++ - str " is not registered as a relation ]]") - | Leibniz (Some ty) -> pr_lconstr ty - | Leibniz None -> str "_" - -let prmorphism_argument_gen prrelation (variance,rel) = - prrelation rel ++ - match variance with - None -> str " ==> " - | Some true -> str " ++> " - | Some false -> str " --> " - -let prargument_class = prmorphism_argument_gen prrelation_class - -let pr_morphism_signature (l,c) = - prlist (prmorphism_argument_gen Ppconstr.pr_constr_expr) l ++ - Ppconstr.pr_constr_expr c - -let prmorphism k m = - pr_lconstr k ++ str ": " ++ - prlist prargument_class m.args ++ - prrelation_class m.output - - -(* A function that gives back the only relation_class on a given carrier *) -(*CSC: this implementation is really inefficient. I should define a new - map to make it efficient. However, is this really worth of? *) -let default_relation_for_carrier ?(filter=fun _ -> true) a = - let rng = Gmap.rng !relation_table in - match List.filter (fun ({rel_a=rel_a} as r) -> rel_a = a && filter r) rng with - [] -> Leibniz (Some a) - | relation::tl -> - if tl <> [] then - Flags.if_warn msg_warning - (str "There are several relations on the carrier \"" ++ - pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++ - str " is chosen.") ; - Relation relation - -let find_relation_class rel = - try Relation (relation_table_find rel) - with - Not_found -> - let rel = Reduction.whd_betadeltaiota (Global.env ()) rel in - match kind_of_term rel with - | App (eq,[|ty|]) when eq_constr eq (Lazy.force coq_eq) -> Leibniz (Some ty) - | _ when eq_constr rel (Lazy.force coq_eq) -> Leibniz None - | _ -> raise Not_found - -let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff)) -let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl)) - -let relation_morphism_of_constr_morphism = - let relation_relation_class_of_constr_relation_class = - function - Leibniz t -> Leibniz t - | Relation aeq -> - Relation (try relation_table_find aeq with Not_found -> assert false) - in - function mor -> - let args' = - List.map - (fun (variance,rel) -> - variance, relation_relation_class_of_constr_relation_class rel - ) mor.args in - let output' = relation_relation_class_of_constr_relation_class mor.output in - {mor with args=args' ; output=output'} - -let subst_relation subst relation = - let rel_a' = subst_mps subst relation.rel_a in - let rel_aeq' = subst_mps subst relation.rel_aeq in - let rel_refl' = Option.map (subst_mps subst) relation.rel_refl in - let rel_sym' = Option.map (subst_mps subst) relation.rel_sym in - let rel_trans' = Option.map (subst_mps subst) relation.rel_trans in - let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in - let rel_Xreflexive_relation_class' = - subst_mps subst relation.rel_Xreflexive_relation_class - in - if rel_a' == relation.rel_a - && rel_aeq' == relation.rel_aeq - && rel_refl' == relation.rel_refl - && rel_sym' == relation.rel_sym - && rel_trans' == relation.rel_trans - && rel_X_relation_class' == relation.rel_X_relation_class - && rel_Xreflexive_relation_class'==relation.rel_Xreflexive_relation_class - then - relation - else - { rel_a = rel_a' ; - rel_aeq = rel_aeq' ; - rel_refl = rel_refl' ; - rel_sym = rel_sym'; - rel_trans = rel_trans'; - rel_quantifiers_no = relation.rel_quantifiers_no; - rel_X_relation_class = rel_X_relation_class'; - rel_Xreflexive_relation_class = rel_Xreflexive_relation_class' - } - -let equiv_list () = List.map (fun x -> x.rel_aeq) (Gmap.rng !relation_table) - -let _ = - Summary.declare_summary "relation-table" - { Summary.freeze_function = (fun () -> !relation_table); - Summary.unfreeze_function = (fun t -> relation_table := t); - Summary.init_function = (fun () -> relation_table := Gmap .empty); - Summary.survive_module = false; - Summary.survive_section = false } - -(* Declare a new type of object in the environment : "relation-theory". *) - -let (relation_to_obj, obj_to_relation)= - let cache_set (_,(s, th)) = - let th' = - if relation_table_mem s then - begin - let old_relation = relation_table_find s in - let th' = - {th with rel_sym = - match th.rel_sym with - None -> old_relation.rel_sym - | Some t -> Some t} in - Flags.if_warn msg_warning - (strbrk "The relation " ++ prrelation th' ++ - strbrk " is redeclared. The new declaration" ++ - (match th'.rel_refl with - None -> mt () - | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ - (match th'.rel_sym with - None -> mt () - | Some t -> - (if th'.rel_refl = None then strbrk " (" else strbrk " and ") - ++ strbrk "symmetry proved by " ++ pr_lconstr t) ++ - (if th'.rel_refl <> None && th'.rel_sym <> None then - str ")" else str "") ++ - strbrk " replaces the old declaration" ++ - (match old_relation.rel_refl with - None -> str "" - | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ - (match old_relation.rel_sym with - None -> str "" - | Some t -> - (if old_relation.rel_refl = None then - strbrk " (" else strbrk " and ") ++ - strbrk "symmetry proved by " ++ pr_lconstr t) ++ - (if old_relation.rel_refl <> None && old_relation.rel_sym <> None - then str ")" else str "") ++ - str "."); - th' - end - else - th - in - relation_table_add (s,th') - and subst_set (_,subst,(s,th as obj)) = - let s' = subst_mps subst s in - let th' = subst_relation subst th in - if s' == s && th' == th then obj else - (s',th') - and export_set x = Some x - in - declare_object {(default_object "relation-theory") with - cache_function = cache_set; - load_function = (fun i o -> 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_find m = Gmap.find m !morphism_table -let morphism_table_add (m,c) = - let old = - try - morphism_table_find m - with - Not_found -> [] - in - try - let old_morph = - List.find - (function mor -> mor.args = c.args && mor.output = c.output) old - in - Flags.if_warn msg_warning - (strbrk "The morphism " ++ prmorphism m old_morph ++ - strbrk " is redeclared. " ++ - strbrk "The new declaration whose compatibility is proved by " ++ - pr_lconstr c.lem ++ strbrk " replaces the old declaration whose" ++ - strbrk " compatibility was proved by " ++ - pr_lconstr old_morph.lem ++ str ".") - with - Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table - -let default_morphism ?(filter=fun _ -> true) m = - match List.filter filter (morphism_table_find m) with - [] -> raise Not_found - | m1::ml -> - if ml <> [] then - Flags.if_warn msg_warning - (strbrk "There are several morphisms associated to \"" ++ - pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ - strbrk " is randomly chosen."); - relation_morphism_of_constr_morphism m1 - -let subst_morph subst morph = - let lem' = subst_mps subst morph.lem in - let args' = list_smartmap (subst_mps_in_argument_class subst) morph.args in - let output' = subst_mps_in_relation_class subst morph.output in - let morphism_theory' = subst_mps subst morph.morphism_theory in - if lem' == morph.lem - && args' == morph.args - && output' == morph.output - && morphism_theory' == morph.morphism_theory - then - morph - else - { args = args' ; - output = output' ; - lem = lem' ; - morphism_theory = morphism_theory' - } - - -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; - load_function = (fun i o -> cache_set o); - subst_function = subst_set; - classify_function = (fun (_,x) -> Substitute x); - export_function = export_set} - -(************************** Printing relations and morphisms **********************) - -let print_setoids () = - Gmap.iter - (fun k relation -> - assert (k=relation.rel_aeq) ; - ppnl (str"Relation " ++ prrelation relation ++ str";" ++ - (match relation.rel_refl with - None -> str "" - | Some t -> str" reflexivity proved by " ++ pr_lconstr t) ++ - (match relation.rel_sym with - None -> str "" - | Some t -> str " symmetry proved by " ++ pr_lconstr t) ++ - (match relation.rel_trans with - None -> str "" - | Some t -> str " transitivity proved by " ++ pr_lconstr t))) - !relation_table ; - Gmap.iter - (fun k l -> - List.iter - (fun ({lem=lem} as mor) -> - ppnl (str "Morphism " ++ prmorphism k mor ++ - str ". Compatibility proved by " ++ - pr_lconstr lem ++ str ".")) - l) !morphism_table -;; - -(***************** 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 = - edited := Gmap.add id m !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 - -(* also returns the triple (args_ty_quantifiers_rev,real_args_ty,real_output) - where the args_ty and the output are delifted *) -let check_is_dependent n args_ty output = - let m = List.length args_ty - n in - let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in - let rec aux m t = - match kind_of_term t with - Prod (n,s,t) when m > 0 -> - if not (dependent (mkRel 1) t) then - let args,out = aux (m - 1) (subst1 (mkRel 1) (* dummy *) t) in - s::args,out - else - errorlabstrm "New Morphism" - (str "The morphism is not a quantified non dependent product.") - | _ -> [],t - in - let ty = compose_prod (List.rev args_ty) output in - let args_ty, output = aux m ty in - List.rev args_ty_quantifiers, args_ty, output - -let cic_relation_class_of_X_relation typ value = - function - {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} -> - mkApp ((Lazy.force coq_AsymmetricReflexive), - [| typ ; value ; rel_a ; rel_aeq; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_SymmetricReflexive), - [| typ ; rel_a ; rel_aeq; sym ; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} -> - mkApp ((Lazy.force coq_AsymmetricAreflexive), - [| typ ; value ; rel_a ; rel_aeq |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_SymmetricAreflexive), - [| typ ; rel_a ; rel_aeq; sym |]) - -let cic_relation_class_of_X_relation_class typ value = - function - Relation {rel_X_relation_class=x_relation_class} -> - mkApp (x_relation_class, [| typ ; value |]) - | Leibniz (Some t) -> - mkApp ((Lazy.force coq_Leibniz), [| typ ; t |]) - | Leibniz None -> assert false - - -let cic_precise_relation_class_of_relation = - function - {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} -> - mkApp ((Lazy.force coq_RAsymmetric), [| rel_a ; rel_aeq; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_RSymmetric), [| rel_a ; rel_aeq; sym ; refl |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} -> - mkApp ((Lazy.force coq_AAsymmetric), [| rel_a ; rel_aeq |]) - | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} -> - mkApp ((Lazy.force coq_ASymmetric), [| rel_a ; rel_aeq; sym |]) - -let cic_precise_relation_class_of_relation_class = - function - Relation - {rel_aeq=rel_aeq; rel_Xreflexive_relation_class=lem; rel_refl=rel_refl } - -> - rel_aeq,lem,not(rel_refl=None) - | Leibniz (Some t) -> - mkApp ((Lazy.force coq_eq), [| t |]), - mkApp ((Lazy.force coq_RLeibniz), [| t |]), true - | Leibniz None -> assert false - -let cic_relation_class_of_relation_class rel = - cic_relation_class_of_X_relation_class - (Lazy.force coq_unit) (Lazy.force coq_tt) rel - -let cic_argument_class_of_argument_class (variance,arg) = - let coq_variant_value = - match variance with - None -> (Lazy.force coq_Covariant) (* dummy value, it won't be used *) - | Some true -> (Lazy.force coq_Covariant) - | Some false -> (Lazy.force coq_Contravariant) - in - cic_relation_class_of_X_relation_class (Lazy.force coq_variance) - coq_variant_value arg - -let cic_arguments_of_argument_class_list args = - let rec aux = - function - [] -> assert false - | [last] -> - mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class; last |]) - | he::tl -> - mkApp ((Lazy.force coq_cons), - [| Lazy.force coq_Argument_Class; he ; aux tl |]) - in - aux (List.map cic_argument_class_of_argument_class args) - -let gen_compat_lemma_statement quantifiers_rev output args m = - let output = cic_relation_class_of_relation_class output in - let args = cic_arguments_of_argument_class_list args in - args, output, - compose_prod quantifiers_rev - (mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m |])) - -let morphism_theory_id_of_morphism_proof_id id = - id_of_string (string_of_id id ^ "_morphism_theory") - -(* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *) -let apply_to_rels c l = - if l = [] then c - else - let len = List.length l in - applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l) - -let apply_to_relation subst rel = - if Array.length subst = 0 then rel - else - let new_quantifiers_no = rel.rel_quantifiers_no - Array.length subst in - assert (new_quantifiers_no >= 0) ; - { rel_a = mkApp (rel.rel_a, subst) ; - rel_aeq = mkApp (rel.rel_aeq, subst) ; - rel_refl = Option.map (fun c -> mkApp (c,subst)) rel.rel_refl ; - rel_sym = Option.map (fun c -> mkApp (c,subst)) rel.rel_sym; - rel_trans = Option.map (fun c -> mkApp (c,subst)) rel.rel_trans; - rel_quantifiers_no = new_quantifiers_no; - rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst); - rel_Xreflexive_relation_class = - mkApp (rel.rel_Xreflexive_relation_class, subst) } - -let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = - let lem = - match lemma_infos with - None -> - (* the Morphism_Theory object has already been created *) - let applied_args = - let len = List.length quantifiers_rev in - let subst = - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 quantifiers_rev) - in - List.map - (fun (v,rel) -> - match rel with - Leibniz (Some t) -> - assert (subst=[||]); - v, Leibniz (Some t) - | Leibniz None -> - assert (Array.length subst = 1); - v, Leibniz (Some (subst.(0))) - | Relation rel -> v, Relation (apply_to_relation subst rel)) args - in - compose_lam quantifiers_rev - (mkApp (Lazy.force coq_Compat, - [| cic_arguments_of_argument_class_list applied_args; - cic_relation_class_of_relation_class output; - apply_to_rels (current_constant mor_name) quantifiers_rev |])) - | Some (lem_name,argsconstr,outputconstr) -> - (* only the compatibility has been proved; we need to declare the - Morphism_Theory object *) - let mext = current_constant lem_name in - ignore ( - Declare.declare_internal_constant mor_name - (DefinitionEntry - {const_entry_body = - compose_lam quantifiers_rev - (mkApp ((Lazy.force coq_Build_Morphism_Theory), - [| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ; - apply_to_rels mext quantifiers_rev |])); - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition)) ; - mext - in - let mmor = current_constant mor_name in - let args_constr = - List.map - (fun (variance,arg) -> - variance, constr_relation_class_of_relation_relation_class arg) args in - let output_constr = constr_relation_class_of_relation_relation_class output in - Lib.add_anonymous_leaf - (morphism_to_obj (m, - { args = args_constr; - output = output_constr; - lem = lem; - morphism_theory = mmor })); - Flags.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism") - -let error_cannot_unify_signature env k t t' = - errorlabstrm "New Morphism" - (str "One morphism argument or its output has type" ++ spc() ++ - pr_lconstr_env env t ++ strbrk " but the signature requires an argument" ++ - (if k = 0 then strbrk " of type " else - strbrk "whose type is an instance of ") ++ pr_lconstr_env env t' ++ - str ".") - -(* first order matching with a bit of conversion *) -let unify_relation_carrier_with_type env rel t = - let args = - match kind_of_term t with - App (he',args') -> - let argsno = Array.length args' - rel.rel_quantifiers_no in - let args1 = Array.sub args' 0 argsno in - let args2 = Array.sub args' argsno rel.rel_quantifiers_no in - if is_conv env Evd.empty rel.rel_a (mkApp (he',args1)) then - args2 - else - error_cannot_unify_signature env rel.rel_quantifiers_no t rel.rel_a - | _ -> - try - let args = - Clenv.clenv_conv_leq env Evd.empty t rel.rel_a rel.rel_quantifiers_no - in - Array.of_list args - with Reduction.NotConvertible -> - error_cannot_unify_signature env rel.rel_quantifiers_no t rel.rel_a - in - apply_to_relation args rel - -let unify_relation_class_carrier_with_type env rel t = - match rel with - Leibniz (Some t') -> - if is_conv env Evd.empty t t' then - rel - else - error_cannot_unify_signature env 0 t t' - | Leibniz None -> Leibniz (Some t) - | Relation rel -> Relation (unify_relation_carrier_with_type env rel t) - -exception Impossible - -(* first order matching with a bit of conversion *) -(* Note: the type checking operations performed by the function could *) -(* be done once and for all abstracting the morphism structure using *) -(* the quantifiers. Would the new structure be more suited than the *) -(* existent one for other tasks to? (e.g. pretty printing would expose *) -(* much more information: is it ok or is it too much information?) *) -let unify_morphism_with_arguments gl (c,av) - {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t -= - let avlen = Array.length av in - let argsno = List.length args in - if avlen < argsno then raise Impossible; (* partial application *) - let al = Array.to_list av in - let quantifiers,al' = Util.list_chop (avlen - argsno) al in - let quantifiersv = Array.of_list quantifiers in - let c' = mkApp (c,quantifiersv) in - if dependent t c' then raise Impossible; - (* these are pf_type_of we could avoid *) - let al'_type = List.map (Tacmach.pf_type_of gl) al' in - let args' = - List.map2 - (fun (var,rel) ty -> - var,unify_relation_class_carrier_with_type (pf_env gl) rel ty) - args al'_type in - (* this is another pf_type_of we could avoid *) - let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in - let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in - let lem' = mkApp (lem,quantifiersv) in - let morphism_theory' = mkApp (morphism_theory,quantifiersv) in - ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'}, - c',Array.of_list al') - -let new_morphism m signature id hook = - if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then - errorlabstrm "New Morphism" (pr_id id ++ str " already exists") - else - let env = Global.env() in - let typeofm = Typing.type_of env Evd.empty m in - let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in - let argsrev, output = - match signature with - None -> decompose_prod typ - | Some (_,output') -> - (* the carrier of the relation output' can be a Prod ==> - we must uncurry on the fly output. - E.g: A -> B -> C vs A -> (B -> C) - args output args output - *) - let rel = - try find_relation_class output' - with Not_found -> errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ pr_lconstr output' ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") in - let rel_a,rel_quantifiers_no = - match rel with - Relation rel -> rel.rel_a, rel.rel_quantifiers_no - | Leibniz (Some t) -> t, 0 - | Leibniz None -> let _,t = decompose_prod typ in t, 0 in - let rel_a_n = - clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a - in - try - let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in - let argsrev,_ = decompose_prod output_rel_a_n in - let n = List.length argsrev in - let argsrev',_ = decompose_prod typ in - let m = List.length argsrev' in - decompose_prod_n (m - n) typ - with UserError(_,_) -> - (* decompose_lam_n failed. This may happen when rel_a is an axiom, - a constructor, an inductive type, etc. *) - decompose_prod typ - in - let args_ty = List.rev argsrev in - let args_ty_len = List.length (args_ty) in - let args_ty_quantifiers_rev,args,args_instance,output,output_instance = - match signature with - None -> - if args_ty = [] then - errorlabstrm "New Morphism" - (str "The term " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that is not a product.") ; - ignore (check_is_dependent 0 args_ty output) ; - let args = - List.map - (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in - let output = default_relation_for_carrier output in - [],args,args,output,output - | Some (args,output') -> - assert (args <> []); - let number_of_arguments = List.length args in - let number_of_quantifiers = args_ty_len - number_of_arguments in - if number_of_quantifiers < 0 then - errorlabstrm "New Morphism" - (str "The morphism " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that expects at most " ++ int args_ty_len ++ - str " arguments. The signature that you specified requires " ++ - int number_of_arguments ++ str " arguments.") - else - begin - (* the real_args_ty returned are already delifted *) - let args_ty_quantifiers_rev, real_args_ty, real_output = - check_is_dependent number_of_quantifiers args_ty output in - let quantifiers_rel_context = - List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in - let env = push_rel_context quantifiers_rel_context env in - let find_relation_class t real_t = - try - let rel = find_relation_class t in - rel, unify_relation_class_carrier_with_type env rel real_t - with Not_found -> - errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ pr_lconstr t ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") - in - let find_relation_class_v (variance,t) real_t = - let relation,relation_instance = find_relation_class t real_t in - match relation, variance with - Leibniz _, None - | Relation {rel_sym = Some _}, None - | Relation {rel_sym = None}, Some _ -> - (variance, relation), (variance, relation_instance) - | Relation {rel_sym = None},None -> - errorlabstrm "Add Morphism" - (str "You must specify the variance in each argument " ++ - str "whose relation is asymmetric.") - | Leibniz _, Some _ - | Relation {rel_sym = Some _}, Some _ -> - errorlabstrm "Add Morphism" - (str "You cannot specify the variance of an argument " ++ - str "whose relation is symmetric.") - in - let args, args_instance = - List.split - (List.map2 find_relation_class_v args real_args_ty) in - let output,output_instance= find_relation_class output' real_output in - args_ty_quantifiers_rev, args, args_instance, output, output_instance - end - in - let argsconstr,outputconstr,lem = - gen_compat_lemma_statement args_ty_quantifiers_rev output_instance - args_instance (apply_to_rels m args_ty_quantifiers_rev) in - (* "unfold make_compatibility_goal" *) - let lem = - Reductionops.clos_norm_flags - (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref)) - env Evd.empty lem in - (* "unfold make_compatibility_goal_aux" *) - let lem = - Reductionops.clos_norm_flags - (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref)) - env Evd.empty lem in - (* "simpl" *) - let lem = Tacred.simpl env Evd.empty lem in - if Lib.is_modtype () then - begin - ignore - (Declare.declare_internal_constant id - (ParameterEntry (lem,false), IsAssumption Logical)) ; - let mor_name = morphism_theory_id_of_morphism_proof_id id in - let lemma_infos = Some (id,argsconstr,outputconstr) in - add_morphism lemma_infos mor_name - (m,args_ty_quantifiers_rev,args,output) - end - else - begin - new_edited id - (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); - Pfedit.start_proof id (Global, Proof Lemma) - (Decls.clear_proofs (Global.named_context ())) - lem hook; - Flags.if_verbose msg (Printer.pr_open_subgoals ()); - end - -let morphism_hook _ ref = - let pf_id = id_of_global ref in - let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in - let (m,quantifiers_rev,args,argsconstr,output,outputconstr) = - what_edited pf_id in - if (is_edited pf_id) - then - begin - add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id - (m,quantifiers_rev,args,output) ; - no_more_edited pf_id - end - -type morphism_signature = - (bool option * Topconstr.constr_expr) list * Topconstr.constr_expr - -let new_named_morphism id m sign = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - let sign = - match sign with - None -> None - | Some (args,out) -> - if args = [] then - error "Morphism signature expects at least one argument."; - Some - (List.map (fun (variance,ty) -> variance, constr_of ty) args, - constr_of out) - in - new_morphism (constr_of m) sign id morphism_hook - -(************************** Adding a relation to the database *********************) - -let check_a env a = - let typ = Typing.type_of env Evd.empty a in - let a_quantifiers_rev,_ = Reduction.dest_arity env typ in - a_quantifiers_rev - -let check_eq env a_quantifiers_rev a aeq = - let typ = - Sign.it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_relation),[| apply_to_rels a a_quantifiers_rev |])) - a_quantifiers_rev in - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ) - then - errorlabstrm "Add Relation Class" - (pr_lconstr aeq ++ str " should have type (" ++ pr_lconstr typ ++ str ")") - -let check_property env a_quantifiers_rev a aeq strprop coq_prop t = - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty t) - (Sign.it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_prop), - [| apply_to_rels a a_quantifiers_rev ; - apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) - then - errorlabstrm "Add Relation Class" - (str "Not a valid proof of " ++ str strprop ++ str ".") - -let check_refl env a_quantifiers_rev a aeq refl = - check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl - -let check_sym env a_quantifiers_rev a aeq sym = - check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetric sym - -let check_trans env a_quantifiers_rev a aeq trans = - check_property env a_quantifiers_rev a aeq "transitivity" coq_transitive trans - -let check_setoid_theory env a_quantifiers_rev a aeq th = - if - not - (is_conv env Evd.empty (Typing.type_of env Evd.empty th) - (Sign.it_mkProd_or_LetIn - (mkApp ((Lazy.force coq_Setoid_Theory), - [| apply_to_rels a a_quantifiers_rev ; - apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev)) - then - errorlabstrm "Add Relation Class" - (str "Not a valid proof of symmetry") - -let int_add_relation id a aeq refl sym trans = - let env = Global.env () in - let a_quantifiers_rev = check_a env a in - check_eq env a_quantifiers_rev a aeq ; - Option.iter (check_refl env a_quantifiers_rev a aeq) refl ; - Option.iter (check_sym env a_quantifiers_rev a aeq) sym ; - Option.iter (check_trans env a_quantifiers_rev a aeq) trans ; - let quantifiers_no = List.length a_quantifiers_rev in - let aeq_rel = - { rel_a = a; - rel_aeq = aeq; - rel_refl = refl; - rel_sym = sym; - rel_trans = trans; - rel_quantifiers_no = quantifiers_no; - rel_X_relation_class = mkProp; (* dummy value, overwritten below *) - rel_Xreflexive_relation_class = mkProp (* dummy value, overwritten below *) - } in - let x_relation_class = - let subst = - let len = List.length a_quantifiers_rev in - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i + 2)) 0 a_quantifiers_rev) in - cic_relation_class_of_X_relation - (mkRel 2) (mkRel 1) (apply_to_relation subst aeq_rel) in - let _ = - Declare.declare_internal_constant id - (DefinitionEntry - {const_entry_body = - Sign.it_mkLambda_or_LetIn x_relation_class - ([ Name (id_of_string "v"),None,mkRel 1; - Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @ - a_quantifiers_rev); - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition) in - let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in - let xreflexive_relation_class = - let subst = - let len = List.length a_quantifiers_rev in - Array.of_list - (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 a_quantifiers_rev) - in - cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in - let _ = - Declare.declare_internal_constant id_precise - (DefinitionEntry - {const_entry_body = - Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, - IsDefinition Definition) in - let aeq_rel = - { aeq_rel with - rel_X_relation_class = current_constant id; - rel_Xreflexive_relation_class = current_constant id_precise } in - Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; - Flags.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation"); - match trans with - None -> () - | Some trans -> - let mor_name = id_of_string (string_of_id id ^ "_morphism") in - let a_instance = apply_to_rels a a_quantifiers_rev in - let aeq_instance = apply_to_rels aeq a_quantifiers_rev in - let sym_instance = - Option.map (fun x -> apply_to_rels x a_quantifiers_rev) sym in - let refl_instance = - Option.map (fun x -> apply_to_rels x a_quantifiers_rev) refl in - let trans_instance = apply_to_rels trans a_quantifiers_rev in - let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output = - match sym_instance, refl_instance with - None, None -> - (Some false, Relation aeq_rel), - (Some true, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_asymmetric_areflexive_transitive_relation), - [| a_instance ; aeq_instance ; trans_instance |]), - Lazy.force coq_impl_relation - | None, Some refl_instance -> - (Some false, Relation aeq_rel), - (Some true, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_asymmetric_reflexive_transitive_relation), - [| a_instance ; aeq_instance ; refl_instance ; trans_instance |]), - Lazy.force coq_impl_relation - | Some sym_instance, None -> - (None, Relation aeq_rel), - (None, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_symmetric_areflexive_transitive_relation), - [| a_instance ; aeq_instance ; sym_instance ; trans_instance |]), - Lazy.force coq_iff_relation - | Some sym_instance, Some refl_instance -> - (None, Relation aeq_rel), - (None, Relation aeq_rel), - mkApp - ((Lazy.force - coq_equality_morphism_of_symmetric_reflexive_transitive_relation), - [| a_instance ; aeq_instance ; refl_instance ; sym_instance ; - trans_instance |]), - Lazy.force coq_iff_relation in - let _ = - Declare.declare_internal_constant mor_name - (DefinitionEntry - {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions()}, - IsDefinition Definition) - in - let a_quantifiers_rev = - List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in - add_morphism None mor_name - (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2], - output) - -(* The vernac command "Add Relation ..." *) -let add_relation id a aeq refl sym trans = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - int_add_relation id (constr_of a) (constr_of aeq) (Option.map constr_of refl) - (Option.map constr_of sym) (Option.map constr_of trans) - -(************************ Add Setoid ******************************************) - -(* The vernac command "Add Setoid" *) -let add_setoid id a aeq th = - Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - let a = constr_of a in - let aeq = constr_of aeq in - let th = constr_of th in - let env = Global.env () in - let a_quantifiers_rev = check_a env a in - check_eq env a_quantifiers_rev a aeq ; - check_setoid_theory env a_quantifiers_rev a aeq th ; - let a_instance = apply_to_rels a a_quantifiers_rev in - let aeq_instance = apply_to_rels aeq a_quantifiers_rev in - let th_instance = apply_to_rels th a_quantifiers_rev in - let refl = - Sign.it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_refl), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - let sym = - Sign.it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_sym), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - let trans = - Sign.it_mkLambda_or_LetIn - (mkApp ((Lazy.force coq_seq_trans), - [| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in - int_add_relation id a aeq (Some refl) (Some sym) (Some trans) - - -(****************************** The tactic itself *******************************) - -type direction = - Left2Right - | Right2Left - -let prdirection = - function - Left2Right -> str "->" - | Right2Left -> str "<-" - -type constr_with_marks = - | MApp of constr * morphism_class * constr_with_marks array * direction - | ToReplace - | ToKeep of constr * relation relation_class * direction - -let is_to_replace = function - | ToKeep _ -> false - | ToReplace -> true - | MApp _ -> true - -let get_mark a = - Array.fold_left (||) false (Array.map is_to_replace a) - -let cic_direction_of_direction = - function - Left2Right -> Lazy.force coq_Left2Right - | Right2Left -> Lazy.force coq_Right2Left - -let opposite_direction = - function - Left2Right -> Right2Left - | Right2Left -> Left2Right - -let direction_of_constr_with_marks hole_direction = - function - MApp (_,_,_,dir) -> cic_direction_of_direction dir - | ToReplace -> hole_direction - | ToKeep (_,_,dir) -> cic_direction_of_direction dir - -type argument = - Toapply of constr (* apply the function to the argument *) - | Toexpand of name * types (* beta-expand the function w.r.t. an argument - of this type *) -let beta_expand c args_rev = - let rec to_expand = - function - [] -> [] - | (Toapply _)::tl -> to_expand tl - | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in - let rec aux n = - function - [] -> [] - | (Toapply arg)::tl -> arg::(aux n tl) - | (Toexpand _)::tl -> (mkRel n)::(aux (n + 1) tl) - in - compose_lam (to_expand args_rev) - (mkApp (c, Array.of_list (List.rev (aux 1 args_rev)))) - -exception Optimize (* used to fall-back on the tactic for Leibniz equality *) - -let relation_class_that_matches_a_constr caller_name new_goals hypt = - let (heq, hargs) = decompose_app hypt in - let rec get_all_but_last_two = - function - [] - | [_] -> - errorlabstrm caller_name (pr_lconstr hypt ++ - str " is not a registered relation.") - | [_;_] -> [] - | he::tl -> he::(get_all_but_last_two tl) in - let all_aeq_args = get_all_but_last_two hargs in - let rec find_relation l subst = - let aeq = mkApp (heq,(Array.of_list l)) in - try - let rel = find_relation_class aeq in - match rel,new_goals with - Leibniz _,[] -> - assert (subst = []); - raise Optimize (* let's optimize the proof term size *) - | Leibniz (Some _), _ -> - assert (subst = []); - rel - | Leibniz None, _ -> - (* for well-typedness reasons it should have been catched by the - previous guard in the previous iteration. *) - assert false - | Relation rel,_ -> Relation (apply_to_relation (Array.of_list subst) rel) - with Not_found -> - if l = [] then - errorlabstrm caller_name - (pr_lconstr (mkApp (aeq, Array.of_list all_aeq_args)) ++ - str " is not a registered relation.") - else - let last,others = Util.list_sep_last l in - find_relation others (last::subst) - in - find_relation all_aeq_args [] - -(* rel1 is a subrelation of rel2 whenever - forall x1 x2, rel1 x1 x2 -> rel2 x1 x2 - The Coq part of the tactic, however, needs rel1 == rel2. - Hence the third case commented out. - Note: accepting user-defined subrelations seems to be the last - useful generalization that does not go against the original spirit of - the tactic. -*) -let subrelation gl rel1 rel2 = - match rel1,rel2 with - Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} -> - Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2 - | Leibniz (Some t1), Leibniz (Some t2) -> - Tacmach.pf_conv_x gl t1 t2 - | Leibniz None, _ - | _, Leibniz None -> assert false -(* This is the commented out case (see comment above) - | Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} -> - Tacmach.pf_conv_x gl t1 t2 -*) - | _,_ -> false - -(* this function returns the list of new goals opened by a constr_with_marks *) -let rec collect_new_goals = - function - MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list a)) - | ToReplace - | ToKeep (_,Leibniz _,_) - | ToKeep (_,Relation {rel_refl=Some _},_) -> [] - | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [mkApp(aeq,[|c ; c|])] - -(* two marked_constr are equivalent if they produce the same set of new goals *) -let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 = - let glc1 = collect_new_goals (to_marked_constr c1) in - let glc2 = collect_new_goals (to_marked_constr c2) in - List.for_all (fun c -> List.exists (fun c' -> pf_conv_x gl c c') glc1) glc2 - -let pr_new_goals i c = - let glc = collect_new_goals c in - str " " ++ int i ++ str ") side conditions:" ++ - (if glc = [] then str " no side conditions" - else - (pr_fnl () ++ str " " ++ - prlist_with_sep (fun () -> str "\n ") - (fun c -> str " ... |- " ++ pr_lconstr c) glc)) - -(* given a list of constr_with_marks, it returns the list where - constr_with_marks than open more goals than simpler ones in the list - are got rid of *) -let elim_duplicates gl to_marked_constr = - let rec aux = - function - [] -> [] - | he:: tl -> - if List.exists - (marked_constr_equiv_or_more_complex to_marked_constr gl he) tl - then aux tl - else he::aux tl - in - aux - -let filter_superset_of_new_goals gl new_goals l = - List.filter - (fun (_,_,c) -> - List.for_all - (fun g -> List.exists (pf_conv_x gl g) (collect_new_goals c)) new_goals) l - -(* given the array of lists [| l1 ; ... ; ln |] it returns the list of arrays - [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *) -let cartesian_product gl a = - let rec aux = - function - [] -> assert false - | [he] -> List.map (fun e -> [e]) he - | he::tl -> - let tl' = aux tl in - List.flatten - (List.map (function e -> List.map (function l -> e :: l) tl') he) - in - List.map Array.of_list - (aux (List.map (elim_duplicates gl identity) (Array.to_list a))) - -let mark_occur gl ~new_goals t in_c input_relation input_direction = - let rec aux output_relation output_directions in_c = - if eq_constr t in_c then - if List.mem input_direction output_directions - && subrelation gl input_relation output_relation then - [ToReplace] - else [] - else - match kind_of_term in_c with - | App (c,al) -> - let mors_and_cs_and_als = - let mors_and_cs_and_als = - let morphism_table_find c = - try morphism_table_find c with Not_found -> [] in - let rec aux acc = - function - [] -> - let c' = mkApp (c, Array.of_list acc) in - let al' = [||] in - List.map (fun m -> m,c',al') (morphism_table_find c') - | (he::tl) as l -> - let c' = mkApp (c, Array.of_list acc) in - let al' = Array.of_list l in - let acc' = acc @ [he] in - (List.map (fun m -> m,c',al') (morphism_table_find c')) @ - (aux acc' tl) - in - aux [] (Array.to_list al) in - let mors_and_cs_and_als = - List.map - (function (m,c,al) -> - relation_morphism_of_constr_morphism m, c, al) - mors_and_cs_and_als in - let mors_and_cs_and_als = - List.fold_left - (fun l (m,c,al) -> - try (unify_morphism_with_arguments gl (c,al) m t) :: l - with Impossible -> l - ) [] mors_and_cs_and_als - in - List.filter - (fun (mor,_,_) -> subrelation gl mor.output output_relation) - mors_and_cs_and_als - in - (* First we look for well typed morphisms *) - let res_mors = - List.fold_left - (fun res (mor,c,al) -> - let a = - let arguments = Array.of_list mor.args in - let apply_variance_to_direction = - function - None -> [Left2Right;Right2Left] - | Some true -> output_directions - | Some false -> List.map opposite_direction output_directions - in - Util.array_map2 - (fun a (variance,relation) -> - (aux relation (apply_variance_to_direction variance) a) - ) al arguments - in - let a' = cartesian_product gl a in - List.flatten (List.map (fun output_direction -> - (List.map - (function a -> - if not (get_mark a) then - ToKeep (in_c,output_relation,output_direction) - else - MApp (c,ACMorphism mor,a,output_direction)) a')) - output_directions) @ res - ) [] mors_and_cs_and_als in - (* Then we look for well typed functions *) - let res_functions = - (* the tactic works only if the function type is - made of non-dependent products only. However, here we - can cheat a bit by partially instantiating c to match - the requirement when the arguments to be replaced are - bound by non-dependent products only. *) - let typeofc = Tacmach.pf_type_of gl c in - let typ = nf_betaiota typeofc in - let rec find_non_dependent_function env c c_args_rev typ f_args_rev - a_rev - = - function - [] -> - if a_rev = [] then - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - else - let a' = - cartesian_product gl (Array.of_list (List.rev a_rev)) - in - List.fold_left - (fun res a -> - if not (get_mark a) then - List.map (fun output_direction -> - (ToKeep (in_c,output_relation,output_direction))) - output_directions @ res - else - let err = - match output_relation with - Leibniz (Some typ') when pf_conv_x gl typ typ' -> - false - | Leibniz None -> assert false - | _ when output_relation = Lazy.force coq_iff_relation - -> false - | _ -> true - in - if err then res - else - let mor = - ACFunction{f_args=List.rev f_args_rev;f_output=typ} in - let func = beta_expand c c_args_rev in - List.map (fun output_direction -> - (MApp (func,mor,a,output_direction))) - output_directions @ res - ) [] a' - | (he::tl) -> - let typnf = Reduction.whd_betadeltaiota env typ in - match kind_of_term typnf with - | Prod (name,s,t) -> - let env' = push_rel (name,None,s) env in - let he = - (aux (Leibniz (Some s)) [Left2Right;Right2Left] he) in - if he = [] then [] - else - let he0 = List.hd he in - begin - match noccurn 1 t, he0 with - _, ToKeep (arg,_,_) -> - (* invariant: if he0 = ToKeep (t,_,_) then every - element in he is = ToKeep (t,_,_) *) - assert - (List.for_all - (function - ToKeep(arg',_,_) when pf_conv_x gl arg arg' -> - true - | _ -> false) he) ; - (* generic product, to keep *) - find_non_dependent_function - env' c ((Toapply arg)::c_args_rev) - (subst1 arg t) f_args_rev a_rev tl - | true, _ -> - (* non-dependent product, to replace *) - find_non_dependent_function - env' c ((Toexpand (name,s))::c_args_rev) - (lift 1 t) (s::f_args_rev) (he::a_rev) tl - | false, _ -> - (* dependent product, to replace *) - (* This limitation is due to the reflexive - implementation and it is hard to lift *) - errorlabstrm "Setoid_replace" - (str "Cannot rewrite in the argument of a " ++ - str "dependent product. If you need this " ++ - str "feature, please report to the author.") - end - | _ -> assert false - in - find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] [] - (Array.to_list al) - in - elim_duplicates gl identity (res_functions @ res_mors) - | Prod (_, c1, c2) -> - if (dependent (mkRel 1) c2) - then - if (occur_term t c2) - then errorlabstrm "Setoid_replace" - (str "Cannot rewrite in the type of a variable bound " ++ - str "in a dependent product.") - else - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - else - let typeofc1 = Tacmach.pf_type_of gl c1 in - if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then - (* to avoid this error we should introduce an impl relation - whose first argument is Type instead of Prop. However, - the type of the new impl would be Type -> Prop -> Prop - that is no longer a Relation_Definitions.relation. Thus - the Coq part of the tactic should be heavily modified. *) - errorlabstrm "Setoid_replace" - (str "Rewriting in a product A -> B is possible only when A " ++ - str "is a proposition (i.e. A is of type Prop). The type " ++ - pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++ - str " that is not convertible to Prop.") - else - aux output_relation output_directions - (mkApp ((Lazy.force coq_impl), - [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |])) - | _ -> - if occur_term t in_c then - errorlabstrm "Setoid_replace" - (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++ - str " that is not an applicative context.") - else - List.map (fun output_direction -> - ToKeep (in_c,output_relation,output_direction)) - output_directions - in - let aux2 output_relation output_direction = - List.map - (fun res -> output_relation,output_direction,res) - (aux output_relation [output_direction] in_c) in - let res = - (aux2 (Lazy.force coq_iff_relation) Right2Left) @ - (* [Left2Right] is the case of a prop of signature A ++> iff or B --> iff *) - (aux2 (Lazy.force coq_iff_relation) Left2Right) @ - (aux2 (Lazy.force coq_impl_relation) Right2Left) in - let res = elim_duplicates gl (function (_,_,t) -> t) res in - let res' = filter_superset_of_new_goals gl new_goals res in - match res' with - [] when res = [] -> - errorlabstrm "Setoid_rewrite" - (strbrk "Either the term " ++ pr_lconstr t ++ strbrk " that must be " ++ - strbrk "rewritten occurs in a covariant position or the goal is not" ++ - strbrk " made of morphism applications only. You can replace only " ++ - strbrk "occurrences that are in a contravariant position and such " ++ - strbrk "that the context obtained by abstracting them is made of " ++ - strbrk "morphism applications only.") - | [] -> - errorlabstrm "Setoid_rewrite" - (str "No generated set of side conditions is a superset of those " ++ - str "requested by the user. The generated sets of side conditions " ++ - str "are: " ++ - pr_fnl () ++ - prlist_with_sepi pr_fnl - (fun i (_,_,mc) -> pr_new_goals i mc) res) - | [he] -> he - | he::_ -> - Flags.if_warn msg_warning - (strbrk "The application of the tactic is subject to one of " ++ - strbrk "the following set of side conditions that the user needs " ++ - strbrk "to prove:" ++ - pr_fnl () ++ - prlist_with_sepi pr_fnl - (fun i (_,_,mc) -> pr_new_goals i mc) res' ++ pr_fnl () ++ - strbrk "The first set is randomly chosen. Use the syntax " ++ - strbrk "\"setoid_rewrite ... generate side conditions ...\" to choose " ++ - strbrk "a different set.") ; - he - -let cic_morphism_context_list_of_list hole_relation hole_direction out_direction -= - let check = - function - (None,dir,dir') -> - mkApp ((Lazy.force coq_MSNone), [| dir ; dir' |]) - | (Some true,dir,dir') -> - assert (dir = dir'); - mkApp ((Lazy.force coq_MSCovariant), [| dir |]) - | (Some false,dir,dir') -> - assert (dir <> dir'); - mkApp ((Lazy.force coq_MSContravariant), [| dir |]) in - let rec aux = - function - [] -> assert false - | [(variance,out),(value,direction)] -> - mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class ; out |]), - mkApp ((Lazy.force coq_fcl_singl), - [| hole_relation; hole_direction ; out ; - direction ; out_direction ; - check (variance,direction,out_direction) ; value |]) - | ((variance,out),(value,direction))::tl -> - let outtl, valuetl = aux tl in - mkApp ((Lazy.force coq_cons), - [| Lazy.force coq_Argument_Class ; out ; outtl |]), - mkApp ((Lazy.force coq_fcl_cons), - [| hole_relation ; hole_direction ; out ; outtl ; - direction ; out_direction ; - check (variance,direction,out_direction) ; - value ; valuetl |]) - in aux - -let rec cic_type_nelist_of_list = - function - [] -> assert false - | [value] -> - mkApp ((Lazy.force coq_singl), [| mkType (Termops.new_univ ()) ; value |]) - | value::tl -> - mkApp ((Lazy.force coq_cons), - [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |]) - -let syntactic_but_representation_of_marked_but hole_relation hole_direction = - let rec aux out (rel_out,precise_out,is_reflexive) = - function - MApp (f, m, args, direction) -> - let direction = cic_direction_of_direction direction in - let morphism_theory, relations = - match m with - ACMorphism { args = args ; morphism_theory = morphism_theory } -> - morphism_theory,args - | ACFunction { f_args = f_args ; f_output = f_output } -> - let mt = - if eq_constr out (cic_relation_class_of_relation_class - (Lazy.force coq_iff_relation)) - then - mkApp ((Lazy.force coq_morphism_theory_of_predicate), - [| cic_type_nelist_of_list f_args; f|]) - else - mkApp ((Lazy.force coq_morphism_theory_of_function), - [| cic_type_nelist_of_list f_args; f_output; f|]) - in - mt,List.map (fun x -> None,Leibniz (Some x)) f_args in - let cic_relations = - List.map - (fun (variance,r) -> - variance, - r, - cic_relation_class_of_relation_class r, - cic_precise_relation_class_of_relation_class r - ) relations in - let cic_args_relations,argst = - cic_morphism_context_list_of_list hole_relation hole_direction direction - (List.map2 - (fun (variance,trel,t,precise_t) v -> - (variance,cic_argument_class_of_argument_class (variance,trel)), - (aux t precise_t v, - direction_of_constr_with_marks hole_direction v) - ) cic_relations (Array.to_list args)) - in - mkApp ((Lazy.force coq_App), - [|hole_relation ; hole_direction ; - cic_args_relations ; out ; direction ; - morphism_theory ; argst|]) - | ToReplace -> - mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |]) - | ToKeep (c,_,direction) -> - let direction = cic_direction_of_direction direction in - if is_reflexive then - mkApp ((Lazy.force coq_ToKeep), - [| hole_relation ; hole_direction ; precise_out ; direction ; c |]) - else - let c_is_proper = - let typ = mkApp (rel_out, [| c ; c |]) in - mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ) - in - mkApp ((Lazy.force coq_ProperElementToKeep), - [| hole_relation ; hole_direction; precise_out ; - direction; c ; c_is_proper |]) - in aux - -let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h) - prop_direction m -= - let hole_relation = cic_relation_class_of_relation_class hole_relation in - let hyp,hole_direction = h,cic_direction_of_direction direction in - let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in - let precise_prop_relation = - cic_precise_relation_class_of_relation_class prop_relation - in - mkApp ((Lazy.force coq_setoid_rewrite), - [| hole_relation ; hole_direction ; cic_prop_relation ; - prop_direction ; c1 ; c2 ; - syntactic_but_representation_of_marked_but hole_relation hole_direction - cic_prop_relation precise_prop_relation m ; hyp |]) - -let check_evar_map_of_evars_defs evd = - let metas = Evd.meta_list evd in - let check_freemetas_is_empty rebus = - Evd.Metaset.iter - (fun m -> - if Evd.meta_defined evd m then () else - raise (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) - in - List.iter - (fun (_,binding) -> - match binding with - Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) -> - check_freemetas_is_empty rebus freemetas - | Evd.Clval (_,({Evd.rebus=rebus1; Evd.freemetas=freemetas1},_), - {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) -> - check_freemetas_is_empty rebus1 freemetas1 ; - check_freemetas_is_empty rebus2 freemetas2 - ) metas - -(* For a correct meta-aware "rewrite in", we split unification - apart from the actual rewriting (Pierre L, 05/04/06) *) - -(* [unification_rewrite] searchs a match for [c1] in [but] and then - returns the modified objects (in particular [c1] and [c2]) *) - -let rewrite_unif_flags = { - modulo_conv_on_closed_terms = None; - use_metas_eagerly = true; - modulo_delta = empty_transparent_state; -} - -let rewrite2_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; - use_metas_eagerly = true; - modulo_delta = empty_transparent_state; -} - -let unification_rewrite c1 c2 cl but gl = - let (env',c1) = - try - (* ~flags:(false,true) to allow to mark occurences that must not be - rewritten simply by replacing them with let-defined definitions - in the context *) - w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd - with - Pretype_errors.PretypeError _ -> - (* ~flags:(true,true) to make Ring work (since it really - exploits conversion) *) - w_unify_to_subterm ~flags:rewrite2_unif_flags - (pf_env gl) (c1,but) cl.evd - in - let cl' = {cl with evd = env' } in - let c2 = Clenv.clenv_nf_meta cl' c2 in - check_evar_map_of_evars_defs env' ; - env',Clenv.clenv_value cl', c1, c2 - -(* no unification is performed in this function. [sigma] is the - substitution obtained from an earlier unification. *) - -let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl = - let but = pf_concl gl in - try - let input_relation = - relation_class_that_matches_a_constr "Setoid_rewrite" - new_goals (Typing.mtype_of (pf_env gl) sigma (snd hyp)) in - let output_relation,output_direction,marked_but = - mark_occur gl ~new_goals c1 but input_relation (fst hyp) in - let cic_output_direction = cic_direction_of_direction output_direction in - let if_output_relation_is_iff gl = - let th = - apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp - cic_output_direction marked_but - in - let new_but = Termops.replace_term c1 c2 but in - let hyp1,hyp2,proj = - match output_direction with - Right2Left -> new_but, but, Lazy.force coq_proj1 - | Left2Right -> but, new_but, Lazy.force coq_proj2 - in - let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in - let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in - let th' = mkApp (proj, [|impl2; impl1; th|]) in - Tactics.refine - (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) - gl in - let if_output_relation_is_if gl = - let th = - apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp - cic_output_direction marked_but - in - let new_but = Termops.replace_term c1 c2 but in - Tactics.refine - (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|])) - gl in - if output_relation = (Lazy.force coq_iff_relation) then - if_output_relation_is_iff gl - else - if_output_relation_is_if gl - with - Optimize -> - !general_rewrite (fst hyp = Left2Right) all_occurrences (snd hyp) gl - -let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl = - let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl (pf_concl gl) gl in - relation_rewrite_no_unif c1 c2 (input_direction,cl) ~new_goals sigma gl - -let analyse_hypothesis gl c = - let ctype = pf_type_of gl c in - let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an equivalence" in - let others,(c1,c2) = split_last_two args in - eqclause,mkApp (equiv, Array.of_list others),c1,c2 - -let general_s_rewrite lft2rgt occs c ~new_goals gl = - if occs <> all_occurrences then - warning "Rewriting at selected occurrences not supported"; - let eqclause,_,c1,c2 = analyse_hypothesis gl c in - if lft2rgt then - relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl - else - relation_rewrite c2 c1 (Right2Left,eqclause) ~new_goals gl - -let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl = - let hyp = pf_type_of gl (mkVar id) in - (* first, we find a match for c1 in the hyp *) - let (sigma,cl,c1,c2) = unification_rewrite c1 c2 eqclause hyp gl in - (* since we will actually rewrite in the opposite direction, we also need - to replace every occurrence of c2 (resp. c1) in hyp with something that - is convertible but not syntactically equal. To this aim we introduce a - let-in and then we will use the intro tactic to get rid of it. - Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *) - let mangled_new_hyp = - let hyp = lift 2 hyp in - (* first, we backup every occurences of c1 in newly allocated (Rel 1) *) - let hyp = Termops.replace_term (lift 2 c1) (mkRel 1) hyp in - (* then, we factorize every occurences of c2 into (Rel 2) *) - let hyp = Termops.replace_term (lift 2 c2) (mkRel 2) hyp in - (* Now we substitute (Rel 1) (i.e. c1) for c2 *) - let hyp = subst1 (lift 1 c2) hyp in - (* Since subst1 has killed Rel 1 and decreased the other Rels, - Rel 1 is now coding for c2, we can build the let-in factorizing c2 *) - mkLetIn (Anonymous,c2,pf_type_of gl c2,hyp) - in - let new_hyp = Termops.replace_term c1 c2 hyp in - let oppdir = opposite_direction direction in - cut_replacing id new_hyp - (tclTHENLAST - (tclTHEN (change_in_concl None mangled_new_hyp) - (tclTHEN intro - (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma)))) - gl - -let general_s_rewrite_in id lft2rgt occs c ~new_goals gl = - if occs <> all_occurrences then - warning "Rewriting at selected occurrences not supported"; - let eqclause,_,c1,c2 = analyse_hypothesis gl c in - if lft2rgt then - relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl - else - relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl - - -(* - [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ] - common part of [setoid_replace] and [setoid_replace_in] (distinction is done using rewrite_tac). - - Algorith sketch: - 1- find the (setoid) relation [rel] between [c1] and [c2] using [relation] - 2- assert [H:rel c2 c1] - 3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the - goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate - new_goals if asked (cf general_s_rewrite) - 4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if - [try_prove_eq_tac_opt] is [None] -*) -let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl = - let try_prove_eq_tac = - match try_prove_eq_tac_opt with - | None -> Tacticals.tclIDTAC - | Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac ) - in - try - let carrier,args = decompose_app (pf_type_of gl c1) in - let relation = - match relation with - Some rel -> - (try - match find_relation_class rel with - Relation sa -> if not (eq_constr carrier sa.rel_a) then - errorlabstrm "Setoid_rewrite" - (str "the carrier of " ++ pr_lconstr rel ++ - str " does not match the type of " ++ pr_lconstr c1); - sa - | Leibniz _ -> raise Optimize - with - Not_found -> - errorlabstrm "Setoid_rewrite" - (pr_lconstr rel ++ str " is not a registered relation.")) - | None -> - match default_relation_for_carrier (pf_type_of gl c1) with - Relation sa -> sa - | Leibniz _ -> raise Optimize - in - let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in - let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in - let replace dir eq = - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac dir all_occurrences (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] - in - tclORELSE - (replace true eq_left_to_right) (replace false eq_right_to_left) gl - with - Optimize -> (* (!replace tac_opt c1 c2) gl *) - let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in - tclTHENS (assert_tac false Anonymous eq) - [onLastHyp (fun id -> - tclTHEN - (rewrite_tac false all_occurrences (mkVar id) ~new_goals) - (clear [id])); - try_prove_eq_tac] gl - -let setoid_replace = general_setoid_replace general_s_rewrite -let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = - general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl - -(* [setoid_]{reflexivity,symmetry,transitivity} tactics *) - -let setoid_reflexivity gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_reflexivity" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_refl with - None -> - errorlabstrm "Setoid_reflexivity" - (str "The relation " ++ prrelation rel ++ str " is not reflexive.") - | Some refl -> apply refl gl - with - Optimize -> reflexivity_red true gl - -let setoid_symmetry gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_symmetry" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_sym with - None -> - errorlabstrm "Setoid_symmetry" - (str "The relation " ++ prrelation rel ++ str " is not symmetric.") - | Some sym -> apply sym gl - with - Optimize -> symmetry_red true gl - -let setoid_symmetry_in id gl = - let ctype = pf_type_of gl (mkVar id) in - let binders,concl = Sign.decompose_prod_assum ctype in - let (equiv, args) = decompose_app concl in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an equivalence" - in - let others,(c1,c2) = split_last_two args in - let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in - let new_hyp' = mkApp (he, [| c2 ; c1 |]) in - let new_hyp = it_mkProd_or_LetIn new_hyp' binders in - tclTHENS (cut new_hyp) - [ intro_replacing id; - tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ] - gl - -let setoid_transitivity c gl = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_transitivity" - [] (pf_concl gl) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - let ctyp = pf_type_of gl c in - let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in - match rel'.rel_trans with - None -> - errorlabstrm "Setoid_transitivity" - (str "The relation " ++ prrelation rel ++ str " is not transitive.") - | Some trans -> - let transty = nf_betaiota (pf_type_of gl trans) in - let argsrev, _ = - Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in - let binder = - match List.rev argsrev with - _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2 - | _ -> assert false - in - apply_with_bindings - (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl - with - Optimize -> transitivity_red true c gl -;; - |