aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--COMPATIBILITY7
-rw-r--r--doc/refman/RefMan-ltac.tex8
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--library/declare.ml33
-rw-r--r--library/declare.mli2
-rw-r--r--parsing/g_proofs.ml414
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--printing/ppvernac.ml9
-rw-r--r--stm/lemmas.ml53
-rw-r--r--stm/stm.ml7
-rw-r--r--test-suite/success/qed_export.v18
-rw-r--r--toplevel/vernacentries.ml2
15 files changed, 113 insertions, 56 deletions
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 10:11:23 +0000