Core tactic documentation #
This file adds the majority of the interactive tactics from core Lean (i.e. premathlib) to the API documentation.
TODO #

Make a PR to core changing core docstrings to the docstrings below, and also changing the docstrings of
cc
,simp
andconv
to the ones already in the API docs. 
SMT tactics are currently not documented.

rsimp
andconstructor_matching
are currently not documented. 
dsimp
deserves better documentation.
Proves a goal of the form s = t
when s
and t
are expressions built up out of a binary
operation, and equality can be proved using associativity and commutativity of that operation.
all_goals { t }
applies the tactic t
to every goal, and succeeds if each application succeeds.
any_goals { t }
applies the tactic t
to every goal, and succeeds if at least one application succeeds.
The apply
tactic tries to match the current goal against the conclusion of the type of term. The argument term should be a term wellformed in the local context of the main goal. 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. Nondependent premises are added before dependent ones.
The apply
tactic uses higherorder pattern matching, type class resolution, and firstorder unification with dependent types.
If the target of the main goal is an auto_param
, executes the associated tactic.
This tactic tries to close the main goal ... ⊢ t
by generating a term of type t
using type class resolution.
If the target of the main goal is an opt_param
, assigns the default value.
Similar to the apply
tactic, but allows the user to provide a apply_cfg
configuration object.
Assuming the target of the goal is a Pi or a let, assume h : t
unifies the type of the binder with t
and introduces it with name h
, just like intro h
. If h
is absent, the tactic uses the name this
. If t
is omitted, it will be inferred.
assume (h₁ : t₁) ... (hₙ : tₙ)
introduces multiple hypotheses. Any of the types may be omitted, but the names must be present.
This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails.
Proves the first goal asynchronously as a separate lemma.
by_cases p
splits the main goal into two cases, assuming h : p
in the first branch, and
h : ¬ p
in the second branch. You can specify the name of the new hypothesis using the syntax
by_cases h : p
.
If p
is not already decidable, by_cases
will use the instance classical.prop_decidable p
.
If the target of the main goal is a proposition p
, by_contra h
reduces the goal to proving
false
using the additional hypothesis h : ¬ p
. If h
is omitted, a name is generated
automatically.
This tactic requires that p
is decidable. To ensure that all propositions are decidable via
classical reasoning, use open_locale classical
(or local attribute [instance, priority 10] classical.prop_decidable
if you are not using
mathlib).
Focuses on a goal ('case') generated by induction
, cases
or with_cases
.
The goal is selected by giving one or more names which must match exactly one goal. A goal is matched if the given names are a suffix of its goal tag. Additionally, each name in the sequence can be abbreviated to a suffix of the corresponding name in the goal tag. Thus, a goal with tag
can be selected with any of these invocations (among others):
Additionally, the form
case C : N₀ ... Nₙ {...}
can be used to rename hypotheses introduced by the preceding
cases
/induction
/with_cases
, using the names Nᵢ
. For example:
example (xs : list ℕ) : xs = xs :=
begin
induction xs,
case nil { reflexivity },
case cons : x xs ih {
 x : ℕ, xs : list ℕ, ih : xs = xs
reflexivity }
end
Note that this renaming functionality only work reliably directly after an
induction
/cases
/with_cases
. If you need to perform additional work after
an induction
or cases
(e.g. introduce hypotheses in all goals), use
with_cases
.
Multiple cases can be handled by the same tactic block with
case [A : N₀ ... Nₙ, B : M₀ ... Mₙ] {...}
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.
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.
cases e
, where e
is an expression instead of a variable, generalizes e
in the goal, and then cases on the resulting variable.
cases e with y₁ ... yₙ
, where e
is a variable or an expression, specifies that the sequence of names y₁ ... yₙ
should be used for the arguments to the constructors, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically.
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 hypothesis, where ...
is the constructor instance for that particular case.
cases_matching p
applies the cases
tactic to a hypothesis h : type
if type
matches the pattern p
.
cases_matching [p_1, ..., p_n]
applies the cases
tactic to a hypothesis h : type
if type
matches one of the given patterns.
cases_matching* p
is a more efficient and compact version
of focus1 { repeat { cases_matching p } }
.
It is more efficient because the pattern is compiled once.
casesm
is shorthand for cases_matching
.
Example: The following tactic destructs all conjunctions and disjunctions in the current context.
cases_matching* [_ ∨ _, _ ∧ _]
cases_type I
applies thecases
tactic to a hypothesish : (I ...)
cases_type I_1 ... I_n
applies thecases
tactic to a hypothesish : (I_1 ...)
or ... orh : (I_n ...)
cases_type* I
is shorthand forfocus1 { repeat { cases_type I } }
cases_type! I
only appliescases
if the number of resulting subgoals is <= 1.
Example: The following tactic destructs all conjunctions and disjunctions in the current context.
change u
replaces the target t
of the main goal to u
provided that t
is well formed with respect to the local context of the main goal and t
and u
are definitionally equal.
change u at h
will change a local hypothesis to u
.
change t with u at h1 h2 ...
will replace t
with u
in all the supplied hypotheses (or *
), or in the goal if no at
clause is specified, provided that t
and u
are definitionally equal.
clear h₁ ... hₙ
tries to clear each hypothesis hᵢ
from the local context.
Close goals of the form n ≠ m
when n
and m
have type nat
, char
, string
, int
or fin sz
, and they are literals. It also closes goals of the form n < m
, n > m
, n ≤ m
and
n ≥ m
for nat
. If the goal is of the form n = m
, then it tries to close it using reflexivity.
In mathlib, consider using norm_num
instead for numeric types.
The congr
tactic attempts to identify both sides of an equality goal A = B
,
leaving as new goals the subterms of A
and B
which are not definitionally equal.
Example: suppose the goal is x * f y = g w * f z
. Then congr
will produce two goals:
x = g w
and y = z
.
If x y : t
, and an instance subsingleton t
is in scope, then any goals of the form
x = y
are solved automatically.
Note that congr
can be overaggressive at times; the congr'
tactic in mathlib
provides a more refined approach, by taking a parameter that limits the recursion depth.
This tactic applies to a goal such that its conclusion is an inductive type (say I
). It tries to apply each constructor of I
until it succeeds.
The contradiction tactic attempts to find in the current local context a hypothesis that is equivalent to an empty inductive type (e.g. false
), a hypothesis of the form c_1 ... = c_2 ...
where c_1
and c_2
are distinct constructors, or two contradictory hypotheses.
Similar to dunfold
, but performs a raw delta reduction, rather than using an equation associated with the defined constants.
Assuming x
is a variable in the local context with an inductive type, destruct x
splits the main goal, producing one goal for each constructor of the inductive type, in which x
is assumed to be a general instance of that constructor. In contrast to cases
, the local context is unchanged, i.e. no elements are reverted or introduced.
For example, given n : nat
and a goal with a hypothesis h : P n
and target Q n
, destruct n
produces one goal with target n = 0 → Q n
, and one goal with target ∀ (a : ℕ), (λ (w : ℕ), n = w → Q n) (nat.succ a)
. Here the name a
is chosen automatically.
dsimp
is similar to simp
, except that it only uses definitional equalities.
Similar to unfold
, but only uses definitional equalities.
Similar to the apply
tactic, but only creates subgoals for nondependent premises that have not been fixed by type inference or type class resolution.
Similar to constructor
, but only nondependent premises are added as new goals.
A variant of rw
that uses the unifier more aggressively, unfolding semireducible definitions.
This tactic provides an exact proof term to solve the main goal. If t
is the goal and p
is a term of type u
then exact p
succeeds if and only if t
and u
can be unified.
Like exact
, but takes a list of terms and checks that all goals are discharged after the tactic.
Replaces the target of the main goal by false
.
existsi e
will instantiate an existential quantifier in the target with e
and leave the
instantiated body as the new target. More generally, it applies to any inductive type with one
constructor and at least two arguments, applying the constructor with e
as the first argument
and leaving the remaining arguments as goals.
existsi [e₁, ..., eₙ]
iteratively does the same for each expression in the list.
Note: in mathlib, the use
tactic is an equivalent tactic which sometimes is smarter with
unification.
Similar to the apply
tactic, but does not reorder goals.
focus { t }
temporarily hides all goals other than the first, applies t
, and then restores the other goals. It fails if there are no goals.
A synonym for exact
that allows writing have/suffices/show ..., from ...
in tactic mode.
Apply function extensionality and introduce new hypotheses.
The tactic funext
will keep applying new 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.
Note also the mathlib tactic ext
, which applies as many extensionality lemmas as possible.
generalize : e = x
replaces all occurrences of e
in the target with a new hypothesis x
of the same type.
generalize h : e = x
in addition registers the hypothesis h : e = x
.
guard_hyp h : t
fails if the hypothesis h
does not have type t
.
We use this tactic for writing tests.
guard_target t
fails if the target of the main goal is not t
.
We use this tactic for writing tests.
have h : t := p
adds the hypothesis h : t
to the current goal if p
a term of type t
. If t
is omitted, it will be inferred.
have h : t
adds the hypothesis h : t
to the current goal and opens a new subgoal with target t
. The new subgoal becomes the main goal. If t
is omitted, it will be replaced by a fresh metavariable.
If h
is omitted, the name this
is used.
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₁
ire chosen automatically.
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 with y₁ ... yₙ
, where e
is a variable or an expression, specifies that the sequence of names y₁ ... yₙ
should be used for the arguments to the constructors and inductive hypotheses, including implicit arguments. If the list does not include enough names for all of the arguments, additional names are generated automatically. If too many names are given, the extra ones are ignored. Underscores can be used in the list, in which case the corresponding names are generated automatically. Note that for long sequences of names, the case
tactic provides a more convenient naming mechanism.
induction e using r
allows the user to specify the principle of induction that should be used. Here r
should be a theorem 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.
induction h : t
will introduce an equality of the form h : t = C x y
, asserting that the input term is equal to the current constructor case, to the context.
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.
injections with h₁ ... hₙ
iteratively applies injection
to hypotheses using the names h₁ ... hₙ
.
If the current goal is a Pi/forall ∀ x : t, u
(resp. let x := t in u
) then intro
puts
x : t
(resp. x := t
) in the local context. The new subgoal target is u
.
If the goal is an arrow t → u
, then it puts h : t
in the local context and the new goal
target is u
.
If the goal is neither a Pi/forall nor begins with a let binder, the tactic intro
applies the
tactic whnf
until an introduction can be applied or the goal is not head reducible. In the latter
case, the tactic fails.
The variant intro z
uses the identifier z
to name the new hypothesis.
The variant intros
will keep introducing new hypotheses until the goal target is not a Pi/forall
or let binder.
The variant intros h₁ ... hₙ
introduces n
new hypotheses using the given identifiers to name
them.
The tactic introv
allows the user to automatically introduce the variables of a theorem and explicitly name the hypotheses involved. The given names are used to name nondependent hypotheses.
Examples:
example : ∀ a b : nat, a = b → b = a :=
begin
introv h,
exact h.symm
end
The state after introv h
is
a b : ℕ,
h : a = b
⊢ b = a
example : ∀ a b : nat, a = b → ∀ c, b = c → a = c :=
begin
introv h₁ h₂,
exact h₁.trans h₂
end
The state after introv h₁ h₂
is
a b : ℕ,
h₁ : a = b,
c : ℕ,
h₂ : b = c
⊢ a = c
iterate { t }
repeatedly applies tactic t
until t
fails. iterate { t }
always succeeds.
iterate n { t }
applies t
n
times.
left
applies the first constructor when the type of the target is an inductive data type with
two constructors.
Similarly, right
applies the second constructor.
let h : t := p
adds the hypothesis h : t := p
to the current goal if p
a term of type t
.
If t
is omitted, it will be inferred.
let h : t
adds the hypothesis h : t := ?M
to the current goal and opens a new subgoal ?M : t
.
The new subgoal becomes the main goal. If t
is omitted, it will be replaced by a fresh
metavariable.
If h
is omitted, the name this
is used.
Note the related mathlib tactic set a := t with h
, which adds the hypothesis h : a = t
to
the local context and replaces t
with a
everywhere it can.
Similar to the apply
tactic, but uses matching instead of unification.
apply_match t
is equivalent to apply_with t {unify := ff}
match_target t
fails if target does not match pattern t
.
This tactic behaves like exact
, but with a big difference: the user can put underscores _
in the expression as placeholders for holes that need to be filled, and refine
will generate as many subgoals as there are holes.
Note that some holes may be implicit. The type of each hole must either be synthesized by the system or declared by an explicit type ascription like (_ : nat → Prop)
.
This tactic applies to a goal whose target has the form t ~ u
where ~
is a reflexive relation,
that is, a relation which has a reflexivity lemma tagged with the attribute [refl]
.
The tactic checks whether t
and u
are definitionally equal and then solves the goal.
Rename one or more local hypotheses. The renamings are given as follows:
rename x y  rename x to y
rename x → y  ditto
rename [x y, a b]  rename x to y and a to b
rename [x → y, a → b]  ditto
Note that if there are multiple hypotheses called x
in the context, then
rename x y
will rename all of them. If you want to rename only one, use
dedup
first.
repeat { t }
applies t
to each goal. If the application succeeds,
the tactic is applied recursively to all the generated subgoals until it eventually fails.
The recursion stops in a subgoal when the tactic has failed to make progress.
The tactic repeat { t }
never fails.
revert h₁ ... hₙ
applies to any goal with hypotheses h₁
... hₙ
. It moves the hypotheses and their dependencies to the target of the goal. This tactic is the inverse of intro
.
rw e
applies an equation or iff e
as a rewrite rule to 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 lemmas associated with e
are used. This provides a convenient
way to unfold e
.
rw [e₁, ..., eₙ]
applies the given rules sequentially.
rw 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.
rewrite
is synonymous with rw
.
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
.
simp_intros h₁ h₂ ... hₙ
is similar to intros h₁ h₂ ... hₙ
except that each hypothesis is simplified as it is introduced, and each introduced hypothesis is used to simplify later ones and the final target.
As with simp
, a list of simplification lemmas can be provided. The modifiers only
and with
behave as with simp
.
solve1 { t }
applies the tactic t
to the main goal and fails if it is not solved.
Closes the main goal using sorry
. Takes an optional ignored tactic block.
The ignored tactic block is useful for "commenting out" part of a proof during development:
begin
split,
sorry { expensive_tactic },
end
```
The tactic specialize h a₁ ... aₙ
works on local hypothesis h
. The premises of this hypothesis, either universal quantifications or nondependent implications, are instantiated by concrete terms coming either 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.
Applies the constructor when the type of the target is an inductive data type with one constructor.
Given hypothesis h : x = t
or h : t = x
, where x
is a local constant, subst h
substitutes x
by t
everywhere in the main goal and then clears h
.
Apply subst
to all hypotheses of the form h : x = t
or h : t = x
.
suffices h : t
is the same as have h : t, tactic.swap
. In other words, it adds the hypothesis h : t
to the current goal and opens a new subgoal with target t
.
This tactic 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
.
Just construct the simp set and trace it. Used for debugging.
This tactic displays the current state in the tracing buffer.
This tactic applies to a goal whose target has the form t ~ u
where ~
is a transitive relation, that is, a relation which has a transitivity lemma tagged with the attribute [trans]
.
transitivity s
replaces the goal with the two subgoals t ~ s
and s ~ u
. If s
is omitted, then a metavariable is used instead.
Tries to solve the current goal using a canonical proof of true
, or the reflexivity
tactic, or the contradiction
tactic.
try { t }
tries to apply tactic t
, but succeeds whether or not t
succeeds.
Type check the given expression, and trace its type.
Given defined constants e₁ ... eₙ
, unfold e₁ ... eₙ
iteratively unfolds all occurrences in the target of the main goal, using equational lemmas associated with the definitions.
As with simp
, the at
modifier can be used to specify locations for the unfolding.
Similar to unfold
, but does not iterate the unfolding.
This tactic unfolds all structure projections.
Apply t
to the main goal and revert any new hypothesis in the generated goals.
If t
is a supported tactic or chain of supported tactics (e.g. induction
,
cases
, apply
, constructor
), the generated goals are also tagged with case
tags. You can then use case
to focus such tagged goals.
Two typical uses of with_cases
:

Applying a custom eliminator:

Enabling the use of
case
after a chain of casesplitting tactics:
Navigate to the lefthandside of a relation.
A goal of  a = b
will turn into the goal  a
.
Navigate to the righthandside of a relation.
A goal of  a = b
will turn into the goal  b
.
Navigate into every argument of the current head function.
A target of  (a * b) * c
will turn into the two targets  a * b
and  c
.
Navigate into the contents of toplevel λ
binders.
A target of  λ a, a + b
will turn into the target  a + b
and introduce a
into the local
context.
If there are multiple binders, all of them will be entered, and if there are none, this tactic is a
noop.
Navigate into the first scope matching the expression.
For a target of  ∀ c, a + (b + c) = 1
, find (b + _) { ... }
will run the tactics within the
{}
with a target of  b + c
.
Navigate into the numbered scopes matching the expression.
For a target of  λ c, 10 * c + 20 * c + 30 * c
, for (_ * _) [1, 3] { ... }
will run the
tactics within the {}
with first a target of  10 * c
, then a target of  30 * c
.
End conversion of the current goal. This is often what is needed when muscle memory would type
sorry
.