fix: grind ring + linarith internalization

This PR ensures that auxliary terms are not internalized by the ring
and linarith modules.

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

@@ -108,6 +108,9 @@ private def internalizeInv (e : Expr) : GoalM Bool := do
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if !(← getConfig).ring && !(← getConfig).ringNull then return ()
+  if isIntModuleVirtualParent parent? then
+    -- `e` is an auxiliary term used to convert `CommRing` to `IntModule`
+    return ()
   if (← internalizeInv e) then return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()

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

@@ -70,7 +70,7 @@ def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Po
 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
+  internalize e generation (some getIntModuleVirtualParent)
   return e
 
 end Lean.Meta.Grind.Arith.Linear

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

@@ -47,6 +47,9 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).linarith do return ()
+  if isIntModuleVirtualParent parent? then
+    -- `e` is an auxiliary term used to convert `CommRing` to `IntModule`
+    return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
   let some structId ← getStructId? type | return ()

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -133,4 +133,22 @@ end CollectDecVars
 
 export CollectDecVars (CollectDecVarsM)
 
+private def ____intModuleMarker____ : Bool := true
+
+/--
+Return auxiliary expression used as "virtual" parent when
+internalizing auxiliary expressions created by `toIntModuleExpr`.
+The function `toIntModuleExpr` converts a `CommRing` polynomial into
+a `IntModule` expression. We don't want this auxiliary expression to be
+internalized by the `CommRing` module since it uses a nonstandard encoding
+with `@HMul.hMul Int α α`, a virtual `One.one` constant, etc.
+ -/
+def getIntModuleVirtualParent : Expr :=
+  mkConst ``____intModuleMarker____
+
+def isIntModuleVirtualParent (parent? : Option Expr) : Bool :=
+  match parent? with
+  | none => false
+  | some parent => parent == getIntModuleVirtualParent
+
 end Lean.Meta.Grind.Arith

tests/lean/run/grind_ring_1.lean

@@ -81,3 +81,17 @@ set_option trace.grind.debug.ring.basis true in
 example [CommRing α] (a b c : α)
     : a^2*b = 1 → a*b^2 = b → False := by
    grind
+
+
+/--
+trace: [grind.ring.assert.basis] a ^ 2 * b + -1 = 0
+[grind.ring.assert.basis] a * b ^ 2 + -1 * b = 0
+[grind.ring.assert.basis] a * b + -1 * b = 0
+[grind.ring.assert.basis] b + -1 = 0
+[grind.ring.assert.basis] a + -1 = 0
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.ring.assert.basis true in
+example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α)
+    : a^2*b = 1 → a*b^2 = b → False := by
+   grind