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 emptyevar_map
(indeed a proof can be triggered by an incomplete pretyping),init
takes an additional argument to represent the initialevar_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 ininit
, except that each element may depend on the previous goals. The telescope passes the goals in the form of aTerm.constr
which represents the goal as anevar
. Theevar_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 typetelescope
instead oflist
. Note that the firstevar_map
of the telescope plays the role of theevar_map
argument ininit
.
val finished : proofview -> bool
finished pv
istrue
if and only ifpv
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 indexi
to indexj
(inclusive, goals are indexed from1
). I.e. goals numberi
toj
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)
wherea
is the return value of the tactic,pv
is the updated proofview,b
a boolean which istrue
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, andgu
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 withLogic_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 exceptione
. 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 liket1
as long ast1
succeeds. Whenever the successes oft1
have been depleted and it failed withe
, then it behaves ast2 e
. In other words,tclOR
inserts a backtracking point. Int2
, exception can be assumed non critical.
val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
tclORELSE t1 t2
is equal tot1
ift1
has at least one success ort2 e
ift1
fails withe
. It is analogous totry/with
handler of exception in that it is not a backtracking point. Int2
, 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 oftclORELSE
: ifa
succeeds at least once then it behaves astclBIND a s
otherwise, ifa
fails withe
, then it behaves asf e
. Inf
exception can be assumed non critical.
val tclONCE : 'a tactic -> 'a tactic
tclONCE t
behave liket
except it has at most one success:tclONCE t
stops after the first success oft
. Ift
fails withe
,tclONCE t
also fails withe
.
exception
MoreThanOneSuccess
tclEXACTLY_ONCE e t
succeeds ast
ift
has exactly one success. Otherwise it fails. The tactict
is run until its first success, then a failure with exceptione
is simulated (e
has to be non critical). Ift
yields another success, thentclEXACTLY_ONCE e t
fails withMoreThanOneSuccess
(it is a user error). Otherwise,tclEXACTLY_ONCE e t
succeeds with the first success oft
. Notice that the choice ofe
is relevant, as the presence of further successes may depend one
(seetclOR
).
type 'a case
=
|
Fail of Exninfo.iexn
|
Next of 'a * Exninfo.iexn -> 'a tactic
tclCASE t
splitst
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 oftclONCE t
. Instead of stopping after the first success, it succeeds liket
until a failure with an exceptione
such thatp e = Some e'
is raised. At which point it drops the remaining successes, failing withe'
.tclONCE t
is equivalent totclBREAK (fun e -> Some e) t
.
Focusing tactics
exception
NoSuchGoals of int
tclFOCUS i j t
appliest
after focusing on the goals numberi
toj
(seefocus
). The rest of the goals is restored after the tactic action. If the specified range doesn't correspond to existing goals, fails with thenosuchgoal
argument, by default raisingNoSuchGoals
(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
appliest
on the list of focused goals described byli
. Each element ofli
is a pair(i, j)
denoting the goals numbered fromi
toj
(inclusive, starting from 1). It will try to applyt
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 withnosuchgoal
, by default raisingNoSuchGoals 0
.
val tclFOCUSID : ?nosuchgoal:'a tactic -> Names.Id.t -> 'a tactic -> 'a tactic
tclFOCUSID x t
appliest
on a (single) focused goal liketclFOCUS
. The goal is found by its name rather than its number. Fails withnosuchgoal
, by default raisingNoSuchGoals 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 ofunit tactic
-s and build aunit 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)
whereg
is the number of available goals, andt
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 oftclDISPATCH
, where ther
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, andr
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 whetherg
appears in another subgoal ofl
. The listl
may containg
, but it does not affect the result. Used byshelve_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 (seeshelve_unifiable
) in the current focus.
val unshelve : Evar.t list -> proofview -> proofview
unshelve l p
moves all the goals inl
from the shelf and put them at the end of the focused goals of p, if they are still undefined afteradvance
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
executestac
and returns its result together with the set of goals shelved bytac
. 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 then
first goal last. Ifn
is negative, then it puts then
last goals first.
val swap : int -> int -> unit tactic
swap i j
swaps the position of goals numberi
andj
(negative numbers can be used to address goals from the end. Goals are indexed from1
. For simplicity index0
corresponds to goal1
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 currentevar_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 viaProofview.Goal.env
.
Put-like primitives
val tclEFFECTS : Evd.side_effects -> unit tactic
tclEFFECTS eff
add the effectseff
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 aftert
. It it is identical to the state before, thentclPROGRESS t
fails, otherwise it succeeds liket
.
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 withtclZERO 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 asc
.
Notations
module Notations : sig ... end