`grind` and `simp +arith` cause deep recursion involving negative integer literal

[datokrat]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

This grind statement fails because of deep recursion:

example (xs : List Int) : xs[0]? = some (-1) := by grind

simp +arith has the same problem:

example (xs : List Int) : xs[0]? = some (-1) := by simp +arith [Option.eq_some_iff_get_eq]

Expected behavior:

At least, I expect grind and simp +arith not to recurse deeply on these examples.

Actual behavior:

deep recursion in both examples

Versions

Lean 4.30.0-nightly-2026-03-05
Target: x86_64-unknown-linux-gnu

Additional Information

An LLM helped me track down this issue. Allow me to provide its analysis that seemed useful (and feel free to ignore!):

The deep recursion occurs during grind's simp preprocessing when simplifying expressions of the form ∃ h : P, body(h) where body contains a proof term using the bound variable h (e.g., ∃ h : 0 < xs.length, xs[0] = -1 where xs[0] is getElem xs 0 h).

The chain of events:

1. exists_prop_congr (@[congr] lemma in Init/PropLemmas.lean:234) fires on the existential. It rewrites the domain 0 < n → 1 ≤ n via Nat.lt_eq, wrapping the bound variable: h becomes Iff.mpr ... h.

2. simpLoop (in Simp/Main.lean:679) sees e != r.expr (the body changed structurally due to Iff.mpr wrapping), so it recursively calls itself via visitPostContinue.

3. On iteration 2+, exists_prop_congr fires again. The domain 1 ≤ n hasn't changed, BUT:

4. The bug: The Lean.Meta.Simp.Arith.Int.simpEq? function (in Simp/Arith/Int/Simp.lean:34-72), called as part of the simpArith post-processing pipeline (only active when arith := true), normalizes the body equation xs[0] = -1. The equation is already normalized, but the function returns some (r, proof) where r == e — it produces a non-trivial proof of (xs[0] = -1) = (xs[0] = -1) instead of returning none.

5. This makes processCongrHypothesis report modified = true (because r.proof?.isSome = true), so exists_prop_congr succeeds and wraps h with another Iff.mpr layer.

6. Each iteration adds one more Iff.mpr wrapper: h → Iff.mpr(..., h) → Iff.mpr(..., Iff.mpr(..., h)) → ..., creating an infinitely growing term that never stabilizes.

Why only +arith / grind?

The simpArith function is hardcoded into simp's post-processing pipeline and only runs when arith := true (default: false). Regular simp never triggers it. Grind sets arith := true in its simp config (Grind/SimpUtil.lean:193). The underlying theorem Int.Linear.norm_eq_var_const is phrased in terms of internal reflection types (Int.Linear.Expr.denote), so adding it as a simp lemma has no effect — it only fires through the reflection-based simpEq? function.

The Fix

Add if r == e then return none to the norm_eq_var_const and norm_eq_var branches of simpEq? to prevent returning a spurious proof when the normalization produces the same expression. This is consistent with the existing check at line 46 for the general case, and with Nat.simpCnstrPos? which already has a correct r != lhs guard.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.