grind in recursive proofs

Stream: lean4

[Chris Henson]

Consider this example (adapted from #new members > ✔ How to use both Nat.le_induction and Nat.twoStepInduction):

@[grind =]
def d : Nat → Int
  | 0 => 3
  | 1 => 1
  | k + 2 => 3 * d (k + 1) + 5 * d k

theorem pow_le_dn (n : Nat) (hn : 4 ≤ n := by grind) : 4 ^ n ≤ d n := by
  match n with
  | 0 | 1 | 2 | 3 | 4 | 5 => grind
  | n + 6 =>
    have := pow_le_dn (n + 4)
    have := pow_le_dn (n + 5)
    grind

Following lean4#11268 you can see how one might think it is reasonable to write

theorem pow_le_dn (n : Nat) (hn : 4 ≤ n := by grind) : 4 ^ n ≤ d n := by
  match n with
  | 0 | 1 | 2 | 3 | 4 | 5 => grind
  | n + 6 => grind [pow_le_dn (n + 5), pow_le_dn (n + 4)]

but this gives an error message

unknown free variable `_fvar.646`

Is this a bug? Or if this is not meant to be supported, could we reasonably provide a better error message stating that recursive proofs are not supported in arbitrary grind paramaters?

[Snir Broshi]

Looks like a bug to me, as this is an internal error and not something related to the user's input.
(I don't know if the correct behavior is for grind to work or fail here, but the error is a bug)
Here's a slightly more simplified repro:

@[grind =]
def f : Nat → Nat
  | 0 => 0
  | n + 1 => f n

/-- error: unknown free variable `_fvar.312` -/
#guard_msgs in
theorem foo (n : Nat) : f n = 0 := by
  match n with
  | 0 => grind
  | n + 1 => grind [foo n]

[Snir Broshi]

I think this unknown free variable thing is pretty common, but your example looks unrelated to the issues already reported so worth reporting

[Kim Morrison]

It is intended that grind can't do this, but I agree the error message is terrible. Could you open an issue?

[Chris Henson]

I have opened #11930. As I noted in the issue this fails on 4.27.0-rc1 and works on 4.28.0-nightly-2026-01-07, which still seems like a problem if this is intended to fail? (But maybe it closes the proof some other way, I didn't look closely)