Simp #
The simp
tactic works by applying a conditional term rewriting system to try and prove, or at
least simplify, your goal. What this basically means is that simp
is equipped with a list of
lemmas (those tagged with the simp
attribute), many of which are of the form X = Y
or X iff Y
,
and attempts to match subterms of the goal with the left hand side of a rule, and then replaces the
subterm with the right hand side. The system is conditional in the sense that lemmas are allowed to
have preconditions (P > (X = Y)
) and in these cases it will try and prove the precondition using
its simp lemmas before applying X = Y
.
You can watch simp
in action by using set_option trace.simplify true
in your code. For example
namespace hidden
definition cong (a b m : ℤ) : Prop := ∃ n : ℤ, b  a = m * n
notation a ` ≡ ` b ` mod ` m := cong a b m
set_option trace.simplify true
theorem cong_refl (m : ℤ) : ∀ a : ℤ, a ≡ a mod m :=
begin
intro a,
unfold cong,
existsi (0:ℤ),
simp
end
end hidden
If you do this exercise you will discover firstly that simp
spends a lot of its time trying random
lemmas and then giving up very shortly afterwards, and also that the unfold
command is also
underlined in green  Lean seems to apply simp
when you do an unfold
as well (apparently
unfold
just asks simp
to do its dirty work for it  unfold X
is close to simp only [X]
).
If you only want to see what worked rather than all the things that didn't, you could try
set_option trace.simplify.rewrite true
.
Simp lemmas #
In case you want to train simp
to use certain extra lemmas (for example because they're coming up
again and again in your work) you can add new lemmas for yourself. For example in mathlib in
algebra/ring.lean
we find the line
@[simp] theorem ne_zero (u : units α) : (u : α) ≠ 0
This lemma is then added to simp
's armoury. Note several things however.
 It might not be wise to make a random theorem into a simp lemma. Ideally the result has to be of
a certain kind, the most important kinds being those of the form
A=B
andA↔B
. Note however that if you want to addfact
tosimp
's weaponry, you can prove
@[simp] lemma my_lemma : fact ↔ true
(and in fact more recent versions of Lean do this automatically when you try to add random theorems to the simp dataset).
 If you are not careful you can add a bad simp lemma of the form
foo x y = [something mentioning foo]
and thensimp
will attempt to rewritefoo
and then end up with another one, and attempt to rewrite that, and so on. This can be fixed by usingrw
instead ofsimp
, or using the config option{single_pass := tt}
.
When it is unadvisable to use simp #
Using simp
in the middle of proofs is a simp
antipattern, which will produce brittle code. In
other words, don't use simp
in the middle of proofs. Use it to finish proofs. If you really need
to simplify a goal in the middle of a proof, then use simp
, but afterwards cut and paste the goal
into your code and write suffices : (simplified thing), by simpa using this
. This is really
important because the behaviour of simp
changes sometimes, and if you put simp
in the middle of
proofs then your code might randomly stop compiling and it will be hard to figure out why if you
didn't write down the exact thing which simp
used to be reducing your goal to. See also
squeeze_simp
.
How to use simp better #
Conversely, if you ever manage to close a goal with simp
, then take a look at the line before you
ran simp
. Could you have run simp one line earlier? How far back did simp start working? Even for
goals where you didn't use simp at all  could you have used simp
for your last line? What about
the lastbut one? And so on.
Recall that simp
lemmas are almost all of the form X = Y
or X ↔ Y
. Hence simp
might work
well for such goals. However what about goals of the form X → Y
? You could try assuming h : X
and then running either simpa using h
or simp {contextual := tt}
to see if Lean can deduce Y
.
Simp options #
The behaviour of simp
can be tweaked by simp
variants and also by passing options to the
algorithm. A good place to start is to look at the docstring for simp
(write simp
in VS Code and
hover your mouse over it to see the docstring). Here are some examples, some of which are covered by
the docstring and some of which are not.

simp only [H1, H2, H3]
uses only lemmasH1
,H2
, andH3
rather thansimp
s full collection of lemmas. Whyever might one want to do this in practice? Because sometimessimp
simplifies things too much  it might unfold things that you wanted to keep folded, for example. Another reason is that usingsimp only
can speed up slowsimp
calls significantly. 
simp [X]
stopssimp
from using lemmaX
. One could imagine using this as another solution when one findssimp
doing more than you would like. Recall from above thatset_option trace.simplify.rewrite true
shows you exactly which lemmassimp
is using. 
simp * at *
. This simplifies everything in sight. Use if life is getting complicated. 
simp {single_pass := tt}
 thissingle_pass
is a config option, one of around 16 at the time of writing. One can usesingle_pass
to avoid loops which would otherwise occur; for examplenat.gcd_def
is an equality withgcd
on both the left and right hand side, sosimp [nat.gcd_def]
is risky behaviour whereassimp [nat.gcd_def] {single_pass := tt}
is not. As you can imagine,simp only [h] {single_pass := tt}
here makes simp behave pretty much likerw h
. 
Search for
structure simp_config
in the fileinit/meta/simp_tactic.lean
in core Lean to see the full list of config options. Others, many undocumented, are:
(max_steps : nat := simp.default_max_steps)
(contextual : bool := ff)
(lift_eq : bool := tt)
(canonize_instances : bool := tt)
(canonize_proofs : bool := ff)
(use_axioms : bool := tt)
(zeta : bool := tt)
(beta : bool := tt)
(eta : bool := tt)
(proj : bool := tt)  reduce projections
(iota : bool := tt)
(iota_eqn : bool := ff)  reduce using all equation lemmas generated by equation/patternmatching compiler
(constructor_eq : bool := tt)
(single_pass : bool := ff)
(fail_if_unchanged := tt)
(memoize := tt)
We see from the changelog that setting constructor_eq
to true will reduce equations of the form
X a1 a2... = Y b1 b2...
to false if X
and Y
are distinct constructors for the same type, and
to a1 = b1 and a2 = b2 and...
if X = Y
are the same constructor. Another interesting example is
iota_eqn
: simp!
is shorthand for simp {iota_eqn := tt}
. This adds nontrivial equation lemmas
generated by the equation/patternmatching compiler to simp's weaponry. See the changelog for more
details.