Module Declare.Proof

Declare.Proof.t Construction of constants using interactive proofs.

type t
val start : info:Info.t -> cinfo:EConstr.t CInfo.t -> ?using:Names.Id.Set.t -> Evd.evar_map -> t

start_proof ~info ~cinfo sigma starts a proof of cinfo. The proof is started in the evar map sigma (which can typically contain universe constraints)

val start_derive : name:Names.Id.t -> info:Info.t -> cinfo:unit CInfo.t list -> Proofview.telescope -> t

start_{derive,equations} are functions meant to handle interactive proofs with multiple goals, they should be considered experimental until we provide a more general API encompassing both of them. Please, get in touch with the developers if you would like to experiment with multi-goal dependent proofs so we can use your input on the design of the new API.

val start_definition : info:Info.t -> cinfo:EConstr.t CInfo.t -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> t

Pretty much internal, used by the Lemma vernaculars

val start_mutual_definitions : info:Info.t -> cinfo:Constr.t CInfo.t list -> bodies:Constr.t option list -> possible_guard:(Pretyping.possible_guard * Sorts.relevance list) -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> t

Pretty much internal, used by mutual Lemma / Fixpoint vernaculars

val start_mutual_definitions_refine : info:Info.t -> cinfo:EConstr.t CInfo.t list -> bodies:EConstr.t option list -> possible_guard:(Pretyping.possible_guard * Evd.erelevance list) -> ?using:Vernacexpr.section_subset_expr -> Evd.evar_map -> t

Pretty much internal, used by mutual Lemma / Fixpoint vernaculars with #refine

val save : pm:OblState.t -> proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list

Qed a proof

val save_regular : proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> Names.GlobRef.t list

For proofs known to have Regular ending, no need to touch program state.

val save_admitted : pm:OblState.t -> proof:t -> OblState.t

Admit a proof

val by : Environ.env -> unit Proofview.tactic -> t -> t * bool

by env tac applies tactic tac to the 1st subgoal of the current focused proof. Returns false if an unsafe tactic has been used.

val get : t -> Proof.t

Operations on ongoing proofs

val get_name : t -> Names.Id.t
val fold : f:(Proof.t -> 'a) -> t -> 'a
val map : f:(Proof.t -> Proof.t) -> t -> t
val map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a
val map_fold_endline : f:(Gentactic.glob_generic_tactic option -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
val set_endline_tactic : Gentactic.glob_generic_tactic -> t -> t

Sets the tactic to be used when a tactic line is closed with ...

type late_init =
  1. | Explicit
  2. | Implicit
  3. | NotRequired

Explicit: explicit Proof command, Implicit: no Proof command, NotRequired: opened by Next Obligation or similar

val finish_late_init : t -> late_init -> t
val has_late_init : t -> late_init option
val definition_scope : t -> Locality.definition_scope
val set_proof_using : t -> Vernacexpr.section_subset_expr option -> t

Sets the section variables assumed by the proof, returns its closure (w.r.t. type dependencies and let-ins covered by it). With None, get the variables from the "using" attribute.

val get_used_variables : t -> Names.Id.Set.t option

Gets the set of variables declared to be used by the proof. None means no "Proof using" or #using was given

val compact : t -> t

Compacts the representation of the proof by pruning all intermediate terms

val update_sigma_univs : UGraph.t -> t -> t

Update the proof's universe information typically after a side-effecting command (e.g. a sublemma definition) has been run inside it.

val get_open_goals : t -> int

Helpers to obtain proof state when in an interactive proof

get_goal_context n returns the context of the nth subgoal of the current focused proof or raises a UserError if there is no focused proof or if there is no more subgoals

val get_goal_context : t -> int -> Evd.evar_map * Environ.env
val get_current_context : t -> Evd.evar_map * Environ.env

get_current_context () returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map.

Proof delay API, warning, internal, not stable

type closed_proof_output
val return_proof : t -> closed_proof_output

Requires a complete proof.

type proof_object

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val close_proof : ?warn_incomplete:bool -> opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
val save_lemma_admitted_delayed : pm:OblState.t -> proof:proof_object -> OblState.t

Special cases for delayed proofs, in this case we must provide the proof information so the proof won't be forced.

val save_lemma_proved_delayed : pm:OblState.t -> proof:proof_object -> idopt:Names.lident option -> OblState.t
val control_only_guard : t -> unit