From 4a53151f846476f2fbe038a4ecb8e84256a26ba9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 14 Feb 2015 18:35:04 +0100 Subject: Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior Of course such proofs cannot be processed asynchronously --- COMPATIBILITY | 7 ++++ doc/refman/RefMan-ltac.tex | 8 +++- intf/vernacexpr.mli | 2 +- library/declare.ml | 33 ++++++++-------- library/declare.mli | 2 +- parsing/g_proofs.ml4 | 14 ++++--- plugins/derive/derive.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/recdef.ml | 8 ++-- printing/ppvernac.ml | 9 ++++- stm/lemmas.ml | 53 +++++++++++++++++--------- stm/stm.ml | 7 ++-- test-suite/success/qed_export.v | 18 +++++++++ toplevel/vernacentries.ml | 2 +- 15 files changed, 113 insertions(+), 56 deletions(-) create mode 100644 test-suite/success/qed_export.v diff --git a/COMPATIBILITY b/COMPATIBILITY index 3b4e8987c..f23dbad1c 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -33,6 +33,13 @@ Type classes. type information and switching to proof mode is no longer available. Use { } (without the vertical bars) instead. +Tactic abstract. + +- Auxiliary lemmas generated by the abstract tactic are removed from + the global environment and inlined in the proof term when a proof + is ended with Qed. The vehavior of 8.4 can be obtained by ending + proofs with "Qed export" or "Qed export ident, .., ident". + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 689ac1425..1704b4d60 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1010,13 +1010,19 @@ Fail all:let n:= numgoals in guard n=2. Reset Initial. \end{coq_eval} -\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract} +\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export} \index{Tacticals!abstract@{\tt abstract}}} From the outside ``\texttt{abstract \tacexpr}'' is the same as {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the current goal and \textit{n} is chosen so that this is a fresh name. +Such auxiliary lemma is inlined in the final proof term +unless the proof is ended with ``\texttt{Qed export}''. In such +case the lemma is preserved. The syntax +``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$'' +is also supported. In such case the system checks that the names given by the +user actually exist when the proof is ended. This tactical is useful with tactics such as \texttt{omega} or \texttt{discriminate} that generate huge proof terms. With that tool diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 3f2d002c7..07891d0b4 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -135,7 +135,7 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = bool (* true = Opaque; false = Transparent *) +type opacity_flag = Opaque of lident list option | Transparent type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) diff --git a/library/declare.ml b/library/declare.ml index 7f42a747e..c3181e4c7 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -253,24 +253,25 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = - let cd = (* We deal with side effects of non-opaque constants *) +let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = + let cd = (* We deal with side effects *) match cd with - | Entries.DefinitionEntry ({ - const_entry_opaque = false; const_entry_body = bo } as de) - | Entries.DefinitionEntry ({ - const_entry_polymorphic = true; const_entry_body = bo } as de) - -> - let _, seff = Future.force bo in - if Declareops.side_effects_is_empty seff then cd - else begin - let seff = Declareops.uniquize_side_effects seff in - Declareops.iter_side_effects - (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; - Entries.DefinitionEntry { de with - const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> - pt, Declareops.no_seff) } + | Entries.DefinitionEntry de -> + if export_seff || + not de.const_entry_opaque || + de.const_entry_polymorphic then + let bo = de.const_entry_body in + let _, seff = Future.force bo in + if Declareops.side_effects_is_empty seff then cd + else begin + let seff = Declareops.uniquize_side_effects seff in + Declareops.iter_side_effects + (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff; + Entries.DefinitionEntry { de with + const_entry_body = Future.chain ~pure:true bo (fun (pt, _) -> + pt, Declareops.no_seff) } end + else cd | _ -> cd in let cst = { diff --git a/library/declare.mli b/library/declare.mli index 03b66271a..d8a00db0c 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,7 +53,7 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 27f14c790..b23841cef 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -52,15 +52,17 @@ GEXTEND Gram | IDENT "Existential"; n = natural; c = constr_body -> VernacSolveExistential (n,c) | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (true,None)) - | IDENT "Save" -> VernacEndProof (Proved (true,None)) + | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None)) + | IDENT "Qed"; IDENT "export"; l = LIST0 identref SEP "," -> + VernacEndProof (Proved (Opaque (Some l),None)) + | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None)) | IDENT "Save"; tok = thm_token; id = identref -> - VernacEndProof (Proved (true,Some (id,Some tok))) + VernacEndProof (Proved (Opaque None,Some (id,Some tok))) | IDENT "Save"; id = identref -> - VernacEndProof (Proved (true,Some (id,None))) - | IDENT "Defined" -> VernacEndProof (Proved (false,None)) + VernacEndProof (Proved (Opaque None,Some (id,None))) + | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (false,Some (id,None))) + VernacEndProof (Proved (Transparent,Some (id,None))) | IDENT "Restart" -> VernacRestart | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 439b1a5c0..711a8aaf0 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -55,7 +55,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque , f_def , lemma_def + opaque <> Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index eb5221fd6..04347537f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -989,7 +989,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.Proved(false,None)) + Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c7b0a0b0..b9d7e0d90 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = -let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) +let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))) (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5558556e2..b1cbea51c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = let ce = definition_entry ~univs:ctx value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None)) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = match (kind_of_term t) with @@ -1247,9 +1247,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> true - | Declarations.Undef _ -> true - | Declarations.Def _ -> false + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None + | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e9e335ec9..e0b94669c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -740,9 +740,14 @@ module Make | VernacEndProof (Proved (opac,o)) -> return ( match o with - | None -> if opac then keyword "Qed" else keyword "Defined" + | None -> (match opac with + | Transparent -> keyword "Defined" + | Opaque None -> keyword "Qed" + | Opaque (Some l) -> + keyword "Qed" ++ spc() ++ str"export" ++ + prlist_with_sep (fun () -> str", ") pr_lident l) | Some (id,th) -> (match th with - | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) ) | VernacExactProof c -> diff --git a/stm/lemmas.ml b/stm/lemmas.ml index f2e687798..63c45116a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -185,7 +185,7 @@ let look_for_possibly_mutual_statements = function (* Saving a goal *) -let save id const cstrs do_guard (locality,poly,kind) hook = +let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try let const = adjust_guardness_conditions const do_guard in @@ -200,7 +200,8 @@ let save id const cstrs do_guard (locality,poly,kind) hook = | Local | Discharge -> true | Global -> false in - let kn = declare_constant id ~local (DefinitionEntry const, k) in + let kn = + declare_constant ?export_seff id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in definition_message id; call_hook (fun exn -> exn) hook l r @@ -273,25 +274,25 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im let save_hook = ref ignore let set_save_hook f = save_hook := f -let save_named proof = +let save_named ?export_seff proof = let id,const,cstrs,do_guard,persistence,hook = proof in - save id const cstrs do_guard persistence hook + save ?export_seff id const cstrs do_guard persistence hook let check_anonymity id save_ident = if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then error "This command can only be used for unnamed theorem." -let save_anonymous proof save_ident = +let save_anonymous ?export_seff proof save_ident = let id,const,cstrs,do_guard,persistence,hook = proof in check_anonymity id save_ident; - save save_ident const cstrs do_guard persistence hook + save ?export_seff save_ident const cstrs do_guard persistence hook -let save_anonymous_with_strength proof kind save_ident = +let save_anonymous_with_strength ?export_seff proof kind save_ident = let id,const,cstrs,do_guard,_,hook = proof in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook + save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook (* Admitted *) @@ -325,34 +326,50 @@ let get_proof proof do_guard hook opacity = (** FIXME *) id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook +let check_exist = + List.iter (fun (loc,id) -> + if not (Nametab.exists_cci (Lib.make_path id)) then + user_err_loc (loc,"",pr_id id ++ str " does not exist.") + ) + let standard_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> admit hook (); Pp.feedback Feedback.AddedAxiom - | Proved (is_opaque,idopt,proof) -> + | Proved (opaque,idopt,proof) -> + let is_opaque, export_seff, exports = match opaque with + | Vernacexpr.Transparent -> false, true, [] + | Vernacexpr.Opaque None -> true, false, [] + | Vernacexpr.Opaque (Some l) -> true, true, l in let proof = get_proof proof compute_guard hook is_opaque in begin match idopt with - | None -> save_named proof - | Some ((_,id),None) -> save_anonymous proof id + | None -> save_named ~export_seff proof + | Some ((_,id),None) -> save_anonymous ~export_seff proof id | Some ((_,id),Some kind) -> - save_anonymous_with_strength proof kind id - end + save_anonymous_with_strength ~export_seff proof kind id + end; + check_exist exports let universe_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> admit (hook None) (); Pp.feedback Feedback.AddedAxiom - | Proved (is_opaque,idopt,proof) -> + | Proved (opaque,idopt,proof) -> + let is_opaque, export_seff, exports = match opaque with + | Vernacexpr.Transparent -> false, true, [] + | Vernacexpr.Opaque None -> true, false, [] + | Vernacexpr.Opaque (Some l) -> true, true, l in let proof = get_proof proof compute_guard (hook (Some proof.Proof_global.universes)) is_opaque in begin match idopt with - | None -> save_named proof - | Some ((_,id),None) -> save_anonymous proof id + | None -> save_named ~export_seff proof + | Some ((_,id),None) -> save_anonymous ~export_seff proof id | Some ((_,id),Some kind) -> - save_anonymous_with_strength proof kind id - end + save_anonymous_with_strength ~export_seff proof kind id + end; + check_exist exports let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = let terminator = standard_proof_terminator compute_guard hook in diff --git a/stm/stm.ml b/stm/stm.ml index 693c673b4..207afd8ae 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1035,7 +1035,7 @@ end = struct (* {{{ *) vernac_interp stop ~proof:(pobject, terminator) { verbose = false; loc; - expr = (VernacEndProof (Proved (true,None))) }) in + expr = (VernacEndProof (Proved (Opaque None,None))) }) in ignore(Future.join checked_proof); RespBuiltProof(proof,time) with @@ -1166,7 +1166,7 @@ end = struct (* {{{ *) Reach.known_state ~cache:`No start; vernac_interp stop ~proof { verbose = false; loc; - expr = (VernacEndProof (Proved (true,None))) }; + expr = (VernacEndProof (Proved (Opaque None,None))) }; Some proof with e -> let (e, info) = Errors.push e in @@ -1564,7 +1564,8 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Id.to_string id in let loc = (snd cur).loc in let is_defined = function - | _, { expr = VernacEndProof (Proved (false,_)) } -> true + | _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } -> + true | _ -> false in let proof_using_ast = function | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v new file mode 100644 index 000000000..ee84cb94e --- /dev/null +++ b/test-suite/success/qed_export.v @@ -0,0 +1,18 @@ +Lemma a : True. +Proof. +assert True as H. + abstract (trivial) using exported_seff. +exact H. +Fail Qed export a_subproof. +Qed export exported_seff. +Check ( exported_seff : True ). + +Lemma b : True. +Proof. +assert True as H. + abstract (trivial) using exported_seff2. +exact H. +Qed. + +Fail Check ( exported_seff2 : True ). + diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7f435ce96..743cfaccd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -496,7 +496,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = by (Tactics.New.exact_proof c) in - save_proof (Vernacexpr.Proved(true,None)); + save_proof (Vernacexpr.(Proved(Opaque None,None))); if not status then Pp.feedback Feedback.AddedAxiom let vernac_assumption locality poly (local, kind) l nl = -- cgit v1.2.3