\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Ltac

This chapter documents the tactic language Ltac.

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 Ltac:

Ltac reduce_and_try_to_solve := simpl; intros; auto. Ltac destruct_bool_and_rewrite b H1 H2 :=   destruct b; [ rewrite H1; eauto | rewrite H2; eauto ].

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.

ltac_expr::=ltac_expr4​binder_tacticltac_expr4::=ltac_expr3 ; ltac_expr3​binder_tactic|ltac_expr3 ; [ for_each_goal ]|ltac_expr3ltac_expr3::=l3_tactic|ltac_expr2ltac_expr2::=ltac_expr1 + ltac_expr2​binder_tactic|ltac_expr1 || ltac_expr2​binder_tactic|l2_tactic|ltac_expr1ltac_expr1::=tactic_value|qualid tactic_arg+|l1_tactic|ltac_expr0tactic_value::=value_tactic​syn_valuetactic_arg::=tactic_value|term|()ltac_expr0::=( ltac_expr )|[> for_each_goal ]|tactic_atomtactic_atom::=integer|qualid|()

Note

Tactics described in other chapters of the documentation are simple_tactics, which only modify the proof state. Ltac 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 Ltac constructs are documented as tactics. Tactics are grouped as follows:

The documentation for these Ltac constructs mentions which group they belong to.

The difference is only relevant in some compound tactics where extra parentheses may be needed. For example, parentheses are required in idtac + (once idtac) because once is an l3_tactic, which the production ltac_expr2 ::= ltac_expr1 + ltac_expr2​binder_tactic doesn't accept after the +.

Note

  • The grammar reserves the token ||.

Values

An Ltac value can be an integer, string, unit (written as "()" ), syntactic value or tactic. 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 Ltac 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. Ltac functions can return values of any type.

Syntactic values

syn_value::=ident : ( nonterminal )

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

ident

a user-specified name

intro

string

string

a string

integer

integer

an integer

reference

qualid

a qualified identifier

uconstr

term

an untyped term

refine

constr

term

a term

exact

ltac

ltac_expr

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_values 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 Ltac are well-typed by default. Building large terms in recursive Ltac 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.

Substitution

names within Ltac expressions are used to represent both terms and Ltac variables. If the name corresponds to an Ltac variable or tactic name, Ltac substitutes the value before applying the expression. Generally it's best to choose distinctive names for Ltac 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 Ltac 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 goal ============================ 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.

Local definitions: let

Tactic let rec? let_clause with let_clause* in ltac_expr
let_clause::=name := ltac_expr|ident name+ := ltac_expr

Binds symbols within ltac_expr. let evaluates each let_clause, substitutes the bound variables into ltac_expr and then evaluates ltac_expr. There are no dependencies between the let_clauses.

Use let rec to create recursive or mutually recursive bindings, which causes the definitions to be evaluated lazily.

let is a binder_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 a binder_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 a Ltac function with at least as many arguments as the provided tactic_args. The tactic_args are evaluated before the function is applied or partially applied.

Functions may be defined with the fun and let tactics and with the Ltac command.

Tactics in terms

term_ltac::=ltac : ( ltac_expr )

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.

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
toplevel_selector::=selector|all|!|par

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 the selector 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
selector::=range_selector+,|[ ident ]range_selector::=natural|natural - natural

Applies ltac_expr3 to the selected goals. (At the beginning of a sentence, use the form selector: tactic rather than only selector: tactic. In the latter, the Default Goal Selector (by default set to 1:) is applied before only is interpreted. This is probably not what you want.)

only is an l3_tactic.

range_selector+,

The selected goals are the union of the specified range_selectors.

[ ident ]

Limits the application of ltac_expr3 to the goal previously named ident by the user (see Existential variables).

natural

Selects a single goal.

natural1 - natural2

Selects the goals natural1 through natural2, inclusive.

Error No such goal.

Example: Selector reordering goals

Goal 1=0 /\ 2=0 /\ 3=0.
1 goal ============================ 1 = 0 /\ 2 = 0 /\ 3 = 0
repeat split.
3 goals ============================ 1 = 0 goal 2 is: 2 = 0 goal 3 is: 3 = 0
1,3: idtac.
3 goals ============================ 1 = 0 goal 2 is: 3 = 0 goal 3 is: 2 = 0

Processing multiple goals

When presented with multiple focused goals, most Ltac 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 goal ============================ True /\ False
split.
2 goals ============================ True goal 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.

Branching and backtracking

Ltac 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.

Control flow

Sequence: ;

A sequence is an expression of the following form:

Tactic ltac_expr31 ; ltac_expr32​binder_tactic

The expression ltac_expr31 is evaluated to v1, which must be a tactic value. The tactic v1 is applied to the current goals, possibly producing more goals. Then the right-hand side is evaluated to produce v2, which must be a tactic value. The tactic v2 is applied to all the goals produced by the prior application. Sequence is associative.

This construct uses backtracking: if ltac_expr32 fails, Coq will try each alternative success (if any) for ltac_expr31, retrying ltac_expr32 for each until both tactics succeed or all alternatives have failed. See Branching and backtracking.

Note

Do loop

Tactic do nat_or_var ltac_expr3

The do loop repeats a tactic nat_or_var times:

ltac_expr is evaluated to v, which must be a tactic value. This tactic value v is applied nat_or_var times. If nat_or_var > 1, after the first application of v, v is applied, at least once, to the generated subgoals and so on. It fails if the application of v fails before nat_or_var applications have been completed.

do is an l3_tactic.

Repeat loop

Tactic repeat ltac_expr3

The repeat loop repeats a tactic until it fails or doesn't change the proof context.

ltac_expr is evaluated to v. If v 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 tactic repeat ltac_expr itself never fails.

repeat is an l3_tactic.

Catching errors: try

We can catch the tactic errors with:

Tactic try ltac_expr3

ltac_expr is evaluated to v which must be a tactic value. The tactic value v is applied to each focused goal independently. If the application of v 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.

try is an l3_tactic.

Conditional branching: tryif

Tactic tryif ltac_exprtest then ltac_exprthen else ltac_expr2else

For each focused goal, independently: Evaluate and apply ltac_exprtest. If ltac_exprtest succeeds at least once, evaluate and apply ltac_exprthen to all the subgoals generated by ltac_exprtest. Otherwise, evaluate and apply ltac_expr2else to all the subgoals generated by ltac_exprtest.

tryif is an l2_tactic.

Alternatives

Branching with backtracking: +

We can branch with backtracking with the following structure:

Tactic ltac_expr1 + ltac_expr2​binder_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, Ltac backtracks and selects the next success for ltac_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, use first 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 to ltac_expr1 + (ltac_expr2 + ltac_expr3). Here's an example where the behavior differs slightly:

Goal True.
1 goal ============================ 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 subsequent fail causes backtracking and the execution of idtac "B".

Goal True.
1 goal ============================ True
idtac "1" + idtac "2".
1
assert_fails ((idtac "A" + idtac "B"); fail).
A B

Local application of tactics: [> ... ]

Tactic [> for_each_goal ]
for_each_goal::=goal_tactics|goal_tactics |? ltac_expr? .. | goal_tactics?goal_tactics::=ltac_expr?*|

Applies a different ltac_expr? to each of the focused goals. In the first form of for_each_goal (without ..), the construct fails if the number of specified ltac_expr? is not the same as the number of focused goals. Omitting an ltac_expr leaves the corresponding goal unchanged.

In the second form (with ltac_expr? ..), the left and right goal_tactics are applied respectively to a prefix or suffix of the list of focused goals. The ltac_expr? before the .. is applied to any focused goals in the middle (possibly none) that are not covered by the goal_tactics. The number of ltac_expr? in the goal_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 as swap, 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 applying ltac_expr3.

Tactic ltac_expr3 ; [ for_each_goal ]

ltac_expr3 ; [ ... ] is equivalent to [> ltac_expr3 ; [> ... ] .. ].

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. The ltac_exprs must evaluate to tactic values. Failures in tactics after the first 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 goal ============================ True

The fail doesn't trigger the second idtac:

assert_fails (first [ idtac "1" | idtac "2" ]; fail).
1

This backtracks within (idtac "1A" + idtac "1B" + fail) but first won't consider the idtac "2" alternative:

assert_fails (first [ (idtac "1A" + idtac "1B" + fail) | idtac "2" ]; fail).
1A 1B

first is an l1_tactic.

Error No applicable tactic.
Variant first ltac_expr

This is an Ltac alias that gives a primitive access to the first tactical as an Ltac definition without going through a parsing rule. It expects to be given a list of tactics through a Tactic 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 and first, ltac_exprs that don't evaluate to tactic values are ignored. So solve [ () | 1 | constructor ] is equivalent to solve [ constructor ]. This may make it harder to debug scripts that inadvertently include non-tactic values.

solve is an l1_tactic.

Variant solve ltac_expr

This is an Ltac alias that gives a primitive access to the solve tactic. See the first tactic for more information.

First tactic to make progress: ||

Yet another way of branching without backtracking is the following structure:

Tactic ltac_expr1 || ltac_expr2​binder_tactic

ltac_expr1 || ltac_expr2 is equivalent to first [ progress ltac_expr1 | ltac_expr2 ], except that if it fails, it fails like ltac_expr2. `|| is left-associative.

ltac_exprs that don't evaluate to tactic values are ignored. See the note at solve.

Detecting progress

We can check if a tactic made progress with:

Tactic progress ltac_expr3

ltac_expr is evaluated to v which must be a tactic value. The tactic value v is applied to each focused subgoal independently. If the application of v 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.

progress is an l3_tactic.

Error Failed to progress.

Success and failure

Checking for success: assert_succeeds

Coq defines an Ltac 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. If ltac_expr3 fails, the tactic fails with the same error.

Checking for failure: assert_fails

Coq defines an Ltac 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. If ltac_expr3 unexpectedly has at least one success, the tactic performs a gfail 0, printing the following message:

Error Tactic failure: <tactic closure> succeeds.

Note

assert_fails and assert_succeeds work as described when ltac_expr3 is a simple_tactic. In some more complex expressions, they may report an error from within ltac_expr3 when they shouldn't. This is due to the order in which parts of the ltac_expr3 are evaluated and executed. For example:

Goal True.
1 goal ============================ 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 an Ltac-defined tactic. That makes it a function that's processed in the evaluation phase, causing the match to find its first success earlier. One workaround is to prefix ltac_expr3 with "idtac;".

assert_fails (idtac; match True with _ => fail end).

Alternatively, substituting the match into the definition of assert_fails works as expected:

tryif (once match True with _ => fail end) then gfail 0 (* tac *) "succeeds" else idtac.

Failing

Tactic fail​gfail nat_or_var? ident​string​natural*

fail is the always-failing tactic: it does not solve any goal. It is useful for defining other tactics since it can be caught by try, 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 after all: and there are no goals left.

fail and gfail are l1_tactics.

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.

nat_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 makes match goal consider the next clause (backtracking). If nonzero, the current match 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 to fail natural is not enclosed in a + construct, respecting the algebraic identity.

ident​string​natural*

The given tokens are used for printing the failure message. If ident is an Ltac variable, its contents are printed; if not, it is an error.

Error Tactic failure.
Error Tactic failure (level natural).
Error No such goal.

Example

Goal True.
1 goal ============================ True
Proof. fail. Abort.
Toplevel input, characters 7-12: > Proof. fail. > ^^^^^ Error: Tactic failure.
Goal True.
1 goal ============================ True
Proof. trivial; fail. Qed.
No more goals.
Goal True.
1 goal ============================ True
Proof. trivial. fail. Abort.
No more goals. Toplevel input, characters 16-21: > Proof. trivial. fail. > ^^^^^ Error: No such goal.
Goal True.
1 goal ============================ True
Proof. trivial. all: fail. Qed.
No more goals.
Goal True.
1 goal ============================ True
Proof. gfail. Abort.
Toplevel input, characters 7-13: > Proof. gfail. > ^^^^^^ Error: Tactic failure.
Goal True.
1 goal ============================ True
Proof. trivial; gfail. Abort.
Toplevel input, characters 7-22: > Proof. trivial; gfail. > ^^^^^^^^^^^^^^^ Error: Tactic failure.
Goal True.
1 goal ============================ True
Proof. trivial. gfail. Abort.
No more goals. Toplevel input, characters 16-22: > Proof. trivial. gfail. > ^^^^^^ Error: No such goal.
Goal True.
1 goal ============================ True
Proof. trivial. all: gfail. Abort.
No more goals. Toplevel input, characters 16-27: > Proof. trivial. all: gfail. > ^^^^^^^^^^^ Error: Tactic failure.

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 to v which must be a tactic value. The tactic value v is applied but only its first success is used. If v fails, once ltac_expr3 fails like v. If v has at least one success, once ltac_expr3 succeeds once, but cannot produce more successes.

once is an l3_tactic.

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 to v which must be a tactic value. The tactic value v is applied if it has at most one success. If v fails, exactly_once ltac_expr3 fails like v. If v has a exactly one success, exactly_once ltac_expr3 succeeds like v. If v has two or more successes, exactly_once ltac_expr3 fails.

exactly_once is an l3_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, normally v would only be executed up to the first success until backtracking is needed, however exactly_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.

Manipulating values

Pattern matching on terms: match

Tactic match_key ltac_exprterm with |? match_pattern => ltac_expr+| end
match_key::=lazymatch|match|multimatchmatch_pattern::=cpattern|context ident? [ cpattern ]cpattern::=term

lazymatch, match and multimatch are ltac_expr1s.

Evaluates ltac_exprterm, which must yield a term, and matches it sequentially with the match_patterns, which may have metavariables. When a match is found, metavariable values are substituted into ltac_expr, which is then applied.

Matching may continue depending on whether lazymatch, match or multimatch is specified.

In the match_patterns, metavariables have the form ?ident, whereas in the ltac_exprs, the question mark is omitted. Choose your metavariable names with care to avoid name conflicts. For example, if you use the metavariable S, then the ltac_expr can't use S to refer to the constructor of nat without qualifying the constructor as Datatypes.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 the match) will not cause selection of a new branch. Examples here and here.

multimatch

If ltac_expr fails, continue matching with the next branch. When an ltac_expr succeeds for a branch, subsequent failures (after the multimatch) causing consumption of all the successes of ltac_expr trigger selection of a new matching branch. Example.

match … is, in fact, shorthand for once multimatch ….

cpattern

The syntax of cpattern is the same as that of terms, 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, say x1, …, xn and the expression matches, the metavariable is instantiated by a term which can then be used in any context which also binds the variables x1, …, 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 variable ident matches any complex expression with (possible) dependencies in the variables identi and returns a functional term of the form fun ident1 … identn => term.

context ident? [ cpattern ]

Matches any term with a subterm matching cpattern. If there is a match and ident is present, it is assigned the "matched context", i.e. the initial term where the matched subterm is replaced by a hole. Note that context (with very similar syntax) appearing after the => is the context tactic.

For match and multimatch, if the evaluation of the ltac_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 the Printing 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 in cpattern.

If ltac_expr evaluates to a tactic, then it is applied. If the tactic succeeds, the result of the match expression is idtac. If ltac_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 a lazymatch or multimatch (but not match) can cause backtracking into ltac_expr to select its next success. (match … is equivalent to once multimatch …. The once prevents backtracking into the match after it has succeeded.)

Note

Each Ltac 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 as fresh, 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 in assert_fails. Please see the note in assert_fails.

Error Expression does not evaluate to a tactic.

ltac_expr must evaluate to a tactic.

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, if ltac_expr fails, the lazymatch fails; it doesn't look for further matches. In match, if ltac_expr fails in a matching branch, it will try to match on subsequent branches.

Goal True.
1 goal ============================ 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, whereas multimatch 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 the pose substitutes (x + 1).

Goal True.
1 goal ============================ 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 goal 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 goal ============================ 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
goal_pattern::=match_hyp*, |- match_pattern|[ match_hyp*, |- match_pattern ]|_match_hyp::=name : match_pattern|name := match_pattern|name := [ match_pattern ] : match_pattern

lazymatch goal, match goal and multimatch goal are l1_tactics.

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 (see match). 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

name : match_patterntype

n : ?t

name := match_patternbinder

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 after Import ListNotations) must be parenthesized or, for the fourth form, use double brackets: [ [ ?l ] ].

termbinders 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_hyps in a branch, there may be multiple ways to match them to hypotheses. For match goal and multimatch goal, if the evaluation of the ltac_expr fails, matching will continue with the next hypothesis combination. When those are exhausted, the next alternative from any context constructs in the match_patterns is tried and then, when the context alternatives are exhausted, the next branch is tried. Example.

reverse

Hypothesis matching for match_hyps normally begins by matching them from left to right, to hypotheses, last to first. Specifying reverse 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.

Error No matching clauses for match goal.

No clause succeeds, i.e. all matching patterns, if any, fail at the application of the ltac_expr.

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 goal ============================ forall A B : Prop, A -> B -> A -> B
intros.
1 goal 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 goals.

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 goal ============================ forall A B : Prop, A -> B -> A -> B
intros.
1 goal 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 goals.

Example: Multiple ways to match hypotheses

Every possible match for the hypotheses is evaluated until the right-hand side succeeds. Note that H1 and H2 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 goal ============================ forall A B : Prop, A -> B -> A -> B
intros A B H.
1 goal 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) substituting term for the hole created by the pattern.

context is a value_tactic.

Error Not a context variable.
Error Unbound context identifier ident.

Example: Substituting a matched context

Goal True /\ True.
1 goal ============================ True /\ True
match goal with | |- context G [True] => let x := context G [False] in idtac x end.
(False /\ True)

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 string​qualid*

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 current ltac_expr). The fresh identifier is formed by concatenating the final ident of each qualid (dropping any qualified components) and each specified string. 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 name H.

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 goal ============================ True -> True
intro x.
1 goal 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 a value_tactic.

Computing in a term: eval

Evaluation of a term can be performed with:

eval red_expr in term

See eval. eval is a value_tactic.

Getting the type of a term

Tactic type of term

This tactic returns the type of term.

type of is a value_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 Ltac, an untyped term can contain references to hypotheses or to Ltac variables containing typed or untyped terms. An untyped term can be type checked with type_term whose argument is parsed as an untyped term and returns a well-typed term which can be used in tactics.

type_term is a value_tactic.

Counting goals: numgoals

Tactic numgoals

The number of goals under focus can be recovered using the numgoals function. Combined with the guard tactic below, it can be used to branch over the number of goals produced by previous tactics.

numgoals is a value_tactic.

Example

Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals".
pr_numgoals is defined
Goal True /\ True /\ True.
1 goal ============================ True /\ True /\ True
split;[|split].
3 goals ============================ True goal 2 is: True goal 3 is: True
all:pr_numgoals.
There are 3 goals

Testing boolean expressions: guard

Tactic guard int_or_var comparison int_or_var
int_or_var::=integer​identcomparison::==|<|<=|>|>=

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: guard

Goal True /\ True /\ True.
1 goal ============================ True /\ True /\ True
split;[|split].
3 goals ============================ True goal 2 is: True goal 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.

Checking properties of terms

Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.

Tactic constr_eq_strict one_term one_term

Succeeds if the arguments are equal modulo alpha conversion and ignoring casts. Universes are considered equal when they are equal in the universe graph.

Error Not equal.
Error Not equal (due to universes).
Tactic constr_eq one_term one_term

Like constr_eq_strict, but may add constraints to make universes equal.

Error Not equal.
Error Not equal (due to universes).
Tactic constr_eq_nounivs one_term one_term

Like constr_eq_strict, but all universes are considered equal.

Tactic unify one_term one_term with ident?

Succeeds if the arguments are unifiable, potentially instantiating existential variables, and fails otherwise.

ident, if specified, is the name of the hint database that specifies which definitions are transparent. Otherwise, all definitions are considered transparent. Unification only expands transparent definitions while matching the two one_terms.

Tactic is_evar one_term

Succeeds if one_term is an existential variable and otherwise fails. Existential variables are uninstantiated variables generated by eapply and some other tactics.

Error Not an evar.
Tactic has_evar one_term

Succeeds if one_term has an existential variable as a subterm and fails otherwise. Unlike context patterns combined with is_evar, this tactic scans all subterms, including those under binders.

Error No evars.
Tactic is_ground one_term

The negation of has_evar one_term. Succeeds if one_term does not have an existential variable as a subterm and fails otherwise.

Error Not ground.
Tactic is_var one_term

Succeeds if one_term is a variable or hypothesis in the current local context and fails otherwise.

Error Not a variable or hypothesis.
Tactic is_const one_term

Succeeds if one_term is a global constant that is neither a (co)inductive type nor a constructor and fails otherwise.

Error not a constant.
Tactic is_fix one_term

Succeeds if one_term is a fix construct (see term_fix) and fails otherwise. Fails for let fix forms.

Error not a fix definition.

Example: is_fix

Goal True.
1 goal ============================ True
is_fix (fix f (n : nat) := match n with S n => f n | O => O end).
Tactic is_cofix one_term

Succeeds if one_term is a cofix construct (see term_cofix) and fails otherwise. Fails for let cofix forms.

Error not a cofix definition.

Example: is_cofix

Require Import Coq.Lists.Streams.
Goal True.
1 goal ============================ True
let c := constr:(cofix f : Stream unit := Cons tt f) in   is_cofix c.
Tactic is_constructor one_term

Succeeds if one_term is the constructor of a (co)inductive type and fails otherwise.

Error not a constructor.
Tactic is_ind one_term

Succeeds if one_term is a (co)inductive type (family) and fails otherwise. Note that is_ind (list nat) fails even though is_ind list succeeds, because list nat is an application.

Error not an (co)inductive datatype.
Tactic is_proj one_term

Succeeds if one_term is a primitive projection applied to a record argument and fails otherwise.

Error not a primitive projection.

Example: is_proj

Set Primitive Projections.
Record Box {T : Type} := box { unbox : T }.
Box is defined unbox is defined
Arguments box {_} _.
Goal True.
1 goal ============================ True
is_proj (unbox (box 0)).

Timing

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 to v which must be a tactic value. The tactic value v is applied normally, except that it is interrupted after nat_or_var seconds if it is still running. In this case the outcome is a failure.

timeout is an l3_tactic.

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. The string argument is optional. When provided, it is used to identify this particular occurrence of time.

time is an l3_tactic.

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 restart_timer string?

Reset a timer

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 goal ============================ 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.001u,0.s) 1 goal n := 100 : nat ============================ True

Tactic toplevel definitions

Defining Ltac symbols

Ltac toplevel definitions are made as follows:

Command Ltac tacdef_body with tacdef_body*
tacdef_body::=qualid name* :=​::= ltac_expr

Defines or redefines an Ltac 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. For definitions, qualid must be a simple ident.

name*

If specified, the symbol defines a function with the given parameter names. If no names are specified, qualid is assigned the value of ltac_expr.

:=

Defines a user-defined symbol, but gives an error if the symbol has already been defined.

Error There is already an Ltac named qualid
::=

Redefines an existing user-defined symbol, but gives an error if the symbol doesn't exist. Note that Tactic Notations do not count as user-defined tactics for ::=. If local is not specified, the redefinition applies across module boundaries.

Error There is no Ltac named qualid
with tacdef_body*

Permits definition of mutually recursive tactics.

Note

The following definitions are equivalent:

Printing Ltac tactics

Command Print Ltac qualid

Defined Ltac functions can be displayed using this command.

Command Print Ltac Signatures

This command displays a list of all user-defined tactics, with their arguments.

Examples of using Ltac

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 goal ============================ ~ (exists x y : nat, forall z : nat, x = z \/ y = z)
Proof.
intros (x & y & Hz).
1 goal x, y : nat Hz : forall z : nat, x = z \/ y = z ============================ False
destruct (Hz 0), (Hz 1), (Hz 2).
8 goals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 ============================ False goal 2 is: False goal 3 is: False goal 4 is: False goal 5 is: False goal 6 is: False goal 7 is: False goal 8 is: False

At this point, the congruence tactic would finish the job:

all: congruence.
No more goals.

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 goal ============================ ~ (exists x y : nat, forall z : nat, x = z \/ y = z)
Proof.
intros (x & y & Hz).
1 goal x, y : nat Hz : forall z : nat, x = z \/ y = z ============================ False
destruct (Hz 0), (Hz 1), (Hz 2).
8 goals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 ============================ False goal 2 is: False goal 3 is: False goal 4 is: False goal 5 is: False goal 6 is: False goal 7 is: False goal 8 is: False
all: match goal with      | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a      end.
8 goals x, y : nat Hz : forall z : nat, x = z \/ y = z H : x = 0 H0 : x = 1 H1 : x = 2 H2 : 1 = 2 ============================ False goal 2 is: False goal 3 is: False goal 4 is: False goal 5 is: False goal 6 is: False goal 7 is: False goal 8 is: False
all: discriminate.
No more goals.

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 goal ============================ perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil)
solve_perm.
No more goals.
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 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)
solve_perm.
No more goals.

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 goal ============================ forall A B : Prop, A /\ B -> A \/ B
Proof. my_tauto. Qed.
No more goals.
Lemma my_tauto_ex2 :   forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
1 goal ============================ forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B
Proof. my_tauto. Qed.
No more goals.

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 goal A, B, C : Set ============================ B = C -> A * B = A * C
Proof.
intro Heq; rewrite Heq; reflexivity.
No more goals.
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 goal ============================ forall A B : Set, A * unit * B = B * (unit * A)
Proof.
  intros; solve_iso.
No more goals.
Qed.
Lemma solve_iso_ex2 :   forall A B C : Set,     (A * unit -> B * (C * unit)) =     (A * unit -> (C -> unit) * C) * (unit -> A -> B).
1 goal ============================ forall A B C : Set, (A * unit -> B * (C * unit)) = (A * unit -> (C -> unit) * C) * (unit -> A -> B)
Proof.
  intros; solve_iso.
No more goals.
Qed.

Debugging Ltac 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 goal ============================ exists n : nat, n = 0
Info 0 t 1||t 0.
exists with 0;<coq-core.plugins.ltac::reflexivity@0> No more goals.
Undo.
1 goal ============================ exists n : nat, n = 0
Info 1 t 1||t 0.
<coq-core.plugins.ltac::exists@1> with 0;simple refine ?X11 No more goals.

The trace produced by Info tries its best to be a reparsable Ltac 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 the idtac tactical at the right position in the script. In particular, the calls to idtac in branches which failed are not printed.

Option Info Level natural

This option is an alternative to the Info command.

This will automatically print the same trace as Info natural at each tactic call. The unfolding level can be overridden by a call to the Info command.

Interactive debugger

Flag Ltac Debug

This flag, when set, enables the step-by-step debugger in the Ltac interpreter. The debugger is supported in coqtop and Proof General by printing information on the console and accepting typed commands. In addition, CoqIDE now supports a visual debugger with additional capabilities.

When the debugger is activated in coqtop, it stops at every step of the evaluation of the current Ltac 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 in coqtop. (It has no effect when running the CoqIDE debugger.) 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 Ltac tactics

It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in Ltac 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 Ltac 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 integer​string?

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.

string

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.

Require Import Lia.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file zify_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
Ltac mytauto := tauto.
mytauto is defined
Ltac tac := intros; repeat split; lia || 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 goal ============================ 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 goals.
Show Ltac Profile.
total time: 3.144s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─tac ----------------------------------- 0.1% 100.0% 1 3.143s ─<Coq.Init.Tauto.with_uniform_flags> --- 0.0% 96.1% 26 0.211s ─<Coq.Init.Tauto.tauto_gen> ------------ 0.0% 96.1% 26 0.211s ─<Coq.Init.Tauto.tauto_intuitionistic> - 0.0% 96.0% 26 0.211s ─t_tauto_intuit ------------------------ 0.1% 96.0% 26 0.210s ─<Coq.Init.Tauto.simplif> -------------- 65.0% 91.7% 26 0.206s ─<Coq.Init.Tauto.is_conj> -------------- 13.2% 13.2% 28756 0.027s ─elim id ------------------------------- 10.4% 10.4% 650 0.110s ─<Coq.Init.Tauto.axioms> --------------- 4.2% 4.2% 1430 0.026s ─lia ----------------------------------- 0.1% 3.5% 28 0.085s ─xlia (tactic) ------------------------- 2.6% 2.8% 28 0.081s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─tac ----------------------------------- 0.1% 100.0% 1 3.143s ├─<Coq.Init.Tauto.with_uniform_flags> - 0.0% 96.1% 26 0.211s │└<Coq.Init.Tauto.tauto_gen> ---------- 0.0% 96.1% 26 0.211s │└<Coq.Init.Tauto.tauto_intuitionistic> 0.0% 96.0% 26 0.211s │└t_tauto_intuit ---------------------- 0.1% 96.0% 26 0.210s │ ├─<Coq.Init.Tauto.simplif> ---------- 65.0% 91.7% 26 0.206s │ │ ├─<Coq.Init.Tauto.is_conj> -------- 13.2% 13.2% 28756 0.027s │ │ └─elim id ------------------------- 10.4% 10.4% 650 0.110s │ └─<Coq.Init.Tauto.axioms> ----------- 4.2% 4.2% 1430 0.026s └─lia --------------------------------- 0.1% 3.5% 28 0.085s └xlia (tactic) ----------------------- 2.6% 2.8% 28 0.081s
Show Ltac Profile "lia".
total time: 3.144s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ ─lia ----------------------------------- 0.1% 3.5% 28 0.085s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
Abort.
Unset Ltac Profiling.
Tactic start ltac profiling

This tactic behaves like idtac but enables the profiler.

Tactic stop ltac profiling

Similarly to start ltac profiling, this tactic behaves like idtac. 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 integer​string?

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 to reset 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 the Optimize Heap command.

Command infoH ltac_expr

Used internally by Proof General. See #12423 for some background.