fix: internalization issue in the interface between linarith and ring (#8708)

This PR fixes an internalization bug in the interface between linarith
and ring modules in `grind`. The `CommRing` module may create new terms
during normalization.

src/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
@@ -66,4 +67,10 @@ def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Po
   | .num k => denoteNum k
   | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).hmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
+def _root_.Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Grind.CommRing.Poly) (generation := 0) : LinearM Expr := do
+  let e ← p.denoteAsIntModuleExpr
+  let e ← preprocessLight e
+  internalize e generation none
+  return e
+
 end Lean.Meta.Grind.Arith.Linear

src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean

@@ -41,9 +41,10 @@ def IneqCnstr.assert (c : IneqCnstr) : LinearM Unit := do
 def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : Bool) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? lhs (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? rhs (skipVar := false) | return ()
+  let gen ← getGeneration e
   if eqTrue then
     let p' := (lhs.sub rhs).toPoly
-    let lhs' ← p'.denoteAsIntModuleExpr
+    let lhs' ← p'.toIntModuleExpr gen
     let some lhs' ← reify? lhs' (skipVar := false) | return ()
     let p := lhs'.norm
     let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs p' lhs' }
@@ -51,7 +52,7 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
   else if (← isLinearOrder) then
     let p' := (rhs.sub lhs).toPoly
     let strict := !strict
-    let lhs' ← p'.denoteAsIntModuleExpr
+    let lhs' ← p'.toIntModuleExpr gen
     let some lhs' ← reify? lhs' (skipVar := false) | return ()
     let p := lhs'.norm
     let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs p' lhs' }

src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean

@@ -25,8 +25,9 @@ private def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
 private def processNewCommRingEq (a b : Expr) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
+  let gen := max (← getGeneration a) (← getGeneration b)
   let p' := (lhs.sub rhs).toPoly
-  let lhs' ← p'.denoteAsIntModuleExpr
+  let lhs' ← p'.toIntModuleExpr gen
   let some lhs' ← reify? lhs' (skipVar := false) | return ()
   let p := lhs'.norm
   if p == .nil then return ()
@@ -34,7 +35,7 @@ private def processNewCommRingEq (a b : Expr) : LinearM Unit := do
   c₁.assert
   let p := p.mul (-1)
   let p' := p'.mulConst (-1)
-  let lhs' ← p'.denoteAsIntModuleExpr
+  let lhs' ← p'.toIntModuleExpr gen
   let some lhs' ← reify? lhs' (skipVar := false) | return ()
   let c₂ : IneqCnstr := { p, strict := false, h := .ofCommRingEq b a rhs lhs p' lhs' }
   c₂.assert

tests/lean/run/grind_linarith_1.lean

@@ -135,3 +135,11 @@ example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
 example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
     : a = 0 → b = 1 → a + b ≤ 2 := by
   grind
+
+example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+    : a*b + b*a > 1 → a*b > 0 := by
+  grind
+
+example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+    : a*b + c > 1 → c = b*a → a*b > 0 := by
+  grind