# 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`

.

`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

`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 -> (Environ.named_context_val * 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

`val apply : name:Names.Id.t -> poly:bool -> Environ.env -> 'a tactic -> proofview -> 'a * proofview * bool * 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 tclTHEN : unit tactic -> 'a tactic -> 'a tactic`

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

###### Failure and backtracking

`val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic`

`tclZERO e`

fails with exception`e`

. It has no success. Exception is supposed to be non critical

`val tclOR : 'a tactic -> (Exninfo.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. In`t2`

, exception can be assumed non critical.

`val tclORELSE : 'a tactic -> (Exninfo.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. In`t2`

, exception can be assumed non critical.

`val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.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`

. In`f`

exception can be assumed non critical.

`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 (`e`

has to be non critical). If`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`

).

`type 'a case`

`=`

`|`

`Fail of Exninfo.iexn`

`|`

`Next of 'a * Exninfo.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 : (Exninfo.iexn -> Exninfo.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`

.

###### 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).

###### 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 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`

moves all the goals in`l`

from the shelf and put them at the end of the focused goals of p, if they are still undefined after`advance`

`val filter_shelf : (Evar.t -> bool) -> proofview -> proofview`

`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 : Evd.side_effects -> 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

`val tclTIMEOUTF : float -> 'a tactic -> 'a tactic`

`tclTIMEOUT n t`

can have only one success. In case of timeout it fails with`tclZERO Tac_Timeout`

.

`val tclTIMEOUT : int -> 'a tactic -> 'a tactic`

`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`

.

###### Notations

`module Notations : sig ... end`