7.3. The Tactic Language🔗

A tactic script consists of a sequence of tactics, separated either by semicolons or newlines. When separated by newlines, tactics must be indented to the same level. Explicit curly braces and semicolons may be used instead of indentation. Tactic sequences may be grouped by parentheses. This allows a sequence of tactics to be used in a position where a single tactic would otherwise be grammatically expected.

Generally, execution proceeds from top to bottom, with each tactic running in the proof state left behind by the prior tactic. The tactic language contains a number of control structures that can modify this flow.

Each tactic is a syntax extension in the tactic category. This means that tactics are free to define their own concrete syntax and parsing rules. However, with a few exceptions, the majority of tactics can be identified by a leading keyword; the exceptions are typically frequently-used built-in control structures such as <;>.

7.3.1. Control Structures🔗

Strictly speaking, there is no fundamental distinction between control structures and other tactics. Any tactic is free to take others as arguments and arrange for their execution in any context that it sees fit. Even if a distinction is arbitrary, however, it can still be useful. The tactics in this section are those that resemble traditional control structures from programming, or those that only recombine other tactics rather than making progress themselves.

7.3.1.1. Success and Failure🔗

When run in a proof state, every tactic either succeeds or fails. Tactic failure is akin to exceptions: failures typically "bubble up" until handled. Unlike exceptions, there is no operator to distinguish between reasons for failure; first simply takes the first branch that succeeds.

tactic

fail

fail msg is a tactic that always fails, and produces an error using the given message.

tactic

fail_if_success

fail_if_success t fails if the tactic t succeeds.

tactic

try

try tac runs tac and succeeds even if tac failed.

tactic

first

first | tac | ... runs each tac until one succeeds, or else fails.

7.3.1.2. Branching🔗

Tactic proofs may use pattern matching and conditionals. However, their meaning is not quite the same as it is in terms. While terms are expected to be executed once the values of their variables are known, proofs are executed with their variables left abstract and should consider all cases simultaneously. Thus, when if and match are used in tactics, their meaning is reasoning by cases rather than selection of a concrete branch. All of their branches are executed, and the condition or pattern match is used to refine the main goal with more information in each branch, rather than to select a single branch.

tactic

if ... then ... else ...

In tactic mode, if t then tac1 else tac2 is alternative syntax for:

by_cases t
· tac1
· tac2

It performs case distinction on h† : t or h† : ¬t, where h† is an anonymous hypothesis, and tac1 and tac2 are the subproofs. (It doesn't actually use nondependent if, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an ite application use refine if t then ?_ else ?_.)

tactic

if h : ... then ... else ...

In tactic mode, if h : t then tac1 else tac2 can be used as alternative syntax for:

by_cases h : t
· tac1
· tac2

It performs case distinction on h : t or h : ¬t and tac1 and tac2 are the subproofs.

You can use ?_ or _ for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for tac1 or tac2 then it will require the goal to be closed by the end of the block.

Reasoning by cases with if

In each branch of the Lean.Parser.Tactic.tacIfThenElse : tacticIn tactic mode, `if t then tac1 else tac2` is alternative syntax for: ``` by_cases t · tac1 · tac2 ``` It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an `ite` application use `refine if t then ?_ else ?_`.)if, an assumption is added that reflects whether n = 0.

example (n : Nat) : if n = 0 then n < 1 else n > 0 := byn:Nat⊢ if n = 0 then n < 1 else n > 0
  if n = 0 thenn:Nath✝:n = 0⊢ if n = 0 then n < 1 else n > 0
    simp [*]All goals completed! 🐙
  elsen:Nath✝:¬n = 0⊢ if n = 0 then n < 1 else n > 0
    simp only [↓reduceIte, gt_iff_lt, *]n:Nath✝:¬n = 0⊢ 0 < n
    omegaAll goals completed! 🐙

tactic

match

match performs case analysis on one or more expressions. See Induction and Recursion. The syntax for the match tactic is the same as term-mode match, except that the match arms are tactics instead of expressions.

example (n : Nat) : n = n := by
  match n with
  | 0 => rfl
  | i+1 => simp

When pattern matching, instances of the scrutinee in the goal are replaced with the patterns that match them in each branch. Each branch must then prove the refined goal. Compared to the cases tactic, using match can allow a greater degree of flexibility in the cases analysis being performed, but the requirement that each branch solve its goal completely makes it more difficult to incorporate into larger automation scripts.

Reasoning by cases with match

In each branch of the Lean.Parser.Tactic.match : tactic`match` performs case analysis on one or more expressions. See [Induction and Recursion][tpil4]. The syntax for the `match` tactic is the same as term-mode `match`, except that the match arms are tactics instead of expressions. ``` example (n : Nat) : n = n := by match n with | 0 => rfl | i+1 => simp ``` [tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.htmlmatch, the scrutinee n has been replaced by either 0 or k + 1.

example (n : Nat) : if n = 0 then n < 1 else n > 0 := byn:Nat⊢ if n = 0 then n < 1 else n > 0
  match n with
  | 0 =>
    simpAll goals completed! 🐙
  | k + 1 =>
    simpAll goals completed! 🐙

7.3.1.3. Goal Selection🔗

Most tactics affect the main goal. Goal selection tactics provide a way to treat a different goal as the main one, rearranging the sequence of goals in the proof state.

tactic

case

case tag => tac focuses on the goal with case name tag and solves it using tac, or else fails.
case tag x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.
case tag₁ | tag₂ => tac is equivalent to (case tag₁ => tac); (case tag₂ => tac).

tactic

case'

case' is similar to the case tag => tac tactic, but does not ensure the goal has been solved after applying tac, nor admits the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

tactic

rotate_left

rotate_left n rotates goals to the left by n. That is, rotate_left 1 takes the main goal and puts it to the back of the subgoal list. If n is omitted, it defaults to 1.

tactic

rotate_right

Rotate the goals to the right by n. That is, take the goal at the back and push it to the front n times. If n is omitted, it defaults to 1.

7.3.1.3.1. Sequencing🔗

In addition to running tactics one after the other, each being used to solve the main goal, the tactic language supports sequencing tactics according to the way in which goals are produced. The <;> tactic combinator allows a tactic to be applied to every subgoal produced by some other tactic. If no new goals are produced, then the second tactic is not run.

tactic

<;>

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

If the tactic fails on any of the subgoals, then the whole <;> tactic fails.

Subgoal Sequencing

In a this proof state:

x:Nath:x = 1 ∨ x = 2⊢ x < 3

the tactic cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 yields the following two goals:

inlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3

Running cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 ; simp [*]inrx:Nath✝:x = 2⊢ x < 3 causes simp to solve the first goal, leaving the second behind:

inrx:Nath✝:x = 2⊢ x < 3

Replacing the ; with <;> and running cases hinlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 <;>inlx:Nath✝:x = 1⊢ x < 3inrx:Nath✝:x = 2⊢ x < 3 simp [*]All goals completed! 🐙 solves both of the new goals with simp:

All goals completed! 🐙

7.3.1.3.2. Working on Multiple Goals🔗

The tactics all_goals and any_goals allow a tactic to be applied to every goal in the proof state. The difference between them is that if the tactic fails for in any of the goals, all_goals itself fails, while any_goals fails only if the tactic fails in all of the goals.

tactic

all_goals

all_goals tac runs tac on each goal, concatenating the resulting goals, if any.

tactic

any_goals

any_goals tac applies the tactic tac to every goal, and succeeds if at least one application succeeds.

7.3.1.4. Focusing🔗

Focusing tactics remove some subset of the proof goals (typically leaving only the main goal) from the consideration of some further tactics. In addition to the tactics described here, the case and case' tactics focus on the selected goal.

tactic

·

· tac focuses on the main goal and tries to solve it using tac, or else fails.

It is generally considered good Lean style to use bullets whenever a tactic line results in more than one new subgoal. This makes it easier to read and maintain proofs, because the connections between steps of reasoning are more clear and any change in the number of subgoals while editing the proof will have a localized effect.

tactic

next

next => tac focuses on the next goal and solves it using tac, or else fails. next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

tactic

focus

focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

7.3.1.5. Repetition and Iteration🔗

tactic

iterate

iterate n tac runs tac exactly n times. iterate tac runs tac repeatedly until failure.

iterate's argument is a tactic sequence, so multiple tactics can be run using iterate n (tac₁; tac₂; ⋯) or

iterate n
  tac₁
  tac₂
  ⋯

tactic

repeat

repeat tac repeatedly applies tac so long as it succeeds. The tactic tac may be a tactic sequence, and if tac fails at any point in its execution, repeat will revert any partial changes that tac made to the tactic state.

The tactic tac should eventually fail, otherwise repeat tac will run indefinitely.

7.3.2. Names and Hygiene🔗

Behind the scenes, tactics generate proof terms. These proof terms exist in a local context, because assumptions in proof states correspond to local binders in terms. Uses of assumptions correspond to variable references. It is very important that the naming of assumptions be predictable; otherwise, small changes to the internal implementation of a tactic could either lead to variable capture or to a broken reference if they cause different names to be selected.

Lean's tactic language is hygienic. This means that the tactic language respects lexical scope: names that occur in a tactic refer to the enclosing binding in the source code, rather than being determined by the generated code, and the tactic framework is responsible for maintaining this property. Variable references in tactic scripts refer either to names that were in scope at the beginning of the script or to bindings that were explicitly introduced as part of the tactics, rather than to the names chosen for use in the proof term behind the scenes.

A consequence of hygienic tactics is that the only way to refer to an assumption is to explicitly name it. Tactics cannot assign assumption names themselves, but must rather accept names from users; users are correspondingly obligated to provide names for assumptions that they wish to refer to. When an assumption does not have a user-provided name, it is shown in the proof state with a dagger ('†', DAGGER 0x2020). The dagger indicates that the name is inaccessible and cannot be explicitly referred to.

Hygiene can be disabled by setting the option tactic.hygienic to false. This is not recommended, as many tactics rely on the hygiene system to prevent capture and thus do not incur the overhead of careful manual name selection.

option

tactic.hygienic

Default value: true

make sure tactics are hygienic

Tactic hygiene: inaccessible assumptions

When proving that ∀ (n : Nat), 0 + n = n, the initial proof state is:

⊢ ∀ (n : Nat), 0 + n = n

The tactic intron✝:Nat⊢ 0 + n✝ = n✝ results in a proof state with an inaccessible assumption:

n✝:Nat⊢ 0 + n✝ = n✝

Tactic hygiene: accessible assumptions

When proving that ∀ (n : Nat), 0 + n = n, the initial proof state is:

⊢ ∀ (n : Nat), 0 + n = n

The tactic intro nn:Nat⊢ 0 + n = n, with the explicit name n, results in a proof state with an accessibly-named assumption:

n:Nat⊢ 0 + n = n

7.3.2.1. Accessing Assumptions🔗

Many tactics provide a means of specifying names for the assumptions that they introduce. For example, intro and intros take assumption names as arguments, and induction's Lean.Parser.Tactic.induction : tacticAssuming `x` is a variable in the local context with an inductive type, `induction x` applies induction on `x` to the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor and an inductive hypothesis is added for each recursive argument to the constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the inductive hypothesis incorporates that hypothesis as well. For example, given `n : Nat` and a goal with a hypothesis `h : P n` and target `Q n`, `induction n` produces one goal with hypothesis `h : P 0` and target `Q 0`, and one goal with hypotheses `h : P (Nat.succ a)` and `ih₁ : P a → Q a` and target `Q (Nat.succ a)`. Here the names `a` and `ih₁` are chosen automatically and are not accessible. You can use `with` to provide the variables names for each constructor. - `induction e`, where `e` is an expression instead of a variable, generalizes `e` in the goal, and then performs induction on the resulting variable. - `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a term whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables - `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized. - Given `x : Nat`, `induction x with | zero => tac₁ | succ x' ih => tac₂` uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.with-form allows simultaneous case selection, assumption naming, and focusing. When an assumption does not have a name, one can be assigned using next, case, or rename_i.

tactic

rename_i

rename_i x_1 ... x_n renames the last n inaccessible names using the given names.

7.3.3. Assumption Management🔗

Larger proofs can benefit from management of proof states, removing irrelevant assumptions and making their names easier to understand. Along with these operators, rename_i allows inaccessible assumptions to be renamed, and intro, intros and rintro convert goals that are implications or universal quantification into goals with additional assumptions.

tactic

rename

rename t => x renames the most recent hypothesis whose type matches t (which may contain placeholders) to x, or fails if no such hypothesis could be found.

tactic

revert

revert x... is the inverse of intro x...: it moves the given hypotheses into the main goal's target type.

tactic

clear

clear x... removes the given hypotheses, or fails if there are remaining references to a hypothesis.

7.3.4. Local Definitions and Proofs🔗

have and let both create local assumptions. Generally speaking, have should be used when proving an intermediate lemma; let should be reserved for local definitions.

tactic

have

The have tactic is for adding hypotheses to the local context of the main goal.

have h : t := e adds the hypothesis h : t if e is a term of type t.
have h := e uses the type of e for t.
have : t := e and have := e use this for the name of the hypothesis.
have pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that have only one applicable constructor. For example, given h : p ∧ q ∧ r, have ⟨h₁, h₂, h₃⟩ := h produces the hypotheses h₁ : p, h₂ : q, and h₃ : r.

tactic

haveI

haveI behaves like have, but inlines the value instead of producing a let_fun term.

tactic

have'

Similar to have, but using refine'

tactic

let

The let tactic is for adding definitions to the local context of the main goal.

let x : t := e adds the definition x : t := e if e is a term of type t.
let x := e uses the type of e for t.
let : t := e and let := e use this for the name of the hypothesis.
let pat := e for a pattern pat is equivalent to match e with | pat => _, where _ stands for the tactics that follow this one. It is convenient for types that let only one applicable constructor. For example, given p : α × β × γ, let ⟨x, y, z⟩ := p produces the local variables x : α, y : β, and z : γ.

tactic

let rec

let rec f : t := e adds a recursive definition f to the current goal. The syntax is the same as term-mode let rec.

tactic

letI

letI behaves like let, but inlines the value instead of producing a let_fun term.

tactic

let'

Similar to let, but using refine'

7.3.5. Namespace and Option Management🔗

Namespaces and options can be adjusted in tactic scripts using the same syntax as in terms.

tactic

set_option

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

tactic

open

open Foo in tacs (the tactic) acts like open Foo at command level, but it opens a namespace only within the tactics tacs.

7.3.5.1. Controlling Unfolding🔗

By default, only definitions marked reducible are unfolded, except when checking definitional equality. These operators allow this default to be adjusted for some part of a tactic script.

tactic

with_reducible_and_instances

with_reducible_and_instances tacs executes tacs using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

tactic

with_reducible

with_reducible tacs executes tacs using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

tactic

with_unfolding_all

with_unfolding_all tacs executes tacs using the .all transparency setting. In this setting all definitions that are not opaque are unfolded.