Module Proofview

This files defines the basic mechanism of proofs: the proofview type is the state which tactics manipulate (a global state for existential variables, together with the list of goals), and the type 'a tactic is the (abstract) type of tactics modifying the proof state and returning a value of type 'a.

type proofview

Main state of tactics

val proofview : proofview -> Evar.t list * Evd.evar_map

Returns a stylised view of a proofview for use by, for instance, ide-s.

Starting and querying a proof view
type entry

Abstract representation of the initial goals of a proof.

val compact : entry -> proofview -> entry * proofview

Optimize memory consumption

val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview

Initialises a proofview, the main argument is a list of environments (including a named_context which are used as hypotheses) pair with conclusion types, creating accordingly many initial goals. Because a proof does not necessarily starts in an empty evar_map (indeed a proof can be triggered by an incomplete pretyping), init takes an additional argument to represent the initial evar_map.

type telescope =
| TNil of Evd.evar_map
| TCons of Environ.env * Evd.evar_map * EConstr.types * Evd.evar_map -> EConstr.constr -> telescope

A telescope is a list of environment and conclusion like in init, except that each element may depend on the previous goals. The telescope passes the goals in the form of a Term.constr which represents the goal as an evar. The evar_map is threaded in state passing style.

val dependent_init : telescope -> entry * proofview

Like init, but goals are allowed to be dependent on one another. Dependencies between goals is represented with the type telescope instead of list. Note that the first evar_map of the telescope plays the role of the evar_map argument in init.

val finished : proofview -> bool

finished pv is true if and only if pv is complete. That is, if it has an empty list of focused goals. There could still be unsolved subgoals, but they would then be out of focus.

val return : proofview -> Evd.evar_map

Returns the current evar state.

val partial_proof : entry -> proofview -> EConstr.constr list
val initial_goals : entry -> (EConstr.constr * EConstr.types) list
val with_empty_state : Proofview_monad.goal -> Proofview_monad.goal_with_state
val drop_state : Proofview_monad.goal_with_state -> Proofview_monad.goal
val goal_with_state : Proofview_monad.goal -> Proofview_monad.StateStore.t -> Proofview_monad.goal_with_state
Focusing commands
type focus_context

A focus_context represents the part of the proof view which has been removed by a focusing action, it can be used to unfocus later on.

val focus_context : focus_context -> Evar.t list * Evar.t list

Returns a stylised view of a focus_context for use by, for instance, ide-s.

val focus : int -> int -> proofview -> proofview * focus_context

focus i j focuses a proofview on the goals from index i to index j (inclusive, goals are indexed from 1). I.e. goals number i to j become the only focused goals of the returned proofview. It returns the focused proofview, and a context for the focus stack.

val unfocus : focus_context -> proofview -> proofview

Unfocuses a proofview with respect to a context.

The tactic monad
type +'a tactic

The abstract type of tactics

val apply : name:Names.Id.t -> poly:bool -> Environ.env -> 'a tactic -> proofview -> 'a * proofview * (bool * Evar.t list * Evar.t list) * Proofview_monad.Info.tree

Applies a tactic to the current proofview. Returns a tuple a,pv,(b,sh,gu) where a is the return value of the tactic, pv is the updated proofview, b a boolean which is true if the tactic has not done any action considered unsafe (such as admitting a lemma), sh is the list of goals which have been shelved by the tactic, and gu the list of goals on which the tactic has given up. In case of multiple success the first one is selected. If there is no success, fails with Logic_monad.TacticFailure

Monadic primitives
val tclUNIT : 'a -> 'a tactic

Unit of the tactic monad.

val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic

Bind operation of the tactic monad.

val tclTHEN : unit tactic -> 'a tactic -> 'a tactic

Interprets the ";" (semicolon) of Ltac. As a monadic operation, it's a specialized "bind".

val tclIGNORE : 'a tactic -> unit tactic

tclIGNORE t has the same operational content as t, but drops the returned value.

module Monad : Monad.S with type +'a t = 'a tactic

Generic monadic combinators for tactics.

Failure and backtracking
val tclZERO : ?⁠info:Exninfo.info -> exn -> 'a tactic

tclZERO e fails with exception e. It has no success.

val tclOR : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic

tclOR t1 t2 behaves like t1 as long as t1 succeeds. Whenever the successes of t1 have been depleted and it failed with e, then it behaves as t2 e. In other words, tclOR inserts a backtracking point.

val tclORELSE : 'a tactic -> (Util.iexn -> 'a tactic) -> 'a tactic

tclORELSE t1 t2 is equal to t1 if t1 has at least one success or t2 e if t1 fails with e. It is analogous to try/with handler of exception in that it is not a backtracking point.

val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Util.iexn -> 'b tactic) -> 'b tactic

tclIFCATCH a s f is a generalisation of tclORELSE: if a succeeds at least once then it behaves as tclBIND a s otherwise, if a fails with e, then it behaves as f e.

val tclONCE : 'a tactic -> 'a tactic

tclONCE t behave like t except it has at most one success: tclONCE t stops after the first success of t. If t fails with e, tclONCE t also fails with e.

exception MoreThanOneSuccess

tclEXACTLY_ONCE e t succeeds as t if t has exactly one success. Otherwise it fails. The tactic t is run until its first success, then a failure with exception e is simulated. It t yields another success, then tclEXACTLY_ONCE e t fails with MoreThanOneSuccess (it is a user error). Otherwise, tclEXACTLY_ONCE e t succeeds with the first success of t. Notice that the choice of e is relevant, as the presence of further successes may depend on e (see tclOR).

val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
type 'a case =
| Fail of Util.iexn
| Next of 'a * Util.iexn -> 'a tactic

tclCASE t splits t into its first success and a continuation. It is the most general primitive to control backtracking.

val tclCASE : 'a tactic -> 'a case tactic
val tclBREAK : (Util.iexn -> Util.iexn option) -> 'a tactic -> 'a tactic

tclBREAK p t is a generalization of tclONCE t. Instead of stopping after the first success, it succeeds like t until a failure with an exception e such that p e = Some e' is raised. At which point it drops the remaining successes, failing with e'. tclONCE t is equivalent to tclBREAK (fun e -> Some e) t.

Focusing tactics
exception NoSuchGoals of int

tclFOCUS i j t applies t after focusing on the goals number i to j (see focus). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to existing goals, fails with the nosuchgoal argument, by default raising NoSuchGoals (a user error). This exception is caught at toplevel with a default message.

val tclFOCUS : ?⁠nosuchgoal:'a tactic -> int -> int -> 'a tactic -> 'a tactic
val tclFOCUSLIST : ?⁠nosuchgoal:'a tactic -> (int * int) list -> 'a tactic -> 'a tactic

tclFOCUSLIST li t applies t on the list of focused goals described by li. Each element of li is a pair (i, j) denoting the goals numbered from i to j (inclusive, starting from 1). It will try to apply t to all the valid goals in any of these intervals. If the set of such goals is not a single range, then it will move goals such that it is a single range. (So, for instance, [1, 3-5]; idtac. is not the identity.) If the set of such goals is empty, it will fail with nosuchgoal, by default raising NoSuchGoals 0.

val tclFOCUSID : ?⁠nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic

tclFOCUSID x t applies t on a (single) focused goal like tclFOCUS. The goal is found by its name rather than its number. Fails with nosuchgoal, by default raising NoSuchGoals 1.

val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic

tclTRYFOCUS i j t behaves like tclFOCUS, except that if the specified range doesn't correspond to existing goals, behaves like tclUNIT () instead of failing.

Dispatching on goals
exception SizeMismatch of int * int

Dispatch tacticals are used to apply a different tactic to each goal under focus. They come in two flavours: tclDISPATCH takes a list of unit tactic-s and build a unit tactic. tclDISPATCHL takes a list of 'a tactic and returns an 'a list tactic.

They both work by applying each of the tactic in a focus restricted to the corresponding goal (starting with the first goal). In the case of tclDISPATCHL, the tactic returns a list of the same size as the argument list (of tactics), each element being the result of the tactic executed in the corresponding goal.

When the length of the tactic list is not the number of goal, raises SizeMismatch (g,t) where g is the number of available goals, and t the number of tactics passed.

val tclDISPATCH : unit tactic list -> unit tactic
val tclDISPATCHL : 'a tactic list -> 'a list tactic
val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic

tclEXTEND b r e is a variant of tclDISPATCH, where the r tactic is "repeated" enough time such that every goal has a tactic assigned to it (b is the list of tactics applied to the first goals, e to the last goals, and r is applied to every goal in between).

val tclINDEPENDENT : unit tactic -> unit tactic

tclINDEPENDENT tac runs tac on each goal successively, from the first one to the last one. Backtracking in one goal is independent of backtracking in another. It is equivalent to tclEXTEND [] tac [].

val tclINDEPENDENTL : 'a tactic -> 'a list tactic
Goal manipulation
val shelve : unit tactic

Shelves all the goals under focus. The goals are placed on the shelf for later use (or being solved by side-effects).

val shelve_goals : Evar.t list -> unit tactic

Shelves the given list of goals, which might include some that are under focus and some that aren't. All the goals are placed on the shelf for later use (or being solved by side-effects).

val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool

unifiable sigma g l checks whether g appears in another subgoal of l. The list l may contain g, but it does not affect the result. Used by shelve_unifiable.

val shelve_unifiable : unit tactic

Shelves the unifiable goals under focus, i.e. the goals which appear in other goals under focus (the unfocused goals are not considered).

val shelve_unifiable_informative : Evar.t list tactic

Idem but also returns the list of shelved variables

val guard_no_unifiable : Names.Name.t list option tactic

guard_no_unifiable returns the list of unifiable goals if some goals are unifiable (see shelve_unifiable) in the current focus.

val unshelve : Evar.t list -> proofview -> proofview

unshelve l p adds all the goals in l at the end of the focused goals of p

val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool

depends_on g1 g2 sigma checks if g1 occurs in the type/ctx of g2

val with_shelf : 'a tactic -> (Evar.t list * 'a) tactic

with_shelf tac executes tac and returns its result together with the set of goals shelved by tac. The current shelf is unchanged and the returned list contains only unsolved goals.

val cycle : int -> unit tactic

If n is positive, cycle n puts the n first goal last. If n is negative, then it puts the n last goals first.

val swap : int -> int -> unit tactic

swap i j swaps the position of goals number i and j (negative numbers can be used to address goals from the end. Goals are indexed from 1. For simplicity index 0 corresponds to goal 1 as well, rather than raising an error.

val revgoals : unit tactic

revgoals reverses the list of focused goals.

val numgoals : int tactic

numgoals returns the number of goals under focus.

Access primitives
val tclEVARMAP : Evd.evar_map tactic

tclEVARMAP doesn't affect the proof, it returns the current evar_map.

val tclENV : Environ.env tactic

tclENV doesn't affect the proof, it returns the current environment. It is not the environment of a particular goal, rather the "global" environment of the proof. The goal-wise environment is obtained via Proofview.Goal.env.

Put-like primitives
val tclEFFECTS : Safe_typing.private_constants -> unit tactic

tclEFFECTS eff add the effects eff to the current state.

val mark_as_unsafe : unit tactic

mark_as_unsafe declares the current tactic is unsafe.

val give_up : unit tactic

Gives up on the goal under focus. Reports an unsafe status. Proofs with given up goals cannot be closed.

Control primitives
val tclPROGRESS : 'a tactic -> 'a tactic

tclPROGRESS t checks the state of the proof after t. It it is identical to the state before, then tclPROGRESS t fails, otherwise it succeeds like t.

module Progress : sig ... end
val tclCHECKINTERRUPT : unit tactic

Checks for interrupts

exception Timeout
val tclTIMEOUT : int -> 'a tactic -> 'a tactic

tclTIMEOUT n t can have only one success. In case of timeout if fails with tclZERO Timeout.

val tclTIME : string option -> 'a tactic -> 'a tactic

tclTIME s t displays time for each atomic call to t, using s as an identifying annotation if present

val tclProofInfo : (Names.Id.t * bool) tactic

Internal, don't use.

Unsafe primitives
module Unsafe : sig ... end

The primitives in the Unsafe module should be avoided as much as possible, since they can make the proof state inconsistent. They are nevertheless helpful, in particular when interfacing the pretyping and the proof engine.

module UnsafeRepr : sig ... end

This module gives access to the innards of the monad. Its use is restricted to very specific cases.

Goal-dependent tactics
module Goal : sig ... end
Trace
module Trace : sig ... end
Non-logical state
module NonLogical : module type of Logic_monad.NonLogical

The NonLogical module allows the execution of effects (including I/O) in tactics (non-logical side-effects are not discarded at failures).

val tclLIFT : 'a NonLogical.t -> 'a tactic

tclLIFT c is a tactic which behaves exactly as c.