From fe7e0859d58d7c28314526a97f6a4e467895210a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 14 Aug 2025 15:28:25 -0700
Subject: [PATCH] fix: div/norm normalization assumptions in `grind` (#9919)

This PR ensures `grind cutsat` does not rely on div/mod terms to have
been normalized. The `grind` preprocessor has normalizers for them, but
sometimes they cannot be applied because of type dependencies.

Closes #9907
---
 src/Init/Data/Int/DivMod/Lemmas.lean          |  6 ++++
 .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean    | 35 +++++++++++++++----
 tests/lean/run/grind_9907.lean                | 15 ++++++++
 3 files changed, 49 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/grind_9907.lean

diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 69254cf445..8da261df2a 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -956,6 +956,12 @@ theorem neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b :
 @[simp] theorem emod_one (a : Int) : a % 1 = 0 := by
   simp [emod_def, Int.one_mul, Int.sub_self]
 
+theorem ediv_minus_one (a : Int) : a / (-1) = -a := by
+  simp
+
+theorem emod_minus_one (a : Int) : a % (-1) = 0 := by
+  simp
+
 @[deprecated sub_emod_right (since := "2025-04-11")]
 theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
   sub_emod_right ..
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 95b00315d8..137489f3e8 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -396,15 +396,36 @@ private def internalizeInt (e : Expr) : GoalM Unit := do
     c.assert
 
 private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
-  if b == 0 || b == 1 || b == -1 then
-    throwError "`grind` internal error, found non-normalized div/mod by {b}"
   if (← get').divMod.contains (a, b) then return ()
   modify' fun s => { s with divMod := s.divMod.insert (a, b) }
-  let n : Int := 1 - b.natAbs
-  let b := mkIntLit b
-  pushNewFact <| mkApp2 (mkConst ``Int.Linear.ediv_emod) a b
-  pushNewFact <| mkApp3 (mkConst ``Int.Linear.emod_nonneg) a b eagerReflBoolTrue
-  pushNewFact <| mkApp4 (mkConst ``Int.Linear.emod_le) a b (toExpr n) eagerReflBoolTrue
+  let b' ← shareCommon (mkIntLit b)
+  if b == 0 || b == 1 || b == -1 then
+    /-
+    We cannot assume terms have been normalized.
+    Recall that terms may not be normalized because of dependencies.
+    -/
+    let gen ← getGeneration a
+    internalize b' gen
+    let ediv ← shareCommon (mkIntDiv a b'); internalize ediv gen
+    let emod ← shareCommon (mkIntMod a b'); internalize emod gen
+    if b == 0 then
+      pushEq emod a <| mkApp (mkConst ``Int.emod_zero) a
+      pushEq ediv b' <| mkApp (mkConst ``Int.ediv_zero) a
+    else if b == 1 then
+      let zero ← shareCommon (mkIntLit 0); internalize zero gen
+      pushEq emod zero <| mkApp (mkConst ``Int.emod_one) a
+      pushEq ediv a <| mkApp (mkConst ``Int.ediv_one) a
+    else
+      assert! b == -1
+      let zero ← shareCommon (mkIntLit 0); internalize zero gen
+      let neg_a ← shareCommon (mkIntNeg a); internalize neg_a gen
+      pushEq emod zero <| mkApp (mkConst ``Int.emod_minus_one) a
+      pushEq ediv neg_a <| mkApp (mkConst ``Int.ediv_minus_one) a
+  else
+    let n : Int := 1 - b.natAbs
+    pushNewFact <| mkApp2 (mkConst ``Int.Linear.ediv_emod) a b'
+    pushNewFact <| mkApp3 (mkConst ``Int.Linear.emod_nonneg) a b' eagerReflBoolTrue
+    pushNewFact <| mkApp4 (mkConst ``Int.Linear.emod_le) a b' (toExpr n) eagerReflBoolTrue
 
 private def propagateDiv (e : Expr) : GoalM Unit := do
   let_expr HDiv.hDiv _ _ _ inst a b ← e | return ()
diff --git a/tests/lean/run/grind_9907.lean b/tests/lean/run/grind_9907.lean
new file mode 100644
index 0000000000..76bc6e78cf
--- /dev/null
+++ b/tests/lean/run/grind_9907.lean
@@ -0,0 +1,15 @@
+structure DepThing {α : Type u} (l : List α) : Type u where
+  suffix : List α
+  property : suffix = l
+
+example (n : Nat) (c : DepThing (List.range' 1 (n/1))) (h : 0 < c.suffix.length) : True :=  by
+  grind
+
+opaque p (n : Int) : Type
+opaque q (n : Int) (h : p n) : Prop
+example (h : p (a / 0)) : q (a / 0) h → q (a / 0) h := by grind
+example (h : p (a / -1)) : q (a / -1) h → q (a / -1) h := by grind
+example (h : p (a / 1)) : q (a / 1) h → q (a / 1) h := by grind
+example (h₁ : p (a / 0)) (h₂ : p 0) : h₁ ≍ h₂ → q (a / 0) h₁ → q 0 h₂ := by grind
+example (h₁ : p (a / 1)) (h₂ : p a) : h₁ ≍ h₂ → q (a / 1) h₁ → q (a) h₂ := by grind
+example (h₁ : p (a / -1)) (h₂ : p (-a)) : h₁ ≍ h₂ → q (a / -1) h₁ → q (-a) h₂ := by grind