From 4b7ea26d91033c2171088972ec991cd326105777 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 13 Jun 2025 12:53:42 -0400
Subject: [PATCH] fix: add `grind` normalization theorem for `Int.negSucc`
 (#8775)

This PR adds a `grind` normalization theorem for `Int.negSucc`. Example:

```lean
example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
    (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
  grind
```
---
 src/Init/Grind/Norm.lean                |  2 +-
 tests/lean/grind/omega_regressions.lean |  6 ------
 tests/lean/run/grind_cutsat_eq_1.lean   | 28 ++++++++++---------------
 3 files changed, 12 insertions(+), 24 deletions(-)

diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean
index 3fa80c06e0..bde0d9a418 100644
--- a/src/Init/Grind/Norm.lean
+++ b/src/Init/Grind/Norm.lean
@@ -182,7 +182,7 @@ init_grind_norm
   Int.emod_neg Int.ediv_neg
   Int.ediv_zero Int.emod_zero
   Int.ediv_one Int.emod_one
-
+  Int.negSucc_eq
   natCast_eq natCast_div natCast_mod
   natCast_add natCast_mul
 
diff --git a/tests/lean/grind/omega_regressions.lean b/tests/lean/grind/omega_regressions.lean
index ed4b4aace6..f5ffe5b2a1 100644
--- a/tests/lean/grind/omega_regressions.lean
+++ b/tests/lean/grind/omega_regressions.lean
@@ -1,9 +1,3 @@
 -- These are test cases extracted from Mathlib, where `omega` works but `grind` does not (yet!)
 
 example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by grind
-
--- TODO: add to the library?
-attribute [grind] Int.negSucc_eq
-
-example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
-  (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by grind
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index baa0503400..f8c405329c 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -12,28 +12,28 @@ example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by
   fail_if_success grind
   sorry
 
-theorem ex₁ (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
+example (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
   grind
 
-theorem ex₂ (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
+example (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
   grind
 
-theorem ex₃ (a b c : Int) (_ : c + 3*a = 0) (_ : 2 ∣ 3*a + 1) (_ : 2*b + c = 0) : False := by
+example (a b c : Int) (_ : c + 3*a = 0) (_ : 2 ∣ 3*a + 1) (_ : 2*b + c = 0) : False := by
   grind
 
-theorem ex₄ (a b c : Int) (_ : 2*c + 3*a = 0) (_ : 2*b + c = 0) (_ : 2 ∣ 3*a + 1) : False := by
+example (a b c : Int) (_ : 2*c + 3*a = 0) (_ : 2*b + c = 0) (_ : 2 ∣ 3*a + 1) : False := by
   grind
 
-theorem ex₅ (a c : Int) (_ : 2*c + 3*a = 0) (_ : c + 1 = 0) : False := by
+example (a c : Int) (_ : 2*c + 3*a = 0) (_ : c + 1 = 0) : False := by
   grind
 
-theorem ex₆ (a c : Int) (_ : c + 3*a = 0) (_ : c + 3*a = 1) : False := by
+example (a c : Int) (_ : c + 3*a = 0) (_ : c + 3*a = 1) : False := by
   grind
 
-theorem ex₇ (a c : Int) (_ : c + 3*a = 0) (_ : c - 3*a = 6) (_ : 2*c + a = 0) : False := by
+example (a c : Int) (_ : c + 3*a = 0) (_ : c - 3*a = 6) (_ : 2*c + a = 0) : False := by
   grind
 
-theorem ex₈ (a b : Int) (_ : 2 ∣ a + 1) (_ : a = 2*b) : False := by
+example (a b : Int) (_ : 2 ∣ a + 1) (_ : a = 2*b) : False := by
   grind
 
 example (a b : Int) (_ : a = 2*b) (_ : 2 ∣ a + 1) : False := by
@@ -70,12 +70,6 @@ example (a b : Int) : a = 0 → b = 1 → a + b > 2 → False := by
 example (a b c : Int) : a = 0 → a + b > 2 → b = c → 1 = c → False := by
   grind
 
-#print ex₁
-#print ex₂
-#print ex₃
-#print ex₄
-#print ex₅
-#print ex₆
-#print ex₇
-#print ex₈
-#print ex₉
+example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
+    (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
+  grind