Grind aggressively includes local hypotheses.

Stream: lean4

[Wrenna Robson]

In the following, if I write:

def idxToCount [BEq α] (xs : List α) (i : Nat) (hi : i < xs.length) : Nat := go xs i hi 0 where
  @[specialize] go : (xs : List α) → (i : Nat) → i < xs.length → Nat → Nat
  | _ :: _, 0, _, acc => acc
  | x :: xs, i + 1, hi, acc =>
    haveI hi := Nat.lt_of_succ_lt_succ hi
    bif x == xs[i] then go xs i hi (acc + 1) else go xs i hi acc

Then go correctly only depends on its inner parameters, wheras if I write:

def idxToCount [BEq α] (xs : List α) (i : Nat) (hi : i < xs.length) : Nat := go xs i hi 0 where
  @[specialize] go : (xs : List α) → (i : Nat) → i < xs.length → Nat → Nat
  | _ :: _, 0, _, acc => acc
  | x :: xs, i + 1, hi, acc =>
    bif x == xs[i]'(by grind) then go xs i (by grind) (acc + 1) else go xs i (by grind) acc

then it gets a dependence on the outer xs etc.

Clearly this is undesirable behaviour. Can it be avoided?

[Kim Morrison]

What is the actual proof term grind produces here?

[Wrenna Robson]

I'm not at my desk so can't check. Would I use show_term?

[Jovan Gerbscheid]

Here's the minimization, including the generated proof term.

def oops (oh_no : List Nat) (hi : 0 < oh_no.length) : True := go where
  go : True := by grind

#print oops._proof_1
/-
theorem oops._proof_1 : ∀ (oh_no : List Nat), 0 < oh_no.length → True :=
fun oh_no hi =>
  Lean.Grind.intro_with_eq (0 < oh_no.length) (1 ≤ oh_no.length) True (Lean.Grind.Nat.lt_eq 0 oh_no.length)
    (fun hi =>
      Classical.byContradiction
        (Lean.Grind.intro_with_eq (¬True) False False Lean.Grind.not_true fun h => False.casesOn (fun x => False) h))
    hi
-/

[Wrenna Robson]

Aha, thank you.

[Kim Morrison]

This is fixed on the latest nightly, as a side effect of a new method of handling hypotheses.

[Wrenna Robson]

Oh brilliant - thank you for the update.

[Markus Himmel]

I am still suffering from this in one of my projects on nightly-2025-11-27. Here is my example:

theorem foo {n l r : Nat} (hn : ∃ d, n = 2 ^ d) (hlr : l < r) : l ≤ r - 1 := by
  grind

The proof is long, but it starts like this:

theorem foo._proof_1_1 : ∀ {n l r : Nat}, (∃ d, n = 2 ^ d) → l < r → l ≤ r - 1 :=
fun {n l r} hn hlr =>
  Classical.byContradiction
    (Lean.Grind.intro_with_eq (¬l ≤ r - 1) (r - 1 + 1 ≤ l) False (Nat.not_le_eq l (r - 1)) fun h =>
      id
        (Exists.casesOn hn fun w h_1 =>
          id
            (Or.casesOn (Lean.Grind.em (-1 * ↑r + 1 ≤ 0))
              (fun h_2 =>

This leads to a similar problem as in the original post:

def irrelevant (l r : Nat) (_hlr : l ≤ r - 1) : Nat :=
  r - l

def irrelevant2 (n : Nat) (_hn : ∃ d, n = 2 ^ d) : Nat :=
  n

def bar {n l r : Nat} (hn : ∃ d, n = 2 ^ d) (hlr : l < r) :=
  baz + irrelevant2 n hn
where
  baz : Nat :=
    irrelevant l r (by grind)

-- I didn't want `n` and `hn` to appear in the signature of `baz` :(
/-- info: bar.baz {n l r : Nat} (hn : ∃ d, n = 2 ^ d) (hlr : l < r) : Nat -/
#guard_msgs in
#check bar.baz

live-lean link

[Kim Morrison]

@Markus Himmel, obviously we should make this better, but at least there is a workaround possible now:

theorem foo {n l r : Nat} (hn : ∃ d, n = 2 ^ d) (hlr : l < r) : l ≤ r - 1 := by
  grind?

gives the suggestion:

  grind => cases #aacf <;> cases #d8dd

which is certainly not very illuminating. However it's then easy to discover that

  grind => cases #d8dd

gives the behaviour you want.

[Kim Morrison]

  grind =>  cases?

gives a slightly more informative message, explaining which "anchor" corresponds to which case split.