Ltac¶
This chapter documents the tactic language L
tac.
We start by giving the syntax followed by the informal semantics. To learn more about the language and especially about its foundations, please refer to [Del00]. (Note the examples in the paper won't work as-is; Coq has evolved since the paper was written.)
Example: Basic tactic macros
Here are some examples of simple tactic macros you can create with L
tac:
See Section Examples of using Ltac for more advanced examples.
Syntax¶
The syntax of the tactic language is given below.
The main entry of the grammar is ltac_expr
, which is used in proof mode
as well as to define new tactics with the Ltac
command.
The grammar uses multiple ltac_expr*
nonterminals to express how subexpressions
are grouped when they're not fully parenthesized. For example, in many programming
languages, a*b+c
is interpreted as (a*b)+c
because *
has
higher precedence than +
. Usually a/b/c
is given the left associative
interpretation (a/b)/c
rather than the right associative interpretation
a/(b/c)
.
In Coq, the expression try repeat tactic1 || tactic2; tactic3; tactic4
is interpreted as (try (repeat (tactic1 || tactic2)); tactic3); tactic4
because ||
is part of ltac_expr2
, which has higher precedence than
try
and repeat
(at the level of ltac_expr3
), which
in turn have higher precedence than ;
, which is part of ltac_expr4
.
(A lower number in the nonterminal name means higher precedence in this grammar.)
The constructs in ltac_expr
are left associative.
Note
Tactics described in other chapters of the documentation are simple_tactic
s,
which only modify the proof state. L
tac provides additional constructs that can generally
be used wherever a simple_tactic
can appear, even though they don't modify the proof
state and that syntactically they're at
varying levels in ltac_expr
. For simplicity of presentation, the L
tac constructs
are documented as tactics. Tactics are grouped as follows:
l3_tactic
s includeL
tac tactics:try
,do
,repeat
,timeout
,time
,progress
,once
,exactly_once
,only
andabstract
l2_tactic
s are:tryif
l1_tactic
s are thesimple_tactic
s,first
,solve
,idtac
,fail
andgfail
as well asmatch
,match goal
and theirlazymatch
andmultimatch
variants.value_tactic
s, which return values rather than change the proof state. They are:eval
,context
,numgoals
,fresh
,type of
andtype_term
.
The documentation for these L
tac constructs mentions which group they belong to.
The difference is only relevant in some compound tactics where
extra parentheses may be needed. For example, parenthesees are required in
idtac + (once idtac)
because once
is an l3_tactic
, which the
production ltac_expr2 ::= ltac_expr1 + ltac_expr2binder_tactic
doesn't
accept after the +
.
Note
The grammar reserves the token
||
.
Semantics¶
Types of values¶
An L
tac value can be a tactic, integer, string, unit (written as "()
" ) or syntactic value.
Syntactic values correspond to certain nonterminal symbols in the grammar,
each of which is a distinct type of value.
Most commonly, the value of an L
tac expression is a tactic that can be executed.
While there are a number of constructs that let you combine multiple tactics into
compound tactics, there are no operations for combining most other types of values.
For example, there's no function to add two integers. Syntactic values are entered
with the syn_value
construct. Values of all types can be assigned to toplevel
symbols with the Ltac
command or to local symbols with the let
tactic.
L
tac functions
can return values of any type.
Syntactic values¶
Provides a way to use the syntax and semantics of a grammar nonterminal as a
value in an ltac_expr
. The table below describes the most useful of
these. You can see the others by running "Print Grammar
tactic
" and
examining the part at the end under "Entry tactic:tactic_value".
ident
name of a grammar nonterminal listed in the table
nonterminal
represents syntax described by
nonterminal
.
Specified
ident
Parsed as
Interpreted as
as in tactic
ident
a user-specified name
string
a string
integer
an integer
reference
a qualified identifier
uconstr
an untyped term
constr
a term
ltac
a tactic
ltac:(ltac_expr)
can be used to indicate that the parenthesized item
should be interpreted as a tactic and not as a term. The constructs can also
be used to pass parameters to tactics written in OCaml. (While all
of the syn_value
s can appear at the beginning of an ltac_expr
,
the others are not useful because they will not evaluate to tactics.)
uconstr:(term)
can be used to build untyped terms.
Terms built in L
tac are well-typed by default. Building large
terms in recursive L
tac functions may give very slow behavior because
terms must be fully type checked at each step. In this case, using
an untyped term may avoid most of the repetitive type checking for the term,
improving performance.
Untyped terms built using uconstr:(…)
can be used as arguments to the
refine
tactic, for example. In that case the untyped term is type
checked against the conclusion of the goal, and the holes which are not solved
by the typing procedure are turned into new subgoals.
Tactics in terms¶
Allows including an ltac_expr
within a term. Semantically,
it's the same as the syn_value
for ltac
, but these are
distinct in the grammar.
Substitution¶
name
s within L
tac expressions are used to represent both terms and
L
tac variables. If the name
corresponds to
an L
tac variable or tactic name, L
tac substitutes the value before applying
the expression. Generally it's best to choose distinctive names for L
tac variables
that won't clash with term names. You can use ltac:(name)
or (name)
to control whether a name
is interpreted as, respectively, an L
tac
variable or a term.
Note that values from toplevel symbols, unlike locally-defined symbols, are
substituted only when they appear at the beginning of an ltac_expr
or
as a tactic_arg
. Local symbols are also substituted into tactics:
Example: Substitution of global and local symbols
- Goal True.
- 1 subgoal ============================ True
- Ltac n := 1.
- n is defined
- let n2 := n in idtac n2.
- 1
- Fail idtac n.
- The command has indeed failed with message: n not found.
Sequence: ;¶
A sequence is an expression of the following form:
-
Tactic
ltac_expr31 ; ltac_expr32binder_tactic
¶ The expression
ltac_expr31
is evaluated tov1
, which must be a tactic value. The tacticv1
is applied to the current goals, possibly producing more goals. Then the right-hand side is evaluated to producev2
, which must be a tactic value. The tacticv2
is applied to all the goals produced by the prior application. Sequence is associative.
Local application of tactics: [> ... ]¶
-
Tactic
[> for_each_goal ]
¶ Applies a different
ltac_expr?
to each of the focused goals. In the first form offor_each_goal
(without..
), the construct fails if the number of specifiedltac_expr?
is not the same as the number of focused goals. Omitting anltac_expr
leaves the corresponding goal unchanged.In the second form (with
ltac_expr? ..
), the left and rightgoal_tactics
are applied respectively to a prefix or suffix of the list of focused goals. Theltac_expr?
before the..
is applied to any focused goals in the middle (possibly none) that are not covered by thegoal_tactics
. The number ofltac_expr?
in thegoal_tactics
must be no more than the number of focused goals.In particular:
goal_tactics | .. | goal_tactics
The goals not covered by the two
goal_tactics
are left unchanged.[> ltac_expr .. ]
ltac_expr
is applied independently to each of the goals, rather than globally. In particular, if there are no goals, the tactic is not run at all. A tactic which expects multiple goals, such asswap
, would act as if a single goal is focused.
Note that
ltac_expr3 ; [ ltac_expr*| ]
is a convenient idiom to process the goals generated by applyingltac_expr3
.
-
Tactic
ltac_expr3 ; [ for_each_goal ]
¶ ltac_expr3 ; [ ... ]
is equivalent to[> ltac_expr3 ; [> ... ] .. ]
.
Goal selectors¶
By default, tactic expressions are applied only to the first goal. Goal
selectors provide a way to apply a tactic expression to another goal or multiple
goals. (The Default Goal Selector
option can be used to change the default
behavior.)
-
Tactic
toplevel_selector : ltac_expr
¶ Reorders the goals and applies
ltac_expr
to the selected goals. It can only be used at the top level of a tactic expression; it cannot be used within a tactic expression. The selected goals are reordered so they appear after the lowest-numbered selected goal, ordered by goal number. Example. If the selector applies to a single goal or to all goals, the reordering will not be apparent. The order of the goals in theselector
is irrelevant. (This may not be what you expect; see #8481.)all
Selects all focused goals.
!
If exactly one goal is in focus, apply
ltac_expr
to it. Otherwise the tactic fails.par
Applies
ltac_expr
to all focused goals in parallel. The number of workers can be controlled via the command line option-async-proofs-tac-j natural
to specify the desired number of workers. Limitations:par:
only works on goals that don't contain existential variables.ltac_expr
must either solve the goal completely or do nothing (i.e. it cannot make some progress).
Selectors can also be used nested within a tactic expression with the
only
tactic:
-
Tactic
only selector : ltac_expr3
¶ Applies
ltac_expr3
to the selected goals.range_selector+,
The selected goals are the union of the specified
range_selector
s.[ ident ]
Limits the application of
ltac_expr3
to the goal previously namedident
by the user (see Existential variables).natural1 - natural2
natural
Selects a single goal.
-
Error
No such goal.
¶
Example: Selector reordering goals
- Goal 1=0 /\ 2=0 /\ 3=0.
- 1 subgoal ============================ 1 = 0 /\ 2 = 0 /\ 3 = 0
- repeat split.
- 3 subgoals ============================ 1 = 0 subgoal 2 is: 2 = 0 subgoal 3 is: 3 = 0
- 1,3: idtac.
- 3 subgoals ============================ 1 = 0 subgoal 2 is: 3 = 0 subgoal 3 is: 2 = 0
Processing multiple goals¶
When presented with multiple focused goals, most L
tac constructs process each goal
separately. They succeed only if there is a success for each goal. For example:
Example: Multiple focused goals
This tactic fails because there no match for the second goal (False
).
- Goal True /\ False.
- 1 subgoal ============================ True /\ False
- split.
- 2 subgoals ============================ True subgoal 2 is: False
- Fail all: let n := numgoals in idtac "numgoals =" n; match goal with | |- True => idtac end.
- numgoals = 2 The command has indeed failed with message: No matching clauses for match.
Do loop¶
-
Tactic
do nat_or_var ltac_expr3
¶ The do loop repeats a tactic
nat_or_var
times:ltac_expr
is evaluated tov
, which must be a tactic value. This tactic valuev
is appliednat_or_var
times. Ifnat_or_var
> 1, after the first application ofv
,v
is applied, at least once, to the generated subgoals and so on. It fails if the application ofv
fails beforenat_or_var
applications have been completed.
Repeat loop¶
-
Tactic
repeat ltac_expr3
¶ The repeat loop repeats a tactic until it fails.
ltac_expr
is evaluated tov
. Ifv
denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed to make progress. The tacticrepeat
ltac_expr
itself never fails.
Catching errors: try¶
We can catch the tactic errors with:
-
Tactic
try ltac_expr3
¶ ltac_expr
is evaluated tov
which must be a tactic value. The tactic valuev
is applied to each focused goal independently. If the application ofv
fails in a goal, it catches the error and leaves the goal unchanged. If the level of the exception is positive, then the exception is re-raised with its level decremented.
Detecting progress¶
We can check if a tactic made progress with:
-
Tactic
progress ltac_expr3
¶ ltac_expr
is evaluated tov
which must be a tactic value. The tactic valuev
is applied to each focused subgoal independently. If the application ofv
to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised.-
Error
Failed to progress.
¶
-
Error
Branching and backtracking¶
L
tac provides several branching tactics that permit trying multiple alternative tactics
for a proof step. For example, first
, which tries several alternatives and selects the first
that succeeds, or tryif
, which tests whether a given tactic would succeed or fail if it was
applied and then, depending on the result, applies one of two alternative tactics. There
are also looping constructs do
and repeat
. The order in which the subparts
of these tactics are evaluated is generally similar to
structured programming constructs in many languages.
The +
, multimatch
and multimatch goal
tactics
provide more complex capability. Rather than applying a single successful
tactic, these tactics generate a series of successful tactic alternatives that are tried sequentially
when subsequent tactics outside these constructs fail. For example:
Example: Backtracking
- Fail multimatch True with | True => idtac "branch 1" | _ => idtac "branch 2" end ; idtac "branch A"; fail.
- branch 1 branch A branch 2 branch A The command has indeed failed with message: Tactic failure.
These constructs are evaluated using backtracking. Each creates a backtracking point. When a subsequent tactic fails, evaluation continues from the nearest prior backtracking point with the next successful alternative and repeats the tactics after the backtracking point. When a backtracking point has no more successful alternatives, evaluation continues from the next prior backtracking point. If there are no more prior backtracking points, the overall tactic fails.
Thus, backtracking tactics can have multiple successes. Non-backtracking constructs that appear
after a backtracking point are reprocessed after backtracking, as in the example
above, in which the ;
construct is reprocessed after backtracking. When a
backtracking construct is within
a non-backtracking construct, the latter uses the first success. Backtracking to
a point within a non-backtracking construct won't change the branch that was selected by the
non-backtracking construct.
The once
tactic stops further backtracking to backtracking points within that tactic.
Branching with backtracking: +¶
We can branch with backtracking with the following structure:
-
Tactic
ltac_expr1 + ltac_expr2binder_tactic
¶ Evaluates and applies
ltac_expr1
to each focused goal independently. If it fails (i.e. there is no initial success), then evaluates and applies the right-hand side. If the right-hand side fails, the construct fails.If
ltac_expr1
has an initial success and a subsequent tactic (outside the+
construct) fails,L
tac backtracks and selects the next success forltac_expr1
. If there are no more successes, then+
similarly evaluates and applies (and backtracks in) the right-hand side. To prevent evaluation of further alternatives after an initial success for a tactic, usefirst
instead.+
is left-associative.In all cases,
(ltac_expr1 + ltac_expr2); ltac_expr3
is equivalent to(ltac_expr1; ltac_expr3) + (ltac_expr2; ltac_expr3)
.Additionally, in most cases,
(ltac_expr1 + ltac_expr2) + ltac_expr3
is equivalent toltac_expr1 + (ltac_expr2 + ltac_expr3)
. Here's an example where the behavior differs slightly:- Goal True.
- 1 subgoal ============================ True
- Fail (fail 2 + idtac) + idtac.
- The command has indeed failed with message: Tactic failure.
- Fail fail 2 + (idtac + idtac).
- The command has indeed failed with message: Tactic failure (level 1).
Example: Backtracking branching with +
In the first tactic,
idtac "2"
is not executed. In the second, the subsequentfail
causes backtracking and the execution ofidtac "B"
.- Goal True.
- 1 subgoal ============================ True
- idtac "1" + idtac "2".
- 1
- assert_fails ((idtac "A" + idtac "B"); fail).
- A B
First tactic to succeed¶
In some cases backtracking may be too expensive.
-
Tactic
first [ ltac_expr*| ]
¶ For each focused goal, independently apply the first
ltac_expr
that succeeds. Theltac_expr
s must evaluate to tactic values. Failures in tactics after thefirst
won't cause backtracking. (To allow backtracking, use the+
construct above instead.)If the
first
contains a tactic that can backtrack, "success" means the first success of that tactic. Consider the following:Example: Backtracking inside a non-backtracking construct
- Goal True.
- 1 subgoal ============================ True
The
fail
doesn't trigger the secondidtac
:- assert_fails (first [ idtac "1" | idtac "2" ]; fail).
- 1
This backtracks within
(idtac "1A" + idtac "1B" + fail)
butfirst
won't consider theidtac "2"
alternative:- assert_fails (first [ (idtac "1A" + idtac "1B" + fail) | idtac "2" ]; fail).
- 1A 1B
-
Error
No applicable tactic.
¶
-
Variant
first ltac_expr
This is an
L
tac alias that gives a primitive access to the first tactical as anL
tac definition without going through a parsing rule. It expects to be given a list of tactics through aTactic Notation
command, permitting notations with the following form to be written:Example
- Tactic Notation "foo" tactic_list(tacs) := first tacs.
Solving¶
Selects and applies the first tactic that solves each goal (i.e. leaves no subgoal) in a series of alternative tactics:
-
Tactic
solve [ ltac_expri*| ]
¶ For each current subgoal: evaluates and applies each
ltac_expr
in order until one is found that solves the subgoal.If any of the subgoals are not solved, then the overall
solve
fails.Note
In
solve
andfirst
,ltac_expr
s that don't evaluate to tactic values are ignored. Sosolve
[ () | 1 |
constructor
]
is equivalent tosolve
[
constructor
]
. This may make it harder to debug scripts that inadvertently include non-tactic values.
First tactic to make progress: ||¶
Yet another way of branching without backtracking is the following structure:
-
Tactic
ltac_expr1 || ltac_expr2binder_tactic
¶ ltac_expr1 || ltac_expr2
is equivalent tofirst [ progress ltac_expr1 | ltac_expr2 ]
, except that if it fails, it fails likeltac_expr2. `||
is left-associative.ltac_expr
s that don't evaluate to tactic values are ignored. See the note atsolve
.
Conditional branching: tryif¶
-
Tactic
tryif ltac_exprtest then ltac_exprthen else ltac_expr2else
¶ For each focused goal, independently: Evaluate and apply
ltac_exprtest
. Ifltac_exprtest
succeeds at least once, evaluate and applyltac_exprthen
to all the subgoals generated byltac_exprtest
. Otherwise, evaluate and applyltac_expr2else
to all the subgoals generated byltac_exprtest
.
Soft cut: once¶
Another way of restricting backtracking is to restrict a tactic to a single success:
-
Tactic
once ltac_expr3
¶ ltac_expr3
is evaluated tov
which must be a tactic value. The tactic valuev
is applied but only its first success is used. Ifv
fails,once
ltac_expr3
fails likev
. Ifv
has at least one success,once
ltac_expr3
succeeds once, but cannot produce more successes.
Checking for a single success: exactly_once¶
Coq provides an experimental way to check that a tactic has exactly one success:
-
Tactic
exactly_once ltac_expr3
¶ ltac_expr3
is evaluated tov
which must be a tactic value. The tactic valuev
is applied if it has at most one success. Ifv
fails,exactly_once
ltac_expr3
fails likev
. Ifv
has a exactly one success,exactly_once
ltac_expr3
succeeds likev
. Ifv
has two or more successes,exactly_once
ltac_expr3
fails.exactly_once
is anl3_tactic
.Warning
The experimental status of this tactic pertains to the fact if
v
has side effects, they may occur in an unpredictable way. Indeed, normallyv
would only be executed up to the first success until backtracking is needed, howeverexactly_once
needs to look ahead to see whether a second success exists, and may run further effects immediately.-
Error
This tactic has more than one success.
¶
-
Error
Checking for failure: assert_fails¶
Coq defines an L
tac tactic in Init.Tactics
to check that a tactic fails:
-
Tactic
assert_fails ltac_expr3
¶ If
ltac_expr3
fails, the proof state is unchanged and no message is printed. Ifltac_expr3
unexpectedly has at least one success, the tactic performs agfail
0
, printing the following message:-
Error
Tactic failure: <tactic closure> succeeds.
¶
Note
assert_fails
andassert_succeeds
work as described whenltac_expr3
is asimple_tactic
. In some more complex expressions, they may report an error from withinltac_expr3
when they shouldn't. This is due to the order in which parts of theltac_expr3
are evaluated and executed. For example:- Goal True.
- 1 subgoal ============================ True
- assert_fails match True with _ => fail end.
- Toplevel input, characters 0-43: > assert_fails match True with _ => fail end. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Tactic failure.
should not show any message. The issue is that
assert_fails
is anL
tac-defined tactic. That makes it a function that's processed in the evaluation phase, causing thematch
to find its first success earlier. One workaround is to prefixltac_expr3
with "idtac;
".- assert_fails (idtac; match True with _ => fail end).
Alternatively, substituting the
match
into the definition ofassert_fails
works as expected:- tryif (once match True with _ => fail end) then gfail 0 "succeeds" else idtac.
-
Error
Checking for success: assert_succeeds¶
Coq defines an L
tac tactic in Init.Tactics
to check that a tactic has at least one
success:
-
Tactic
assert_succeeds ltac_expr3
¶ If
ltac_expr3
has at least one success, the proof state is unchanged and no message is printed. Ifltac_expr3
fails, the tactic performs agfail
0
, printing the following message:-
Error
Tactic failure: <tactic closure> fails.
¶
-
Error
Print/identity tactic: idtac¶
Failing¶
-
Tactic
failgfail int_or_var? identstringnatural*
¶ fail
is the always-failing tactic: it does not solve any goal. It is useful for defining other tactics since it can be caught bytry
,repeat
,match goal
, or the branching tacticals.gfail
fails even when used after;
and there are no goals left. Similarly,gfail
fails even when used afterall:
and there are no goals left.fail
andgfail
arel1_tactic
s.See the example for a comparison of the two constructs.
Note that if Coq terms have to be printed as part of the failure, term construction always forces the tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like
let
x := H in
fail
0 x
will succeed.int_or_var
The failure level. If no level is specified, it defaults to 0. The level is used by
try
,repeat
,match goal
and the branching tacticals. If 0, it makesmatch goal
consider the next clause (backtracking). If nonzero, the currentmatch goal
block,try
,repeat
, or branching command is aborted and the level is decremented. In the case of+
, a nonzero level skips the first backtrack point, even if the call tofail
natural
is not enclosed in a+
construct, respecting the algebraic identity.identstringnatural*
The given tokens are used for printing the failure message. If
ident
is anL
tac variable, its contents are printed; if not, it is an error.
-
Error
Tactic failure.
¶
-
Error
No such goal.
¶
Example
- Goal True.
- 1 subgoal ============================ True
- Proof. fail. Abort.
- Toplevel input, characters 7-12: > Proof. fail. > ^^^^^ Error: Tactic failure.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial; fail. Qed.
- No more subgoals.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial. fail. Abort.
- No more subgoals. Toplevel input, characters 16-21: > Proof. trivial. fail. > ^^^^^ Error: No such goal.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial. all: fail. Qed.
- No more subgoals.
- Goal True.
- 1 subgoal ============================ True
- Proof. gfail. Abort.
- Toplevel input, characters 7-13: > Proof. gfail. > ^^^^^^ Error: Tactic failure.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial; gfail. Abort.
- Toplevel input, characters 7-22: > Proof. trivial; gfail. > ^^^^^^^^^^^^^^^ Error: Tactic failure.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial. gfail. Abort.
- No more subgoals. Toplevel input, characters 16-22: > Proof. trivial. gfail. > ^^^^^^ Error: No such goal.
- Goal True.
- 1 subgoal ============================ True
- Proof. trivial. all: gfail. Abort.
- No more subgoals. Toplevel input, characters 16-27: > Proof. trivial. all: gfail. > ^^^^^^^^^^^ Error: Tactic failure.
Timeout¶
We can force a tactic to stop if it has not finished after a certain amount of time:
-
Tactic
timeout nat_or_var ltac_expr3
¶ ltac_expr3
is evaluated tov
which must be a tactic value. The tactic valuev
is applied normally, except that it is interrupted afternat_or_var
seconds if it is still running. In this case the outcome is a failure.Warning
For the moment, timeout is based on elapsed time in seconds, which is very machine-dependent: a script that works on a quick machine may fail on a slow one. The converse is even possible if you combine a timeout with some other tacticals. This tactical is hence proposed only for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that this tactical isn’t available on the native Windows port of Coq.
Timing a tactic¶
A tactic execution can be timed:
-
Tactic
time string? ltac_expr3
¶ evaluates
ltac_expr3
and displays the running time of the tactic expression, whether it fails or succeeds. In case of several successes, the time for each successive run is displayed. Time is in seconds and is machine-dependent. Thestring
argument is optional. When provided, it is used to identify this particular occurrence oftime
.
Timing a tactic that evaluates to a term: time_constr¶
Tactic expressions that produce terms can be timed with the experimental tactic
-
Tactic
time_constr ltac_expr
¶ which evaluates
ltac_expr ()
and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is machine-dependent.This tactic currently does not support nesting, and will report times based on the innermost execution. This is due to the fact that it is implemented using the following internal tactics:
-
Tactic
finish_timing ( string )? string?
¶ Display an optionally named timer. The parenthesized string argument is also optional, and determines the label associated with the timer for printing.
By copying the definition of time_constr
from the standard library,
users can achieve support for a fixed pattern of nesting by passing
different string
parameters to restart_timer
and
finish_timing
at each level of nesting.
Example
- Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in let ret := tac () in let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) "(depth 1)" end in ret.
- time_constr1 is defined
- Goal True.
- 1 subgoal ============================ True
- let v := time_constr ltac:(fun _ => let x := time_constr1 ltac:(fun _ => constr:(10 * 10)) in let y := time_constr1 ltac:(fun _ => eval compute in x) in y) in pose v.
- Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s) Tactic evaluation (depth 1) ran for 0. secs (0.u,0.s) Tactic evaluation ran for 0.001 secs (0.u,0.001s) 1 subgoal n := 100 : nat ============================ True
Local definitions: let¶
-
Tactic
let rec? let_clause with let_clause* in ltac_expr
¶ -
Binds symbols within
ltac_expr
.let
evaluates eachlet_clause
, substitutes the bound variables intoltac_expr
and then evaluatesltac_expr
. There are no dependencies between thelet_clause
s.Use
let
rec
to create recursive or mutually recursive bindings, which causes the definitions to be evaluated lazily.let
is abinder_tactic
.
Function construction and application¶
A parameterized tactic can be built anonymously (without resorting to local definitions) with:
-
Tactic
fun name+ => ltac_expr
¶ Indeed, local definitions of functions are syntactic sugar for binding a
fun
tactic to an identifier.fun
is abinder_tactic
.
Functions can return values of any type.
A function application is an expression of the form:
-
Tactic
qualid tactic_arg+
qualid
must be bound to aL
tac function with at least as many arguments as the providedtactic_arg
s. Thetactic_arg
s are evaluated before the function is applied or partially applied.Functions may be defined with the
fun
andlet
tactics and with theLtac
command.
Pattern matching on terms: match¶
-
Tactic
match_key ltac_exprterm with |? match_pattern => ltac_expr+| end
¶ lazymatch
,match
andmultimatch
areltac_expr1
s.Evaluates
ltac_exprterm
, which must yield a term, and matches it sequentially with thematch_pattern
s, which may have metavariables. When a match is found, metavariable values are substituted intoltac_expr
, which is then applied.Matching may continue depending on whether
lazymatch
,match
ormultimatch
is specified.In the
match_pattern
s, metavariables have the form?ident
, whereas in theltac_expr
s, the question mark is omitted. Choose your metavariable names with care to avoid name conflicts. For example, if you use the metavariableS
, then theltac_expr
can't useS
to refer to the constructor ofnat
without qualifying the constructor asDatatypes.S
.Matching is non-linear: if a metavariable occurs more than once, each occurrence must match the same expression. Expressions match if they are syntactically equal or are α-convertible. Matching is first-order except on variables of the form
@?ident
that occur in the head position of an application. For these variables, matching is second-order and returns a functional term.lazymatch
Causes the match to commit to the first matching branch rather than trying a new match if
ltac_expr
fails. Example.match
If
ltac_expr
fails, continue matching with the next branch. Failures in subsequent tactics (after thematch
) will not cause selection of a new branch. Examples here and here.multimatch
If
ltac_expr
fails, continue matching with the next branch. When anltac_expr
succeeds for a branch, subsequent failures (after themultimatch
) causing consumption of all the successes ofltac_expr
trigger selection of a new matching branch. Example.match
…
is, in fact, shorthand foronce
multimatch
…
.cpattern
The syntax of
cpattern
is the same as that ofterm
s, but it can contain pattern matching metavariables in the form?ident
._
can be used to match irrelevant terms. Example.When a metavariable in the form
?id
occurs under binders, sayx1, …, xn
and the expression matches, the metavariable is instantiated by a term which can then be used in any context which also binds the variablesx1, …, xn
with same types. This provides with a primitive form of matching under context which does not require manipulating a functional term.There is also a special notation for second-order pattern matching: in an applicative pattern of the form
@?ident ident1 … identn
, the variableident
matches any complex expression with (possible) dependencies in the variablesidenti
and returns a functional term of the formfun ident1 … identn => term
.
context ident? [ cpattern ]
Matches any term with a subterm matching
cpattern
. If there is a match andident
is present, it is assigned the "matched context", i.e. the initial term where the matched subterm is replaced by a hole. Note thatcontext
(with very similar syntax) appearing after the=>
is thecontext
tactic.For
match
andmultimatch
, if the evaluation of theltac_expr
fails, the next matching subterm is tried. If no further subterm matches, the next branch is tried. Matching subterms are considered from top to bottom and from left to right (with respect to the raw printing obtained by setting thePrinting All
flag). Example.
ltac_expr
The tactic to apply if the construct matches. Metavariable values from the pattern match are substituted into
ltac_expr
before it's applied. Note that metavariables are not prefixed with the question mark as they are incpattern
.If
ltac_expr
evaluates to a tactic, then it is applied. If the tactic succeeds, the result of the match expression isidtac
. Ifltac_expr
does not evaluate to a tactic, that value is the result of the match expression.If
ltac_expr
is a tactic with backtracking points, then subsequent failures after alazymatch
ormultimatch
(but notmatch
) can cause backtracking intoltac_expr
to select its next success. (match
…
is equivalent toonce
multimatch
…
. Theonce
prevents backtracking into thematch
after it has succeeded.)
Note
Each
L
tac construct is processed in two phases: an evaluation phase and an execution phase. In most cases, tactics that may change the proof state are applied in the second phase. (Tactics that generate integer, string or syntactic values, such asfresh
, are processed during the evaluation phase.)Unlike other tactics,
*match*
tactics get their first success (applying tactics to do so) as part of the evaluation phase. Among other things, this can affect how early failures are processed inassert_fails
. Please see the note inassert_fails
.-
Error
No matching clauses for match.
¶ For at least one of the focused goals, there is no branch that matches its pattern and gets at least one success for
ltac_expr
.
-
Error
Argument of match does not evaluate to a term.
¶ This happens when
ltac_exprterm
does not denote a term.
Example: Comparison of lazymatch and match
In
lazymatch
, ifltac_expr
fails, thelazymatch
fails; it doesn't look for further matches. Inmatch
, ifltac_expr
fails in a matching branch, it will try to match on subsequent branches.
- Goal True.
- 1 subgoal ============================ True
- Fail lazymatch True with | True => idtac "branch 1"; fail | _ => idtac "branch 2" end.
- branch 1 The command has indeed failed with message: Tactic failure.
- match True with | True => idtac "branch 1"; fail | _ => idtac "branch 2" end.
- branch 1 branch 2
Example: Comparison of match and multimatch
match
tactics are only evaluated once, whereasmultimatch
tactics may be evaluated more than once if the following constructs trigger backtracking:
- Fail match True with | True => idtac "branch 1" | _ => idtac "branch 2" end ; idtac "branch A"; fail.
- branch 1 branch A The command has indeed failed with message: Tactic failure.
- Fail multimatch True with | True => idtac "branch 1" | _ => idtac "branch 2" end ; idtac "branch A"; fail.
- branch 1 branch A branch 2 branch A The command has indeed failed with message: Tactic failure.
Example: Matching a pattern with holes
Notice the
idtac
prints(z + 1)
while thepose
substitutes(x + 1)
.
- Goal True.
- 1 subgoal ============================ True
- match constr:(fun x => (x + 1) * 3) with | fun z => ?y * 3 => idtac "y =" y; pose (fun z: nat => y * 5) end.
- y = (z + 1) 1 subgoal n := fun x : nat => (x + 1) * 5 : nat -> nat ============================ True
Example: Multiple matches for a "context" pattern.
Internally "x <> y" is represented as "(~ (x = y))", which produces the first match.
- Ltac f t := match t with | context [ (~ ?t) ] => idtac "?t = " t; fail | _ => idtac end.
- f is defined
- Goal True.
- 1 subgoal ============================ True
- f ((~ True) <> (~ False)).
- ?t = ((~ True) = (~ False)) ?t = True ?t = False
Pattern matching on goals and hypotheses: match goal¶
-
Tactic
match_key reverse? goal with |? goal_pattern => ltac_expr+| end
¶ - |_
lazymatch goal
,match goal
andmultimatch goal
arel1_tactic
s.Use this form to match hypotheses and/or goals in the local context. These patterns have zero or more subpatterns to match hypotheses followed by a subpattern to match the conclusion. Except for the differences noted below, this works the same as the corresponding
match_key ltac_expr
construct (seematch
). Each current goal is processed independently.Matching is non-linear: if a metavariable occurs more than once, each occurrence must match the same expression. Within a single term, expressions match if they are syntactically equal or α-convertible. When a metavariable is used across multiple hypotheses or across a hypothesis and the current goal, the expressions match if they are convertible.
match_hyp*,
Patterns to match with hypotheses. Each pattern must match a distinct hypothesis in order for the branch to match.
Hypotheses have the form
name := termbinder? : type
. Patterns bind each of these nonterminals separately:Pattern syntax
Example pattern
n : ?t
n := ?b
name := termbinder : type
n := ?b : ?t
name := [ match_patternbinder ] : match_patterntype
n := [ ?b ] : ?t
name
can't have a?
. Note that the last two forms are equivalent except that:if the
:
in the third form has been bound to something else in a notation, you must use the fourth form. Note that cmd:Require Import
ssreflect
loads a notation that does this.a
termbinder
such as[ ?l ]
(e.g., denoting a singleton list afterImport
ListNotations
) must be parenthesized or, for the fourth form, use double brackets:[ [ ?l ] ]
.
termbinder
s in the form[?x ; ?y]
for a list are not parsed correctly. The workaround is to add parentheses or to use the underlying term instead of the notation, i.e.(cons ?x ?y)
.If there are multiple
match_hyp
s in a branch, there may be multiple ways to match them to hypotheses. Formatch goal
andmultimatch goal
, if the evaluation of theltac_expr
fails, matching will continue with the next hypothesis combination. When those are exhausted, the next alternative from anycontext
constructs in thematch_pattern
s is tried and then, when the context alternatives are exhausted, the next branch is tried. Example.reverse
Hypothesis matching for
match_hyp
s normally begins by matching them from left to right, to hypotheses, last to first. Specifyingreverse
begins matching in the reverse order, from first to last. Normal and reverse examples.|- match_pattern
A pattern to match with the current goal
goal_pattern with [ ... ]
The square brackets don't affect the semantics. They are permitted for aesthetics.
Examples:
Example: Matching hypotheses
Hypotheses are matched from the last hypothesis (which is by default the newest hypothesis) to the first until the
apply
succeeds.
- Goal forall A B : Prop, A -> B -> (A->B).
- 1 subgoal ============================ forall A B : Prop, A -> B -> A -> B
- intros.
- 1 subgoal A, B : Prop H : A H0 : B H1 : A ============================ B
- match goal with | H : _ |- _ => idtac "apply " H; apply H end.
- apply H1 apply H0 No more subgoals.
Example: Matching hypotheses with reverse
Hypotheses are matched from the first hypothesis to the last until the
apply
succeeds.
- Goal forall A B : Prop, A -> B -> (A->B).
- 1 subgoal ============================ forall A B : Prop, A -> B -> A -> B
- intros.
- 1 subgoal A, B : Prop H : A H0 : B H1 : A ============================ B
- match reverse goal with | H : _ |- _ => idtac "apply " H; apply H end.
- apply A apply B apply H apply H0 No more subgoals.
Example: Multiple ways to match hypotheses
Every possible match for the hypotheses is evaluated until the right-hand side succeeds. Note that
H1
andH2
are never matched to the same hypothesis. Observe that the number of permutations can grow as the factorial of the number of hypotheses and hypothesis patterns.
- Goal forall A B : Prop, A -> B -> (A->B).
- 1 subgoal ============================ forall A B : Prop, A -> B -> A -> B
- intros A B H.
- 1 subgoal A, B : Prop H : A ============================ B -> A -> B
- match goal with | H1 : _, H2 : _ |- _ => idtac "match " H1 H2; fail | _ => idtac end.
- match B H match A H match H B match A B match H A match B A
Filling a term context¶
The following expression is not a tactic in the sense that it does not produce subgoals but generates a term to be used in tactic expressions:
-
Tactic
context ident [ term ]
¶ Returns the term matched with the
context
pattern (described here) substitutingterm
for the hole created by the pattern.context
is avalue_tactic
.-
Error
Not a context variable.
¶
Example: Substituting a matched context
- Goal True /\ True.
- 1 subgoal ============================ True /\ True
- match goal with | |- context G [True] => let x := context G [False] in idtac x end.
- (False /\ True)
-
Error
Generating fresh hypothesis names¶
Tactics sometimes need to generate new names for hypothesis. Letting Coq choose a name with the intro tactic is not so good since it is very awkward to retrieve that name. The following expression returns an identifier:
-
Tactic
fresh stringqualid*
¶ Returns a fresh identifier name (i.e. one that is not already used in the local context and not previously returned by
fresh
in the currentltac_expr
). The fresh identifier is formed by concatenating the finalident
of eachqualid
(dropping any qualified components) and each specifiedstring
. If the resulting name is already used, a number is appended to make it fresh. If no arguments are given, the name is a fresh derivative of the nameH
.Note
We recommend generating the fresh identifier immediately before adding it to the local context. Using
fresh
in a local function may not work as you expect:Successive calls to
fresh
give distinct names even if the names haven't yet been added to the local context:- Goal True -> True.
- 1 subgoal ============================ True -> True
- intro x.
- 1 subgoal x : True ============================ True
- let a := fresh "x" in let b := fresh "x" in idtac a b.
- x0 x1
When applying
fresh
in a function, the name is chosen based on the tactic context at the point where the function was defined:- let a := fresh "x" in let f := fun _ => fresh "x" in let c := f () in let d := f () in idtac a c d.
- x0 x1 x1
fresh
is avalue_tactic
.
Computing in a term: eval¶
Evaluation of a term can be performed with:
-
Tactic
eval red_expr in term
¶ eval
is avalue_tactic
.
Getting the type of a term¶
-
Tactic
type of term
¶ This tactic returns the type of
term
.type of
is avalue_tactic
.
Manipulating untyped terms: type_term¶
The uconstr : ( term )
construct can be used to build an untyped term.
See syn_value
.
-
Tactic
type_term one_term
¶ In
L
tac, an untyped term can contain references to hypotheses or toL
tac variables containing typed or untyped terms. An untyped term can be type checked withtype_term
whose argument is parsed as an untyped term and returns a well-typed term which can be used in tactics.type_term
is avalue_tactic
.
Counting goals: numgoals¶
-
Tactic
numgoals
¶ The number of goals under focus can be recovered using the
numgoals
function. Combined with theguard
tactic below, it can be used to branch over the number of goals produced by previous tactics.numgoals
is avalue_tactic
.Example
- Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals".
- pr_numgoals is defined
- Goal True /\ True /\ True.
- 1 subgoal ============================ True /\ True /\ True
- split;[|split].
- 3 subgoals ============================ True subgoal 2 is: True subgoal 3 is: True
- all:pr_numgoals.
- There are 3 goals
Testing boolean expressions: guard¶
-
Tactic
guard int_or_var comparison int_or_var
¶ Tests a boolean expression. If the expression evaluates to true, it succeeds without affecting the proof. The tactic fails if the expression is false.
The accepted tests are simple integer comparisons.
Example
- Goal True /\ True /\ True.
- 1 subgoal ============================ True /\ True /\ True
- split;[|split].
- 3 subgoals ============================ True subgoal 2 is: True subgoal 3 is: True
- all:let n:= numgoals in guard n<4.
- Fail all:let n:= numgoals in guard n=2.
- The command has indeed failed with message: Condition not satisfied: 3=2
-
Error
Condition not satisfied.
¶
Proving a subgoal as a separate lemma: abstract¶
-
Tactic
abstract ltac_expr2 using identname?
¶ Does a
solve
[ ltac_expr2 ]
and saves the subproof as an auxiliary lemma. ifidentname
is specified, the lemma is saved with that name; otherwise the lemma is saved with the nameident
_subproof
natural?
whereident
is the name of the current goal (e.g. the theorem name) andnatural
is chosen to get a fresh name. If the proof is closed withQed
, the auxiliary lemma is inlined in the final proof term.This is useful with tactics such as
omega
ordiscriminate
that generate huge proof terms with many intermediate goals. It can significantly reduce peak memory use. In most cases it doesn't have a significant impact on run time. One case in which it can reduce run time is when a tacticfoo
is known to always pass type checking when it succeeds, such as in reflective proofs. In this case, the idiom "abstract
exact_no_check
foo
" will save half the type checking type time compared to "exact
foo
".Warning
The abstract tactic, while very useful, still has some known limitations. See #9146 for more details. We recommend caution when using it in some "non-standard" contexts. In particular,
abstract
doesn't work properly when used inside quotationsltac:(...)
. If used as part of typeclass resolution, it may produce incorrect terms when in polymorphic universe mode.Warning
Provide
identname
at your own risk; explicitly named and reused subterms don’t play well with asynchronous proofs.
-
Tactic
transparent_abstract ltac_expr3 using ident?
¶ Like
abstract
, but save the subproof in a transparent lemma with a name in the formident
_subterm
natural?
.Warning
Use this feature at your own risk; building computationally relevant terms with tactics is fragile, and explicitly named and reused subterms don’t play well with asynchronous proofs.
-
Error
Proof is not complete.
¶
-
Error
Tactic toplevel definitions¶
Defining L
tac symbols¶
L
tac toplevel definitions are made as follows:
-
Command
Ltac tacdef_body with tacdef_body*
¶ Defines or redefines an
L
tac symbol.If the
local
attribute is specified, the definition will not be exported outside the current module.qualid
Name of the symbol being defined or redefined
name*
If specified, the symbol defines a function with the given parameter names. If no names are specified,
qualid
is assigned the value ofltac_expr
.:=
Defines a user-defined symbol, but gives an error if the symbol has already been defined.
::=
Redefines an existing user-defined symbol, but gives an error if the symbol doesn't exist. Note that
Tactic Notation
s do not count as user-defined tactics for::=
. Iflocal
is not specified, the redefinition applies across module boundaries.with tacdef_body*
Permits definition of mutually recursive tactics.
Examples of using L
tac¶
Proof that the natural numbers have at least two elements¶
Example: Proof that the natural numbers have at least two elements
The first example shows how to use pattern matching over the proof context to prove that natural numbers have at least two elements. This can be done as follows:
- Lemma card_nat : ~ exists x y : nat, forall z:nat, x = z \/ y = z.
- 1 subgoal ============================ ~ (exists x y : nat, forall z : nat, x = z \/ y = z)
- Proof.
- intros (x & y & Hz).
- 1 subgoal x, y : nat Hz : forall z : nat, x = z \/ y = z ============================ False
- destruct (Hz 0), (Hz 1), (Hz 2).
- 8 subgoals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 ============================ False subgoal 2 is: False subgoal 3 is: False subgoal 4 is: False subgoal 5 is: False subgoal 6 is: False subgoal 7 is: False subgoal 8 is: False
At this point, the congruence
tactic would finish the job:
- all: congruence.
- No more subgoals.
But for the purpose of the example, let's craft our own custom tactic to solve this:
- Lemma card_nat : ~ exists x y : nat, forall z:nat, x = z \/ y = z.
- 1 subgoal ============================ ~ (exists x y : nat, forall z : nat, x = z \/ y = z)
- Proof.
- intros (x & y & Hz).
- 1 subgoal x, y : nat Hz : forall z : nat, x = z \/ y = z ============================ False
- destruct (Hz 0), (Hz 1), (Hz 2).
- 8 subgoals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 ============================ False subgoal 2 is: False subgoal 3 is: False subgoal 4 is: False subgoal 5 is: False subgoal 6 is: False subgoal 7 is: False subgoal 8 is: False
- all: match goal with | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a end.
- 8 subgoals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 H2 : 1 = 2 ============================ False subgoal 2 is: False subgoal 3 is: False subgoal 4 is: False subgoal 5 is: False subgoal 6 is: False subgoal 7 is: False subgoal 8 is: False
- all: discriminate.
- No more subgoals.
Notice that all the (very similar) cases coming from the three
eliminations (with three distinct natural numbers) are successfully
solved by a match goal
structure and, in particular, with only one
pattern (use of non-linear matching).
Proving that a list is a permutation of a second list¶
Example: Proving that a list is a permutation of a second list
Let's first define the permutation predicate:
- Section Sort.
- Variable A : Set.
- A is declared
- Inductive perm : list A -> list A -> Prop := | perm_refl : forall l, perm l l | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2.
- perm is defined perm_ind is defined perm_sind is defined
- End Sort.
- Require Import List.
Next we define an auxiliary tactic perm_aux
which takes an
argument used to control the recursion depth. This tactic works as
follows: If the lists are identical (i.e. convertible), it
completes the proof. Otherwise, if the lists have identical heads,
it looks at their tails. Finally, if the lists have different
heads, it rotates the first list by putting its head at the end.
Every time we perform a rotation, we decrement n
. When n
drops down to 1
, we stop performing rotations and we fail.
The idea is to give the length of the list as the initial value of
n
. This way of counting the number of rotations will avoid
going back to a head that had been considered before.
From Section Syntax we know that Ltac has a primitive
notion of integers, but they are only used as arguments for
primitive tactics and we cannot make computations with them. Thus,
instead, we use Coq's natural number type nat
.
- Ltac perm_aux n := match goal with | |- (perm _ ?l ?l) => apply perm_refl | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => let newn := eval compute in (length l1) in (apply perm_cons; perm_aux newn) | |- (perm ?A (?a :: ?l1) ?l2) => match eval compute in n with | 1 => fail | _ => let l1' := constr:(l1 ++ a :: nil) in (apply (perm_trans A (a :: l1) l1' l2); [ apply perm_append | compute; perm_aux (pred n) ]) end end.
- perm_aux is defined
The main tactic is solve_perm
. It computes the lengths of the
two lists and uses them as arguments to call perm_aux
if the
lengths are equal. (If they aren't, the lists cannot be
permutations of each other.)
- Ltac solve_perm := match goal with | |- (perm _ ?l1 ?l2) => match eval compute in (length l1 = length l2) with | (?n = ?n) => perm_aux n end end.
- solve_perm is defined
And now, here is how we can use the tactic solve_perm
:
- Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
- 1 subgoal ============================ perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil)
- solve_perm.
- No more subgoals.
- Goal perm nat (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
- 1 subgoal ============================ perm nat (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil)
- solve_perm.
- No more subgoals.
Deciding intuitionistic propositional logic¶
Pattern matching on goals allows powerful backtracking when returning tactic values. An interesting application is the problem of deciding intuitionistic propositional logic. Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92], it is quite natural to code such a tactic using the tactic language as shown below.
- Ltac basic := match goal with | |- True => trivial | _ : False |- _ => contradiction | _ : ?A |- ?A => assumption end.
- basic is defined
- Ltac simplify := repeat (intros; match goal with | H : ~ _ |- _ => red in H | H : _ /\ _ |- _ => elim H; do 2 intro; clear H | H : _ \/ _ |- _ => elim H; intro; clear H | H : ?A /\ ?B -> ?C |- _ => cut (A -> B -> C); [ intro | intros; apply H; split; assumption ] | H: ?A \/ ?B -> ?C |- _ => cut (B -> C); [ cut (A -> C); [ intros; clear H | intro; apply H; left; assumption ] | intro; apply H; right; assumption ] | H0 : ?A -> ?B, H1 : ?A |- _ => cut B; [ intro; clear H0 | apply H0; assumption ] | |- _ /\ _ => split | |- ~ _ => red end).
- simplify is defined
- Ltac my_tauto := simplify; basic || match goal with | H : (?A -> ?B) -> ?C |- _ => cut (B -> C); [ intro; cut (A -> B); [ intro; cut C; [ intro; clear H | apply H; assumption ] | clear H ] | intro; apply H; intro; assumption ]; my_tauto | H : ~ ?A -> ?B |- _ => cut (False -> B); [ intro; cut (A -> False); [ intro; cut B; [ intro; clear H | apply H; assumption ] | clear H ] | intro; apply H; red; intro; assumption ]; my_tauto | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) end.
- my_tauto is defined
The tactic basic
tries to reason using simple rules involving truth, falsity
and available assumptions. The tactic simplify
applies all the reversible
rules of Dyckhoff’s system. Finally, the tactic my_tauto
(the main
tactic to be called) simplifies with simplify
, tries to conclude with
basic
and tries several paths using the backtracking rules (one of the
four Dyckhoff’s rules for the left implication to get rid of the contraction
and the right or
).
Having defined my_tauto
, we can prove tautologies like these:
- Lemma my_tauto_ex1 : forall A B : Prop, A /\ B -> A \/ B.
- 1 subgoal ============================ forall A B : Prop, A /\ B -> A \/ B
- Proof. my_tauto. Qed.
- No more subgoals.
- Lemma my_tauto_ex2 : forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
- 1 subgoal ============================ forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B
- Proof. my_tauto. Qed.
- No more subgoals.
Deciding type isomorphisms¶
A trickier problem is to decide equalities between types modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for example, [dC95]). The axioms of this λ-calculus are given below.
- Open Scope type_scope.
- Section Iso_axioms.
- Variables A B C : Set.
- A is declared B is declared C is declared
- Axiom Com : A * B = B * A.
- Com is declared
- Axiom Ass : A * (B * C) = A * B * C.
- Ass is declared
- Axiom Cur : (A * B -> C) = (A -> B -> C).
- Cur is declared
- Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
- Dis is declared
- Axiom P_unit : A * unit = A.
- P_unit is declared
- Axiom AR_unit : (A -> unit) = unit.
- AR_unit is declared
- Axiom AL_unit : (unit -> A) = A.
- AL_unit is declared
- Lemma Cons : B = C -> A * B = A * C.
- 1 subgoal A, B, C : Set ============================ B = C -> A * B = A * C
- Proof.
- intro Heq; rewrite Heq; reflexivity.
- No more subgoals.
- Qed.
- End Iso_axioms.
- Ltac simplify_type ty := match ty with | ?A * ?B * ?C => rewrite <- (Ass A B C); try simplify_type_eq | ?A * ?B -> ?C => rewrite (Cur A B C); try simplify_type_eq | ?A -> ?B * ?C => rewrite (Dis A B C); try simplify_type_eq | ?A * unit => rewrite (P_unit A); try simplify_type_eq | unit * ?B => rewrite (Com unit B); try simplify_type_eq | ?A -> unit => rewrite (AR_unit A); try simplify_type_eq | unit -> ?B => rewrite (AL_unit B); try simplify_type_eq | ?A * ?B => (simplify_type A; try simplify_type_eq) || (simplify_type B; try simplify_type_eq) | ?A -> ?B => (simplify_type A; try simplify_type_eq) || (simplify_type B; try simplify_type_eq) end with simplify_type_eq := match goal with | |- ?A = ?B => try simplify_type A; try simplify_type B end.
- simplify_type is defined simplify_type_eq is defined
- Ltac len trm := match trm with | _ * ?B => let succ := len B in constr:(S succ) | _ => constr:(1) end.
- len is defined
- Ltac assoc := repeat rewrite <- Ass.
- assoc is defined
- Ltac solve_type_eq n := match goal with | |- ?A = ?A => reflexivity | |- ?A * ?B = ?A * ?C => apply Cons; let newn := len B in solve_type_eq newn | |- ?A * ?B = ?C => match eval compute in n with | 1 => fail | _ => pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) end end.
- solve_type_eq is defined
- Ltac compare_structure := match goal with | |- ?A = ?B => let l1 := len A with l2 := len B in match eval compute in (l1 = l2) with | ?n = ?n => solve_type_eq n end end.
- compare_structure is defined
- Ltac solve_iso := simplify_type_eq; compare_structure.
- solve_iso is defined
The tactic to judge equalities modulo this axiomatization is shown above.
The algorithm is quite simple. First types are simplified using axioms that
can be oriented (this is done by simplify_type
and simplify_type_eq
).
The normal forms are sequences of Cartesian products without a Cartesian product
in the left component. These normal forms are then compared modulo permutation
of the components by the tactic compare_structure
. If they have the same
length, the tactic solve_type_eq
attempts to prove that the types are equal.
The main tactic that puts all these components together is solve_iso
.
Here are examples of what can be solved by solve_iso
.
- Lemma solve_iso_ex1 : forall A B : Set, A * unit * B = B * (unit * A).
- 1 subgoal ============================ forall A B : Set, A * unit * B = B * (unit * A)
- Proof.
- intros; solve_iso.
- No more subgoals.
- Qed.
- Lemma solve_iso_ex2 : forall A B C : Set, (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B).
- 1 subgoal ============================ forall A B C : Set, (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B)
- Proof.
- intros; solve_iso.
- No more subgoals.
- Qed.
Debugging L
tac tactics¶
Backtraces¶
-
Flag
Ltac Backtrace
¶ Setting this flag displays a backtrace on Ltac failures that can be useful to find out what went wrong. It is disabled by default for performance reasons.
Tracing execution¶
-
Command
Info natural ltac_expr
¶ Applies
ltac_expr
and prints a trace of the tactics that were successfully applied, discarding branches that failed.idtac
tactics appear in the trace as comments containing the output.This command is valid only in proof mode. It accepts Goal selectors.
The number
natural
is the unfolding level of tactics in the trace. At level 0, the trace contains a sequence of tactics in the actual script, at level 1, the trace will be the concatenation of the traces of these tactics, etc…Example
- Ltac t x := exists x; reflexivity.
- t is defined
- Goal exists n, n=0.
- 1 subgoal ============================ exists n : nat, n = 0
- Info 0 t 1||t 0.
- exists with 0;<ltac_plugin::reflexivity@0> No more subgoals.
- Undo.
- 1 subgoal ============================ exists n : nat, n = 0
- Info 1 t 1||t 0.
- <ltac_plugin::exists@1> with 0;simple refine ?X11 No more subgoals.
The trace produced by
Info
tries its best to be a reparsableL
tac script, but this goal is not achievable in all generality. So some of the output traces will contain oddities.As an additional help for debugging, the trace produced by
Info
contains (in comments) the messages produced by theidtac
tactical at the right position in the script. In particular, the calls to idtac in branches which failed are not printed.
Interactive debugger¶
-
Flag
Ltac Debug
¶ This flag governs the step-by-step debugger that comes with the
L
tac interpreter.
When the debugger is activated, it stops at every step of the evaluation of
the current L
tac expression and prints information on what it is doing.
The debugger stops, prompting for a command which can be one of the
following:
newline |
go to the next step |
h |
get help |
r n |
advance n steps further |
r string |
advance up to the next call to “idtac string” |
s |
continue current evaluation without stopping |
x |
exit current evaluation |
-
Error
Debug mode not available in the IDE
¶
A non-interactive mode for the debugger is available via the flag:
-
Flag
Ltac Batch Debug
¶ This flag has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require user input to generate when this flag is set, can then be run through external tools such as diff.
Profiling L
tac tactics¶
It is possible to measure the time spent in invocations of primitive
tactics as well as tactics defined in L
tac and their inner
invocations. The primary use is the development of complex tactics,
which can sometimes be so slow as to impede interactive usage. The
reasons for the performance degradation can be intricate, like a slowly
performing L
tac match or a sub-tactic whose performance only
degrades in certain situations. The profiler generates a call tree and
indicates the time spent in a tactic depending on its calling context. Thus
it allows to locate the part of a tactic definition that contains the
performance issue.
-
Flag
Ltac Profiling
¶ This flag enables and disables the profiler.
-
Command
Show Ltac Profile CutOff integerstring?
¶ Prints the profile.
CutOff integer
By default, tactics that account for less than 2% of the total time are not displayed.
CutOff
lets you specify a different percentage.
Limits the profile to all tactics that start with
string
. Append a period (.) to the string if you only want exactly that name.
-
Command
Reset Ltac Profile
¶ Resets the profile, that is, deletes all accumulated information.
Warning
Backtracking across a
Reset Ltac Profile
will not restore the information.
- Set Warnings "-omega-is-deprecated".
- Require Import Coq.omega.Omega.
- [Loading ML file ring_plugin.cmxs ... done] [Loading ML file zify_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done]
- Ltac mytauto := tauto.
- mytauto is defined
- Ltac tac := intros; repeat split; omega || mytauto.
- tac is defined
- Notation max x y := (x + (y - x)) (only parsing).
- Goal forall x y z A B C D E F G H I J K L M N O P Q R S T U V W X Y Z, max x (max y z) = max (max x y) z /\ max x (max y z) = max (max x y) z /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A).
- 1 subgoal ============================ forall (x y z : nat) (A B C D E F G H I J K L M N O P Q R S T U V W X Y Z : Prop), x + (y + (z - y) - x) = x + (y - x) + (z - (x + (y - x))) /\ x + (y + (z - y) - x) = x + (y - x) + (z - (x + (y - x))) /\ (A /\ B /\ C /\ D /\ E /\ F /\ G /\ H /\ I /\ J /\ K /\ L /\ M /\ N /\ O /\ P /\ Q /\ R /\ S /\ T /\ U /\ V /\ W /\ X /\ Y /\ Z -> Z /\ Y /\ X /\ W /\ V /\ U /\ T /\ S /\ R /\ Q /\ P /\ O /\ N /\ M /\ L /\ K /\ J /\ I /\ H /\ G /\ F /\ E /\ D /\ C /\ B /\ A)
- Proof.
- Set Ltac Profiling.
- tac.
- No more subgoals.
- Show Ltac Profile.
- total time: 5.023s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─tac ----------------------------------- 0.1% 100.0% 1 5.023s ─<Coq.Init.Tauto.with_uniform_flags> --- 0.0% 79.5% 26 0.284s ─<Coq.Init.Tauto.tauto_gen> ------------ 0.0% 79.4% 26 0.284s ─<Coq.Init.Tauto.tauto_intuitionistic> - 0.0% 79.4% 26 0.284s ─t_tauto_intuit ------------------------ 0.0% 79.3% 26 0.284s ─<Coq.Init.Tauto.simplif> -------------- 55.9% 76.1% 26 0.273s ─omega --------------------------------- 20.2% 20.2% 28 0.362s ─<Coq.Init.Tauto.is_conj> -------------- 11.0% 11.0% 28756 0.015s ─elim id ------------------------------- 6.7% 6.7% 650 0.048s ─<Coq.Init.Tauto.axioms> --------------- 2.7% 3.2% 0 0.020s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─tac ----------------------------------- 0.1% 100.0% 1 5.023s ├─<Coq.Init.Tauto.with_uniform_flags> - 0.0% 79.5% 26 0.284s │└<Coq.Init.Tauto.tauto_gen> ---------- 0.0% 79.4% 26 0.284s │└<Coq.Init.Tauto.tauto_intuitionistic> 0.0% 79.4% 26 0.284s │└t_tauto_intuit ---------------------- 0.0% 79.3% 26 0.284s │ ├─<Coq.Init.Tauto.simplif> ---------- 55.9% 76.1% 26 0.273s │ │ ├─<Coq.Init.Tauto.is_conj> -------- 11.0% 11.0% 28756 0.015s │ │ └─elim id ------------------------- 6.7% 6.7% 650 0.048s │ └─<Coq.Init.Tauto.axioms> ----------- 2.7% 3.2% 0 0.020s └─omega ------------------------------- 20.2% 20.2% 28 0.362s
- Show Ltac Profile "omega".
- total time: 5.023s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─omega --------------------------------- 20.2% 20.2% 28 0.362s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
- Abort.
- Unset Ltac Profiling.
-
Tactic
stop ltac profiling
¶ Similarly to
start ltac profiling
, this tactic behaves likeidtac
. Together, they allow you to exclude parts of a proof script from profiling.
-
Tactic
reset ltac profile
¶ Equivalent to the
Reset Ltac Profile
command, which allows resetting the profile from tactic scripts for benchmarking purposes.
-
Tactic
show ltac profile cutoff integerstring?
¶ Equivalent to the
Show Ltac Profile
command, which allows displaying the profile from tactic scripts for benchmarking purposes.
-
Warning
Ltac Profiler encountered an invalid stack (no self node). This can happen if you reset the profile during tactic execution
¶ Currently,
reset ltac profile
is not very well-supported, as it clears all profiling information about all tactics, including ones above the current tactic. As a result, the profiler has trouble understanding where it is in tactic execution. This mixes especially poorly with backtracking into multi-success tactics. In general, non-top-level calls toreset ltac profile
should be avoided.
You can also pass the -profile-ltac
command line option to coqc
, which
turns the Ltac Profiling
flag on at the beginning of each document,
and performs a Show Ltac Profile
at the end.
Run-time optimization tactic¶
-
Tactic
optimize_heap
¶ This tactic behaves like
idtac
, except that running it compacts the heap in the OCaml run-time system. It is analogous to theOptimize Heap
command.
-
Tactic
infoH ltac_expr3
¶ Used internally by Proof General. See #12423 for some background.