Guide: Conversion mode tactic #
This is a curated guide to point you toward how conv
mode works and what tactics are available.
It is not meant to be comprehensive, but rather a "cheat sheet." See also the
conv
introduction.
Syntax #
The syntax for the conv
tactic is
"conv" ("at" ident)? ("in" ("(occs :=" ("*" <> num+) ")")? term)? "=>" convSeq
where convSeq
is any sequence of "conv
tactics", which are tactics specifically written
for conv
mode.
The in
clause is exactly the same as the arguments to the conv
tactic pattern
.
conv in ...pattArgs... =>
...
is short for
conv =>
pattern ...patArgs...
...
Note that conv in (occs := 1 2 3) pat => ...
starts with three goals (one for each occurrence),
but conv in (occs := *) pat => ...
starts with a single goal that converts in all occurrences
simultaneously.
Mathlib also provides conv_lhs
and conv_rhs
variants to immediately apply either the
lhs
or rhs
tactic.
What is conv
mode? #
conv
mode is essentially the normal tactic mode but with two differences.

Only "
conv
tactics" can appear in theconv
block. These are tactics with syntax in theconv
category. 
The goals are all of the form
⊢ lhs = ?rhs
with?rhs
a metavariable, but the goals are annotated in such a way that they display as lhs
.
Each conv
tactic is aware that the goal is of this form, and in addition to solving for the
goal like normal, they also solve for the ?rhs
metavariable in some controlled way.
For example, the rfl
tactic uses rfl
to solve the goal, which sets ?rhs := lhs
.
Other tactics, like congr
, partially solve for ?rhs
and create new goal metavariables
for each unsolvedfor hole.
Once all the tactics have had a chance to run, conv
mode itself uses rfl
to solve
any remaining goals (note that in conv
mode, every goal can be solved for by rfl
!), and
then it uses the resulting lhs = rhs
proof to rewrite the goal in the surrounding normal
tactic mode.
Conv tactics from Lean 4, Std4, and Mathlib4 #
Unless they're annotated with "Std4" or "Mathlib", the following tactics are defined in Lean 4 core.
Control #

done
checks that there are noconv
goals remaining. 
skip
does nothing. It can be used to be the single tactic in an otherwise emptyconv
block. It does not skip aconv
goal. 
rfl
skips/closes aconv
goal by usingrfl
. (Remember, the actual goal is⊢ lhs = ?rhs
, so this sets?rhs := lhs
and usesrfl
to provelhs = lhs
.) 
conv => convSeq
is a nestedconv
. It usesconv
to change the current goal without closing it. For example, this is how you can do aconv
targeted rewrite of the current expression and then applyconv
tactics to the result. 
all_goals convSeq
runs theconv
tactics on everyconv
goal, collecting all the produced subgoals (if any). 
any_goals convSeq
is likeall_goals
but succeeds if the tactic sequence succees for any of the goals. 
case tag => convSeq
focuses on a goal with a given tag, runs the tactic sequence, and then autocloses the focused goal withrfl
. Has the same syntax as thecase
tactic. 
case' tag => convSeq
is likecase
but does not autoclose the goal if the tactics do not close it. 
next => convSeq
andnext x1 ... xn => convSeq
are like thenext
tactic, but they autoclose the focused goal withrfl
. 
· convSeq
focuses on the current goal and autocloses it withrfl
. 
focus => convSeq
focuses on the current goal. It does not autoclose the goal, unlikenext
. 
{ convSeq }
is likenext
. 
first  convSeq1  convSeq2  ...
tries eachconv
sequence one at a time until one of them succeeds, or else fails. 
try convSeq
runs theconv
sequence and succeeds even if it fails. Same asfirst  convSeq  skip
. 
repeat convSeq
repeatedly runsconvSeq
until it fails. 
( convSeq )
is for grouping. Useful when usingconv
tactic combinators. 
conv1 <;> conv2
is for runningconv1
and runningconv2
on every goal produced byconv
. 
tactic => tacticSeq
converts the goal into⊢ lhs = ?rhs
form and applies the tactic sequence. The tactic does not have to solve the goal completely, and remaining goals are turned back intoconv
goals. (Internal: there's also atactic' => tacticSeq
that does not remove theconv
annotations from the goal before applying the tactic sequence.) 
discharge => tacticSeq
takes a goal p
withp
a proposition, uses the tactic sequence to prove⊢ p
, and then closes the goal to convertp
toTrue
. (Mathlib) 
with_reducible convSeq
changes the transparency settings toreducible
while evaluating theconv
sequence. (Mathlib)
Navigation #

congr
(synonym:args
) creates subgoals for every immediate subexpression of the expression. You can userfl
to skip any of these subgoals. 
lhs
(synonym:left
) traverses into the secondtolast argument of the expression. (Implemented usingcongr
.) 
rhs
(synonym:right
) traverses into the last argument of the expression. (Implemented usingcongr
.) 
arg i
(andarg @i
) traverses into thei
th explicit argument (resp. thei
th argument) of the expression. (Implemented usingcongr
.) 
ext
(synonym:intro
) traverses into lambda, forall, andlet
expressions.ext x
gives the resulting binder the namex
.ext x y z ...
appliesext
once for each provided binder. 
enter [...]
is a compact way to describe a path to a subterm.enter [i]
(wherei
is a natural number) is equivalent toarg i
.enter [@i]
is equivalent toarg @i
.enter [x]
(wherex
is an identifier) is equivalent toext x
.enter [a,b,c,...]
isenter [a]; enter [b]; enter [c]; enter [...]
.

pattern
is for navigating into subexpressions that match a given patternpattern pat
traverses to the first subterm of the target that matchespat
.pattern (occs := *) pat
traverses to every subterm of the target that matchespat
which is not contained in another match ofpat
. It generates one subgoal.pattern (occs := 1 2 4) pat
matches occurrences1, 2, 4
ofpat
and produces three subgoals. Occurrences are numbered left to right from the outside in.
Manipulation #

change t
changes the expression tot
if the expression andt
are definitionally equal. 
equals t => tacticSeq
changes the current expression, saye
, tot
, and asks you to prove the equalitye = t
. (Std4) 
rw [thms...]
rewrites the expression using the given theorems. The syntax is similar torw
. 
erw [thms...]
rewrites the expression using the given theorems. The syntax is similar toerw
. 
simp [thms...]
appliessimp
to rewrite the expression. The syntax is similar tosimp
. 
dsimp [thms...]
appliesdsimp
to rewrite the expression. The syntax is similar todsimp
. 
simp_match
simplifiesmatch
expressions. 
apply e
appliese
to the goal (which remember is⊢ lhs = ?rhs
) using theapply
tactic. Strange results may occur if the hypotheses ofe
are not equalities. 
refine e
appliese
to the goal (which remember is⊢ lhs = ?rhs
) using therefine
tactic. Strange results may occur if the placeholders ine
are not equalities. 
exact e
closes the goal, wheree : lhs = ?rhs
. (Std4) 
Mathlib provides a number of tactics as
conv
tactics:abel
andabel_nf
ring
andring_nf
norm_cast
norm_num1
andnorm_num
push_neg

apply_congr
applies a relevant@[congr]
lemma, which can be better suited for a function than the congruence lemma that thecongr
tactic might generate. (Mathlib) 
slice i j
(for category theory) reassociates a composition of morphisms to focus on the composition of morphismsi
throughj
. (Mathlib)
Reductions #

whnf
reduces the expression to weakhead normal form. 
zeta
applies zeta reduction to the expression (i.e., substitutes alllet
expressions and expands all local variables). 
reduce
reduces the expression like the#reduce
command. (Documentation says "for debugging purposes only.") 
unfold id1 id2 ...
unfolds the definitions for the given constants using each definitions equational lemmas. For recursive definitions, only one layer of unfolding is performed. 
delta id1 id2 ...
applies delta reduction for the given constants (i.e., substitutes the values of each constant). It is primitive: it ignores definitional equations and uses the raw definition of each constant. Usingunfold
is preferred.
Debugging, for internal use, or otherwise technical #

trace_state
prints the current goal state (runs thetrace_state
tactic) 
fail_if_success convSeq
fails if theconv
sequence succeeds. 
guard_expr
andguard_target
for asserting that certain expressions are equal to others. (Std4) 
unreachable!
, which is the same as theunreachable!
tactic. (Std4) 
run_tac doSeq
evaluates a monadic value and runs it as a tactic usingtactic'
. (Mathlib)
Tactics and commands related to conv
#

conv_lhs ... => ...
andconv_rhs ... => ...
are likeconv
, but they immediately uselhs
orrhs
(respectively). (Mathlib) 
conv' ... => ...
is likeconv
but assumes the goal is already annotated as aconv
goal. Used internally to go back and forth between tactic mode and conv mode. 
#conv convTactic => e
is a command to apply theconvTactic
to the expressione
, yielding the converted expression (and dropping the generated proof). This is used to implement#simp
,#whnf
,#norm_num
, and#push_neg
. (Mathlib)