blob: 6984fff63aad5ad5acfab637464aa6c9cb93b5db (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** This module defines proof facilities relevant to the
toplevel. In particular it defines the global proof
environment. *)
type pstate
type t
val get_current_pstate : t -> pstate
val get_current_proof_name : pstate -> Names.Id.t
val get_current_persistence : pstate -> Decl_kinds.goal_kind
val get_all_proof_names : t -> Names.Id.t list
val discard : Names.lident -> t -> t option
val discard_current : t -> t option
val give_me_the_proof : pstate -> Proof.t
val compact_the_proof : pstate -> pstate
(** When a proof is closed, it is reified into a [proof_object], where
[id] is the name of the proof, [entries] the list of the proof terms
(in a form suitable for definitions). Together with the [terminator]
function which takes a [proof_object] together with a [proof_end]
(i.e. an proof ending command) and registers the appropriate
values. *)
type lemma_possible_guards = int list list
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
universes: UState.t;
}
type opacity_flag = Opaque | Transparent
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
UState.t
| Proved of opacity_flag *
Names.lident option *
proof_object
type proof_terminator
type closed_proof = proof_object * proof_terminator
val make_terminator : (proof_ending -> unit) -> proof_terminator
val apply_terminator : proof_terminator -> proof_ending -> unit
val push : ontop:t option -> pstate -> t
val maybe_push : ontop:t option -> pstate option -> t option
(** [start_proof ~ontop id str pl goals terminator] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
is; [terminator] is used at the end of the proof to close the proof
(e.g. to declare the built constructions as a coercion or a setoid
morphism). The proof is started in the evar map [sigma] (which can
typically contain universe constraints), and with universe bindings
pl. *)
val start_proof :
Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list ->
proof_terminator -> pstate
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
val start_dependent_proof :
Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
Proofview.telescope -> proof_terminator -> pstate
(** Update the proofs global environment after a side-effecting command
(e.g. a sublemma definition) has been run inside it. Assumes
there_are_pending_proofs. *)
val update_global_env : pstate -> pstate
(* Takes a function to add to the exceptions data relative to the
state in which the proof was built *)
val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn ->
pstate -> closed_proof
(* Intermediate step necessary to delegate the future.
* Both access the current proof state. The former is supposed to be
* chained with a computation that completed the proof *)
type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
(* If allow_partial is set (default no) then an incomplete proof
* is allowed (no error), and a warn is given if the proof is complete. *)
val return_proof : ?allow_partial:bool -> pstate -> closed_proof_output
val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> pstate ->
closed_proof_output Future.computation -> closed_proof
(** Gets the current terminator without checking that the proof has
been completed. Useful for the likes of [Admitted]. *)
val get_terminator : pstate -> proof_terminator
val set_terminator : proof_terminator -> pstate -> pstate
val get_open_goals : pstate -> int
(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
no current proof.
The return boolean is set to [false] if an unsafe tactic has been used. *)
val with_current_proof :
(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
val simple_with_current_proof :
(unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t
val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> pstate -> pstate * 'a
val modify_proof : (Proof.t -> Proof.t) -> pstate -> pstate
val with_current_pstate : (pstate -> pstate * 'a) -> t -> t * 'a
val modify_current_pstate : (pstate -> pstate) -> t -> t
(** Sets the tactic to be used when a tactic line is closed with [...] *)
val set_endline_tactic : Genarg.glob_generic_argument -> pstate -> pstate
(** Sets the section variables assumed by the proof, returns its closure
* (w.r.t. type dependencies and let-ins covered by it) + a list of
* ids to be cleared *)
val set_used_variables : pstate ->
Names.Id.t list -> (Constr.named_context * Names.lident list) * pstate
val get_used_variables : pstate -> Constr.named_context option
(** Get the universe declaration associated to the current proof. *)
val get_universe_decl : pstate -> UState.universe_decl
val copy_terminators : src:t -> tgt:t -> t
|
