Why can't reduce?

Stream: lean4

[Vasilii Nesterov]

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]

rfl can close this goal but I want to understand why reduce doesn't work.

[Kevin Buzzard]

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]

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]

Also, please add all the relevant imports when you post your code.

[Shreyas Srinivas]

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]

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]

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]

my guess would be that it has to do with the fact that factorial uses the inductive structure on Nat...

[Edward van de Meent]

according to #print, factorial isn't marked as irreducible?

[Vasilii Nesterov]

It is marked as reducible.

[Jannis Limperg]

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]

Thank you all for your answers!

[Kyle Miller]

@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]

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]

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]

Not sure of the verbiage here, but is there a piece of documentation that describes the various "levels" of reducibility and transparency?

[Kyle Miller]

docs#Lean.Meta.TransparencyMode is one source

[Kyle Miller]

That's for configuring isDefEq/whnf. On the other side, there's annotating definitions with transparency levels.

[Kyle Miller]

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]

Kyle Miller said:

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.

Ah! Thanks, and sorry for spreading misinformation.