dbfd0d35f2
This PR adds `r == e` guards to the `norm_eq_var` and `norm_eq_var_const` branches of `Int.Linear.simpEq?`. Without these guards, `simpEq?` returns a non-trivial proof for already-normalized equations like `x = -1`, causing `exists_prop_congr` to fire repeatedly and build an infinitely growing term. The existing `Nat.simpCnstrPos?` already had the equivalent guard (`if r != lhs then ... else return none`). Closes #12812 --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
15 lines
678 B
Text
15 lines
678 B
Text
-- Tests for https://github.com/leanprover/lean4/issues/12812
|
|
-- `grind` and `simp +arith` should not loop on already-normalized Int equalities
|
|
|
|
-- The original report: deep recursion on negative integer literal
|
|
example (xs : List Int) (h : xs[0]? = some (-1)) : xs[0]? = some (-1) := by grind
|
|
|
|
-- Variant with simp +arith
|
|
example (xs : List Int) (h : xs[0]? = some (-1)) : xs[0]? = some (-1) := by simp +arith [h]
|
|
|
|
-- norm_eq_var branch: x = y already normalized
|
|
example (a b : Int) (h : a = b) : a = b := by grind
|
|
|
|
-- norm_eq_var_const branch: x = -k already normalized
|
|
example (a : Int) (h : a = -1) : a = -1 := by grind
|
|
example (a : Int) (h : a = -42) : a = -42 := by grind
|