|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Find_subterm
open Namegen
open Declarations
open Inductiveops
open Reductionops
open Globnames
open Evd
open Tacred
open Genredexpr
open Tacmach.New
open Logic
open Clenv
open Refiner
open Tacticals
open Hipattern
open Coqlib
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 inj_with_occurrences e = (AllOccurrences,e)
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
{ optdepr = false;
optname = "default clearing of hypotheses after use";
optkey = ["Default";"Clearing";"Used";"Hypotheses"];
optread = (fun () -> !clear_hyp_by_default) ;
optwrite = (fun b -> clear_hyp_by_default := b) }
(* Compatibility option useful in developments using apply intensively
in ltac code *)
let universal_lemma_under_conjunctions = ref false
let accept_universal_lemma_under_conjunctions () =
!universal_lemma_under_conjunctions
let () =
declare_bool_option
{ optdepr = false;
optname = "trivial unification in tactics applying under conjunctions";
optkey = ["Universal";"Lemma";"Under";"Conjunction"];
optread = (fun () -> !universal_lemma_under_conjunctions) ;
optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
(* The following boolean governs what "intros []" do on examples such
as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
if false, it behaves as "intro H; case H; clear H" for fresh H.
Kept as false for compatibility.
*)
let bracketing_last_or_and_intro_pattern = ref true
let use_bracketing_last_or_and_intro_pattern () =
!bracketing_last_or_and_intro_pattern
let () =
declare_bool_option
{ optdepr = true;
optname = "bracketing last or-and introduction pattern";
optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
optread = (fun () -> !bracketing_last_or_and_intro_pattern);
optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
(*********************************************)
(* Tactics *)
(*********************************************)
(******************************************)
(* Primitive tactics *)
(******************************************)
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
(sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
end
let introduction id =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.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
user_err ~hdr:"Tactics.introduction"
(str "Variable " ++ Id.print id ++ str " is already declared.")
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)) b
| LetIn (id0, c, t, b) -> unsafe_intro env (LocalDef ({id0 with binder_name=id}, c, t)) b
| _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
end
let error msg = CErrors.user_err Pp.(str msg)
let convert_concl ?(check=true) ty k =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let conclty = Proofview.Goal.concl gl in
Refine.refine ~typecheck:false begin fun sigma ->
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
match Reductionops.infer_conv env sigma ty conclty with
| None -> error "Not convertible."
| Some sigma -> sigma
end else sigma in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
(sigma, ans)
end
end
let convert_hyp ?(check=true) d =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
let sign = convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ty
end
end
let convert_concl_no_check = convert_concl ~check:false
let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
| Some sigma -> Proofview.Unsafe.tclEVARS sigma
| None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
| exception _ ->
(* FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
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 pp = clear_in_global_msg inglobal in
match err with
| Evarutil.OccurHypInSimpleClause None ->
Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
| Evarutil.NoCandidatesLeft ev ->
str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++
Printer.pr_existential_key sigma ev ++ str" without candidates."
let error_clear_dependency env sigma id err inglobal =
user_err (clear_dependency_msg env sigma id err inglobal)
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_existential env sigma ev ++ str"."
| Evarutil.NoCandidatesLeft ev ->
str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++
Printer.pr_existential_key sigma ev ++ str" without candidates."
let error_replacing_dependency env sigma id err inglobal =
user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him 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.New.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 ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
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 =
Proofview.tclEVARMAP >>= fun sigma ->
let check_isvar c =
if not (isVar sigma c) then
error "keep/clear modifiers apply only to hypothesis names." in
let doclear = match clear_flag with
| None -> dft && isVar sigma c
| Some true -> check_isvar c; true
| Some false -> false in
if doclear then clear [destVar sigma c]
else Tacticals.New.tclIDTAC
(* Moving hypotheses *)
let move_hyp id dest =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.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 ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ty
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 -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
| Some (src, dst) ->
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
(* Check that we do not mess variables *)
let fold accu decl = Id.Set.add (NamedDecl.get_id decl) accu in
let vars = List.fold_left fold Id.Set.empty hyps 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
CErrors.user_err (Id.print elt ++ str " is already used")
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 subst c in
let map decl =
decl |> NamedDecl.map_id (fun id -> try List.assoc_f Id.equal id repl with Not_found -> id)
|> NamedDecl.map_constr subst
in
let nhyps = List.map map hyps in
let nconcl = subst concl in
let nctx = val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
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 id avoid
let fresh_id avoid id gl =
fresh_id_in_env avoid id (pf_env gl)
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 s =
if Sorts.is_small 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 (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.New.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.New.pf_ids_set_of_hyps gl in
if not mayrepl && Id.Set.mem id ids_of_hyps then
user_err ?loc (Id.print id ++ str" is already used.");
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
let sigma = Evd.clear_metas sigma in
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_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.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 sign',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 concl in
let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
sign',t,concl,sigma
else
(if check && mem_named_context_val id sign then
user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
let nf_t = nf_betaiota env sigma t in
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
let (sigma,ev,ev') =
if dir then
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
(sigma,ev,ev')
else
let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
(sigma,ev,ev') in
let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
(sigma, term)
end)
end
let internal_cut ?(check=true) = internal_cut_gen ~check true
let internal_cut_rev ?(check=true) = internal_cut_gen ~check false
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.New.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 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.New.tclTHENFIRST
(internal_cut_rev b id t)
(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) with
| Prod (na, c1, b) ->
if Int.equal k 1 then
try
let ((sp, _), u), _ = find_inductive env sigma c1 in
(sp, u)
with Not_found -> error "Cannot do a fixpoint on a non inductive type."
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 "Not enough products."
(* 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.New.project gl in
let concl = Proofview.Goal.concl gl in
let (sp, u) = check_mutind env sigma n concl in
let firsts, lasts = List.chop j rest in
let all = firsts @ (f, n, concl) :: lasts in
let rec mk_sign sign = function
| [] -> sign
| (f, n, ar) :: oth ->
let open Context.Named.Declaration in
let (sp', u') = check_mutind env sigma n ar in
if not (MutInd.equal sp sp') then
error "Fixpoints should be on the same mutual inductive declaration.";
if mem_named_context_val f sign then
user_err ~hdr:"Logic.prim_refiner"
(str "Name " ++ Id.print f ++ str " already used in the environment");
mk_sign (push_named_context_val (LocalAssum (make_annot f Sorts.Relevant, 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 pi3 all) in
let ids = List.map pi1 all in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
(* TODO relevance *)
let funnames = Array.of_list (List.map (fun i -> make_annot (Name i) Sorts.Relevant) ids) in
let typarray = Array.of_list (List.map pi3 all) in
let bodies = Array.of_list evs 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 "All methods must construct elements in coinductive types."
(* 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.New.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 rec mk_sign sign = function
| [] -> sign
| (f, ar) :: oth ->
let open Context.Named.Declaration in
if mem_named_context_val f sign then
error "Name already used in the environment.";
mk_sign (push_named_context_val (LocalAssum (make_annot f Sorts.Relevant, 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, types) = List.split all in
let (sigma, evs) = mk_holes nenv sigma types in
let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
(* TODO relevance *)
let funnames = Array.of_list (List.map (fun i -> make_annot (Name i) Sorts.Relevant) ids) 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 e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
let open Context.Named.Declaration in
match decl with
| LocalAssum (id,ty) ->
if where == InHypValueOnly then
user_err (Id.print id.binder_name ++ str " has no value.");
let (sigma, ty') = redfun false env sigma ty in
(sigma, LocalAssum (id, ty'))
| LocalDef (id,b,ty) ->
let (sigma, b') =
if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
in
let (sigma, ty') =
if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
in
(sigma, LocalDef (id,b',ty'))
(* Possibly equip a reduction with the occurrences mentioned in an
occurrence clause *)
let error_illegal_clause () =
error "\"at\" clause not supported in presence of an occurrence clause."
let error_illegal_non_atomic_clause () =
error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
let error_occurrences_not_unsupported () =
error "Occurrences not supported for this reduction tactic."
let bind_change_occurrences occs = function
| None -> None
| Some c -> Some (Redexpr.out_with_occurrences (occs,c))
let bind_red_expr_occurrences occs nbcl redexp =
let has_at_clause = function
| Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Simpl (_,Some (occl,_)) -> occl != AllOccurrences
| _ -> false in
if occs == AllOccurrences then
if nbcl > 1 && has_at_clause redexp then
error_illegal_non_atomic_clause ()
else
redexp
else
match redexp with
| Unfold (_::_::_) ->
error_illegal_clause ()
| Unfold [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Unfold [(occs,c)]
| Pattern (_::_::_) ->
error_illegal_clause ()
| Pattern [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Pattern [(occs,c)]
| Simpl (f,Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Simpl (f,Some (occs,c))
| CbvVm (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvVm (Some (occs,c))
| CbvNative (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvNative (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
| ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
error_occurrences_not_unsupported ()
| Unfold [] | Pattern [] ->
assert false
(* 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 ?(check = false) (redfun, sty) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(convert_concl ~check c' sty)
end
let e_change_in_hyp ?(check = false) redfun (id,where) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let hyp = Tacmach.New.pf_get_hyp id gl in
let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(convert_hyp ~check c)
end
let e_change_in_hyps ?(check=true) f args =
Proofview.Goal.enter begin fun gl ->
let fold (env, sigma) arg =
let (redfun, id, where) = f arg in
let hyp =
try lookup_named id env
with Not_found ->
raise (RefinerError (env, sigma, NoSuchHyp id))
in
let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
let sign = Logic.convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
(env, sigma)
in
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (env, sigma) = List.fold_left fold (env, sigma) args in
let ty = Proofview.Goal.concl gl in
Proofview.Unsafe.tclEVARS sigma
<*>
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ty
end
end
let e_reduct_in_concl = e_change_in_concl
let reduct_in_concl ?(check = false) (redfun, sty) =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_change_in_concl ~check (redfun, sty)
let e_reduct_in_hyp ?(check=false) redfun (id, where) =
let redfun _ env sigma c = redfun env sigma c in
e_change_in_hyp ~check redfun (id, where)
let reduct_in_hyp ?(check = false) redfun (id, where) =
let redfun _ env sigma c = (sigma, redfun env sigma c) in
e_change_in_hyp ~check redfun (id, where)
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
let e_reduct_option ?(check=false) redfun = function
| Some id -> e_reduct_in_hyp ~check (fst redfun) id
| None -> e_change_in_concl ~check (revert_cast redfun)
let reduct_option ?(check = false) (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
let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
let check_types env sigma mayneedglobalcheck deep newc origc =
let t1 = Retyping.get_type_of env sigma newc in
if deep then begin
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:Reduction.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
user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
| Some sigma -> sigma
end
else
if not (isSort sigma (whd_all env sigma t1)) then
user_err ~hdr:"convert-check-hyp" (str "Not a type.")
else sigma
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
let (sigma, t') = t env sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
match infer_conv ~pb:cv_pb env sigma t' c with
| None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
| Some sigma -> (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 (sigma, c) = 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 Reduction.CONV mayneedglobalcheck true (t subst)
else
fun env sigma _c -> t subst env sigma) env sigma c in
if !mayneedglobalcheck then
begin
try ignore (Typing.unsafe_type_of env sigma c)
with e when catchable_exception e ->
error "Replacement would lead to an ill-typed term."
end;
(sigma, c)
let change_in_concl ?(check=true) occl t =
(* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
let change_in_hyp ?(check=true) occl t id =
(* FIXME: we set the [check] flag only to reorder hypotheses in case of
introduction of dependencies in new variables. We should separate this
check from the conversion function. *)
e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id
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=true) chg c cls =
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.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 Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
e_change_in_hyps ~check f hyps
end
let change_concl t =
change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
let red_in_hyp = reduct_in_hyp red_product
let red_option = reduct_option (red_product,REVERTcast)
let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast)
let hnf_in_hyp = reduct_in_hyp hnf_constr
let hnf_option = reduct_option (hnf_constr,REVERTcast)
let simpl_in_concl = reduct_in_concl (simpl,REVERTcast)
let simpl_in_hyp = reduct_in_hyp simpl
let simpl_option = reduct_option (simpl,REVERTcast)
let normalise_in_concl = reduct_in_concl (compute,REVERTcast)
let normalise_in_hyp = reduct_in_hyp compute
let normalise_option = reduct_option (compute,REVERTcast)
let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
(* The main reduction function *)
let reduce redexp cl =
let trace env sigma =
let open Printer in
let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
in
Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.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
begin match cl.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
| occs ->
let redexp = bind_red_expr_occurrences occs nbcl redexp in
let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in
e_change_in_concl ~check (revert_cast redfun)
end
<*>
let f (id, occs, where) =
let redexp = bind_red_expr_occurrences occs nbcl redexp in
let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in
let redfun _ env sigma c = redfun env sigma c in
(redfun, id, where)
in
e_change_in_hyps ~check f hyps
end
end
(* Unfolding occurrences of a constant *)
let unfold_constr = function
| ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
| VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
| _ -> user_err ~hdr:"unfold_constr" (str "Cannot unfold a non-constant.")
(*******************************************)
(* 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 ctxt gl =
let _, res, _ = List.fold_right
(fun decl acc ->
let env,idl,avoid = acc in
let name = fresh_id avoid (default_id env gl.sigma decl) gl in
let newenv = push_rel decl env in
(newenv, name :: idl, Id.Set.add name avoid))
ctxt (pf_env gl, [], Id.Set.empty) in
List.rev res
let build_intro_tac id dest tac = match dest with
| MoveLast -> Tacticals.New.tclTHEN (introduction id) (tac id)
| dest -> Tacticals.New.tclTHENLIST
[introduction id; move_hyp id dest; tac id]
let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Tacmach.New.pf_env gl in
let concl = Proofview.Goal.concl gl in
match EConstr.kind sigma concl with
| Prod (name,t,u) when not dep_flag || 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_flag || 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_flag ->
let sigma, t = Evardefine.define_evar_as_product env sigma ev in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
begin if not force_flag then Proofview.tclZERO (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.New.tclTHEN hnf_in_concl
(intro_then_gen name_flag move_flag false dep_flag tac))
begin function (e, info) -> match e with
| RefinerError (env, sigma, IntroNeedsProduct) ->
Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
end
let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false
let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false
let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false
let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false
let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
let intro_move_avoid idopt avoid hto = match idopt with
| None -> intro_gen (NamingAvoid avoid) hto true false
| Some id -> intro_gen (NamingMustBe (CAst.make id)) hto true 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.New.tclTHEN (intro_using str) (intros_using l)
let intros = Tacticals.New.tclREPEAT intro
let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
let rec aux n ids =
(* Note: we always use the bound when there is one for "*" and "**" *)
if (match bound with None -> true | Some (_,p) -> n < p) then
Proofview.tclORELSE
begin
intro_then_gen name_flag move_flag false dep_flag
(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.New.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.New.tclTHEN
(Tacticals.New.tclMAP (fun id ->
Tacticals.New.tclTRY (clear_for_replacing [id]))
(if suboptimal then ids else List.rev ids))
(Tacticals.New.tclMAP (fun (id,pos) ->
Tacticals.New.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.New.tclTHEN
(clear_for_replacing ids)
(Tacticals.New.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.New.tclMAP (fun name -> intro_gen (naming name) MoveLast true false) (List.rev ids)
(* 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
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.New.project gl) ccl h with
| None when red ->
let (redfun, _) = Redexpr.reduction_of_red_expr env (Red true) in
let (_, c) = redfun env (Proofview.Goal.sigma gl) ccl in
aux c
| x -> x
in
try aux (Proofview.Goal.concl gl)
with Redelimination -> None
let is_quantified_hypothesis id gl =
match lookup_hypothesis_as_renamed_gen false (NamedHyp id) gl with
| Some _ -> true
| None -> false
let msg_quantified_hypothesis = function
| NamedHyp id ->
str "quantified hypothesis named " ++ Id.print id
| AnonHyp n ->
pr_nth n ++
str " non dependent hypothesis"
let warn_deprecated_intros_until_0 =
CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics"
(fun () ->
strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"")
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 ->
user_err ~hdr:"lookup_quantified_hypothesis"
(str "No " ++ msg_quantified_hypothesis h ++
strbrk " in current goal" ++
(if red then strbrk " even after head-reduction" else mt ()) ++
str".")
let intros_until_gen red h =
Proofview.Goal.enter begin fun gl ->
let n = depth_of_quantified_hypothesis red h gl in
Tacticals.New.tclDO n (if red then introf else intro)
end
let intros_until_id id = intros_until_gen false (NamedHyp 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.New.pf_get_hyp id gl in
Proofview.tclUNIT ()
end
let try_intros_until_id_check id =
Tacticals.New.tclORELSE (intros_until_id id) (tclCHECKVAR id)
let try_intros_until tac = function
| NamedHyp id -> Tacticals.New.tclTHEN (try_intros_until_id_check id) (tac id)
| AnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHypId tac)
let rec intros_move = function
| [] -> Proofview.tclUNIT ()
| (hyp,destopt) :: rest ->
Tacticals.New.tclTHEN (intro_gen (NamingMustBe (CAst.make hyp)) destopt false false)
(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_typeclasses = true;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
Pretyping.polymorphic = 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 onOpenInductionArg env sigma tac = function
| clear_flag,ElimOnConstr f ->
let (sigma', cbl) = f env sigma in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS sigma')
(tac clear_flag (sigma,cbl))
| clear_flag,ElimOnAnonHyp n ->
Tacticals.New.tclTHEN
(intros_until_n n)
(Tacticals.New.onLastHyp
(fun c ->
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
tac clear_flag (sigma,(c,NoBindings))
end))
| clear_flag,ElimOnIdent {CAst.v=id} ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
(Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
tac clear_flag (sigma,(mkVar id,NoBindings))
end)
let onInductionArg tac = function
| clear_flag,ElimOnConstr cbl ->
tac clear_flag cbl
| clear_flag,ElimOnAnonHyp n ->
Tacticals.New.tclTHEN
(intros_until_n n)
(Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
| clear_flag,ElimOnIdent {CAst.v=id} ->
(* A quantified hypothesis *)
Tacticals.New.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_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' (sigma,c) in
(sigma', (c, lbind))
let with_no_bindings (c, lbind) =
if lbind != NoBindings then error "'with' clause not supported here.";
c
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 normalize_cut = false
let cut c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let relevance =
try
(* Backward compat: ensure that [c] is well-typed. Plus we
need to know the relevance *)
let typ = Typing.unsafe_type_of env sigma c in
let typ = whd_all env sigma typ in
match EConstr.kind sigma typ with
| Sort s -> Some (Sorts.relevance_of_sort (ESorts.kind sigma s))
| _ -> None
with e when Pretype_errors.precatchable_exception e -> None
in
match relevance with
| Some r ->
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
(* Backward compat: normalize [c]. *)
let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
Refine.refine ~typecheck:false begin fun h ->
let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
let (h, x) = Evarutil.new_evar env h c in
let f = mkLetIn (make_annot (Name id) r, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
(h, f)
end
| None ->
Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
end
let error_uninstantiated_metas t clenv =
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".")
let check_unresolved_evars_of_metas sigma clenv =
(* This checks that Metas turned into Evars by *)
(* Refiner.pose_all_metas_as_evars are resolved *)
List.iter (fun (mv,b) -> match b with
| Clval (_,(c,_),_) ->
(match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with
| Evar (evk,_) when Evd.is_undefined clenv.evd evk
&& not (Evd.mem sigma evk) ->
error_uninstantiated_metas (mkMeta mv) clenv
| _ -> ())
| _ -> ())
(meta_list clenv.evd)
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 ?(sidecond_first=false) with_evars ?(with_classes=true)
targetid id sigma0 clenv tac =
let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses
~fail:(not with_evars) clenv.env clenv.evd }
else clenv
in
let new_hyp_typ = clenv_type clenv in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
if not with_evars && occur_meta clenv.evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
(if sidecond_first then
Tacticals.New.tclTHENFIRST
(assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
else
Tacticals.New.tclTHENLAST
(assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac)
(********************************************)
(* Elimination tactics *)
(********************************************)
let last_arg sigma c = match EConstr.kind sigma c with
| App (f,cl) ->
Array.last cl
| _ -> anomaly (Pp.str "last_arg.")
let nth_arg sigma i c =
if Int.equal i (-1) then last_arg sigma c else
match EConstr.kind sigma c with
| App (f,cl) -> cl.(i)
| _ -> anomaly (Pp.str "nth_arg.")
let index_of_ind_arg sigma t =
let rec aux i j t = match EConstr.kind sigma t with
| 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 "Could not find inductive argument of elimination scheme."
in aux None 0 t
let rec contract_letin_in_lam_header sigma c =
match EConstr.kind sigma c with
| Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c)
| LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c)
| _ -> c
let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ())
rename i (elim, elimty, bindings) indclause =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header sigma elim in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv =
(match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with
| Meta mv -> mv
| _ -> user_err ~hdr:"elimination_clause"
(str "The type of elimination clause is not well-formed."))
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags
end
(*
* 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 = {
elimindex : int option; (* None = find it automatically *)
elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *)
elimbody : EConstr.constr with_bindings
}
let general_elim_clause_gen elimtac indclause elim =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (elimc,lbindelimc) = elim.elimbody in
let elimt = Retyping.get_type_of env sigma elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in
elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
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.New.project gl in
let ct = Retyping.get_type_of env sigma c in
let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
let elimtac = elimination_clause_scheme with_evars in
let indclause = make_clenv_binding env sigma (c, t) lbindc in
let sigma = meta_merge sigma (clear_metas indclause.evd) in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.New.tclTHEN
(general_elim_clause_gen elimtac indclause elim)
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
end
(* Case analysis tactics *)
let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let t = Retyping.get_type_of env sigma c in
let (mind,_) = reduce_to_quantified_ind env sigma t in
let sort = Tacticals.New.elimination_sort_of_goal gl in
let mind = on_snd (fun u -> EInstance.kind sigma u) mind in
let (sigma, elim) =
if dependent sigma c concl then
build_case_analysis_scheme env sigma mind true sort
else
build_case_analysis_scheme_default env sigma mind sort in
let elim = EConstr.of_constr elim in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(general_elim with_evars clear_flag (c,lbindc)
{elimindex = None; elimbody = (elim,NoBindings);
elimrename = Some (false, constructors_nrealdecls (fst mind))})
end
let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
(general_case_analysis_in_context with_evars clear_flag cx)
| _ ->
general_case_analysis_in_context with_evars clear_flag cx
let simplest_case c = general_case_analysis false None (c,NoBindings)
let simplest_ecase c = general_case_analysis true None (c,NoBindings)
(* Elimination tactic with bindings but using the default elimination
* constant associated with the type. *)
exception IsNonrec
let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
Tacmach.New.pf_apply Evd.fresh_global gl gr
let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
if is_nonrec ind then raise IsNonrec;
let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
evd, {elimindex = None; elimbody = (c,NoBindings);
elimrename = Some (true, constructors_nrealdecls ind)}
let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
(Proofview.Goal.enter begin fun gl ->
let sigma, elim = find_eliminator c gl in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(general_elim with_evars clear_flag cx elim)
end)
begin function (e, info) -> match e with
| IsNonrec ->
(* For records, induction principles aren't there by default
anymore. Instead, we do a case analysis. *)
general_case_analysis with_evars clear_flag cx
| e -> Proofview.tclZERO ~info e
end
let elim_in_context with_evars clear_flag c = function
| Some elim ->
general_elim with_evars clear_flag c
{elimindex = Some (-1); elimbody = elim; elimrename = None}
| None -> default_elim with_evars clear_flag c
let elim with_evars clear_flag (c,lbindc as cx) elim =
Proofview.tclEVARMAP >>= fun sigma ->
match EConstr.kind sigma c with
| Var id when lbindc == NoBindings ->
Tacticals.New.tclTHEN (try_intros_until_id_check id)
(elim_in_context with_evars clear_flag cx elim)
| _ ->
elim_in_context with_evars clear_flag cx elim
(* The simplest elimination tactic, with no substitutions at all. *)
let simplest_elim c = default_elim false None (c,NoBindings)
(* Elimination in hypothesis *)
(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
indclause : forall ..., hyps -> a=b (to take place of ?Heq)
id : phi(a) (to take place of ?H)
and the result is to overwrite id with the proof of phi(b)
but this generalizes to any elimination scheme with one constructor
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
(* The evarmap of elimclause is assumed to be an extension of hypclause, so
we do not need to merge the universes coming from hypclause. *)
try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause
with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
id rename i (elim, elimty, bindings) indclause =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header sigma elim in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
let hypmv =
match List.remove Int.equal indmv (clenv_independent elimclause) with
| [a] -> a
| _ -> user_err ~hdr:"elimination_clause"
(str "The type of elimination clause is not well-formed.")
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
let hyp = mkVar id in
let hyp_typ = Retyping.get_type_of env sigma hyp in
let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
user_err ~hdr:"general_rewrite_in"
(str "Nothing to rewrite in " ++ Id.print id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
(fun id -> Proofview.tclUNIT ())
end
let general_elim_clause with_evars flags id c e =
let elim = match id with
| None -> elimination_clause_scheme with_evars ~with_classes:true ~flags
| Some id -> elimination_in_clause_scheme with_evars ~flags id
in
general_elim_clause_gen elim c e
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
| DefinedRecord of Constant.t option list
| NotADefinedRecordUseScheme of constr
let make_projection env sigma params cstr sign elim i n c u =
let open Context.Rel.Declaration in
let elim = match elim with
| NotADefinedRecordUseScheme elim ->
(* bugs: goes from right to left when i increases! *)
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cstr.cs_args in
let decl = List.nth cs_args i in
let t = RelDecl.get_type decl in
let b = match decl with LocalAssum _ -> mkRel (i+1) | LocalDef (_,b,_) -> b in
let branch = it_mkLambda_or_LetIn b cs_args in
if
(* excludes dependent projection types *)
noccur_between sigma 1 (n-i-1) t
(* to avoid surprising unifications, excludes flexible
projection types or lambda which will be instantiated by Meta/Evar *)
&& not (isEvar sigma (fst (whd_betaiota_stack sigma t)))
&& (accept_universal_lemma_under_conjunctions () || not (isRel sigma t))
then
let t = lift (i+1-n) t in
let abselim = beta_applist sigma (elim, params@[t;branch]) in
let args = Context.Rel.to_extended_vect mkRel 0 sign in
let c = beta_applist sigma (abselim, [mkApp (c, args)]) in
Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
else
None
| DefinedRecord l ->
(* goes from left to right when i increases! *)
match List.nth l i with
| Some proj ->
let args = Context.Rel.to_extended_vect mkRel 0 sign in
let proj =
match Recordops.find_primitive_projection proj with
| Some proj ->
mkProj (Projection.make proj false, mkApp (c, args))
| None ->
mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
[|mkApp (c, args)|])
in
let app = it_mkLambda_or_LetIn proj sign in
let t = Retyping.get_type_of env sigma app in
Some (app, t)
| None -> None
in elim
let descend_in_conjunctions avoid tac (err, info) c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
try
let t = Retyping.get_type_of env sigma c in
let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
let sign,ccl = EConstr.decompose_prod_assum sigma t in
match match_with_tuple sigma ccl with
| Some (_,_,isrec) ->
let n = (constructors_nrealargs ind).(0) in
let sort = Tacticals.New.elimination_sort_of_goal gl in
let IndType (indf,_) = find_rectype env sigma ccl in
let (_,inst), params = dest_ind_family indf in
let params = List.map EConstr.of_constr params in
let cstr = (get_constructors env indf).(0) in
let elim =
try DefinedRecord (Recordops.lookup_projections ind)
with Not_found ->
let u = EInstance.kind sigma u in
let (_, elim) = build_case_analysis_scheme env sigma (ind,u) false sort in
let elim = EConstr.of_constr elim in
NotADefinedRecordUseScheme elim in
Tacticals.New.tclORELSE0
(Tacticals.New.tclFIRST
(List.init n (fun i ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
match make_projection env sigma params cstr sign elim i n c u with
| None -> Tacticals.New.tclFAIL 0 (mt())
| Some (p,pt) ->
Tacticals.New.tclTHENS
(assert_before_gen false (NamingAvoid avoid) pt)
[Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
end)))
(Proofview.tclZERO ~info err)
| None -> Proofview.tclZERO ~info err
with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
end
(****************************************************)
(* Resolution tactics *)
(****************************************************)
let tclORELSEOPT t k =
Proofview.tclORELSE t
(fun e -> match k e with
| None ->
let (e, info) = e in
Proofview.tclZERO ~info e
| Some tac -> tac)
let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
let concl_nprod = nb_prod_modulo_zeta sigma concl in
let rec try_main_apply with_destruct c =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ts =
if respect_opaque then Conv_oracle.get_transp_state (oracle env)
else TransparentState.full
in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.235 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
