Tactics

The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.

(

(tacs) executes a list of tactics in sequence, without requiring that the goal be closed at the end like · tacs. Like by itself, the tactics can be either separated by newlines or ;.

Tags:
Defined in module:: Init.Tactics

.

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

Tags:
Defined in module:: Init.NotationExtra

<;>

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

Tags:
Defined in module:: Init.Tactics

Lean.Parser.Tactic.nestedTactic

This tactic has no documentation.

Tags:
Defined in module:: Lean.Parser.Tactic

ac_nf

ac_nf normalizes equalities up to application of an associative and commutative operator.

ac_nf normalizes all hypotheses and the goal target of the goal.
ac_nf at l normalizes at location(s) l, where l is either * or a list of hypotheses in the local context. In the latter case, a turnstile ⊢ or |- can also be used, to signify the target of the goal.

instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
 ac_nf
 -- goal: a + (b + (c + d)) = a + (b + (c + d))

Tags:
Defined in module:: Init.Tactics

ac_nf0

Implementation of ac_nf (the full ac_nf calls trivial afterwards).

Tags:
Defined in module:: Init.Tactics

ac_rfl

ac_rfl proves equalities up to application of an associative and commutative operator.

instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl

Tags:
Defined in module:: Init.Tactics

admit

admit is a synonym for sorry.

Tags:
Defined in module:: Init.Tactics

all_goals

all_goals tac runs tac on each goal, concatenating the resulting goals. If the tactic fails on any goal, the entire all_goals tactic fails.

and_intros

and_intros applies And.intro until it does not make progress.

Tags:
Defined in module:: Init.Tactics

any_goals

any_goals tac applies the tactic tac to every goal, concatenating the resulting goals for successful tactic applications. If the tactic fails on all of the goals, the entire any_goals tactic fails.

This tactic is like all_goals try tac except that it fails if none of the applications of tac succeeds.

Tags:
Defined in module:: Init.Tactics

apply

apply e tries to match the current goal against the conclusion of e's type. If it succeeds, then the tactic returns as many subgoals as the number of premises that have not been fixed by type inference or type class resolution. Non-dependent premises are added before dependent ones.

The apply tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.

Tags:
Defined in module:: Init.Tactics

apply?

Searches environment for definitions or theorems that can refine the goal using apply with conditions resolved when possible with solve_by_elim.

The optional using clause provides identifiers in the local context that must be used when closing the goal.

Use +grind to enable grind as a fallback discharger for subgoals. Use +try? to enable try? as a fallback discharger for subgoals. Use -star to disable fallback to star-indexed lemmas. Use +all to collect all successful lemmas instead of stopping at the first.

Tags:
Defined in module:: Init.Tactics

apply_assumption

apply_assumption looks for an assumption of the form ... → ∀ _, ... → head where head matches the current goal.

You can specify additional rules to apply using apply_assumption [...]. By default apply_assumption will also try rfl, trivial, congrFun, and congrArg. If you don't want these, or don't want to use all hypotheses, use apply_assumption only [...]. You can use apply_assumption [-h] to omit a local hypothesis. You can use apply_assumption using [a₁, ...] to use all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

apply_assumption will use consequences of local hypotheses obtained via symm.

If apply_assumption fails, it will call exfalso and try again. Thus if there is an assumption of the form P → ¬ Q, the new tactic state will have two goals, P and Q.

You can pass a further configuration via the syntax apply_rules (config := {...}) lemmas. The options supported are the same as for solve_by_elim (and include all the options for apply).

Tags:
Defined in module:: Init.Tactics

apply_ext_theorem

Apply a single extensionality theorem to the current goal.

Tags:
Defined in module:: Init.Ext

apply_mod_cast

Normalize casts in the goal and the given expression, then apply the expression to the goal.

Tags:
Defined in module:: Init.TacticsExtra

apply_rfl

The same as rfl, but without trying eq_refl at the end.

Tags:
Defined in module:: Init.Tactics

apply_rules

apply_rules [l₁, l₂, ...] tries to solve the main goal by iteratively applying the list of lemmas [l₁, l₂, ...] or by applying a local hypothesis. If apply generates new goals, apply_rules iteratively tries to solve those goals. You can use apply_rules [-h] to omit a local hypothesis.

apply_rules will also use rfl, trivial, congrFun and congrArg. These can be disabled, as can local hypotheses, by using apply_rules only [...].

You can use apply_rules using [a₁, ...] to use all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

You can pass a further configuration via the syntax apply_rules (config := {...}). The options supported are the same as for solve_by_elim (and include all the options for apply).

apply_rules will try calling symm on hypotheses and exfalso on the goal as needed. This can be disabled with apply_rules (config := {symm := false, exfalso := false}).

You can bound the iteration depth using the syntax apply_rules (config := {maxDepth := n}).

Unlike solve_by_elim, apply_rules does not perform backtracking, and greedily applies a lemma from the list until it gets stuck.

Tags:
Defined in module:: Init.Tactics

array_get_dec

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf arr[i] < sizeOf arr, which is useful for well founded recursions over a nested inductive like inductive T | mk : Array T → T.

Tags:
Defined in module:: Init.Data.Array.Mem

array_mem_dec

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf arr provided that a ∈ arr which is useful for well founded recursions over a nested inductive like inductive T | mk : Array T → T.

Tags:
Defined in module:: Init.Data.Array.Mem

as_aux_lemma

as_aux_lemma => tac does the same as tac, except that it wraps the resulting expression into an auxiliary lemma. In some cases, this significantly reduces the size of expressions because the proof term is not duplicated.

Tags:
Defined in module:: Init.Tactics

assumption

assumption tries to solve the main goal using a hypothesis of compatible type, or else fails. Note also the ‹t› term notation, which is a shorthand for show t by assumption.

Tags:
Defined in module:: Init.Tactics

assumption_mod_cast

assumption_mod_cast is a variant of assumption that solves the goal using a hypothesis. Unlike assumption, it first pre-processes the goal and each hypothesis to move casts as far outwards as possible, so it can be used in more situations.

Concretely, it runs norm_cast on the goal. For each local hypothesis h, it also normalizes h with norm_cast and tries to use that to close the goal.

Tags:
Defined in module:: Init.Tactics

attempt_all

Helper internal tactic for implementing the tactic try?.

Tags:
Defined in module:: Init.Try

attempt_all_par

Helper internal tactic for implementing the tactic try? with parallel execution.

Tags:
Defined in module:: Init.Try

bv_check

This tactic works just like bv_decide but skips calling a SAT solver by using a proof that is already stored on disk. It is called with the name of an LRAT file in the same directory as the current Lean file:

bv_check "proof.lrat"

Tags:
Defined in module:: Std.Tactic.BVDecide.Syntax

bv_decide

Close fixed-width BitVec and Bool goals by obtaining a proof from an external SAT solver and verifying it inside Lean. The solvable goals are currently limited to

the Lean equivalent of QF_BV
automatically splitting up structures that contain information about BitVec or Bool

example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
  intros
  bv_decide

If bv_decide encounters an unknown definition it will be treated like an unconstrained BitVec variable. Sometimes this enables solving goals despite not understanding the definition because the precise properties of the definition do not matter in the specific proof.

If bv_decide fails to close a goal it provides a counter-example, containing assignments for all terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with bv_decide?.

If solving your problem relies inherently on using associativity or commutativity, consider enabling the bv.ac_nf option.

Note: bv_decide uses ofReduceBool and thus trusts the correctness of the code generator.

Note: include import Std.Tactic.BVDecide

Tags:
Defined in module:: Init.Tactics

bv_decide?

Suggest a proof script for a bv_decide tactic call. Useful for caching LRAT proofs.

Note: include import Std.Tactic.BVDecide

Tags:
Defined in module:: Init.Tactics

bv_normalize

Run the normalization procedure of bv_decide only. Sometimes this is enough to solve basic BitVec goals already.

Note: include import Std.Tactic.BVDecide

Tags:
Defined in module:: Init.Tactics

bv_omega

bv_omega is omega with an additional preprocessor that turns statements about BitVec into statements about Nat. Currently the preprocessor is implemented as try simp only [bitvec_to_nat] at *. bitvec_to_nat is a @[simp] attribute that you can (cautiously) add to more theorems.

Tags:
Defined in module:: Init.Tactics

by_cases

by_cases (h :)? p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch.

Tags:
Defined in module:: Init.ByCases

calc

Step-wise reasoning over transitive relations.

calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz

proves a = z from the given step-wise proofs. = can be replaced with any relation implementing the typeclass Trans. Instead of repeating the right- hand sides, subsequent left-hand sides can be replaced with _.

calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz

It is also possible to write the first relation as <lhs>\n _ = <rhs> := <proof>. This is useful for aligning relation symbols, especially on longer identifiers:

calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz

calc works as a term, as a tactic or as a conv tactic.

See Theorem Proving in Lean 4 for more information.

Tags:
Defined in module:: Init.NotationExtra

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

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

cases

Assuming x is a variable in the local context with an inductive type, cases x splits 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. If the type of an element in the local context depends on x, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well. cases detects unreachable cases and closes them automatically.

For example, given n : Nat and a goal with a hypothesis h : P n and target Q n, cases n produces one goal with hypothesis h : P 0 and target Q 0, and one goal with hypothesis h : P (Nat.succ a) and target Q (Nat.succ a). Here the name a is chosen automatically and is not accessible. You can use with to provide the variables names for each constructor.

cases e, where e is an expression instead of a variable, generalizes e in the goal, and then cases on the resulting variable.
Given as : List α, cases as with | nil => tac₁ | cons a as' => tac₂, uses tactic tac₁ for the nil case, and tac₂ for the cons case, and a and as' are used as names for the new variables introduced.
cases h : e, where e is a variable or an expression, performs cases on e as above, but also adds a hypothesis h : e = ... to each goal, where ... is the constructor instance for that particular case.

Tags:
Defined in module:: Init.Tactics

change

change tgt' will change the goal from tgt to tgt', assuming these are definitionally equal.
change t' at h will change hypothesis h : t to have type t', assuming assuming t and t' are definitionally equal.
change a with b will change occurrences of a to b in the goal, assuming a and b are definitionally equal.
change a with b at h similarly changes a to b in the type of hypothesis h.

Tags:
Defined in module:: Init.Tactics

classical

classical tacs runs tacs in a scope where Classical.propDecidable is a low priority local instance.

Note that classical is a scoping tactic: it adds the instance only within the scope of the tactic.

Tags:
Defined in module:: Init.Tactics

clean_wf

This tactic is used internally by lean before presenting the proof obligations from a well-founded definition to the user via decreasing_by. It is not necessary to use this tactic manually.

Tags:
Defined in module:: Init.WFTactics

clear

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

Tags:
Defined in module:: Init.Tactics

clear_value

clear_value x... clears the values of the given local definitions. A local definition x : α := v becomes a hypothesis x : α.
clear_value (h : x = _) adds a hypothesis h : x = v before clearing the value of x. This is short for have h : x = v := rfl; clear_value x. Any value definitionally equal to v can be used in place of _.
clear_value * clears values of all hypotheses that can be cleared. Fails if none can be cleared.

These syntaxes can be combined. For example, clear_value x y * ensures that x and y are cleared while trying to clear all other local definitions, and clear_value (hx : x = _) y * with hx does the same while first adding the hx : x = v hypothesis.

Tags:
Defined in module:: Init.Tactics

congr

Apply congruence (recursively) to goals of the form ⊢ f as = f bs and ⊢ f as ≍ f bs. The optional parameter is the depth of the recursive applications. This is useful when congr is too aggressive in breaking down the goal. For example, given ⊢ f (g (x + y)) = f (g (y + x)), congr produces the goals ⊢ x = y and ⊢ y = x, while congr 2 produces the intended ⊢ x + y = y + x.

Tags:
Defined in module:: Init.Tactics

constructor

If the main goal's target type is an inductive type, constructor solves it with the first matching constructor, or else fails.

Tags:
Defined in module:: Init.Tactics

contradiction

contradiction closes the main goal if its hypotheses are "trivially contradictory".

Inductive type/family with no applicable constructors
```
example (h : False) : p := by contradiction
```

Injectivity of constructors

example (h : none = some true) : p := by contradiction  --

Decidable false proposition

example (h : 2 + 2 = 3) : p := by contradiction

Contradictory hypotheses

example (h : p) (h' : ¬ p) : q := by contradiction

Other simple contradictions such as

example (x : Nat) (h : x ≠ x) : p := by contradiction

Tags:
Defined in module:: Init.Tactics

conv

conv => ... allows the user to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

See https://lean-lang.org/theorem_proving_in_lean4/conv.html for more details.

Basic forms:

conv => cs will rewrite the goal with conv tactics cs.
conv at h => cs will rewrite hypothesis h.
conv in pat => cs will rewrite the first subexpression matching pat (see pattern).

Tags:
Defined in module:: Init.Conv

conv'

Executes the given conv block without converting regular goal into a conv goal.

Tags:
Defined in module:: Init.Conv

cutsat

cutsat solves linear integer arithmetic goals.

It is a implemented as a thin wrapper around the grind tactic, enabling only the lia solver. Please use grind instead if you need additional capabilities.

Deprecated: Use lia instead.

Tags:
Defined in module:: Init.Grind.Tactics

dbg_trace

dbg_trace "foo" prints foo when elaborated. Useful for debugging tactic control flow:

example : False ∨ True := by
  first
  | apply Or.inl; trivial; dbg_trace "left"
  | apply Or.inr; trivial; dbg_trace "right"

Tags:
Defined in module:: Init.Tactics

decide

decide attempts to prove the main goal (with target type p) by synthesizing an instance of Decidable p and then reducing that instance to evaluate the truth value of p. If it reduces to isTrue h, then h is a proof of p that closes the goal.

The target is not allowed to contain local variables or metavariables. If there are local variables, you can first try using the revert tactic with these local variables to move them into the target, or you can use the +revert option, described below.

Options:

decide +revert begins by reverting local variables that the target depends on, after cleaning up the local context of irrelevant variables. A variable is relevant if it appears in the target, if it appears in a relevant variable, or if it is a proposition that refers to a relevant variable.
decide +kernel uses kernel for reduction instead of the elaborator. It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything, and (2) it reduces the Decidable instance only once instead of twice.
decide +native uses the native code compiler (#eval) to evaluate the Decidable instance, admitting the result via the Lean.ofReduceBool axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size of the trusted code base. Namely, it depends on the correctness of the Lean compiler and all definitions with an @[implemented_by] attribute. Like with +kernel, the Decidable instance is evaluated only once.

Limitation: In the default mode or +kernel mode, since decide uses reduction to evaluate the term, Decidable instances defined by well-founded recursion might not work because evaluating them requires reducing proofs. Reduction can also get stuck on Decidable instances with Eq.rec terms. These can appear in instances defined using tactics (such as rw and simp). To avoid this, create such instances using definitions such as decidable_of_iff instead.

Examples #

Proving inequalities:

example : 2 + 2 ≠ 5 := by decide

Trying to prove a false proposition:

example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
  1 ≠ 1
is false
-/

Trying to prove a proposition whose Decidable instance fails to reduce

opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
  unknownProp
since its 'Decidable' instance reduced to
  Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/

Properties and relations #

For equality goals for types with decidable equality, usually rfl can be used in place of decide.

example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl

Tags:
Defined in module:: Init.Tactics

decreasing_tactic

decreasing_tactic is called by default on well-founded recursions in order to synthesize a proof that recursive calls decrease along the selected well founded relation. It can be locally overridden by using decreasing_by tac on the recursive definition, and it can also be globally extended by adding more definitions for decreasing_tactic (or decreasing_trivial, which this tactic calls).

Tags:
Defined in module:: Init.WFTactics

decreasing_trivial

Extensible helper tactic for decreasing_tactic. This handles the "base case" reasoning after applying lexicographic order lemmas. It can be extended by adding more macro definitions, e.g.

macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)

Tags:
Defined in module:: Init.WFTactics

decreasing_trivial_pre_omega

Variant of decreasing_trivial that does not use omega, intended to be used in core modules before omega is available.

Tags:
Defined in module:: Init.WFTactics

decreasing_with

Constructs a proof of decreasing along a well founded relation, by simplifying, then applying lexicographic order lemmas and finally using ts to solve the base case. If it fails, it prints a message to help the user diagnose an ill-founded recursive definition.

Tags:
Defined in module:: Init.WFTactics

delta

delta id1 id2 ... delta-expands the definitions id1, id2, .... This is a low-level tactic, it will expose how recursive definitions have been compiled by Lean.

Tags:
Defined in module:: Init.Tactics

deriving_LawfulEq_tactic

This tactic has no documentation.

Tags:
Defined in module:: Init.LawfulBEqTactics

deriving_LawfulEq_tactic_step

This tactic has no documentation.

Tags:
Defined in module:: Init.LawfulBEqTactics

deriving_ReflEq_tactic

This tactic has no documentation.

Tags:
Defined in module:: Init.LawfulBEqTactics

done

done succeeds iff there are no remaining goals.

Tags:
Defined in module:: Init.Tactics

dsimp

The dsimp tactic is the definitional simplifier. It is similar to simp but only applies theorems that hold by reflexivity. Thus, the result is guaranteed to be definitionally equal to the input.

Tags:
Defined in module:: Init.Tactics

dsimp!

dsimp! is shorthand for dsimp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

Tags:
Defined in module:: Init.Meta

dsimp?

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

dsimp?!

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

eq_refl

eq_refl is equivalent to exact rfl, but has a few optimizations.

Tags:
Defined in module:: Init.Tactics

erw

erw [rules] is a shorthand for rw (transparency := .default) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

Tags:
Defined in module:: Init.Meta

exact

exact e closes the main goal if its target type matches that of e.

Tags:
Defined in module:: Init.Tactics

exact?

Searches environment for definitions or theorems that can solve the goal using exact with conditions resolved by solve_by_elim.

The optional using clause provides identifiers in the local context that must be used by exact? when closing the goal. This is most useful if there are multiple ways to resolve the goal, and one wants to guide which lemma is used.

Use +grind to enable grind as a fallback discharger for subgoals. Use +try? to enable try? as a fallback discharger for subgoals. Use -star to disable fallback to star-indexed lemmas (like Empty.elim, And.left). Use +all to collect all successful lemmas instead of stopping at the first.

Tags:
Defined in module:: Init.Tactics

exact_mod_cast

Normalize casts in the goal and the given expression, then close the goal with exact.

Tags:
Defined in module:: Init.TacticsExtra

exfalso

exfalso converts a goal ⊢ tgt into ⊢ False by applying False.elim.

Tags:
Defined in module:: Init.Tactics

exists

exists e₁, e₂, ... is shorthand for refine ⟨e₁, e₂, ...⟩; try trivial. It is useful for existential goals.

Tags:
Defined in module:: Init.Tactics

expose_names

expose_names renames all inaccessible variables with accessible names, making them available for reference in generated tactics. However, this renaming introduces machine-generated names that are not fully under user control. expose_names is primarily intended as a preamble for auto-generated end-game tactic scripts. It is also useful as an alternative to set_option tactic.hygienic false. If explicit control over renaming is needed in the middle of a tactic script, consider using structured tactic scripts with match .. with, induction .. with, or intro with explicit user-defined names, as well as tactics such as next, case, and rename_i.

Tags:
Defined in module:: Init.Tactics

ext

Applies extensionality lemmas that are registered with the @[ext] attribute.

ext pat* applies extensionality theorems as much as possible, using the patterns pat* to introduce the variables in extensionality theorems using rintro. For example, the patterns are used to name the variables introduced by lemmas such as funext.
Without patterns,ext applies extensionality lemmas as much as possible but introduces anonymous hypotheses whenever needed.
ext pat* : n applies ext theorems only up to depth n.

The ext1 pat* tactic is like ext pat* except that it only applies a single extensionality theorem.

Unused patterns will generate warning. Patterns that don't match the variables will typically result in the introduction of anonymous hypotheses.

Tags:
Defined in module:: Init.Ext

ext1

ext1 pat* is like ext pat* except that it only applies a single extensionality theorem rather than recursively applying as many extensionality theorems as possible.

The pat* patterns are processed using the rintro tactic. If no patterns are supplied, then variables are introduced anonymously using the intros tactic.

Tags:
Defined in module:: Init.Ext

extract_lets

Extracts let and have expressions from within the target or a local hypothesis, introducing new local definitions.

extract_lets extracts all the lets from the target.
extract_lets x y z extracts all the lets from the target and uses x, y, and z for the first names. Using _ for a name leaves it unnamed.
extract_lets x y z at h operates on the local hypothesis h instead of the target.

For example, given a local hypotheses if the form h : let x := v; b x, then extract_lets z at h introduces a new local definition z := v and changes h to be h : b z.

Tags:
Defined in module:: Init.Tactics

fail

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

Tags:
Defined in module:: Init.Tactics

fail_if_success

fail_if_success t fails if the tactic t succeeds.

Tags:
Defined in module:: Init.Tactics

false_or_by_contra

Changes the goal to False, retaining as much information as possible:

If the goal is False, do nothing.
If the goal is an implication or a function type, introduce the argument and restart. (In particular, if the goal is x ≠ y, introduce x = y.)
Otherwise, for a propositional goal P, replace it with ¬ ¬ P (attempting to find a Decidable instance, but otherwise falling back to working classically) and introduce ¬ P.
For a non-propositional goal use False.elim.

Tags:
Defined in module:: Init.Tactics

first

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

Tags:
Defined in module:: Init.Tactics

first_par

Helper internal tactic for implementing the tactic try? with parallel execution, returning first success.

Tags:
Defined in module:: Init.Try

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.

Tags:
Defined in module:: Init.Tactics

fun_cases

The fun_cases tactic is a convenience wrapper of the cases tactic when using a functional cases principle.

The tactic invocation

fun_cases f x ... y ...`

is equivalent to

cases y, ... using f.fun_cases_unfolding x ...

where the arguments of f are used as arguments to f.fun_cases_unfolding or targets of the case analysis, as appropriate.

The form

fun_cases f

(with no arguments to f) searches the goal for a unique eligible application of f, and uses these arguments. An application of f is eligible if it is saturated and the arguments that will become targets are free variables.

The form fun_cases f x y with | case1 => tac₁ | case2 x' ih => tac₂ works like with cases.

Under set_option tactic.fun_induction.unfolding true (the default), fun_induction uses the f.fun_cases_unfolding theorem, which will try to automatically unfold the call to f in the goal. With set_option tactic.fun_induction.unfolding false, it uses f.fun_cases instead.

Tags:
Defined in module:: Init.Tactics

fun_induction

The fun_induction tactic is a convenience wrapper around the induction tactic to use the functional induction principle.

The tactic invocation

fun_induction f x₁ ... xₙ y₁ ... yₘ

where f is a function defined by non-mutual structural or well-founded recursion, is equivalent to

induction y₁, ... yₘ using f.induct_unfolding x₁ ... xₙ

where the arguments of f are used as arguments to f.induct_unfolding or targets of the induction, as appropriate.

The form

fun_induction f

The forms fun_induction f x y generalizing z₁ ... zₙ and fun_induction f x y with | case1 => tac₁ | case2 x' ih => tac₂ work like with induction.

Under set_option tactic.fun_induction.unfolding true (the default), fun_induction uses the f.induct_unfolding induction principle, which will try to automatically unfold the call to f in the goal. With set_option tactic.fun_induction.unfolding false, it uses f.induct instead.

Tags:
Defined in module:: Init.Tactics

funext

Apply function extensionality and introduce new hypotheses. The tactic funext will keep applying the funext lemma until the goal target is not reducible to

  |-  ((fun x => ...) = (fun x => ...))

The variant funext h₁ ... hₙ applies funext n times, and uses the given identifiers to name the new hypotheses. Patterns can be used like in the intro tactic. Example, given a goal

  |-  ((fun x : Nat × Bool => ...) = (fun x => ...))

funext (a, b) applies funext once and performs pattern matching on the newly introduced pair.

Tags:
Defined in module:: Init.NotationExtra

generalize

generalize ([h :] e = x),+ replaces all occurrences es in the main goal with a fresh hypothesis xs. If h is given, h : e = x is introduced as well.
generalize e = x at h₁ ... hₙ also generalizes occurrences of e inside h₁, ..., hₙ.
generalize e = x at * will generalize occurrences of e everywhere.

Tags:
Defined in module:: Init.Tactics

get_elem_tactic

get_elem_tactic is the tactic automatically called by the notation arr[i] to prove any side conditions that arise when constructing the term (e.g. the index is in bounds of the array). It just delegates to get_elem_tactic_extensible and gives a diagnostic error message otherwise; users are encouraged to extend get_elem_tactic_extensible instead of this tactic.

Tags:
Defined in module:: Init.Tactics

get_elem_tactic_extensible

get_elem_tactic_extensible is an extensible tactic automatically called by the notation arr[i] to prove any side conditions that arise when constructing the term (e.g. the index is in bounds of the array). The default behavior is to try simp +arith and omega (for doing linear arithmetic in the index).

(Note that the core tactic get_elem_tactic has already tried done and assumption before the extensible tactic is called.)

Tags:
Defined in module:: Init.Tactics

get_elem_tactic_trivial

get_elem_tactic_trivial has been deprecated in favour of get_elem_tactic_extensible.

Tags:
Defined in module:: Init.Tactics

grind

grind is a tactic inspired by modern SMT solvers. Picture a virtual whiteboard: every time grind discovers a new equality, inequality, or logical fact, it writes it on the board, groups together terms known to be equal, and lets each reasoning engine read from and contribute to the shared workspace. These engines work together to handle equality reasoning, apply known theorems, propagate new facts, perform case analysis, and run specialized solvers for domains like linear arithmetic and commutative rings.

See the reference manual's chapter on grind for more information.

grind is not designed for goals whose search space explodes combinatorially, think large pigeonhole instances, graph‑coloring reductions, high‑order N‑queens boards, or a 200‑variable Sudoku encoded as Boolean constraints. Such encodings require thousands (or millions) of case‑splits that overwhelm grind’s branching search.

For bit‑level or combinatorial problems, consider using bv_decide. bv_decide calls a state‑of‑the‑art SAT solver (CaDiCaL) and then returns a compact, machine‑checkable certificate.

Equality reasoning #

grind uses congruence closure to track equalities between terms. When two terms are known to be equal, congruence closure automatically deduces equalities between more complex expressions built from them. For example, if a = b, then congruence closure will also conclude that f a = f b for any function f. This forms the foundation for efficient equality reasoning in grind. Here is an example:

example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := by
  grind

Applying theorems using E-matching #

To apply existing theorems, grind uses a technique called E-matching, which finds matches for known theorem patterns while taking equalities into account. Combined with congruence closure, E-matching helps grind discover non-obvious consequences of theorems and equalities automatically.

Consider the following functions and theorems:

def f (a : Nat) : Nat :=
  a + 1

def g (a : Nat) : Nat :=
  a - 1

@[grind =]
theorem gf (x : Nat) : g (f x) = x := by
  simp [f, g]

The theorem gf asserts that g (f x) = x for all natural numbers x. The attribute [grind =] instructs grind to use the left-hand side of the equation, g (f x), as a pattern for E-matching. Suppose we now have a goal involving:

example {a b} (h : f b = a) : g a = b := by
  grind

Although g a is not an instance of the pattern g (f x), it becomes one modulo the equation f b = a. By substituting a with f b in g a, we obtain the term g (f b), which matches the pattern g (f x) with the assignment x := b. Thus, the theorem gf is instantiated with x := b, and the new equality g (f b) = b is asserted. grind then uses congruence closure to derive the implied equality g a = g (f b) and completes the proof.

The pattern used to instantiate theorems affects the effectiveness of grind. For example, the pattern g (f x) is too restrictive in the following case: the theorem gf will not be instantiated because the goal does not even contain the function symbol g.

example (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind

You can use the command grind_pattern to manually select a pattern for a given theorem. In the following example, we instruct grind to use f x as the pattern, allowing it to solve the goal automatically:

grind_pattern gf => f x

example {a b c} (h₁ : f b = a) (h₂ : f c = a) : b = c := by
  grind

You can enable the option trace.grind.ematch.instance to make grind print a trace message for each theorem instance it generates.

You can also specify a multi-pattern to control when grind should apply a theorem. A multi-pattern requires that all specified patterns are matched in the current context before the theorem is applied. This is useful for theorems such as transitivity rules, where multiple premises must be simultaneously present for the rule to apply. The following example demonstrates this feature using a transitivity axiom for a binary relation R:

opaque R : Int → Int → Prop
axiom Rtrans {x y z : Int} : R x y → R y z → R x z

grind_pattern Rtrans => R x y, R y z

example {a b c d} : R a b → R b c → R c d → R a d := by
  grind

By specifying the multi-pattern R x y, R y z, we instruct grind to instantiate Rtrans only when both R x y and R y z are available in the context. In the example, grind applies Rtrans to derive R a c from R a b and R b c, and can then repeat the same reasoning to deduce R a d from R a c and R c d.

Instead of using grind_pattern to explicitly specify a pattern, you can use the @[grind] attribute or one of its variants, which will use a heuristic to generate a (multi-)pattern. The complete list is available in the reference manual. The main ones are:

@[grind →] will select a multi-pattern from the hypotheses of the theorem (i.e. it will use the theorem for forwards reasoning). In more detail, it will traverse the hypotheses of the theorem from left-to-right, and each time it encounters a minimal indexable (i.e. has a constant as its head) subexpression which "covers" (i.e. fixes the value of) an argument which was not previously covered, it will add that subexpression as a pattern, until all arguments have been covered.
@[grind ←] will select a multi-pattern from the conclusion of theorem (i.e. it will use the theorem for backwards reasoning). This may fail if not all the arguments to the theorem appear in the conclusion.
@[grind] will traverse the conclusion and then the hypotheses left-to-right, adding patterns as they increase the coverage, stopping when all arguments are covered.
@[grind =] checks that the conclusion of the theorem is an equality, and then uses the left-hand-side of the equality as a pattern. This may fail if not all of the arguments appear in the left-hand-side.

Here is the previous example again but using the attribute [grind →]

opaque R : Int → Int → Prop
@[grind →] axiom Rtrans {x y z : Int} : R x y → R y z → R x z

example {a b c d} : R a b → R b c → R c d → R a d := by
  grind

To control theorem instantiation and avoid generating an unbounded number of instances, grind uses a generation counter. Terms in the original goal are assigned generation zero. When grind applies a theorem using terms of generation ≤ n n, any new terms it creates are assigned generation n + 1 + 1 1. This limits how far the tactic explores when applying theorems and helps prevent an excessive number of instantiations.

Key options: #

grind (ematch := <num>) controls the number of E-matching rounds.
grind [<name>, ...] instructs grind to use the declaration name during E-matching.
grind only [<name>, ...] is like grind [<name>, ...] but does not use theorems tagged with @[grind].
grind (gen := <num>) sets the maximum generation.

Linear integer arithmetic (`lia`) #

grind can solve goals that reduce to linear integer arithmetic (LIA) using an integrated decision procedure called lia. It understands

equalities p = 0
inequalities p ≤ 0
disequalities p ≠ 0
divisibility d ∣ p

The solver incrementally assigns integer values to variables; when a partial assignment violates a constraint it adds a new, implied constraint and retries. This model-based search is complete for LIA.

Key options: #

grind -lia disable the solver (useful for debugging)
grind +qlia accept rational models (shrinks the search space but is incomplete for ℤ)

Examples: #

-- Even + even is never odd.
example {x y : Int} : 2 * x + 4 * y ≠ 5 := by
  grind

-- Mixing equalities and inequalities.
example {x y : Int} :
    2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
  grind

-- Reasoning with divisibility.
example (a b : Int) :
    2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
  grind

example (x y : Int) :
    27 ≤ 11*x + 13*y →
    11*x + 13*y ≤ 45 →
    -10 ≤ 7*x - 9*y →
    7*x - 9*y ≤ 4 → False := by
  grind

-- Types that implement the `ToInt` type-class.
example (a b c : UInt64)
    : a ≤ 2 → b ≤ 3 → c - a - b = 0 → c ≤ 5 := by
  grind

Algebraic solver (`ring`) #

grind ships with an algebraic solver nick-named ring for goals that can be phrased as polynomial equations (or disequations) over commutative rings, semirings, or fields.

Works out of the box All core numeric types and relevant Mathlib types already provide the required type-class instances, so the solver is ready to use in most developments.

What it can decide:

equalities of the form p = q
disequalities p ≠ q
basic reasoning under field inverses (a / b := a * b⁻¹)
goals that mix ring facts with other grind engines

Key options: #

grind -ring turn the solver off (useful when debugging)
grind (ringSteps := n) cap the number of steps performed by this procedure.

Examples #

open Lean Grind

example [CommRing α] (x : α) : (x + 1) * (x - 1) = x^2 - 1 := by
  grind

-- Characteristic 256 means 16 * 16 = 0.
example [CommRing α] [IsCharP α 256] (x : α) :
    (x + 16) * (x - 16) = x^2 := by
  grind

-- Works on built-in rings such as `UInt8`.
example (x : UInt8) : (x + 16) * (x - 16) = x^2 := by
  grind

example [CommRing α] (a b c : α) :
    a + b + c = 3 →
    a^2 + b^2 + c^2 = 5 →
    a^3 + b^3 + c^3 = 7 →
    a^4 + b^4 = 9 - c^4 := by
  grind

example [Field α] [NoNatZeroDivisors α] (a : α) :
    1 / a + 1 / (2 * a) = 3 / (2 * a) := by
  grind

Other options #

grind (splits := <num>) caps the depth of the search tree. Once a branch performs num splits grind stops splitting further in that branch.
grind -splitIte disables case splitting on if-then-else expressions.
grind -splitMatch disables case splitting on match expressions.
grind +splitImp instructs grind to split on any hypothesis A → B whose antecedent A is propositional.
grind -linarith disables the linear arithmetic solver for (ordered) modules and rings.

Additional Examples #

example {a b} {as bs : List α} : (as ++ bs ++ [b]).getLastD a = b := by
  grind

example (x : BitVec (w+1)) : (BitVec.cons x.msb (x.setWidth w)) = x := by
  grind

example (as : Array α) (lo hi i j : Nat) :
    lo ≤ i → i < j → j ≤ hi → j < as.size → min lo (as.size - 1) ≤ i := by
  grind

Tags:
Defined in module:: Init.Grind.Tactics

grind?

grind? takes the same arguments as grind, but reports an equivalent call to grind only that would be sufficient to close the goal. This is useful for reducing the size of the grind theorems in a local invocation.

Tags:
Defined in module:: Init.Grind.Tactics

grobner

grobner solves goals that can be phrased as polynomial equations (with further polynomial equations as hypotheses) over commutative (semi)rings, using the Grobner basis algorithm.

It is a implemented as a thin wrapper around the grind tactic, enabling only the grobner solver. Please use grind instead if you need additional capabilities.

Tags:
Defined in module:: Init.Grind.Tactics

guard_expr

Tactic to check equality of two expressions.

guard_expr e = e' checks that e and e' are defeq at reducible transparency.
guard_expr e =~ e' checks that e and e' are defeq at default transparency.
guard_expr e =ₛ e' checks that e and e' are syntactically equal.
guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

Tags:
Defined in module:: Init.Guard

guard_hyp

Tactic to check that a named hypothesis has a given type and/or value.

guard_hyp h : t checks the type up to reducible defeq,
guard_hyp h :~ t checks the type up to default defeq,
guard_hyp h :ₛ t checks the type up to syntactic equality,
guard_hyp h :ₐ t checks the type up to alpha equality.
guard_hyp h := v checks value up to reducible defeq,
guard_hyp h :=~ v checks value up to default defeq,
guard_hyp h :=ₛ v checks value up to syntactic equality,
guard_hyp h :=ₐ v checks the value up to alpha equality.

The value v is elaborated using the type of h as the expected type.

Tags:
Defined in module:: Init.Guard

guard_target

Tactic to check that the target agrees with a given expression.

guard_target = e checks that the target is defeq at reducible transparency to e.
guard_target =~ e checks that the target is defeq at default transparency to e.
guard_target =ₛ e checks that the target is syntactically equal to e.
guard_target =ₐ e checks that the target is alpha-equivalent to e.

The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

Tags:
Defined in module:: Init.Guard

have

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded, unlike definitions added by the let tactic.

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.
The syntax have (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the have term.

Properties and relations #

It is not possible to unfold a variable introduced using have, since the definition's value is forgotten. The let tactic introduces definitions that can be unfolded.
The have h : t := e is like doing let h : t := e; clear_value h.
The have tactic is preferred for propositions, and let is preferred for non-propositions.
Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons. Consider using the equivalent let +nondep to indicate the intent.

Tags:
Defined in module:: Init.Tactics

have'

Similar to have, but using refine'

Tags:
Defined in module:: Init.Tactics

haveI

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

Tags:
Defined in module:: Init.Tactics

ident

This tactic has no documentation.

Tags:
Defined in module:: Lean.Parser.Tactic

if

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 ?_.)

The assumptions in each subgoal can be named. 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.

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.

Tags:
Defined in module:: Init.Tactics

induction

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

Tags:
Defined in module:: Init.Tactics

infer_instance

infer_instance is an abbreviation for exact inferInstance. It synthesizes a value of any target type by typeclass inference.

Tags:
Defined in module:: Init.Tactics

injection

The injection tactic is based on the fact that constructors of inductive data types are injections. That means that if c is a constructor of an inductive datatype, and if (c t₁) and (c t₂) are two terms that are equal then t₁ and t₂ are equal too. If q is a proof of a statement of conclusion t₁ = t₂, then injection applies injectivity to derive the equality of all arguments of t₁ and t₂ placed in the same positions. For example, from (a::b) = (c::d) we derive a=c and b=d. To use this tactic t₁ and t₂ should be constructor applications of the same constructor. Given h : a::b = c::d, the tactic injection h adds two new hypothesis with types a = c and b = d to the main goal. The tactic injection h with h₁ h₂ uses the names h₁ and h₂ to name the new hypotheses.

Tags:
Defined in module:: Init.Tactics

injections

injections applies injection to all hypotheses recursively (since injection can produce new hypotheses). Useful for destructing nested constructor equalities like (a::b::c) = (d::e::f).

Tags:
Defined in module:: Init.Tactics

intro

Introduces one or more hypotheses, optionally naming and/or pattern-matching them. For each hypothesis to be introduced, the remaining main goal's target type must be a let or function type.

intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption. It is equivalent to intro _.
intro x y introduces two hypotheses and names them. Individual hypotheses can be anonymized via _, given a type ascription, or matched against a pattern:
```
-- ... ⊢ α × β → ...
intro (a, b)
-- ..., a : α, b : β ⊢ ...
```
intro rfl is short for intro h; subst h, if h is an equality where the left-hand or right-hand side is a variable.
Alternatively, intro can be combined with pattern matching much like fun:
```
intro
| n + 1, 0 => tac
| ...
```

Tags:
Defined in module:: Init.Tactics

intros

intros repeatedly applies intro to introduce zero or more hypotheses until the goal is no longer a binding expression (i.e., a universal quantifier, function type, implication, or have/let), without performing any definitional reductions (no unfolding, beta, eta, etc.). The introduced hypotheses receive inaccessible (hygienic) names.

intros x y z is equivalent to intro x y z and exists only for historical reasons. The intro tactic should be preferred in this case.

Properties and relations #

intros succeeds even when it introduces no hypotheses.
repeat intro is like intros, but it performs definitional reductions to expose binders, and as such it may introduce more hypotheses than intros.
intros is equivalent to intro _ _ … _, with the fewest trailing _ placeholders needed so that the goal is no longer a binding expression. The trailing introductions do not perform any definitional reductions.

Examples #

Implications:

example (p q : Prop) : p → q → p := by
  intros
  /- Tactic state
     a✝¹ : p
     a✝ : q
     ⊢ p      -/
  assumption

Let-bindings:

example : let n := 1; let k := 2; n + k = 3 := by
  intros
  /- n✝ : Nat := 1
     k✝ : Nat := 2
     ⊢ n✝ + k✝ = 3 -/
  rfl

Does not unfold definitions:

def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0

example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
  intros
  /- Tactic state
     f✝ : Nat → Nat
     a✝ : AllEven f✝
     ⊢ AllEven fun k => f✝ (k + 1) -/
  sorry

Tags:
Defined in module:: Init.Tactics

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₂
  ⋯

Tags:
Defined in module:: Init.TacticsExtra

left

Applies the first constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.

example : True ∨ False := by
  left
  trivial

Tags:
Defined in module:: Init.Tactics

let

The let tactic is for adding definitions to the local context of the main goal. The definition can be unfolded, unlike definitions introduced by have.

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 : γ.
The syntax let (eq := h) pat := e is equivalent to match h : e with | pat => _, which adds the equation h : e = pat to the local context.

The tactic supports all the same syntax variants and options as the let term.

Properties and relations #

Unlike have, it is possible to unfold definitions introduced using let, using tactics such as simp, dsimp, unfold, and subst.
The clear_value tactic turns a let definition into a have definition after the fact. The tactic might fail if the local context depends on the value of the variable.
The let tactic is preferred for data (non-propositions).
Sometimes have is used for non-propositions to ensure that the variable is never unfolded, which may be important for performance reasons.

Tags:
Defined in module:: Init.Tactics

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.

The tactic supports all the same syntax variants and options as the let term.

Tags:
Defined in module:: Init.Tactics

let'

Similar to let, but using refine'

Tags:
Defined in module:: Init.Tactics

letI

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

Tags:
Defined in module:: Init.Tactics

let_to_have

Transforms let expressions into have expressions when possible.

let_to_have transforms lets in the target.
let_to_have at h transforms lets in the given local hypothesis.

Tags:
Defined in module:: Init.Tactics

lia

lia solves linear integer arithmetic goals.

It is a implemented as a thin wrapper around the grind tactic, enabling only the lia solver. Please use grind instead if you need additional capabilities.

Tags:
Defined in module:: Init.Grind.Tactics

lift_lets

Lifts let and have expressions within a term as far out as possible. It is like extract_lets +lift, but the top-level lets at the end of the procedure are not extracted as local hypotheses.

lift_lets lifts let expressions in the target.
lift_lets at h lifts let expressions at the given local hypothesis.

For example,

example : (let x := 1; x) = 1 := by
  lift_lets
  -- ⊢ let x := 1; x = 1
  ...

Tags:
Defined in module:: Init.Tactics

massumption

massumption is like assumption, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
  mintro _ _
  massumption

Tags:
Defined in module:: Init.Tactics

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

Tags:
Defined in module:: Lean.Parser.Tactic

mcases

Like rcases, but operating on stateful Std.Do.SPred goals. Example: Given a goal h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R, mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩ will yield two goals: (hq : Q, hqr : Q → R) ⊢ₛ R and (hr : R) ⊢ₛ R.

That is, mcases h with pat has the following semantics, based on pat:

pat=□h' renames h to h' in the stateful context, regardless of whether h is pure
pat=⌜h'⌝ introduces h' : φ to the pure local context if h : ⌜φ⌝ (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure)
pat=h' is like pat=⌜h'⌝ if h is pure (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure), otherwise it is like pat=□h'.
pat=_ renames h to an inaccessible name
pat=- discards h
⟨pat₁, pat₂⟩ matches on conjunctions and existential quantifiers and recurses via pat₁ and pat₂.
⟨pat₁ | pat₂⟩ matches on disjunctions, matching the left alternative via pat₁ and the right alternative via pat₂.

Tags:
Defined in module:: Init.Tactics

mclear

mclear is like clear, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
  mintro HP
  mintro HQ
  mclear HP
  mexact HQ

Tags:
Defined in module:: Init.Tactics

mconstructor

mconstructor is like constructor, but operating on a stateful Std.Do.SPred goal.

example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
  mintro HQ
  mconstructor <;> mexact HQ

Tags:
Defined in module:: Init.Tactics

mdup

Duplicate a stateful Std.Do.SPred hypothesis.

Tags:
Defined in module:: Std.Tactic.Do.Syntax

mexact

mexact is like exact, but operating on a stateful Std.Do.SPred goal.

example (Q : SPred σs) : Q ⊢ₛ Q := by
  mstart
  mintro HQ
  mexact HQ

Tags:
Defined in module:: Init.Tactics

mexfalso

mexfalso is like exfalso, but operating on a stateful Std.Do.SPred goal.

example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
  mintro HP
  mexfalso
  mexact HP

Tags:
Defined in module:: Init.Tactics

mexists

mexists is like exists, but operating on a stateful Std.Do.SPred goal.

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mexists 42

Tags:
Defined in module:: Init.Tactics

mframe

mframe infers which hypotheses from the stateful context can be moved into the pure context. This is useful because pure hypotheses "survive" the next application of modus ponens (Std.Do.SPred.mp) and transitivity (Std.Do.SPred.entails.trans).

It is used as part of the mspec tactic.

example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
  mintro _
  mframe
  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
  mcases h with hP
  mexact h

Tags:
Defined in module:: Init.Tactics

mhave

mhave is like have, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HQ

Tags:
Defined in module:: Init.Tactics

mintro

Like intro, but introducing stateful hypotheses into the stateful context of the Std.Do.SPred proof mode. That is, given a stateful goal (hᵢ : Hᵢ)* ⊢ₛ P → T, mintro h transforms into (hᵢ : Hᵢ)*, (h : P) ⊢ₛ T.

Furthermore, mintro ∀s is like intro s, but preserves the stateful goal. That is, mintro ∀s brings the topmost state variable s:σ in scope and transforms (hᵢ : Hᵢ)* ⊢ₛ T (where the entailment is in Std.Do.SPred (σ::σs)) into (hᵢ : Hᵢ s)* ⊢ₛ T s (where the entailment is in Std.Do.SPred σs).

Beyond that, mintro supports the full syntax of mcases patterns (mintro pat = (mintro h; mcases h with pat), and can perform multiple introductions in sequence.

Tags:
Defined in module:: Init.Tactics

mleave

Leaves the stateful proof mode of Std.Do.SPred, tries to eta-expand through all definitions related to the logic of the Std.Do.SPred and gently simplifies the resulting pure Lean proposition. This is often the right thing to do after mvcgen in order for automation to prove the goal.

Tags:
Defined in module:: Init.Tactics

mleft

mleft is like left, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
  mintro HP
  mleft
  mexact HP

Tags:
Defined in module:: Init.Tactics

mpure

mpure moves a pure hypothesis from the stateful context into the pure context.

example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
  mintro Hφ
  mpure Hφ
  mexact (ψ Hφ)

Tags:
Defined in module:: Init.Tactics

mpure_intro

mpure_intro operates on a stateful Std.Do.SPred goal of the form P ⊢ₛ ⌜φ⌝. It leaves the stateful proof mode (thereby discarding P), leaving the regular goal φ.

theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
  mpure_intro
  exact True.intro

Tags:
Defined in module:: Init.Tactics

mrefine

Like refine, but operating on stateful Std.Do.SPred goals.

example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
  mintro ⟨HP, HQ, HR⟩
  mrefine ⟨HP, HR⟩

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mrefine ⟨⌜42⌝, H⟩

Tags:
Defined in module:: Init.Tactics

mrename_i

mrename_i is like rename_i, but names inaccessible stateful hypotheses in a Std.Do.SPred goal.

Tags:
Defined in module:: Init.Tactics

mreplace

mreplace is like replace, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HPQ

Tags:
Defined in module:: Init.Tactics

mrevert

mrevert is like revert, but operating on a stateful Std.Do.SPred goal.

example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
  mintro ⟨HP, HQ, HR⟩
  mrevert HR
  mrevert HP
  mintro HP'
  mintro HR'
  mexact HR'

Tags:
Defined in module:: Init.Tactics

mright

mright is like right, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
  mintro HP
  mright
  mexact HP

Tags:
Defined in module:: Init.Tactics

mspec

mspec is an apply-like tactic that applies a Hoare triple specification to the target of the stateful goal.

Given a stateful goal H ⊢ₛ wp⟦prog⟧ Q', mspec foo_spec will instantiate foo_spec : ... → ⦃P⦄ foo ⦃Q⦄, match foo against prog and produce subgoals for the verification conditions ?pre : H ⊢ₛ P and ?post : Q ⊢ₚ Q'.

If prog = x >>= f, then mspec Specs.bind is tried first so that foo is matched against x instead. Tactic mspec_no_bind does not attempt to do this decomposition.
If ?pre or ?post follow by .rfl, then they are discharged automatically.
?post is automatically simplified into constituent ⊢ₛ entailments on success and failure continuations.
?pre and ?post.* goals introduce their stateful hypothesis under an inaccessible name. You can give it a name with the mrename_i tactic.
Any uninstantiated MVar arising from instantiation of foo_spec becomes a new subgoal.
If the target of the stateful goal looks like fun s => _ then mspec will first mintro ∀s.
If P has schematic variables that can be instantiated by doing mintro ∀s, for example foo_spec : ∀(n:Nat), ⦃fun s => ⌜n = s⌝⦄ foo ⦃Q⦄, then mspec will do mintro ∀s first to instantiate n = s.
Right before applying the spec, the mframe tactic is used, which has the following effect: Any hypothesis Hᵢ in the goal h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T that is pure (i.e., equivalent to some ⌜φᵢ⌝) will be moved into the pure context as hᵢ:φᵢ.

Additionally, mspec can be used without arguments or with a term argument:

mspec without argument will try and look up a spec for x registered with @[spec].
mspec (foo_spec blah ?bleh) will elaborate its argument as a term with expected type ⦃?P⦄ x ⦃?Q⦄ and introduce ?bleh as a subgoal. This is useful to pass an invariant to e.g., Specs.forIn_list and leave the inductive step as a hole.

Tags:
Defined in module:: Init.Tactics

mspec_no_bind

mspec_no_simp $spec first tries to decompose Bind.binds before applying $spec. This variant of mspec_no_simp does not; mspec_no_bind $spec is defined as

try with_reducible mspec_no_bind Std.Do.Spec.bind
mspec_no_bind $spec

Tags:
Defined in module:: Std.Tactic.Do.Syntax

mspec_no_simp

Like mspec, but does not attempt slight simplification and closing of trivial sub-goals. mspec $spec is roughly (the set of simp lemmas below might not be up to date)

mspec_no_simp $spec
all_goals
  ((try simp only [SPred.true_intro_simp, SPred.apply_pure]);
   (try mpure_intro; trivial))

Tags:
Defined in module:: Std.Tactic.Do.Syntax

mspecialize

mspecialize is like specialize, but operating on a stateful Std.Do.SPred goal. It specializes a hypothesis from the stateful context with hypotheses from either the pure or stateful context or pure terms.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ

Tags:
Defined in module:: Init.Tactics

mspecialize_pure

mspecialize_pure is like mspecialize, but it specializes a hypothesis from the pure context with hypotheses from either the pure or stateful context or pure terms.

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
  mintro HQ
  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
  mexact HΨ

Tags:
Defined in module:: Init.Tactics

mstart

Start the stateful proof mode of Std.Do.SPred. This will transform a stateful goal of the form H ⊢ₛ T into ⊢ₛ H → T upon which mintro can be used to re-introduce H and give it a name. It is often more convenient to use mintro directly, which will try mstart automatically if necessary.

Tags:
Defined in module:: Init.Tactics

mstop

Stops the stateful proof mode of Std.Do.SPred. This will simply forget all the names given to stateful hypotheses and pretty-print a bit differently.

Tags:
Defined in module:: Init.Tactics

mvcgen

mvcgen will break down a Hoare triple proof goal like ⦃P⦄ prog ⦃Q⦄ into verification conditions, provided that all functions used in prog have specifications registered with @[spec].

Verification Conditions and specifications #

A verification condition is an entailment in the stateful logic of Std.Do.SPred in which the original program prog no longer occurs. Verification conditions are introduced by the mspec tactic; see the mspec tactic for what they look like. When there's no applicable mspec spec, mvcgen will try and rewrite an application prog = f a b c with the simp set registered via @[spec].

Features #

When used like mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat], mvcgen will additionally

add a Hoare triple specification foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄ to spec set for a function foo occurring in prog,
unfold a definition def bar_def ... := ... in prog,
unfold any method of the instBEqFloat : BEq Float instance in prog.
it will no longer substitute away let-expressions that occur at most once in P, Q or prog.

Config options #

+noLetElim is just one config option of many. Check out Lean.Elab.Tactic.Do.VCGen.Config for all options. Of particular note is stepLimit = some 42, which is useful for bisecting bugs in mvcgen and tracing its execution.

Extended syntax #

Often, mvcgen will be used like this:

mvcgen [...]
case inv1 => by exact I1
case inv2 => by exact I2
all_goals (mleave; try grind)

There is special syntax for this:

mvcgen [...] invariants
· I1
· I2
with grind

When I1 and I2 need to refer to inaccessibles (mvcgen will introduce a lot of them for program variables), you can use case label syntax:

mvcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2
with grind

This is more convenient than the equivalent · by rename_i _ acc _; exact I1 acc.

Invariant suggestions #

mvcgen will suggest invariants for you if you use the invariants? keyword.

mvcgen [...] invariants?

This is useful if you do not recall the exact syntax to construct invariants. Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and this must hold at the end of the loop" by looking at the corresponding VCs. Although the suggested invariant is a good starting point, it is too strong and requires users to interpolate it such that the inductive step can be proved. Example:

def mySum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for x in l do
    acc := acc + x
  return acc

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen invariants?
  all_goals admit

Tags:
Defined in module:: Init.Tactics

mvcgen?

A hint tactic that expands to mvcgen invariants?.

Tags:
Defined in module:: Std.Tactic.Do.Syntax

mvcgen_trivial

mvcgen_trivial is the tactic automatically called by mvcgen to discharge VCs. It tries to discharge the VC by applying (try mpure_intro); trivial and otherwise delegates to mvcgen_trivial_extensible. Users are encouraged to extend mvcgen_trivial_extensible instead of this tactic in order not to override the default (try mpure_intro); trivial behavior.

Tags:
Defined in module:: Std.Tactic.Do.Syntax

mvcgen_trivial_extensible

This tactic has no documentation.

Tags:
Defined in module:: Std.Tactic.Do.Syntax

native_decide

native_decide is a synonym for decide +native. It will attempt to prove a goal of type p by synthesizing an instance of Decidable p and then evaluating it to isTrue ... Unlike decide, this uses #eval to evaluate the decidability instance.

This should be used with care because it adds the entire lean compiler to the trusted part, and the axiom Lean.ofReduceBool will show up in #print axioms for theorems using this method or anything that transitively depends on them. Nevertheless, because it is compiled, this can be significantly more efficient than using decide, and for very large computations this is one way to run external programs and trust the result.

example : (List.range 1000).length = 1000 := by native_decide

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

nofun

The tactic nofun is shorthand for exact nofun: it introduces the assumptions, then performs an empty pattern match, closing the goal if the introduced pattern is impossible.

Tags:
Defined in module:: Init.Tactics

nomatch

The tactic nomatch h is shorthand for exact nomatch h.

Tags:
Defined in module:: Init.Tactics

norm_cast

The norm_cast family of tactics is used to normalize certain coercions (casts) in expressions.

norm_cast normalizes casts in the target.
norm_cast at h normalizes casts in hypothesis h.

The tactic is basically a version of simp with a specific set of lemmas to move casts upwards in the expression. Therefore even in situations where non-terminal simp calls are discouraged (because of fragility), norm_cast is considered to be safe. It also has special handling of numerals.

For instance, given an assumption

a b : ℤ
h : ↑a + ↑b < (10 : ℚ)

writing norm_cast at h will turn h into

h : a + b < 10

There are also variants of basic tactics that use norm_cast to normalize expressions during their operation, to make them more flexible about the expressions they accept (we say that it is a tactic modulo the effects of norm_cast):

exact_mod_cast for exact and apply_mod_cast for apply. Writing exact_mod_cast h and apply_mod_cast h will normalize casts in the goal and h before using exact h or apply h.
rw_mod_cast for rw. It applies norm_cast between rewrites.
assumption_mod_cast for assumption. This is effectively norm_cast at *; assumption, but more efficient. It normalizes casts in the goal and, for every hypothesis h in the context, it will try to normalize casts in h and use exact h.

See also push_cast, which moves casts inwards rather than lifting them outwards.

Tags:
Defined in module:: Init.Tactics

norm_cast0

Implementation of norm_cast (the full norm_cast calls trivial afterwards).

Tags:
Defined in module:: Init.Tactics

obtain

The obtain tactic is a combination of have and rcases. See rcases for a description of supported patterns.

obtain ⟨patt⟩ : type := proof

is equivalent to

have h : type := proof
rcases h with ⟨patt⟩

If ⟨patt⟩ is omitted, rcases will try to infer the pattern.

If type is omitted, := proof is required.

Tags:
Defined in module:: Init.RCases

omega

The omega tactic, for resolving integer and natural linear arithmetic problems.

It is not yet a full decision procedure (no "dark" or "grey" shadows), but should be effective on many problems.

We handle hypotheses of the form x = y, x < y, x ≤ y, and k ∣ x for x y in Nat or Int (and k a literal), along with negations of these statements.

We decompose the sides of the inequalities as linear combinations of atoms.

If we encounter x / k or x % k for literal integers k we introduce new auxiliary variables and the relevant inequalities.

On the first pass, we do not perform case splits on natural subtraction. If omega fails, we recursively perform a case split on a natural subtraction appearing in a hypothesis, and try again.

The options

omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax

can be used to:

splitDisjunctions: split any disjunctions found in the context, if the problem is not otherwise solvable.
splitNatSub: for each appearance of ((a - b : Nat) : Int), split on a ≤ b if necessary.
splitNatAbs: for each appearance of Int.natAbs a, split on 0 ≤ a if necessary.
splitMinMax: for each occurrence of min a b, split on min a b = a ∨ min a b = b Currently, all of these are on by default.

Tags:
Defined in module:: Init.Tactics

open

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

Tags:
Defined in module:: Lean.Parser.Command

push_cast

push_cast rewrites the goal to move certain coercions (casts) inward, toward the leaf nodes. This uses norm_cast lemmas in the forward direction. For example, ↑(a + b) will be written to ↑a + ↑b.

push_cast moves casts inward in the goal.
push_cast at h moves casts inward in the hypothesis h. It can be used with extra simp lemmas with, for example, push_cast [Int.add_zero].

Example:

example (a b : Nat)
    (h1 : ((a + b : Nat) : Int) = 10)
    (h2 : ((a + b + 0 : Nat) : Int) = 10) :
    ((a + b : Nat) : Int) = 10 := by
  /-
  h1 : ↑(a + b) = 10
  h2 : ↑(a + b + 0) = 10
  ⊢ ↑(a + b) = 10
  -/
  push_cast
  /- Now
  ⊢ ↑a + ↑b = 10
  -/
  push_cast at h1
  push_cast [Int.add_zero] at h2
  /- Now
  h1 h2 : ↑a + ↑b = 10
  -/
  exact h1

rcases

rcases is a tactic that will perform cases recursively, according to a pattern. It is used to destructure hypotheses or expressions composed of inductive types like h1 : a ∧ b ∧ c ∨ d or h2 : ∃ x y, trans_rel R x y. Usual usage might be rcases h1 with ⟨ha, hb, hc⟩ | hd or rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩ for these examples.

Each element of an rcases pattern is matched against a particular local hypothesis (most of which are generated during the execution of rcases and represent individual elements destructured from the input expression). An rcases pattern has the following grammar:

A name like x, which names the active hypothesis as x.
A blank _, which does nothing (letting the automatic naming system used by cases name the hypothesis).
A hyphen -, which clears the active hypothesis and any dependents.
The keyword rfl, which expects the hypothesis to be h : a = b, and calls subst on the hypothesis (which has the effect of replacing b with a everywhere or vice versa).
A type ascription p : ty, which sets the type of the hypothesis to ty and then matches it against p. (Of course, ty must unify with the actual type of h for this to work.)
A tuple pattern ⟨p1, p2, p3⟩, which matches a constructor with many arguments, or a series of nested conjunctions or existentials. For example if the active hypothesis is a ∧ b ∧ c, then the conjunction will be destructured, and p1 will be matched against a, p2 against b and so on.
A @ before a tuple pattern as in @⟨p1, p2, p3⟩ will bind all arguments in the constructor, while leaving the @ off will only use the patterns on the explicit arguments.
An alternation pattern p1 | p2 | p3, which matches an inductive type with multiple constructors, or a nested disjunction like a ∨ b ∨ c.

A pattern like ⟨a, b, c⟩ | ⟨d, e⟩ will do a split over the inductive datatype, naming the first three parameters of the first constructor as a,b,c and the first two of the second constructor d,e. If the list is not as long as the number of arguments to the constructor or the number of constructors, the remaining variables will be automatically named. If there are nested brackets such as ⟨⟨a⟩, b | c⟩ | d then these will cause more case splits as necessary. If there are too many arguments, such as ⟨a, b, c⟩ for splitting on ∃ x, ∃ y, p x, then it will be treated as ⟨a, ⟨b, c⟩⟩, splitting the last parameter as necessary.

rcases also has special support for quotient types: quotient induction into Prop works like matching on the constructor quot.mk.

rcases h : e with PAT will do the same as rcases e with PAT with the exception that an assumption h : e = PAT will be added to the context.

Tags:
Defined in module:: Init.RCases

refine

refine e behaves like exact e, except that named (?x) or unnamed (?_) holes in e that are not solved by unification with the main goal's target type are converted into new goals, using the hole's name, if any, as the goal case name.

Tags:
Defined in module:: Init.Tactics

refine'

refine' e behaves like refine e, except that unsolved placeholders (_) and implicit parameters are also converted into new goals.

Tags:
Defined in module:: Init.Tactics

refine_lift

Auxiliary macro for lifting have/suffices/let/... It makes sure the "continuation" ?_ is the main goal after refining.

Tags:
Defined in module:: Init.Tactics

refine_lift'

Similar to refine_lift, but using refine'

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

rename_i

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

Tags:
Defined in module:: Init.Tactics

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.

repeat'

repeat' tac recursively applies tac on all of the goals so long as it succeeds. That is to say, if tac produces multiple subgoals, then repeat' tac is applied to each of them.

repeat1'

repeat1' tac recursively applies to tac on all of the goals so long as it succeeds, but repeat1' tac fails if tac succeeds on none of the initial goals.

replace

Acts like have, but removes a hypothesis with the same name as this one if possible. For example, if the state is:

f : α → β
h : α
⊢ goal

Then after replace h := f h the state will be:

f : α → β
h : β
⊢ goal

whereas have h := f h would result in:

f : α → β
h† : α
h : β
⊢ goal

This can be used to simulate the specialize and apply at tactics of Coq.

Tags:
Defined in module:: Init.Tactics

revert

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

Tags:
Defined in module:: Init.Tactics

rewrite

rewrite [e] applies identity e as a rewrite rule to the target of the main goal. If e is preceded by left arrow (← or <-), the rewrite is applied in the reverse direction. If e is a defined constant, then the equational theorems associated with e are used. This provides a convenient way to unfold e.

rewrite [e₁, ..., eₙ] applies the given rules sequentially.
rewrite [e] at l rewrites e at location(s) l, where l is either * or a list of hypotheses in the local context. In the latter case, a turnstile ⊢ or |- can also be used, to signify the target of the goal.

Using rw (occs := .pos L) [e], where L : List Nat, you can control which "occurrences" are rewritten. (This option applies to each rule, so usually this will only be used with a single rule.) Occurrences count from 1. At each allowed occurrence, arguments of the rewrite rule e may be instantiated, restricting which later rewrites can be found. (Disallowed occurrences do not result in instantiation.) (occs := .neg L) allows skipping specified occurrences.

Tags:
Defined in module:: Init.Tactics

rfl

This tactic applies to a goal whose target has the form x ~ x, where ~ is equality, heterogeneous equality or any relation that has a reflexivity lemma tagged with the attribute @[refl].

Tags:
Defined in module:: Init.Tactics

rfl'

rfl' is similar to rfl, but disables smart unfolding and unfolds all kinds of definitions, theorems included (relevant for declarations defined by well-founded recursion).

Tags:
Defined in module:: Init.Tactics

right

Applies the second constructor when the goal is an inductive type with exactly two constructors, or fails otherwise.

example {p q : Prop} (h : q) : p ∨ q := by
  right
  exact h

Tags:
Defined in module:: Init.Tactics

rintro

The rintro tactic is a combination of the intros tactic with rcases to allow for destructuring patterns while introducing variables. See rcases for a description of supported patterns. For example, rintro (a | ⟨b, c⟩) ⟨d, e⟩ will introduce two variables, and then do case splits on both of them producing two subgoals, one with variables a d e and the other with b c d e.

rintro, unlike rcases, also supports the form (x y : ty) for introducing and type-ascripting multiple variables at once, similar to binders.

Tags:
Defined in module:: Init.RCases

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.

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

run_tac

The run_tac doSeq tactic executes code in TacticM Unit.

Tags:
Defined in module:: Init.Tactics

rw

rw is like rewrite, but also tries to close the goal by "cheap" (reducible) rfl afterwards.

Tags:
Defined in module:: Init.Tactics

rw?

rw? tries to find a lemma which can rewrite the goal.

rw? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as rw [h] or rw [← h].

You can use rw? [-my_lemma, -my_theorem] to prevent rw? using the named lemmas.

Tags:
Defined in module:: Init.Tactics

rw_mod_cast

Rewrites with the given rules, normalizing casts prior to each step.

Tags:
Defined in module:: Init.TacticsExtra

rwa

rwa is short-hand for rw; assumption.

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Lean.Parser.Command

show

show t finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.

Tags:
Defined in module:: Init.Tactics

show_term

show_term tac runs tac, then prints the generated term in the form "exact X Y Z" or "refine X ?_ Z" (prefixed by expose_names if necessary) if there are remaining subgoals.

(For some tactics, the printed term will not be human readable.)

Tags:
Defined in module:: Init.Tactics

simp

The simp tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses. It has many variants:

simp simplifies the main goal target using lemmas tagged with the attribute [simp].
simp [h₁, h₂, ..., hₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp] and the given hᵢ's, where the hᵢ's are expressions.-
If an hᵢ is a defined constant f, then f is unfolded. If f has equational lemmas associated with it (and is not a projection or a reducible definition), these are used to rewrite with f.
simp [*] simplifies the main goal target using the lemmas tagged with the attribute [simp] and all hypotheses.
simp only [h₁, h₂, ..., hₙ] is like simp [h₁, h₂, ..., hₙ] but does not use [simp] lemmas.
simp [-id₁, ..., -idₙ] simplifies the main goal target using the lemmas tagged with the attribute [simp], but removes the ones named idᵢ.
simp at h₁ h₂ ... hₙ simplifies the hypotheses h₁ : T₁ ... hₙ : Tₙ. If the target or another hypothesis depends on hᵢ, a new simplified hypothesis hᵢ is introduced, but the old one remains in the local context.
simp at * simplifies all the hypotheses and the target.
simp [*] at * simplifies target and all (propositional) hypotheses using the other hypotheses.

Tags:
Defined in module:: Init.Tactics

simp!

simp! is shorthand for simp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

Tags:
Defined in module:: Init.Meta

simp?

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

simp?!

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

simp_all

simp_all is a stronger version of simp [*] at * where the hypotheses and target are simplified multiple times until no simplification is applicable. Only non-dependent propositional hypotheses are considered.

Tags:
Defined in module:: Init.Tactics

simp_all!

simp_all! is shorthand for simp_all with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

Tags:
Defined in module:: Init.Meta

simp_all?

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

simp_all?!

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"

This command can also be used in simp_all and dsimp.

Tags:
Defined in module:: Init.Tactics

simp_all_arith

simp_all_arith has been deprecated. It was a shorthand for simp_all +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

Tags:
Defined in module:: Init.Meta

simp_all_arith!

simp_all_arith! has been deprecated. It was a shorthand for simp_all! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

Tags:
Defined in module:: Init.Meta

simp_arith

simp_arith has been deprecated. It was a shorthand for simp +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

Tags:
Defined in module:: Init.Meta

simp_arith!

simp_arith! has been deprecated. It was a shorthand for simp! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

Tags:
Defined in module:: Init.Meta

simp_wf

Unfold definitions commonly used in well founded relation definitions.

Since Lean 4.12, Lean unfolds these definitions automatically before presenting the goal to the user, and this tactic should no longer be necessary. Calls to simp_wf can be removed or replaced by plain calls to simp.

Tags:
Defined in module:: Init.WFTactics

simpa

This is a "finishing" tactic modification of simp. It has two forms.

simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

Tags:
Defined in module:: Init.Tactics

simpa!

This is a "finishing" tactic modification of simp. It has two forms.

simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

Tags:
Defined in module:: Init.Tactics

simpa?

This is a "finishing" tactic modification of simp. It has two forms.

simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

Tags:
Defined in module:: Init.Tactics

simpa?!

This is a "finishing" tactic modification of simp. It has two forms.

simpa [rules, ⋯] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

simpa [rules, ⋯] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

Tags:
Defined in module:: Init.Tactics

sizeOf_list_dec

This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions over a nested inductive like inductive T | mk : List T → T.

Tags:
Defined in module:: Init.Data.List.BasicAux

skip

skip does nothing.

Tags:
Defined in module:: Init.Tactics

sleep

The tactic sleep ms sleeps for ms milliseconds and does nothing. It is used for debugging purposes only.

Tags:
Defined in module:: Init.Tactics

solve

Similar to first, but succeeds only if one the given tactics solves the current goal.

Tags:
Defined in module:: Init.NotationExtra

solve_by_elim

solve_by_elim calls apply on the main goal to find an assumption whose head matches and then repeatedly calls apply on the generated subgoals until no subgoals remain, performing at most maxDepth (defaults to 6) recursive steps.

solve_by_elim discharges the current goal or fails.

solve_by_elim performs backtracking if subgoals can not be solved.

By default, the assumptions passed to apply are the local context, rfl, trivial, congrFun and congrArg.

The assumptions can be modified with similar syntax as for simp:

solve_by_elim [h₁, h₂, ..., hᵣ] also applies the given expressions.
solve_by_elim only [h₁, h₂, ..., hᵣ] does not include the local context, rfl, trivial, congrFun, or congrArg unless they are explicitly included.
solve_by_elim [-h₁, ... -hₙ] removes the given local hypotheses.
solve_by_elim using [a₁, ...] uses all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

solve_by_elim* tries to solve all goals together, using backtracking if a solution for one goal makes other goals impossible. (Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)

Optional arguments passed via a configuration argument as solve_by_elim (config := { ... })

maxDepth: number of attempts at discharging generated subgoals
symm: adds all hypotheses derived by symm (defaults to true).
exfalso: allow calling exfalso and trying again if solve_by_elim fails (defaults to true).
transparency: change the transparency mode when calling apply. Defaults to .default, but it is often useful to change to .reducible, so semireducible definitions will not be unfolded when trying to apply a lemma.

See also the doc-comment for Lean.Meta.Tactic.Backtrack.BacktrackConfig for the options proc, suspend, and discharge which allow further customization of solve_by_elim. Both apply_assumption and apply_rules are implemented via these hooks.

Tags:
Defined in module:: Init.Tactics

sorry

The sorry tactic is a temporary placeholder for an incomplete tactic proof, closing the main goal using exact sorry.

This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton. Lean will give a warning whenever a proof uses sorry, so you aren't likely to miss it, but you can double check if a theorem depends on sorry by looking for sorryAx in the output of the #print axioms my_thm command, the axiom used by the implementation of sorry.

Tags:
Defined in module:: Init.Tactics

specialize

The tactic specialize h a₁ ... aₙ works on local hypothesis h. The premises of this hypothesis, either universal quantifications or non-dependent implications, are instantiated by concrete terms coming from arguments a₁ ... aₙ. The tactic adds a new hypothesis with the same name h := h a₁ ... aₙ and tries to clear the previous one.

Tags:
Defined in module:: Init.Tactics

split

The split tactic is useful for breaking nested if-then-else and match expressions into separate cases. For a match expression with n cases, the split tactic generates at most n subgoals.

For example, given n : Nat, and a target if n = 0 then Q else R, split will generate one goal with hypothesis n = 0 and target Q, and a second goal with hypothesis ¬n = 0 and target R. Note that the introduced hypothesis is unnamed, and is commonly renamed using the case or next tactics.

split will split the goal (target).
split at h will split the hypothesis h.

Tags:
Defined in module:: Init.Tactics

stop

stop is a helper tactic for "discarding" the rest of a proof: it is defined as repeat sorry. It is useful when working on the middle of a complex proofs, and less messy than commenting the remainder of the proof.

Tags:
Defined in module:: Init.Tactics

subst

subst x... substitutes each hypothesis x with a definition found in the local context, then eliminates the hypothesis.

If x is a local definition, then its definition is used.
Otherwise, if there is a hypothesis of the form x = e or e = x, then e is used for the definition of x.

If h : a = b, then subst h may be used if either a or b unfolds to a local hypothesis. This is similar to the cases h tactic.

See also: subst_vars for substituting all local hypotheses that have a defining equation.

Tags:
Defined in module:: Init.Tactics

subst_eqs

subst_eq repeatedly substitutes according to the equality proof hypotheses in the context, replacing the left side of the equality with the right, until no more progress can be made.

Tags:
Defined in module:: Init.Tactics

subst_vars

Applies subst to all hypotheses of the form h : x = t or h : t = x.

Tags:
Defined in module:: Init.Tactics

suffices

Given a main goal ctx ⊢ t, suffices h : t' from e replaces the main goal with ctx ⊢ t', e must have type t in the context ctx, h : t'.

The variant suffices h : t' by tac is a shorthand for suffices h : t' from by tac. If h : is omitted, the name this is used.

Tags:
Defined in module:: Init.Tactics

suggestions

#suggestions will suggest relevant theorems from the library for the current goal, using the currently registered library suggestion engine.

The suggestions are printed in the order of their confidence, from highest to lowest.

Tags:
Defined in module:: Init.Tactics

symm

symm applies to a goal whose target has the form t ~ u where ~ is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute [symm]. It replaces the target with u ~ t.
symm at h will rewrite a hypothesis h : t ~ u to h : u ~ t.

Tags:
Defined in module:: Init.Tactics

symm_saturate

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Tags:
Defined in module:: Init.Tactics

trace

trace msg displays msg in the info view.

Tags:
Defined in module:: Init.Tactics

trace_state

trace_state displays the current state in the info view.

Tags:
Defined in module:: Init.Tactics

trivial

trivial tries different simple tactics (e.g., rfl, contradiction, ...) to close the current goal. You can use the command macro_rules to extend the set of tactics used. Example:

macro_rules | `(tactic| trivial) => `(tactic| simp)

Tags:
Defined in module:: Init.Tactics

try

try tac runs tac and succeeds even if tac failed.

Tags:
Defined in module:: Init.Tactics

try?

This tactic has no documentation.

Tags:
Defined in module:: Init.Try

try_suggestions

Helper internal tactic used to implement evalSuggest in try?

Tags:
Defined in module:: Init.Try

unfold

unfold id unfolds all occurrences of definition id in the target.
unfold id1 id2 ... is equivalent to unfold id1; unfold id2; ....
unfold id at h unfolds at the hypothesis h.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to delta. For recursive global definitions, it uses the "unfolding lemma" id.eq_def, which is generated for each recursive definition, to unfold according to the recursive definition given by the user. Only one level of unfolding is performed, in contrast to simp only [id], which unfolds definition id recursively.

Tags:
Defined in module:: Init.Tactics

unhygienic

unhygienic tacs runs tacs with name hygiene disabled. This means that tactics that would normally create inaccessible names will instead make regular variables. Warning: Tactics may change their variable naming strategies at any time, so code that depends on autogenerated names is brittle. Users should try not to use unhygienic if possible.

example : ∀ x : Nat, x = x := by unhygienic
  intro            -- x would normally be intro'd as inaccessible
  exact Eq.refl x  -- refer to x

Tags:
Defined in module:: Init.Tactics

wait_for_unblock_async

Spawns a logSnapshotTask that waits for unblock to be called, which is expected to happen in a subsequent document version that does not invalidate this tactic. Complains if cancellation token was set before unblocking, i.e. if the tactic was invalidated after all.

Tags:
Defined in module:: Lean.Server.Test.Cancel

with_reducible

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

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

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.

Tags:
Defined in module:: Init.Tactics

with_unfolding_none

with_unfolding_none tacs executes tacs using the .none transparency setting. In this setting no definitions are unfolded.

Tags:
Defined in module:: Init.Tactics

∎

∎ (typed as \qed) is a macro that expands to try? in tactic mode.

Tags:
Defined in module:: Init.Try