simp taking a long time on a small definition

Stream: lean4

[Son Ho]

In the following example, simp takes a very long time to finish, which is proportional to the number I put in the bound for the for ...:

import Lean

def f (n : Nat) : Nat := Id.run do
  let mut n := n
  let mut i := 1 -- We need to have two mutable variables
  for _ in [0:256] do -- We need the upper bound to be high
    i := i + 1
    n := n
  pure n

example : f 0 = 0 := by
  simp only [f] -- takes seconds to finish

Does someone have an idea about what is going on? In the case above it only takes a few seconds, but I have a development for which this issue makes one of my definitions completely unusable.

Note that I tried introducing an intermediate, irreducible definition for the upper bound, but it has no effect:

import Lean

@[irreducible]
def LEN: Nat := 256

def f (n : Nat) : Nat := Id.run do
  let mut n := n
  let mut i := 1 -- We need to have two mutable variables
  for _ in [0:LEN] do -- We need the upper bound to be high
    i := i + 1
    n := n
  pure n

example : f 0 = 0 := by
  simp only [f] -- takes seconds to finish

[Aaron Liu]

The problem is not the simp, which is very fast, but the kernel typechecking the definition, and the kernel ignores transparency. I couldn't find any good kernel trace options, but the problem might be the for-loop, since the implementation for for-loops was defined using well-founded recursion.

[Son Ho]

Thanks! What is the problem with using well-founded recursion ? Is it that the kernel doesn't have a simple criteria to use to stop unfolding recursive definitions ?

[Aaron Liu]

Aaron Liu said:

I think David Renshaw has a good video explaining the problem with reduction of well-founded recursion.
Basically, when you use well founded recursion on Nat to go from n₁ down to n₂, this takes time proportional to n₂ * (n₁ - n₂) to reduce, and this happens again when you go from n₂ to n₃, and n₃ to n₄, and this ends up taking a very long time, which is why you can time out trying to reduce terms such as Nat.log2 1000.

In this case, probably something is causing the kernel to think that unfolding the for loop is a good idea, and it gets stuck trying that for a long time.

[Son Ho]

Thanks! This is extremely useful. But from that I don't see any good workaround put aside completely reworking my definition...

[Son Ho]

I managed to get away by introducing an alternative definition for Std.Range so that I could write my own instance of ForIn', which is equivalent to the instance of Std.Range but under the hood uses a fuel parameter (it's easy to find an upper bound on the fuel). This and an appropriate notation for [x:y] allowed me to circumvent the issue.

[Son Ho]

I essentially copy-pasted this to add a fuel:
https://github.com/leanprover/lean4/blob/b6db90a31601866d58a07e86aba3720991aa73c8/src/Init/Data/Range/Basic.lean#L28