summaryrefslogtreecommitdiff
path: root/stm/lemmas.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /stm/lemmas.ml
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r--stm/lemmas.ml116
1 files changed, 78 insertions, 38 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index f06abfcc..022c89ad 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -9,7 +9,7 @@
(* Created by Hugo Herbelin from contents related to lemma proofs in
file command.ml, Aug 2009 *)
-open Errors
+open CErrors
open Util
open Flags
open Pp
@@ -31,20 +31,22 @@ open Reductionops
open Constrexpr
open Constrintern
open Impargs
+open Context.Rel.Declaration
type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
let call_hook fix_exn hook l c =
try hook l c
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
iraise (fix_exn e)
(* Support for mutually proved theorems *)
let retrieve_first_recthm = function
| VarRef id ->
- (pi2 (Global.lookup_named id),variable_opacity id)
+ let open Context.Named.Declaration in
+ (get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
(Global.body_of_constant_body cb, is_opaque cb)
@@ -77,7 +79,7 @@ let adjust_guardness_conditions const = function
List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
- search_guard Loc.ghost env
+ search_guard Loc.ghost env
possible_indexes fixdecls in
(mkFix ((indexes,0),fixdecls), ctx), eff
| _ -> (body, ctx), eff) }
@@ -104,20 +106,21 @@ let find_mutually_recursive_statements thms =
(* Cofixpoint or fixpoint w/o explicit decreasing argument *)
| None | Some (None, CStructRec) ->
let whnf_hyp_hds = map_rel_context_in_env
- (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+ (fun env c -> fst (whd_all_stack env Evd.empty c))
(Global.env()) hyps in
let ind_hyps =
- List.flatten (List.map_i (fun i (_,b,t) ->
+ List.flatten (List.map_i (fun i decl ->
+ let t = get_type decl in
match kind_of_term t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+ mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
[ind,x,i]
| _ ->
[]) 0 (List.rev whnf_hyp_hds)) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
- let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+ let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
match kind_of_term whnf_ccl with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
@@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose msg_info (str "Assuming mutual coinductive statements.");
+ if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -207,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
definition_message id;
Option.iter (Universes.register_universe_binders r) pl;
call_hook (fun exn -> exn) hook l r
- with e when Errors.noncritical e ->
- let e = Errors.push e in
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
iraise (fix_exn e)
let default_thm_id = Id.of_string "Unnamed_thm"
@@ -249,10 +252,14 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
| Some body ->
let body = norm body in
let k = Kindops.logical_kind_of_goal_kind kind in
- let body_i = match kind_of_term body with
+ let rec body_i t = match kind_of_term t with
| Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
| CoFix (0,decls) -> mkCoFix (i,decls)
+ | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
+ | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
+ | App (t, args) -> mkApp (body_i t, args)
| _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+ let body_i = body_i body in
match locality with
| Discharge ->
let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
@@ -298,13 +305,16 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
(* Admitted *)
+let warn_let_as_axiom =
+ CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+ (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++
+ spc () ++ strbrk "declared as an axiom.")
+
let admit (id,k,e) pl hook () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
- | Local, _, _ | Discharge, _, _ ->
- msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
- str "declared as an axiom.")
+ | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
in
let () = assumption_message id in
Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
@@ -329,10 +339,11 @@ let check_exist =
)
let universe_proof_terminator compute_guard hook =
- let open Proof_global in function
+ let open Proof_global in
+ make_terminator begin function
| Admitted (id,k,pe,(ctx,pl)) ->
admit (id,k,pe) pl (hook (Some ctx)) ();
- Pp.feedback Feedback.AddedAxiom
+ Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
| Vernacexpr.Transparent -> false, true, []
@@ -347,12 +358,16 @@ let universe_proof_terminator compute_guard hook =
save_anonymous_with_strength ~export_seff proof kind id
end;
check_exist exports
+ end
let standard_proof_terminator compute_guard hook =
universe_proof_terminator compute_guard (fun _ -> hook)
-let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = standard_proof_terminator compute_guard hook in
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+ let terminator = match terminator with
+ | None -> standard_proof_terminator compute_guard hook
+ | Some terminator -> terminator compute_guard hook
+ in
let sign =
match sign with
| Some sign -> sign
@@ -361,8 +376,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
!start_hook c;
Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = universe_proof_terminator compute_guard hook in
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+ let terminator = match terminator with
+ | None -> universe_proof_terminator compute_guard hook
+ | Some terminator -> terminator compute_guard hook
+ in
let sign =
match sign with
| Some sign -> sign
@@ -392,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
| Anonymous -> Tactics.intro) (List.rev ids) in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
- let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+ let rec_tac = rec_tac_initializer finite guard thms snl in
Some (match init_tac with
| None ->
if Flags.is_auto_intros () then
@@ -422,7 +440,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+ let ctx = UState.context_set (*FIXME*) ctx in
let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
@@ -431,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
call_hook (fun exn -> exn) hook strength ref) thms_data in
start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
-let start_proof_com kind thms hook =
+let start_proof_com ?inference_hook kind thms hook =
let env0 = Global.env () in
let levels = Option.map snd (fst (List.hd thms)) in
let evdref = ref (match levels with
@@ -441,8 +459,10 @@ let start_proof_com kind thms hook =
let thms = List.map (fun (sopt,(bl,t,guard)) ->
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
- evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
- let ids = List.map pi1 ctx in
+ let flags = all_and_fail_flags in
+ let flags = { flags with use_hook = inference_hook } in
+ evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref);
+ let ids = List.map get_name ctx in
(compute_proof_name (pi1 kind) sopt,
(nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (List.length ids) imps'),
@@ -451,6 +471,11 @@ let start_proof_com kind thms hook =
let recguard,thms,snl = look_for_possibly_mutual_statements thms in
let evd, nf = Evarutil.nf_evars_and_universes !evdref in
let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+ let () =
+ match levels with
+ | None -> ()
+ | Some l -> ignore (Evd.universe_context evd ?names:l)
+ in
let evd =
if pi2 kind then evd
else (* We fix the variables to ensure they won't be lowered to Set *)
@@ -461,6 +486,18 @@ let start_proof_com kind thms hook =
(* Saving a proof *)
+let keep_admitted_vars = ref true
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "keep section variables in admitted proofs";
+ optkey = ["Keep"; "Admitted"; "Variables"];
+ optread = (fun () -> !keep_admitted_vars);
+ optwrite = (fun b -> keep_admitted_vars := b) }
+
let save_proof ?proof = function
| Vernacexpr.Admitted ->
let pe =
@@ -474,14 +511,18 @@ let save_proof ?proof = function
error "Admitted requires an explicit statement";
let typ = Option.get const_entry_type in
let ctx = Evd.evar_context_universe_context (fst universes) in
- Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
+ let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
+ Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
| None ->
+ let pftree = Pfedit.get_pftreestate () in
let id, k, typ = Pfedit.current_proof_statement () in
+ let universes = Proof.initial_euctx pftree in
(* This will warn if the proof is complete *)
- let pproofs, universes =
+ let pproofs, _univs =
Proof_global.return_proof ~allow_partial:true () in
let sec_vars =
- match Pfedit.get_used_variables(), pproofs with
+ if not !keep_admitted_vars then None
+ else match Pfedit.get_used_variables(), pproofs with
| Some _ as x, _ -> x
| None, (pproof, _) :: _ ->
let env = Global.env () in
@@ -490,11 +531,12 @@ let save_proof ?proof = function
Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
| _ -> None in
let names = Pfedit.get_universe_binders () in
- let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+ let evd = Evd.from_ctx universes in
+ let binders, ctx = Evd.universe_context ?names evd in
Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
(universes, Some binders))
in
- Proof_global.get_terminator() pe
+ Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
let (proof_obj,terminator) =
match proof with
@@ -504,12 +546,10 @@ let save_proof ?proof = function
in
(* if the proof is given explicitly, nothing has to be deleted *)
if Option.is_empty proof then Pfedit.delete_current_proof ();
- terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+ Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
(* Miscellaneous *)
let get_current_context () =
- try Pfedit.get_current_goal_context ()
- with e when Logic.catchable_exception e ->
- let env = Global.env () in
- (Evd.from_env env, env)
+ Pfedit.get_current_context ()
+