fix: apply ring normalizer to equalities coming from grind to core to lia (#11613)

This PR ensures we apply the ring normalizer to equalities being
propagated from the `grind` core module to `grind lia`. It also ensures
we use the safe/managed polynomial functions when normalizing.

Closes #11539

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat
 /-!
@@ -22,7 +23,7 @@ CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
 /-- Returns `true` if `p` contains a nonlinear monomial. -/
 def _root_.Int.Linear.Poly.isNonlinear (p : Poly) : GoalM Bool := do
   let .add _ x p := p | return false
-  if (← getVar x).isAppOf ``HMul.hMul then return true
+  if (← getVar x).isAppOf ``HMul.hMul || (← getVar x).isAppOf ``HPow.hPow then return true
   p.isNonlinear
 
 def _root_.Int.Linear.Poly.getGeneration (p : Poly) : GoalM Nat := do
@@ -46,7 +47,7 @@ def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.Ri
     let e ← shareCommon (← canon e)
     let gen ← p.getGeneration
     let some re ← CommRing.reify? e (gen := gen) | return none
-    let p' := re.toPoly
+    let some p' ← re.toPolyM? | return none
     let e' ← p'.denoteExpr
     let e' ← preprocessLight e'
     -- Remark: we are reusing the `IntModule` virtual parent.

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -386,13 +386,6 @@ private def exprAsPoly (a : Expr) : GoalM Poly := do
   else
     throwError "internal `grind` error, expression is not relevant to cutsat{indentExpr a}"
 
-private def processNewIntEq (a b : Expr) : GoalM Unit := do
-  let p₁ ← exprAsPoly a
-  let p₂ ← exprAsPoly b
-  -- Remark: we don't need to use the comm ring normalizer here because `p` is always linear.
-  let p := p₁.combine (p₂.mul (-1))
-  { p, h := .core a b p₁ p₂ : EqCnstr }.assert
-
 /-- Asserts a constraint coming from the core. -/
 private def EqCnstr.assertCore (c : EqCnstr) : GoalM Unit := do
   if let some (re, rp, p) ← c.p.normCommRing? then
@@ -401,6 +394,14 @@ private def EqCnstr.assertCore (c : EqCnstr) : GoalM Unit := do
   else
     c.assert
 
+private def processNewIntEq (a b : Expr) : GoalM Unit := do
+  let p₁ ← exprAsPoly a
+  let p₂ ← exprAsPoly b
+  -- Remark: we don't need to use the comm ring normalizer here because `p` is always linear.
+  let p := p₁.combine (p₂.mul (-1))
+  let c := { p, h := .core a b p₁ p₂ : EqCnstr }
+  c.assertCore
+
 /--
 Similar to `natToInt`, but checks first whether the term has already been internalized.
 -/

tests/lean/run/grind_11539.lean

@@ -0,0 +1,11 @@
+example {n a b : Nat}
+  (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤
+          (↑b + (↑a - ↑b)) ^ (n + 1)) :
+    (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by
+grind (splits := 0)
+
+example {n a b : Nat}
+  (this : (b : Int) ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤
+          (↑b + (↑a - ↑b)) ^ (n + 1)) :
+    (n + 1) * a * b ^ n ≤ a ^ (n + 1) + n * b * b ^ n := by
+grind