| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/tactics/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 141 kB |
|
Quelle tactics.ml Sprache: SML |
|||||||||
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open Names open Nameops open Constr open Context open Termops open Environ open EConstr open Vars open Namegen open Declarations open Inductiveops open Reductionops open Evd open Tacred open Genredexpr open Logic open Clenv open Tacticals open Hipattern open Rocqlib open Evarutil open Indrec open Pretype_errors open Unification open Locus open Locusops open Tactypes open Proofview.Notations open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration let tclEVARS = Proofview.Unsafe.tclEVARS let tclEVARSTHEN sigma t = Proofview.tclTHEN (tclEVARS sigma) t let typ_of env sigma c = let open Retyping in try get_type_of ~lax:true env sigma c with RetypeError e -> user_err (print_retype_error e) open Goptions let clear_hyp_by_default = ref false let use_clear_hyp_by_default () = !clear_hyp_by_default let () = declare_bool_option { optstage = Summary.Stage.Interp; optdepr = None; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } (*********************************************) (* Errors *) (*********************************************) exception IntroAlreadyDeclared of Id.t exception ClearDependency of env * evar_map * Id.t option * Evarutil.clear_dependency_erro exception ReplacingDependency of env * evar_map * Id.t * Evarutil.clear_dependency_error * exception AlreadyUsed of Id.t exception UsedTwice of Id.t exception VariableHasNoValue of Id.t exception ConvertIncompatibleTypes of env * evar_map * constr * constr exception ConvertNotAType exception NotConvertible exception NotUnfoldable exception NoQuantifiedHypothesis of quantified_hypothesis * bool exception CannotFindInstance of Id.t exception NothingToRewrite of Id.t exception IllFormedEliminationType exception UnableToApplyLemma of env * evar_map * constr * constr exception DependsOnBody of Id.t list * Id.Set.t * Id.t option exception NotRightNumberConstructors of int exception NotEnoughConstructors exception ConstructorNumberedFromOne exception NoConstructors exception UnexpectedExtraPattern of int option * delayed_open_constr intro_pattern_expr exception CannotFindInductiveArgument exception OneIntroPatternExpected exception KeepAndClearModifierOnlyForHypotheses exception FixpointOnNonInductiveType exception NotEnoughProducts exception AllMethodsInCoinductiveType exception ReplacementIllTyped of exn exception NotEnoughPremises exception NeedDependentProduct let error ?loc e = Loc.raise ?loc e let clear_in_global_msg = function | None -> mt () | Some ref -> str " implicitly in " ++ Printer.pr_global ref let clear_dependency_msg env sigma id err inglobal = let ppidupper = function Some id -> Id.print id | None -> str "This variable" in let ppid = function Some id -> Id.print id | None -> str "this variable" in let pp = clear_in_global_msg inglobal in match err with | Evarutil.OccurHypInSimpleClause None -> ppidupper id ++ str " is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> ppidupper id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot remove " ++ ppid id ++ strbrk " without breaking the typing of " ++ Printer.pr_leconstr_env env sigma (mkEvar ev) ++ str"." | Evarutil.NoCandidatesLeft ev -> str "Cannot remove " ++ ppid id ++ str " as it would leave the existential " ++ Printer.pr_existential_key env sigma ev ++ str" without candidates." let replacing_dependency_msg env sigma id err inglobal = let pp = clear_in_global_msg inglobal in match err with | Evarutil.OccurHypInSimpleClause None -> str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> str "Cannot change " ++ Id.print id ++ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_leconstr_env env sigma (mkEvar ev) ++ str"." | Evarutil.NoCandidatesLeft ev -> str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++ Printer.pr_existential_key env sigma ev ++ str" without candidates." let msg_quantified_hypothesis = function | NamedHyp id -> str "quantified hypothesis named " ++ Id.print id.CAst.v | AnonHyp n -> pr_nth n ++ str " non dependent hypothesis" let explain_unexpected_extra_pattern bound pat = let nb = Option.get bound in let s1,s2,s3 = match pat with | IntroNaming (IntroIdentifier _) -> "name", (String.plural nb " introduction pattern"), "no" | _ -> "introduction pattern", "", "none" in str "Unexpected " ++ str s1 ++ str " (" ++ (if Int.equal nb 0 then (str s3 ++ str s2) else (str "at most " ++ int nb ++ str s2)) ++ spc () ++ str (if Int.equal nb 1 then "was" else "were") ++ strbrk " expected in the branch)." exception Unhandled let wrap_unhandled f e = try Some (f e) with Unhandled -> None let tactic_interp_error_handler = function | IntroAlreadyDeclared id -> Id.print id ++ str " is already declared." | ClearDependency (env,sigma,id,err,inglobal) -> clear_dependency_msg env sigma id err inglobal | ReplacingDependency (env,sigma,id,err,inglobal) -> replacing_dependency_msg env sigma id err inglobal | AlreadyUsed id -> Id.print id ++ str " is already used." | UsedTwice id -> Id.print id ++ str" is used twice." | VariableHasNoValue id -> Id.print id ++ str" is not a defined hypothesis." | ConvertIncompatibleTypes (env,sigma,t1,t2) -> str "The first term has type" ++ spc () ++ quote (Termops.Internal.print_constr_env env sigma t1) ++ spc () ++ strbrk "while the second term has incompatible type" ++ spc () ++ quote (Termops.Internal.print_constr_env env sigma t2) ++ str "." | ConvertNotAType -> str "Not a type." | NotConvertible -> str "Not convertible." | NotUnfoldable -> str "Cannot unfold a non-constant." | NoQuantifiedHypothesis (id,red) -> str "No " ++ msg_quantified_hypothesis id ++ strbrk " in current goal" ++ (if red then strbrk " even after head-reduction" else mt ()) ++ str"." | CannotFindInstance id -> str "Cannot find an instance for " ++ Id.print id ++ str"." | NothingToRewrite id -> str "Nothing to rewrite in " ++ Id.print id ++ str"." | IllFormedEliminationType -> str "The type of elimination clause is not well-formed." | UnableToApplyLemma (env,sigma,thm,t) -> str "Unable to apply lemma of type" ++ brk(1,1) ++ quote (Printer.pr_leconstr_env env sigma thm) ++ spc() ++ str "on hypothesis of type" ++ brk(1,1) ++ quote (Printer.pr_leconstr_env env sigma t) ++ str "." | DependsOnBody (idl,ids,where) -> let idl = List.filter (fun id -> Id.Set.mem id ids) idl in let on_the_bodies = function | [] -> assert false | [id] -> str " depends on the body of " ++ Id.print id | l -> str " depends on the bodies of " ++ pr_sequence Id.print l in (match where with | None -> str "Conclusion" ++ on_the_bodies idl | Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies idl) | NotRightNumberConstructors n -> str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ". | NotEnoughConstructors -> str "Not enough constructors." | ConstructorNumberedFromOne -> str "The constructors are numbered starting from 1." | NoConstructors -> str "The type has no constructors." | UnexpectedExtraPattern (bound,pat) -> explain_unexpected_extra_pattern bound pat | CannotFindInductiveArgument -> str "Cannot find inductive argument of elimination scheme." | OneIntroPatternExpected -> str "Introduction pattern for one hypothesis expected." | KeepAndClearModifierOnlyForHypotheses -> str "keep/clear modifiers apply only to hypothesis names." | FixpointOnNonInductiveType -> str "Cannot do a fixpoint on a non inductive type." | NotEnoughProducts -> str "Not enough products." | AllMethodsInCoinductiveType -> str "All methods must construct elements in coinductive types." | ReplacementIllTyped e -> str "Replacement would lead to an ill-typed term:" ++ spc () ++ CErrors.print e | NotEnoughPremises -> str "Applied theorem does not have enough premises." | NeedDependentProduct -> str "Needs a non-dependent product." | _ -> raise Unhandled let _ = CErrors.register_handler (wrap_unhandled tactic_interp_error_handler) let error_clear_dependency env sigma id err inglobal = error (ClearDependency (env,sigma,Some id,err,inglobal)) let error_replacing_dependency env sigma id err inglobal = error (ReplacingDependency (env,sigma,id,err,inglobal)) (*********************************************) (* Tactics *) (*********************************************) (******************************************) (* Primitive tactics *) (******************************************) (** This tactic creates a partial proof realizing the introduction rule, but does not check anything. *) let unsafe_intro env decl ~relevance b = Refine.refine_with_principal ~typecheck:false begin fun sigma -> let ctx = named_context_val env in let nctx = push_named_context_val decl ctx in let inst = EConstr.identity_subst_val (named_context_val env) in let ninst = SList.cons (mkRel 1) inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_pure_evar nctx sigma ~relevance nb in (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) (mkEvar (ev, ninst)), Some ev) end let introduction id = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let relevance = Proofview.Goal.relevance gl in let sigma = Tacmach.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in let env = Proofview.Goal.env gl in let () = if mem_named_context_val id hyps then error (IntroAlreadyDeclared id) in let open Context.Named.Declaration in match EConstr.kind sigma concl with | Prod (id0, t, b) -> unsafe_intro env (LocalAssum ({id0 with binder_name=id}, t)) ~relevance b | LetIn (id0, c, t, b) -> unsafe_intro env (LocalDef ({id0 with binder_name=id}, c, t)) ~relevan | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct)) end (* Not sure if being able to disable [cast] is useful. Uses seem picked somewhat randomly. *) let convert_concl ~cast ~check ty k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let conclty = Proofview.Goal.concl gl in Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma = if check then begin let sigma, _ = Typing.type_of env sigma ty in match Reductionops.infer_conv env sigma ty conclty with | None -> error NotConvertible | Some sigma -> sigma end else sigma in let (sigma, x) = Evarutil.new_evar env sigma ty in let ans = if not cast then x else mkCast(x,k,conclty) in (sigma, ans, Some (fst @@ destEvar sigma x)) end end let convert_hyp ~check ~reorder d = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let ty = Proofview.Goal.concl gl in let sign = convert_hyp ~check ~reorder env sigma d in let env = reset_with_named_context sign env in Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_evar env sigma ty in sigma, ev, Some (fst @@ destEvar sigma ev) end end let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> match Tacmach.pf_apply (Reductionops.infer_conv ~pb) gl x y with | Some sigma -> Proofview.Unsafe.tclEVARS sigma | None -> error NotConvertible | exception e when CErrors.noncritical e -> let _, info = Exninfo.capture e in (* FIXME: Sometimes an anomaly is raised from conversion *) error ?loc:(Loc.get_loc info) NotConvertible end let convert x y = convert_gen Conversion.CONV x y let convert_leq x y = convert_gen Conversion.CUMUL x y (* This tactic enables users to remove hypotheses from the signature. * Some care is taken to prevent them from removing variables that are * subsequently used in other hypotheses or in the conclusion of the * goal. *) let clear_gen fail = function | [] -> Proofview.tclUNIT () | ids -> Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in (* clear_hyps_in_evi does not require nf terms *) let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let concl = Proofview.Goal.concl gl in let (sigma, hyps, concl) = try clear_hyps_in_evi env sigma (named_context_val env) concl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_evar env sigma concl in sigma, ev, Some (fst @@ destEvar sigma ev) end) end let clear ids = clear_gen error_clear_dependency ids let clear_for_replacing ids = clear_gen error_replacing_dependency ids let apply_clear_request clear_flag dft c = let doclear = match clear_flag with | None -> if dft then c else None | Some true -> begin match c with | None -> error KeepAndClearModifierOnlyForHypotheses | Some id -> Some id end | Some false -> None in match doclear with | None -> Proofview.tclUNIT () | Some id -> clear [id] (* Moving hypotheses *) let move_hyp id dest = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let ty = Proofview.Goal.concl gl in let sign = named_context_val env in let sign' = move_hyp_in_named_context env sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_evar env sigma ty in sigma, ev, Some (fst @@ destEvar sigma ev) end end (* Renaming hypotheses *) let rename_hyp repl = let fold accu (src, dst) = match accu with | None -> None | Some (srcs, dsts) -> if Id.Set.mem src srcs then None else if Id.Set.mem dst dsts then None else let srcs = Id.Set.add src srcs in let dsts = Id.Set.add dst dsts in Some (srcs, dsts) in let init = Some (Id.Set.empty, Id.Set.empty) in let dom = List.fold_left fold init repl in match dom with | None -> let info = Exninfo.reify () in Tacticals.tclZEROMSG ~info (str "Not a one-to-one name mapping") | Some (src, dst) -> Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sign = named_context_val env in let sigma = Proofview.Goal.sigma gl in let relevance = Proofview.Goal.relevance gl in (* Check that we do not mess variables *) let vars = ids_of_named_context_val sign in let () = if not (Id.Set.subset src vars) then let hyp = Id.Set.choose (Id.Set.diff src vars) in raise (RefinerError (env, sigma, NoSuchHyp hyp)) in let mods = Id.Set.diff vars src in let () = try let elt = Id.Set.choose (Id.Set.inter dst mods) in error (AlreadyUsed elt) with Not_found -> () in (* All is well *) let make_subst (src, dst) = (src, mkVar dst) in let subst = List.map make_subst repl in let subst c = Vars.replace_vars sigma subst c in let replace id = try List.assoc_f Id.equal id repl with Not_found -> id in let map decl = decl |> NamedDecl.map_id replace |> NamedDecl.map_constr subst in let ohyps = named_context_of_val sign in let nhyps = List.map map ohyps in let nconcl = subst concl in let nctx = val_of_named_context nhyps in let fold odecl ndecl accu = if Id.equal (NamedDecl.get_id odecl) (NamedDecl.get_id ndecl) then SList.default accu else SList.cons (mkVar @@ NamedDecl.get_id odecl) accu in let instance = List.fold_right2 fold ohyps nhyps SList.empty in Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_pure_evar nctx sigma ~relevance nconcl in sigma, mkEvar (ev, instance), Some ev end end (**************************************************************) (* Fresh names *) (**************************************************************) let fresh_id_in_env avoid id env = let avoid' = ids_of_named_context_val (named_context_val env) in let avoid = if Id.Set.is_empty avoid then avoid' else Id.Set.union avoid' avoid in next_ident_away_in_goal (Global.env ()) id avoid let new_fresh_id avoid id gl = fresh_id_in_env avoid id (Proofview.Goal.env gl) let id_of_name_with_default id = function | Anonymous -> id | Name id -> id let default_id_of_sort sigma s = if ESorts.is_small sigma s then default_small_ident else default_type_ident let default_id env sigma decl = let open Context.Rel.Declaration in match decl with | LocalAssum (name,t) -> let dft = default_id_of_sort sigma (Retyping.get_sort_of env sigma t) in id_of_name_with_default dft name.binder_name | LocalDef (name,b,_) -> id_of_name_using_hdchar env sigma b name.binder_name (* Non primitive introduction tactics are treated by intro_then_gen There is possibly renaming, with possibly names to avoid and possibly a move to do after the introduction *) type name_flag = | NamingAvoid of Id.Set.t | NamingBasedOn of Id.t * Id.Set.t | NamingMustBe of lident let naming_of_name = function | Anonymous -> NamingAvoid Id.Set.empty | Name id -> NamingMustBe (CAst.make id) let find_name mayrepl decl naming gl = match naming with | NamingAvoid idl -> (* this case must be compatible with [find_intro_names] below. *) let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe {CAst.loc;v=id} -> (* When name is given, we allow to hide a global name *) let ids_of_hyps = Tacmach.pf_ids_set_of_hyps gl in if not mayrepl && Id.Set.mem id ids_of_hyps then error ?loc (AlreadyUsed id); id (**************************************************************) (* Computing position of hypotheses for replacing *) (**************************************************************) let get_next_hyp_position env sigma id = let rec aux = function | [] -> error_no_such_hypothesis env sigma id | decl :: right -> if Id.equal (NamedDecl.get_id decl) id then match right with decl::_ -> MoveBefore (NamedDecl.get_id decl) | [] -> MoveFirst else aux right in aux let get_previous_hyp_position env sigma id = let rec aux dest = function | [] -> error_no_such_hypothesis env sigma id | decl :: right -> let hyp = NamedDecl.get_id decl in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in aux MoveLast (**************************************************************) (* Cut rule *) (**************************************************************) let clear_hyps2 env sigma ids sign t cl = try Evarutil.clear_hyps2_in_evi env sigma sign t cl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> error_replacing_dependency env sigma id err inglobal let internal_cut ?(check=true) replace id t = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let concl = Proofview.Goal.concl gl in let sign = named_context_val env in let r = Retyping.relevance_of_type env sigma t in let env',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t conc let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t Environ.reset_with_named_context sign' env,t,concl,sigma else (if check && mem_named_context_val id sign then error (IntroAlreadyDeclared id); push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine_with_principal ~typecheck:false begin fun sigma -> let (sigma, ev) = Evarutil.new_evar env sigma nf_t in let (sigma, ev') = Evarutil.new_evar env' sigma concl in let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var sigma id ev') in (sigma, term, Some (fst @@ destEvar sigma ev')) end) end let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in Tacticals.tclTHENLAST (internal_cut b id t) (tac id) end let assert_before_gen b naming t = assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ()) let assert_before na = assert_before_gen false (naming_of_name na) let assert_before_replacing id = assert_before_gen true (NamingMustBe (CAst.make id)) let replace_error_option err tac = match err with | None -> tac | Some (e, info) -> Proofview.tclORELSE tac (fun _ -> Proofview.tclZERO ~info e) let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let id = find_name b (LocalAssum (make_annot Anonymous Sorts.Relevant,t)) naming gl in Tacticals.tclTHENFIRST (internal_cut b id t <*> Proofview.cycle 1) (tac id) end let assert_after_gen b naming t = assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ())) let assert_after na = assert_after_gen false (naming_of_name na) let assert_after_replacing id = assert_after_gen true (NamingMustBe (CAst.make id)) (**************************************************************) (* Fixpoints and CoFixpoints *) (**************************************************************) let rec mk_holes env sigma = function | [] -> (sigma, []) | arg :: rem -> let (sigma, arg) = Evarutil.new_evar env sigma arg in let (sigma, rem) = mk_holes env sigma rem in (sigma, arg :: rem) let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) wit | Prod (na, c1, b) -> if Int.equal k 1 then try ignore (find_inductive env sigma c1) with Not_found -> error FixpointOnNonInductiveType else let open Context.Rel.Declaration in check_mutind (push_rel (LocalAssum (na, c1)) env) sigma (pred k) b | LetIn (na, c1, t, b) -> let open Context.Rel.Declaration in check_mutind (push_rel (LocalDef (na, c1, t)) env) sigma k b | _ -> error NotEnoughProducts (* Refine as a fixpoint *) let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let concl = Proofview.Goal.concl gl in let () = check_mutind env sigma n concl in let firsts, lasts = List.chop j rest in let all = firsts @ (f, n, concl) :: lasts in let all = List.map (fun (f, n, ar) -> let r = Retyping.relevance_of_type env sigma ar in (f, r, n, ar)) all in let rec mk_sign sign = function | [] -> sign | (f, r, n, ar) :: oth -> let open Context.Named.Declaration in let () = check_mutind env sigma n ar in if mem_named_context_val f sign then error (IntroAlreadyDeclared f); mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine ~typecheck:false begin fun sigma -> let (sigma, evs) = mk_holes nenv sigma (List.map (fun (_,_,_,ar) -> ar) all) in let ids, rs, _, ars = List.split4 all in let evs = List.map (Vars.subst_vars sigma (List.rev ids)) evs in let indxs = Array.of_list (List.map (fun n -> n-1) (List.map (fun (_,_,n,_) -> n) all)) in let funnames = Array.of_list (List.map2 (fun i r -> make_annot (Name i) r) ids rs) in let bodies = Array.of_list evs in let typarray = Array.of_list ars in let oterm = mkFix ((indxs,0),(funnames,typarray,bodies)) in (sigma, oterm) end end let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in match EConstr.kind sigma b with | Prod (na, c1, b) -> let open Context.Rel.Declaration in check_is_mutcoind (push_rel (LocalAssum (na,c1)) env) sigma b | _ -> try let _ = find_coinductive env sigma b in () with Not_found -> error AllMethodsInCoinductiveType (* Refine as a cofixpoint *) let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let concl = Proofview.Goal.concl gl in let firsts,lasts = List.chop j others in let all = firsts @ (f, concl) :: lasts in List.iter (fun (_, c) -> check_is_mutcoind env sigma c) all; let all = List.map (fun (id,t) -> (id, Retyping.relevance_of_type env sigma t, t)) all in let rec mk_sign sign = function | [] -> sign | (f, r, ar) :: oth -> let open Context.Named.Declaration in if mem_named_context_val f sign then error (AlreadyUsed f); mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine ~typecheck:false begin fun sigma -> let (ids, rs, types) = List.split3 all in let (sigma, evs) = mk_holes nenv sigma types in let evs = List.map (Vars.subst_vars sigma (List.rev ids)) evs in (* TODO relevance *) let funnames = Array.of_list (List.map2 (fun i r -> make_annot (Name i) r) ids rs) in let typarray = Array.of_list types in let bodies = Array.of_list evs in let oterm = mkCoFix (0, (funnames, typarray, bodies)) in (sigma, oterm) end end let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) (**************************************************************) type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function let[@ocaml.inline] (let*) m f = match m with | NoChange -> NoChange | Changed v -> f v let e_pf_change_decl (redfun : bool -> Tacred.change_function) where env sigma decl = let open Context.Named.Declaration in match decl with | LocalAssum (id,ty) -> let () = if where == InHypValueOnly then error (VariableHasNoValue id.binder_name) in let* (sigma, ty') = redfun false env sigma ty in Changed (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> let (sigma, b') = if where != InHypTypeOnly then match redfun true env sigma b with | NoChange -> (sigma, NoChange) | Changed (sigma, b') -> (sigma, Changed b') else (sigma, NoChange) in let (sigma, ty') = if where != InHypValueOnly then match redfun false env sigma ty with | NoChange -> (sigma, NoChange) | Changed (sigma, ty') -> (sigma, Changed ty') else (sigma, NoChange) in match b', ty' with | NoChange, NoChange -> NoChange | Changed b', NoChange -> Changed (sigma, LocalDef (id, b', ty)) | NoChange, Changed ty' -> Changed (sigma, LocalDef (id, b, ty')) | Changed b', Changed ty' -> Changed (sigma, LocalDef (id, b', ty')) let bind_change_occurrences occs = function | None -> None | Some c -> Some (Redexpr.out_with_occurrences (occs,c)) (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a certain hypothesis *) (** Tactic reduction modulo evars (for universes essentially) *) let e_change_in_concl ~cast ~check (redfun, sty) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in match redfun (Tacmach.pf_env gl) sigma (Tacmach.pf_concl gl) with | NoChange -> Proofview.tclUNIT () | Changed (sigma, c') -> Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_concl ~cast ~check c' sty) end let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.pf_get_hyp id gl in match e_pf_change_decl redfun where (Proofview.Goal.env gl) sigma hyp with | NoChange -> Proofview.tclUNIT () | Changed (sigma, c) -> Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp ~check ~reorder c) end let e_change_option ~check ~reorder (redfun, sty) = function | None -> e_change_in_concl ~cast:true ~check (redfun, sty) | Some id -> let redfun _ env sigma c = redfun env sigma c in e_change_in_hyp ~check ~reorder redfun id type hyp_conversion = | AnyHypConv (** Arbitrary conversion *) | StableHypConv (** Does not introduce new dependencies on variables *) | LocalHypConv (** Same as above plus no dependence on the named environment *) let e_change_in_hyps ~check ~reorder f args = match args with | [] -> Proofview.tclUNIT () | _ :: _ -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let (env, sigma) = match reorder with | LocalHypConv -> (* If the reduction function is known not to depend on the named context, then we can perform it in parallel. *) let fold accu arg = let (id, redfun) = f arg in let old = try Id.Map.find id accu with Not_found -> [] in Id.Map.add id (redfun :: old) accu in let reds = List.fold_left fold Id.Map.empty args in let evdref = ref sigma in let map d = let id = NamedDecl.get_id d in match Id.Map.find id reds with | reds -> let d = EConstr.of_named_decl d in let fold redfun (sigma, d) = match redfun env sigma d with | NoChange -> sigma, d | Changed (sigma, d) -> sigma, d in let (sigma, d) = List.fold_right fold reds (sigma, d) in let () = evdref := sigma in EConstr.Unsafe.to_named_decl d | exception Not_found -> d in let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in (env, !evdref) | StableHypConv | AnyHypConv -> let reorder = reorder == AnyHypConv in let fold (env, sigma) arg = let (id, redfun) = f arg in let hyp = try lookup_named id env with Not_found -> raise (RefinerError (env, sigma, NoSuchHyp id)) in match redfun env sigma hyp with | NoChange -> (env, sigma) | Changed (sigma, d) -> let sign = Logic.convert_hyp ~check ~reorder env sigma d in let env = reset_with_named_context sign env in (env, sigma) in List.fold_left fold (env, sigma) args in let ty = Proofview.Goal.concl gl in Proofview.Unsafe.tclEVARS sigma <*> Refine.refine_with_principal ~typecheck:false begin fun sigma -> let sigma, ev = Evarutil.new_evar env sigma ty in sigma, ev, Some (fst @@ destEvar sigma ev) end end let e_reduct_in_concl ~cast ~check (redfun, sty) = let redfun env sigma c = Changed (redfun env sigma c) in e_change_in_concl ~cast ~check (redfun, sty) let reduct_in_concl ~cast ~check (redfun, sty) = let redfun env sigma c = Changed (sigma, redfun env sigma c) in e_change_in_concl ~cast ~check (redfun, sty) let e_reduct_in_hyp ~check ~reorder redfun (id, where) = let redfun _ env sigma c = Changed (redfun env sigma c) in e_change_in_hyp ~check ~reorder redfun (id, where) let reduct_in_hyp ~check ~reorder redfun (id, where) = let redfun _ env sigma c = Changed (sigma, redfun env sigma c) in e_change_in_hyp ~check ~reorder redfun (id, where) let e_reduct_option ~check redfun = function | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id | None -> e_reduct_in_concl ~cast:true ~check redfun let reduct_option ~check (redfun, sty) where = let redfun env sigma c = (sigma, redfun env sigma c) in e_reduct_option ~check (redfun, sty) where type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> (evar_map * EConstr.constr) Tac let make_change_arg c pats env sigma = Changed (sigma, replace_vars sigma (Id.Map.bindings pats) c) (* TODO: fast-path *) let is_partial_template_head env sigma c = let (hd, args) = decompose_app sigma c in match destRef sigma hd with | (ConstructRef (ind, _) | IndRef ind), _ -> let (mib, _) = Inductive.lookup_mind_specif env ind in begin match mib.mind_template with | None -> false | Some _ -> Array.length args < mib.mind_nparams end | (VarRef _ | ConstRef _), _ -> false | exception DestKO -> false let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in if deep then begin let () = (* When changing a partially applied template term in a context, one must be careful to resynthetize the constraints as the implicit levels from the arguments are not written in the term. *) if is_partial_template_head env sigma newc || is_partial_template_head env sigma origc then mayneedglobalcheck := true in let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in match infer_conv ~pb:Conversion.CUMUL env sigma t1 t2 with | None -> if isSort sigma (whd_all env sigma t1) && isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else error (ConvertIncompatibleTypes (env,sigma,t2,t1)) | Some sigma -> sigma end else if not (isSort sigma (whd_all env sigma t1)) then error ConvertNotAType else sigma (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = match t env sigma with | NoChange -> NoChange | Changed (sigma, t') -> let sigma = check_types env sigma mayneedglobalcheck deep t' c in match infer_conv ~pb:cv_pb env sigma t' c with | None -> error NotConvertible | Some sigma -> Changed (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm ~check cv_pb deep t where env sigma c = let mayneedglobalcheck = ref false in let ans = match where with | None -> if check then change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c else t Id.Map.empty env sigma | Some occl -> e_contextually false occl (fun subst -> if check then change_and_check Conversion.CONV mayneedglobalcheck true (t subst) else fun env sigma _c -> t subst env sigma) env sigma c in match ans with | NoChange -> NoChange | Changed (sigma, c) -> let sigma = if !mayneedglobalcheck then begin try fst (Typing.type_of env sigma c) with e when noncritical e -> error (ReplacementIllTyped e) end else sigma in Changed (sigma, c) let change_in_concl ~check occl t = (* No need to check in e_change_in_concl, the check is done in change_on_subterm *) e_change_in_concl ~cast:false ~check:false ((change_on_subterm ~check Conversion.CUMUL false t occl),DEFAULTcast) let change_in_hyp ~check occl t id = (* Same as above *) e_change_in_hyp ~check:false ~reorder:check (fun x -> change_on_subterm ~check Conversion let concrete_clause_of enum_hyps cl = match cl.onhyps with | None -> let f id = (id, AllOccurrences, InHyp) in List.map f (enum_hyps ()) | Some l -> List.map (fun ((occs, id), w) -> (id, occs, w)) l let change ~check chg c cls = Proofview.Goal.enter begin fun gl -> let hyps = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in begin match cls.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> change_in_concl ~check (bind_change_occurrences occs chg) c end <*> let f (id, occs, where) = let occl = bind_change_occurrences occs chg in let redfun deep env sigma t = change_on_subterm ~check Conversion.CONV deep c occl env sigma t i let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) in let reorder = if check then AnyHypConv else StableHypConv in (* Don't check, we do it already in [change_on_subterm] *) e_change_in_hyps ~check:false ~reorder f hyps end let change_concl t = change_in_concl ~check:true None (make_change_arg t) let red_product_exn env sigma c = match red_product env sigma c with | None -> user_err Pp.(str "No head constant to reduce.") | Some c -> c (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl ~cast:true ~check:false (red_product_exn,DEFAULTcas let red_in_hyp = reduct_in_hyp ~check:false ~reorder:false red_product_exn let red_option = reduct_option ~check:false (red_product_exn,DEFAULTcast) let hnf_in_concl = reduct_in_concl ~cast:true ~check:false (hnf_constr,DEFAULTcast) let hnf_in_hyp = reduct_in_hyp ~check:false ~reorder:false hnf_constr let hnf_option = reduct_option ~check:false (hnf_constr,DEFAULTcast) let simpl_in_concl = reduct_in_concl ~cast:true ~check:false (simpl,DEFAULTcast) let simpl_in_hyp = reduct_in_hyp ~check:false ~reorder:false simpl let simpl_option = reduct_option ~check:false (simpl,DEFAULTcast) let normalise_in_concl = reduct_in_concl ~cast:true ~check:false (compute,DEFAULTcast) let normalise_in_hyp = reduct_in_hyp ~check:false ~reorder:false compute let normalise_option = reduct_option ~check:false (compute,DEFAULTcast) let normalise_vm_in_concl = reduct_in_concl ~cast:true ~check:false (Redexpr.cbv_vm,VM let unfold_in_concl loccname = reduct_in_concl ~cast:true ~check:false (unfoldn loccname let unfold_in_hyp loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname let unfold_option loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast) let pattern_option l = e_change_option ~check:false ~reorder:false (pattern_occs l,DEFAU (* The main reduction function *) let is_local_flag env flags = if flags.rDelta then false else let check = function | Evaluable.EvalVarRef _ -> false | Evaluable.EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.Const | Evaluable.EvalProjectionRef c -> false (* FIXME *) in List.for_all check flags.rConst let is_local_unfold env flags = let check (_, c) = match c with | Evaluable.EvalVarRef _ -> false | Evaluable.EvalConstRef c -> Id.Set.is_empty (Environ.vars_of_global env (GlobRef.Const | Evaluable.EvalProjectionRef c -> false (* FIXME *) in List.for_all check flags let change_of_red_expr_val ?occs redexp = let (redfun, kind) = Redexpr.reduction_of_red_expr_val ?occs redexp in let redfun env sigma c = Changed (redfun env sigma c) in (* TODO: fast-path *) (redfun, kind) let reduce redexp cl = let trace env sigma = let open Printer in let pr = ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference, pr_ Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp)) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let hyps = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in let reorder = match redexp with | Fold _ | Pattern _ -> AnyHypConv | Simpl (flags, _) | Cbv flags | Cbn flags | Lazy flags -> if is_local_flag env flags then LocalHypConv else StableHypConv | Unfold flags -> if is_local_unfold env flags then LocalHypConv else StableHypConv | Red | Hnf | CbvVm _ | CbvNative _ -> StableHypConv | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) in let redexp = Redexpr.eval_red_expr env redexp in Proofview.Trace.name_tactic (fun () -> trace env sigma) begin begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> let occs = Redexpr.out_occurrences occs in let redfun = change_of_red_expr_val ~occs:(occs, nbcl) redexp in e_change_in_concl ~cast:true ~check redfun end <*> let f (id, occs, where) = let occs = Redexpr.out_occurrences occs in let (redfun, _) = change_of_red_expr_val ~occs:(occs, nbcl) redexp in let redfun _ env sigma c = redfun env sigma c in let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) in e_change_in_hyps ~check ~reorder f hyps end end (* Unfolding occurrences of a constant *) let unfold_constr = function | GlobRef.ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp] | GlobRef.VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id] | _ -> error NotUnfoldable (*******************************************) (* Introduction tactics *) (*******************************************) (* Returns the names that would be created by intros, without doing intros. This function is supposed to be compatible with an iteration of [find_name] above. As [default_id] checks the sort of the type to build hyp names, we maintain an environment to be able to type dependent hyps. *) let find_intro_names env0 sigma ctxt = let _, res, _ = List.fold_right (fun decl acc -> let env,idl,avoid = acc in let name = fresh_id_in_env avoid (default_id env sigma decl) env0 in let newenv = push_rel decl env in (newenv, name :: idl, Id.Set.add name avoid)) ctxt (env0, [], Id.Set.empty) in List.rev res let build_intro_tac id dest tac = match dest with | MoveLast -> Tacticals.tclTHEN (introduction id) (tac id) | dest -> Tacticals.tclTHENLIST [introduction id; move_hyp id dest; tac id] let rec intro_then_gen name_flag move_flag ~force ~dep tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.project gl in let env = Tacmach.pf_env gl in let concl = Proofview.Goal.concl gl in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep || not (noccurn sigma 1 u) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in build_intro_tac name move_flag tac | LetIn (name,b,t,u) when not dep || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | Evar ev when force -> let name = find_name false (LocalAssum (anonR,concl)) name_flag gl in let sigma, t = Evardefine.define_evar_as_product env sigma ~name ev in Tacticals.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (intro_then_gen name_flag move_flag ~force ~dep tac) | _ -> begin if not force then let info = Exninfo.reify () in Proofview.tclZERO ~info (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) (* this since at least V6.3 (a pity *) (* that intro do betaiotazeta only when reduction is needed; and *) (* probably also a pity that intro does zeta *) else Proofview.tclUNIT () end <*> Proofview.tclORELSE (Tacticals.tclTHEN hnf_in_concl (intro_then_gen name_flag move_flag ~force:false ~dep tac)) begin function (e, info) -> match e with | RefinerError (env, sigma, IntroNeedsProduct) -> Tacticals.tclZEROMSG ~info (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end end let drop_intro_name (_ : Id.t) = Proofview.tclUNIT () let intro_gen n m ~force ~dep = intro_then_gen n m ~force ~dep drop_intro_name let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast ~force:true ~ let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast ~for let intro_using id = intro_using_then id drop_intro_name let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast ~force:false ~dep:fa let intro = intro_then drop_intro_name let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast ~force:true ~dep:false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast ~force:false ~dep:false let intro_move_avoid idopt avoid hto = match idopt with | None -> intro_gen (NamingAvoid avoid) hto ~force:true ~dep:false | Some id -> intro_gen (NamingMustBe (CAst.make id)) hto ~force:true ~dep:false let intro_move idopt hto = intro_move_avoid idopt Id.Set.empty hto (**** Multiple introduction tactics ****) let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.tclTHEN (intro_using str) (intros_using l) let rec intros_mustbe_force = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.tclTHEN (intro_mustbe_force str) (intros_mustbe_force l) let rec intros_using_then_helper tac acc = function | [] -> tac (List.rev acc) | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l let intros_using_then l tac = intros_using_then_helper tac [] l let is_overbound bound n = match bound with None -> false | Some p -> n >= p let intro_forthcoming_last_then_gen avoid dep_flag bound n tac = let open RelDecl in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in let relevance = Proofview.Goal.relevance gl in let avoid = let avoid' = ids_of_named_context_val (named_context_val env) in if Id.Set.is_empty avoid then avoid' else Id.Set.union avoid' avoid in let rec decompose env avoid n concl subst decls ndecls = let decl = if is_overbound bound n then None else match EConstr.kind sigma concl with | Prod (na, t, u) when not dep_flag || not (noccurn sigma 1 u) -> Some (LocalAssum (na, t), u) | LetIn (na, b, t, u) when not dep_flag || not (noccurn sigma 1 u) -> Some (LocalDef (na, b, t), u) | _ -> None in match decl with | None -> ndecls, decls, Vars.esubst Vars.lift_substituend subst concl | Some (decl, concl) -> let id = default_id env sigma decl in let id = next_ident_away_in_goal (Global.env ()) id avoid in let avoid = Id.Set.add id avoid in let env = EConstr.push_rel decl env in let ndecl = NamedDecl.of_rel_decl (fun _ -> id) decl in let ndecl = NamedDecl.map_constr (fun c -> Vars.esubst Vars.lift_substituend subst c) ndecl i let subst = Esubst.subs_cons (make_substituend @@ mkVar id) subst in decompose env avoid (n + 1) concl subst (decl :: decls) (ndecl :: ndecls) in let (ndecls, decls, nconcl) = decompose env avoid n concl (Esubst.subs_id 0) [] [] in let ids = List.map NamedDecl.get_id ndecls in if List.is_empty ids then tac [] else Refine.refine_with_principal ~typecheck:false begin fun sigma -> let ctx = named_context_val env in let nctx = List.fold_right push_named_context_val ndecls ctx in let inst = SList.defaultn (List.length @@ Environ.named_context env) SList.empty in let rels = List.init (List.length decls) (fun i -> mkRel (i + 1)) in let ninst = List.fold_right (fun c accu -> SList.cons c accu) rels inst in let (sigma, ev) = new_pure_evar nctx sigma ~relevance nconcl in (sigma, it_mkLambda_or_LetIn (mkEvar (ev, ninst)) decls, Some ev) end <*> tac ids end let intros = intro_forthcoming_last_then_gen Id.Set.empty false None 0 (fun _ -> tclIDTAC) let intro_forthcoming_then_gen avoid move_flag ~dep bound n tac = match move_flag with | MoveLast -> (* Fast path *) intro_forthcoming_last_then_gen avoid dep bound n tac | MoveFirst | MoveAfter _ | MoveBefore _ -> let rec aux n ids = (* Note: we always use the bound when there is one for "*" and "**" *) if not (is_overbound bound n) then Proofview.tclORELSE begin intro_then_gen (NamingAvoid avoid) move_flag ~force:false ~dep (fun id -> aux (n+1) (id::ids)) end begin function (e, info) -> match e with | RefinerError (env, sigma, IntroNeedsProduct) -> tac ids | e -> Proofview.tclZERO ~info e end else tac ids in aux n [] let intro_replacing id = Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps gl in let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.tclTHENLIST [ clear_for_replacing [id]; introduction id; move_hyp id next_hyp; ] end (* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to reintroduce y, y,' y''. Note that we have to clear y, y' and y'' before introducing y because y' or y'' can e.g. depend on old y. *) (* This version assumes that replacement is actually possible *) (* (ids given in the introduction order) *) (* We keep a sub-optimality in cleaing for compatibility with *) (* the behavior of inversion *) let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in let hyps = Proofview.Goal.hyps gl in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (clear_for_replacing [id])) (if suboptimal then ids else List.rev ids)) (Tacticals.tclMAP (fun (id,pos) -> Tacticals.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) end (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in let env, sigma = Proofview.Goal.(env gl, sigma gl) in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.tclTHEN (clear_for_replacing ids) (Tacticals.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) end (* The standard for implementing Automatic Introduction *) let auto_intros_tac ids = let fold used = function | Name id -> Id.Set.add id used | Anonymous -> used in let avoid = NamingAvoid (List.fold_left fold Id.Set.empty ids) in let naming = function | Name id -> NamingMustBe CAst.(make id) | Anonymous -> avoid in Tacticals.tclMAP (fun name -> intro_gen (naming name) MoveLast ~force:true ~dep:false) (Lis (* User-level introduction tactics *) let lookup_hypothesis_as_renamed env sigma ccl = function | AnonHyp n -> Detyping.lookup_index_as_renamed env sigma ccl n | NamedHyp id -> Detyping.lookup_name_as_displayed env sigma ccl id.CAst.v let lookup_hypothesis_as_renamed_gen red h gl = let env = Proofview.Goal.env gl in let rec aux ccl = match lookup_hypothesis_as_renamed env (Tacmach.project gl) ccl h with | None when red -> begin match red_product env (Proofview.Goal.sigma gl) ccl with | None -> None | Some c -> aux c end | x -> x in aux (Proofview.Goal.concl gl) let is_quantified_hypothesis id gl = match lookup_hypothesis_as_renamed_gen false (NamedHyp (CAst.make id)) gl with | Some _ -> true | None -> false let warn_deprecated_intros_until_0 = CWarnings.create ~name:"deprecated-intros-until-0" ~category:CWarnings.CoreCategor (fun () -> strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\ let depth_of_quantified_hypothesis red h gl = if h = AnonHyp 0 then warn_deprecated_intros_until_0 (); match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> error (NoQuantifiedHypothesis(h,red)) let intros_until_gen red h = Proofview.Goal.enter begin fun gl -> let n = depth_of_quantified_hypothesis red h gl in Tacticals.tclDO n (if red then introf else intro) end let intros_until_id id = intros_until_gen false (NamedHyp (CAst.make id)) let intros_until_n_gen red n = intros_until_gen red (AnonHyp n) let intros_until = intros_until_gen true let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = Proofview.Goal.enter begin fun gl -> let _ = Tacmach.pf_get_hyp id gl in Proofview.tclUNIT () end let try_intros_until_id_check id = Tacticals.tclORELSE (intros_until_id id) (tclCHECKVAR id) let try_intros_until tac = function | NamedHyp {CAst.v=id} -> Tacticals.tclTHEN (try_intros_until_id_check id) (tac id) | AnonHyp n -> Tacticals.tclTHEN (intros_until_n n) (Tacticals.onLastHypId tac) let rec intros_move = function | [] -> Proofview.tclUNIT () | (hyp,destopt) :: rest -> Tacticals.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt ~force:false ~dep:f (intros_move rest) (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) let tactic_infer_flags with_evar = Pretyping.{ use_coercions = true; use_typeclasses = UseTC; solve_unification_constraints = true; fail_evar = not with_evar; expand_evars = true; program_mode = false; polymorphic = false; undeclared_evars_patvars = false; patvars_abstract = false; unconstrained_sorts = false; } type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) type 'a core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = clear_flag * 'a core_destruction_arg let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> tac clear_flag cbl | clear_flag,ElimOnAnonHyp n -> Tacticals.tclTHEN (intros_until_n n) (Tacticals.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.tclTHEN (try_intros_until_id_check id) (tac clear_flag (mkVar id,NoBindings)) let map_destruction_arg f sigma = function | clear_flag,ElimOnConstr g -> let sigma,x = f sigma g in (sigma, (clear_flag,ElimOnConstr x)) | clear_flag,ElimOnAnonHyp n as x -> (sigma,x) | clear_flag,ElimOnIdent id as x -> (sigma,x) let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (p let sigma = Pretyping.solve_remaining_evars flags env current_sigma ?initial:pending in (sigma, nf_evar sigma c) let finish_delayed_evar_resolution with_evars env sigma f = let (sigma', (c, lbind)) = f env sigma in let flags = tactic_infer_flags with_evars in let (sigma', c) = finish_evar_resolution ~flags env sigma' (Some sigma,c) in (sigma', (c, lbind)) let force_destruction_arg with_evars env sigma c = map_destruction_arg (finish_delayed_evar_resolution with_evars env) sigma c (****************************************) (* tactic "cut" (actually modus ponens) *) (****************************************) let cut c = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let concl = Proofview.Goal.concl gl in (* Backward compat: ensure that [c] is well-typed. Plus we need to know the relevance *) match Typing.sort_of env sigma c with | exception e when noncritical e -> let _, info = Exninfo.capture e in Tacticals.tclZEROMSG ~info (str "Not a proposition or a type.") | sigma, s -> let r = ESorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.pf_ids_set_of_hyps gl) in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine_with_principal ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar env h (mkArrow c r concl) in let ev = fst @@ destEvar h f in let (h, x) = Evarutil.new_evar env h c in let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (f, [|mkRel 1|])) in (h, f, Some ev) end) end let check_unresolved_evars_of_metas sigma clenv = (* This checks that Metas turned into Evars by *) (* Refiner.pose_all_metas_as_evars are resolved *) let metas = clenv_meta_list clenv in let iter mv () = match Unification.Meta.meta_opt_fvalue metas mv with | Some c -> begin match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with | Evar (evk,_) when Evd.is_undefined (clenv_evd clenv) evk && not (Evd.mem sigma evk) -> let na = Unification.Meta.meta_name metas mv in let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") in error (CannotFindInstance id) | _ -> () end | None -> () in Unification.Meta.fold iter metas () let do_replace id = function | NamingMustBe {CAst.v=id'} when Option.equal Id.equal id (Some id') -> true | _ -> false (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last ones (resp [n] first ones if [sidecond_first] is [true]) being the [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) let clenv_refine_in with_evars targetid replace env sigma0 clenv = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) env (clenv_evd clenv) in let clenv = Clenv.update_clenv_evd clenv evd (Clenv.clenv_meta_list clenv) in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; let [@ocaml.warning "-3"] exact_tac = Clenv.Internal.refiner clenv in let naming = NamingMustBe (CAst.make targetid) in Proofview.Unsafe.tclEVARS evd <*> Proofview.Goal.enter begin fun gl -> let id = find_name replace (LocalAssum (make_annot Anonymous Sorts.Relevant, new_hyp_typ) Tacticals.tclTHENLAST (internal_cut replace id new_hyp_typ <*> Proofview.cycle 1) exact_ta end (********************************************) (* Elimination tactics *) (********************************************) let nth_arg i c = match i with | None -> List.last c | Some i -> List.nth c i let index_of_ind_arg sigma t = let rec aux i j t = match EConstr.kind sigma t with | LetIn (_, _, _, t) -> aux i j t | Prod (_,t,u) -> (* heuristic *) if isInd sigma (fst (decompose_app sigma t)) then aux (Some j) (j+1) u else aux i (j+1) u | _ -> match i with | Some i -> i | None -> error CannotFindInductiveArgument in aux None 0 t (* * Elimination tactic with bindings and using an arbitrary * elimination constant called elimc. This constant should end * with a clause (x:I)(P .. ), where P is a bound variable. * The term c is of type t, which is a product ending with a type * matching I, lbindc are the expected terms for c arguments *) type eliminator = | ElimConstant of (Constant.t * EInstance.t) (* Constant generated by a scheme function *) | ElimClause of EConstr.constr with_bindings (* Arbitrary expression provided by the user *) let general_elim_clause0 with_evars flags (submetas, c, ty) elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let clause, bindings, index = match elim with | ElimConstant cst -> let elimc = mkConstU cst in let elimt = Retyping.get_type_of env sigma elimc in let i = index_of_ind_arg sigma elimt in (elimc, elimt), NoBindings, Some i | ElimClause (elimc, lbindelimc) -> let elimt = Retyping.get_type_of env sigma elimc in (elimc, elimt), lbindelimc, None in let elimclause = make_clenv_binding env sigma clause bindings in let indmv = try nth_arg index (clenv_arguments elimclause) with Failure _ | Invalid_argument _ -> error IllFormedEliminationType in let elimclause = clenv_instantiate ~flags ~submetas indmv elimclause (c, ty) in Clenv.res_pf elimclause ~with_evars ~with_classes:true ~flags end let general_elim_clause_in0 with_evars flags id (submetas, c, ty) elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let elimc = mkConstU elim in let elimt = Retyping.get_type_of env sigma elimc in let i = index_of_ind_arg sigma elimt in let elimclause = mk_clenv_from env sigma (elimc, elimt) in let indmv = try nth_arg (Some i) (clenv_arguments elimclause) with Failure _ | Invalid_argument _ -> error IllFormedEliminationType in (* Assumes that the metas of [c] are part of [sigma] already *) let hypmv = match List.remove Int.equal indmv (clenv_independent elimclause) with | [a] -> a | _ -> error IllFormedEliminationType in let elimclause = clenv_instantiate ~flags ~submetas indmv elimclause (c, ty) in let hyp = mkVar id in let hyp_typ = Retyping.get_type_of env sigma hyp in let elimclause = try clenv_instantiate ~flags hypmv elimclause (hyp, hyp_typ) with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) in let new_hyp_typ = clenv_type elimclause in if EConstr.eq_constr sigma hyp_typ new_hyp_typ then error (NothingToRewrite id); clenv_refine_in with_evars id true env sigma elimclause end let general_elim with_evars clear_flag (c, lbindc) elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.project gl in let ct = Retyping.get_type_of env sigma c in let id = try Some (destVar sigma c) with DestKO -> None in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let indclause = make_clenv_binding env sigma (c, t) lbindc in let flags = elim_flags () in let metas = clenv_meta_list indclause in let submetas = (clenv_arguments indclause, metas) in Proofview.Unsafe.tclEVARS (clenv_evd indclause) <*> Tacticals.tclTHEN (general_elim_clause0 with_evars flags (submetas, c, clenv_type indclause) elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) id) end let general_elim_clause with_evars flags where arg elim = Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> let (sigma, (elim, u)) = Evd.fresh_constant_instance env sigma elim in Proofview.Unsafe.tclEVARS sigma <*> match where with --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28