grind stack overflow

Stream: lean4

[Julian Berman]

theorem foo
  (f : Nat → Nat → Nat)
  (g : Nat → Nat)
  (h₂ : ∀ x y, f x y = f x (f x y))
  (h₃ : g 0 = 0)
  (h₄ : ∀ n, g (n + 1) = 2^(g n)) :
  f 0 0 = g 0 - 1 := by
grind

produces a Stack overflow detected. Aborting. on both 4.24.0-rc1 and lean4 master. The stack trace seems to suggest it's some interaction between lean_nat_big_sub and Int.pow -- besides confirming this isn't a known issue I'm curious to learn how to diagnose further.

(CC @Leo who found the example.)

[Mac Malone]

@Paul Reichert, This seems like it could be a similar issue to your instance of lean4#5935.

[Paul Reichert]

Interesting! I was suspecting that my issue was related to BitVec arithmetic in kernel and elaborator, so I'm surprised that there is also an example the only uses Nat.

[Aaron Liu]

Julian Berman said:

and Int.pow

Could it be related to the fact that Int.pow is not tail recursive (see https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Large.20powers.20of.20.601.60.20and.20.60-1.60/near/530617797)

[Kim Morrison]

(Sorry to raise this old thread from the dead, but just noting that this has been fixed in the meantime.)