Zulip Chat Archive
Stream: lean4
Topic: Why can't reduce?
Vasilii Nesterov (Jul 11 2024 at 13:22):
Hi! Why can't Lean reduce f 5
in the example below? At the same time #reduce
works well.
def f (x : ℕ) : ℕ :=
if 10 < x then
0
else
f (x + 1)
termination_by (11 - x)
#reduce f 5 -- 0
example : f 5 = 0 := by
reduce -- the goal is still f 5 = 0
Vasilii Nesterov (Jul 11 2024 at 13:25):
rfl
can close this goal but I want to understand why reduce
doesn't work.
Kevin Buzzard (Jul 11 2024 at 13:37):
I know nothing about the reduce
tactic (indeed I didn't even know of its existence until now) but is this something to do with the fact that definitions are by default semireducible, which might mean that they won't reduce unless you unfold
them first? Apologies if I'm barking up the wrong tree.
Shreyas Srinivas (Jul 11 2024 at 13:38):
Here's the fix:
import Mathlib
abbrev f (x : ℕ) : ℕ :=
if 10 < x then
0
else
f (x + 1)
termination_by (11 - x)
#reduce f 5 -- 0
example : f 5 = 0 := by
reduce
Shreyas Srinivas (Jul 11 2024 at 13:39):
Also, please add all the relevant imports when you post your code.
Shreyas Srinivas (Jul 11 2024 at 13:39):
Kevin's diagnosis is correct. All I have done is change def
to abbrev
which is a neat way of saying "make this definition reducible".
Shreyas Srinivas (Jul 11 2024 at 13:42):
That being said, for larger proof developments, unless you are defining type synonyms, using reducible defs can be a performance issue. If you just want to forcibly normalise the term anyway you can use unfold f
as Kevin says, or even simp [f]
which will simplify the result of the unfolding.
Vasilii Nesterov (Jul 11 2024 at 13:44):
Thanks! But why it works with factorial then?
def factorial (x : ℕ) : ℕ :=
match x with
| .zero => 1
| .succ y => x * factorial y
example : factorial 3 = 6 := by
reduce -- the goal is 6 = 6
Edward van de Meent (Jul 11 2024 at 13:48):
my guess would be that it has to do with the fact that factorial
uses the inductive structure on Nat
...
Edward van de Meent (Jul 11 2024 at 13:49):
according to #print
, factorial
isn't marked as irreducible
?
Vasilii Nesterov (Jul 11 2024 at 13:52):
It is marked as reducible
.
Jannis Limperg (Jul 11 2024 at 13:55):
Definitions by well-founded recursion, such as f
, are marked as irreducible
by default. Shreyas' abbrev
overrides this and makes f
reducible
. This is a questionable fix, though, since some parts of Lean assume that reducible
definitions are always non-recursive. If you want to go this route, @[semireducible] def f
would be better. However, note that definitions by well-founded recursion sometimes have very bad reduction performance; that's why they're marked as irreducible
by default.
factorial
does not use well-founded recursion and therefore doesn't have this issue.
#reduce
uses kernel reduction, which ignores the irreducible
annotation. reduce
apparently uses a different reduction algorithm that respects the irreducible
annotation(?).
Vasilii Nesterov (Jul 11 2024 at 14:07):
Thank you all for your answers!
Kyle Miller (Jul 11 2024 at 17:13):
@Jannis Limperg #reduce
uses the elaborator's whnf (see docs#Lean.Meta.reduce). Mathlib's reduce
tactic uses the same reduce
function. It looks like the major difference is that #reduce
turns off smart unfolding.
Kyle Miller (Jul 11 2024 at 17:17):
Oh, that's a minor difference. The major difference is that #reduce
sets transparency to .all
.
example : f 5 = 0 := by
with_unfolding_all reduce
-- ⊢ 0 = 0
Kyle Miller (Jul 11 2024 at 17:18):
In a recent Lean you can use the unseal
command:
unseal f in
example : f 5 = 0 := by
reduce
-- ⊢ 0 = 0
I would suggest not using abbrev
.
Chris Henson (Jul 11 2024 at 19:42):
Not sure of the verbiage here, but is there a piece of documentation that describes the various "levels" of reducibility and transparency?
Kyle Miller (Jul 11 2024 at 19:44):
docs#Lean.Meta.TransparencyMode is one source
Kyle Miller (Jul 11 2024 at 19:44):
That's for configuring isDefEq/whnf. On the other side, there's annotating definitions with transparency levels.
Kyle Miller (Jul 11 2024 at 19:46):
I think instances
is slightly incorrect in the docs. It's that it will unfold projections of instances, not instances themselves (so for example functions from a class
will be unfolded)
Jannis Limperg (Jul 11 2024 at 20:14):
Kyle Miller said:
Jannis Limperg
#reduce
uses the elaborator's whnf (see docs#Lean.Meta.reduce). Mathlib'sreduce
tactic uses the samereduce
function. It looks like the major difference is that#reduce
turns off smart unfolding.
Ah! Thanks, and sorry for spreading misinformation.
Last updated: May 02 2025 at 03:31 UTC