Module `Declare.Proof`Source

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

Sourcetype t

Sourceval start : info:Info.t -> cinfo:EConstr.t CInfo.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)

Source

val start_derive : 
  f:Names.Id.t ->
  name:Names.Id.t ->
  info:Info.t ->
  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.

Source

val start_equations : 
  name:Names.Id.t ->
  info:Info.t ->
  hook:(pm:OblState.t -> Names.Constant.t list -> Evd.evar_map -> OblState.t) ->
  types:
    (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr)
      list ->
  Evd.evar_map ->
  Proofview.telescope ->
  t

Source

val start_with_initialization : 
  info:Info.t ->
  cinfo:Constr.t CInfo.t ->
  Evd.evar_map ->
  t

Pretty much internal, used by the Lemma vernaculars

Sourcetype mutual_info = bool * lemma_possible_guards * Constr.t option list option

Source

val start_mutual_with_initialization : 
  info:Info.t ->
  cinfo:Constr.t CInfo.t list ->
  mutual_info:mutual_info ->
  Evd.evar_map ->
  int list option ->
  t

Pretty much internal, used by mutual Lemma / Fixpoint vernaculars

Source

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

Qed a proof

Source

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.

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

Admit a proof

Sourceval by : unit Proofview.tactic -> t -> t * bool

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

Sourceval get : t -> Proof.t

Operations on ongoing proofs

Sourceval get_name : t -> Names.Id.t

Sourceval fold : f:(Proof.t -> 'a) -> t -> 'a

Sourceval map : f:(Proof.t -> Proof.t) -> t -> t

Sourceval map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a

Source

val map_fold_endline : 
  f:(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) ->
  t ->
  t * 'a

Sourceval set_endline_tactic : Genarg.glob_generic_argument -> t -> t

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

Sourceval set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t

Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it)

Sourceval 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

Sourceval compact : t -> t

Compacts the representation of the proof by pruning all intermediate terms

Sourceval 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.

Sourceval 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

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

Sourceval get_current_goal_context : t -> Evd.evar_map * Environ.env

get_current_goal_context () works as get_goal_context 1

Sourceval 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

Sourcetype closed_proof_output

Sourceval return_proof : t -> closed_proof_output

Requires a complete proof.

Sourceval return_partial_proof : t -> closed_proof_output

An incomplete proof is allowed (no error), and a warn is given if the proof is complete.

Sourcetype 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

Source

val close_proof : 
  opaque:Vernacexpr.opacity_flag ->
  keep_body_ucst_separate:bool ->
  t ->
  proof_object

Source

val close_future_proof : 
  feedback_id:Stateid.t ->
  t ->
  closed_proof_output Future.computation ->
  proof_object

Source

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.

Source

val save_lemma_proved_delayed : 
  pm:OblState.t ->
  proof:proof_object ->
  idopt:Names.lident option ->
  OblState.t * Names.GlobRef.t list

Sourceval get_po_name : proof_object -> Names.Id.t

Used by the STM only to store info, should go away

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Declare/Proof/index.html

Module `Declare.Proof`Source

Proof delay API, warning, internal, not stable

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Declare/Proof/index.html

Module Declare.ProofSource

Proof delay API, warning, internal, not stable

Module `Declare.Proof`Source