Module `Obligations`

Coq's Program mode support. This mode extends declarations of constants and fixpoints with Program Definition and Program Fixpoint to support incremental construction of terms using delayed proofs, called "obligations"

The mode also provides facilities for managing and auto-solving sets of obligations.

The basic code flow of programs/obligations is as follows:

add_definition / add_mutual_definitions are called from the respective Program vernacular command interpretation; at this point the only extra work we do is to prepare the new definition d using RetrieveObl, which consists in turning unsolved evars into obligations. d is not sent to the kernel yet, as it is not complete and cannot be typchecked, but saved in a special data-structure. Auto-solving of obligations is tried at this stage (see below)

next_obligation will retrieve the next obligation (RetrieveObl sorts them by topological order) and will try to solve it. When all obligations are solved, the original constant d is grounded and sent to the kernel for addition to the global environment. Auto-solving of obligations is also triggered on obligation completion.

Solving of obligations: Solved obligations are stored as regular global declarations in the global environment, usually with name constant_obligation_number where constant is the original constant and number is the corresponding (internal) number.

Solving an obligation can trigger a bit of a complex cascaded callback path; closing an obligation can indeed allow all other obligations to be closed, which in turn may trigged the declaration of the original constant. Care must be taken, as this can modify Global.env in arbitrarily ways. Current code takes some care to refresh the env in the proper boundaries, but the invariants remain delicate.

Saving of obligations: as open obligations use the regular proof mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason obligations code is split in two: this file, Obligations, taking care of the top-level vernac commands, and DeclareObl, which is called by `Lemmas` to close an obligation proof and eventually to declare the top-level Programed constant.

There is little obligations-specific code in DeclareObl, so eventually that file should be integrated in the regular Declare path, as it gains better support for "dependent_proofs".

val default_tactic : unit Proofview.tactic Stdlib.ref
val add_definition : name:Names.Id.t -> ?⁠term:Constr.constr -> Constr.types -> uctx:UState.t -> ?⁠udecl:UState.universe_decl -> ?⁠impargs:Impargs.manual_implicits -> poly:bool -> ?⁠scope:Declare.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠tactic:unit Proofview.tactic -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Declare.Hook.t -> ?⁠opaque:bool -> RetrieveObl.obligation_info -> DeclareObl.progress: Start a Program Definition c proof. uctx udecl impargs kind scope poly etc... come from the interpretation of the vernacular; `obligation_info` was generated by RetrieveObl It will return whether all the obligations were solved; if so, it will also register c with the kernel.

val add_mutual_definitions : (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?⁠udecl:UState.universe_decl -> ?⁠tactic:unit Proofview.tactic -> poly:bool -> ?⁠scope:Declare.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Declare.Hook.t -> ?⁠opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit: Start a Program Fixpoint declaration, similar to the above, except it takes a list now.

val obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> Lemmas.t: Implementation of the Obligation command

val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t: Implementation of the Next Obligation command

val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress: Implementation of the Solve Obligation command

val solve_all_obligations : unit Proofview.tactic option -> unit
val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit: Number of remaining obligations to be solved for this program

val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
val show_obligations : ?⁠msg:bool -> Names.Id.t option -> unit
val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit

exception NoObligations of Names.Id.t option

val explain_no_obligations : Names.Id.t option -> Pp.t
val check_program_libraries : unit -> unit