From 5d46391dde280f817f7605a9f1568eefaaa03e91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 6 Jul 2025 20:29:42 -0700
Subject: [PATCH] perf: generate `grind ring` instances on demand (#9228)

This PR improves the startup time for `grind ring` by generating the
required type classes on demand. This optimization is particularly
relevant for files that make hundreds of calls to `grind`, such as
`tests/lean/run/grind_bitvec2.lean`. For example, before this change,
`grind` spent 6.87 seconds synthesizing type classes, compared to 3.92
seconds after this PR.
---
 .../Grind/Arith/CommRing/DenoteExpr.lean      |  38 +--
 .../Tactic/Grind/Arith/CommRing/EqCnstr.lean  |  16 +-
 .../Grind/Arith/CommRing/Internalize.lean     |  14 +-
 .../Meta/Tactic/Grind/Arith/CommRing/PP.lean  |  17 +-
 .../Tactic/Grind/Arith/CommRing/Proof.lean    |  13 +-
 .../Tactic/Grind/Arith/CommRing/Reify.lean    |  72 +++---
 .../Tactic/Grind/Arith/CommRing/RingId.lean   | 112 +--------
 .../Tactic/Grind/Arith/CommRing/Types.lean    |  30 +--
 .../Tactic/Grind/Arith/CommRing/Util.lean     | 222 +++++++++++++++++-
 .../Meta/Tactic/Grind/Arith/Linear/Util.lean  |   7 +-
 tests/lean/run/grind_const_pattern.lean       |  12 +-
 tests/lean/run/grind_cutsat_diseq_2.lean      |   1 -
 tests/lean/run/grind_cutsat_div_1.lean        |   9 +-
 tests/lean/run/grind_cutsat_eq_1.lean         |   1 -
 tests/lean/run/grind_cutsat_nat_le.lean       |   1 -
 tests/lean/run/grind_split_issue.lean         |   2 +-
 16 files changed, 334 insertions(+), 233 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean
index 7a0ee0ff7c..9de8e30658 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean
@@ -14,18 +14,24 @@ namespace Lean.Meta.Grind.Arith.CommRing
 Helper functions for converting reified terms back into their denotations.
 -/
 
-variable [Monad M] [MonadGetRing M]
+variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadRing M]
 
 def denoteNum (k : Int) : M Expr := do
   let ring ← getRing
-  return denoteNumCore ring.u ring.type ring.semiringInst ring.negFn k
+  let n := mkRawNatLit k.natAbs
+  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
+  let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
+  if k < 0 then
+    return mkApp (← getNegFn) n
+  else
+    return n
 
 def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : M Expr := do
   let x := (← getRing).vars[pw.x]!
   if pw.k == 1 then
     return x
   else
-    return mkApp2 (← getRing).powFn x (toExpr pw.k)
+    return mkApp2 (← getPowFn) x (toExpr pw.k)
 
 def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : M Expr := do
   match m with
@@ -35,7 +41,7 @@ where
   go (m : Mon) (acc : Expr) : M Expr := do
     match m with
     | .unit => return acc
-    | .mult pw m => go m (mkApp2 (← getRing).mulFn acc (← pw.denoteExpr))
+    | .mult pw m => go m (mkApp2 (← getMulFn) acc (← pw.denoteExpr))
 
 def _root_.Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : M Expr := do
   match p with
@@ -46,13 +52,13 @@ where
     if k == 1 then
       m.denoteExpr
     else
-      return mkApp2 (← getRing).mulFn (← denoteNum k) (← m.denoteExpr)
+      return mkApp2 (← getMulFn) (← denoteNum k) (← m.denoteExpr)
 
   go (p : Poly) (acc : Expr) : M Expr := do
     match p with
     | .num 0 => return acc
-    | .num k => return mkApp2 (← getRing).addFn acc (← denoteNum k)
-    | .add k m p => go p (mkApp2 (← getRing).addFn acc (← denoteTerm k m))
+    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
+    | .add k m p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k m))
 
 def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
   go e
@@ -60,11 +66,11 @@ where
   go : RingExpr → M Expr
   | .num k => denoteNum k
   | .var x => return (← getRing).vars[x]!
-  | .add a b => return mkApp2 (← getRing).addFn (← go a) (← go b)
-  | .sub a b => return mkApp2 (← getRing).subFn (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getRing).mulFn (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getRing).powFn (← go a) (toExpr k)
-  | .neg a => return mkApp (← getRing).negFn (← go a)
+  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
+  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
+  | .neg a => return mkApp (← getNegFn) (← go a)
 
 private def mkEq (a b : Expr) : M Expr := do
   let r ← getRing
@@ -84,9 +90,9 @@ def _root_.Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr (e : SemiringExpr) :
 where
   go : SemiringExpr → SemiringM Expr
   | .num k => denoteNum k
-  | .var x => return mkApp (← getSemiring).toQFn (← getSemiring).vars[x]!
-  | .add a b => return mkApp2 (← getRing).addFn (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getRing).mulFn (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getRing).powFn (← go a) (toExpr k)
+  | .var x => return mkApp (← getToQFn) (← getSemiring).vars[x]!
+  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
 
 end Lean.Meta.Grind.Arith.CommRing
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
index 573a79af46..7e2079a6c1 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
@@ -359,13 +359,13 @@ private def diseqToEq (a b : Expr) : RingM Unit := do
   let gen := max (← getGeneration a) (← getGeneration b)
   let ring ← getRing
   let some fieldInst := ring.fieldInst? | unreachable!
-  let e ← pre <| mkApp2 ring.subFn a b
+  let e ← pre <| mkApp2 (← getSubFn) a b
   modifyRing fun s => { s with invSet := s.invSet.insert e }
-  let eInv ← pre <| mkApp (← getRing).invFn?.get! e
-  let lhs ← pre <| mkApp2 ring.mulFn e eInv
+  let eInv ← pre <| mkApp (← getInvFn) e
+  let lhs ← pre <| mkApp2 (← getMulFn) e eInv
   internalize lhs gen none
   trace[grind.debug.ring.rabinowitsch] "{lhs}"
-  pushEq lhs ring.one <| mkApp5 (mkConst ``Grind.CommRing.diseq_to_eq [ring.u]) ring.type fieldInst a b (← mkDiseqProof a b)
+  pushEq lhs (← getOne) <| mkApp5 (mkConst ``Grind.CommRing.diseq_to_eq [ring.u]) ring.type fieldInst a b (← mkDiseqProof a b)
 
 private def diseqZeroToEq (a b : Expr) : RingM Unit := do
   -- Rabinowitsch transformation for `b = 0` case
@@ -373,11 +373,11 @@ private def diseqZeroToEq (a b : Expr) : RingM Unit := do
   let ring ← getRing
   let some fieldInst := ring.fieldInst? | unreachable!
   modifyRing fun s => { s with invSet := s.invSet.insert a }
-  let aInv ← pre <| mkApp (← getRing).invFn?.get! a
-  let lhs ← pre <| mkApp2 ring.mulFn a aInv
+  let aInv ← pre <| mkApp (← getInvFn) a
+  let lhs ← pre <| mkApp2 (← getMulFn) a aInv
   internalize lhs gen none
   trace[grind.debug.ring.rabinowitsch] "{lhs}"
-  pushEq lhs ring.one <| mkApp4 (mkConst ``Grind.CommRing.diseq0_to_eq [ring.u]) ring.type fieldInst a (← mkDiseqProof a b)
+  pushEq lhs (← getOne) <| mkApp4 (mkConst ``Grind.CommRing.diseq0_to_eq [ring.u]) ring.type fieldInst a (← mkDiseqProof a b)
 
 @[export lean_process_ring_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
@@ -400,7 +400,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
       ofSemiring? := none
     }
   else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
-    if (← getSemiring).addRightCancelInst?.isSome then
+    if (← getAddRightCancelInst?).isSome then
       if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter
       trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
       let some sa ← toSemiringExpr? a | return ()
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
index a561b691bf..7e3bd099ff 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
@@ -46,11 +46,11 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
 private partial def toInt? (e : Expr) : RingM (Option Int) := do
   match_expr e with
   | Neg.neg _ i a =>
-    if isNegInst (← getRing) i then return (- .) <$> (← toInt? a) else return none
+    if (← isNegInst i) then return (- .) <$> (← toInt? a) else return none
   | IntCast.intCast _ i a =>
-    if isIntCastInst (← getRing) i then getIntValue? a else return none
+    if (← isIntCastInst i) then getIntValue? a else return none
   | NatCast.natCast _ i a =>
-    if isNatCastInst (← getRing) i then
+    if (← isNatCastInst i) then
       let some v ← getNatValue? a | return none
       return some (Int.ofNat v)
     else
@@ -61,8 +61,8 @@ private partial def toInt? (e : Expr) : RingM (Option Int) := do
   | _ => return none
 
 private def isInvInst (inst : Expr) : RingM Bool := do
-  let some fn := (← getRing).invFn? | return false
-  return isSameExpr fn.appArg! inst
+  if (← getRing).fieldInst?.isNone then return false
+  return isSameExpr (← getInvFn).appArg! inst
 
 /--
 Given `e` of the form `@Inv.inv _ inst a`,
@@ -80,7 +80,7 @@ private def processInv (e inst a : Expr) : RingM Unit := do
     if (← hasChar) then
       let (charInst, c) ← getCharInst
       if c == 0 then
-        let expected ← mkEq (mkApp2 ring.mulFn a e) (← denoteNum 1)
+        let expected ← mkEq (mkApp2 (← getMulFn) a e) (← denoteNum 1)
         pushNewFact <| mkExpectedPropHint
           (mkApp5 (mkConst ``Grind.CommRing.inv_int_eq [ring.u]) ring.type fieldInst charInst (mkIntLit k) reflBoolTrue)
           expected
@@ -90,7 +90,7 @@ private def processInv (e inst a : Expr) : RingM Unit := do
           (mkApp6 (mkConst ``Grind.CommRing.inv_zero_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst (mkIntLit k) reflBoolTrue)
           expected
       else
-        let expected ← mkEq (mkApp2 ring.mulFn a e) (← denoteNum 1)
+        let expected ← mkEq (mkApp2 (← getMulFn) a e) (← denoteNum 1)
         pushNewFact <| mkExpectedPropHint
           (mkApp6 (mkConst ``Grind.CommRing.inv_int_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst (mkIntLit k) reflBoolTrue)
           expected
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean
index 5f786c0189..48731a1f6c 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean
@@ -8,10 +8,13 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
-instance : MonadGetRing (ReaderT Ring MetaM) where
-  getRing := read
+private abbrev M := StateT Ring MetaM
 
-private def M := ReaderT Goal (StateT (Array MessageData) MetaM)
+instance : MonadRing M where
+  getRing := get
+  modifyRing := modify
+  canonExpr e := return e
+  synthInstance? e := Meta.synthInstance? e none
 
 private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array MessageData) : Option MessageData :=
   if msgs.isEmpty then
@@ -22,19 +25,19 @@ private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array Mes
 private def push (msgs : Array MessageData) (msg? : Option MessageData) : Array MessageData :=
   if let some msg := msg? then msgs.push msg else msgs
 
-def ppBasis? : ReaderT Ring MetaM (Option MessageData) := do
+def ppBasis? : M (Option MessageData) := do
   let mut basis := #[]
   for c in (← getRing).basis do
     basis := basis.push (toTraceElem (← c.denoteExpr))
   return toOption `basis "Basis" basis
 
-def ppDiseqs? : ReaderT Ring MetaM (Option MessageData) := do
+def ppDiseqs? : M (Option MessageData) := do
   let mut diseqs := #[]
   for d in (← getRing).diseqs do
     diseqs := diseqs.push (toTraceElem (← d.denoteExpr))
   return toOption `diseqs "Disequalities" diseqs
 
-def ppRing? : ReaderT Ring MetaM (Option MessageData) := do
+def ppRing? : M (Option MessageData) := do
   let msgs := #[]
   let msgs := push msgs (← ppBasis?)
   let msgs := push msgs (← ppDiseqs?)
@@ -43,7 +46,7 @@ def ppRing? : ReaderT Ring MetaM (Option MessageData) := do
 def pp? (goal : Goal) : MetaM (Option MessageData) := do
   let mut msgs := #[]
   for ring in goal.arith.ring.rings do
-    let some msg ← ppRing? ring | pure ()
+    let some msg ← ppRing? |>.run' ring | pure ()
     msgs := msgs.push msg
   if msgs.isEmpty then
     return none
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
index e22bdae829..5b965b0844 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
@@ -23,14 +23,14 @@ def toContextExpr : RingM Expr := do
   if h : 0 < ring.vars.size then
     RArray.toExpr ring.type id (RArray.ofFn (ring.vars[·]) h)
   else
-    RArray.toExpr ring.type id (RArray.leaf (mkApp ring.natCastFn (toExpr 0)))
+    RArray.toExpr ring.type id (RArray.leaf (mkApp (← getNatCastFn) (toExpr 0)))
 
 private def toSContextExpr' : SemiringM Expr := do
   let semiring ← getSemiring
   if h : 0 < semiring.vars.size then
     RArray.toExpr semiring.type id (RArray.ofFn (semiring.vars[·]) h)
   else
-    RArray.toExpr semiring.type id (RArray.leaf (mkApp semiring.natCastFn (toExpr 0)))
+    RArray.toExpr semiring.type id (RArray.leaf (mkApp (← getNatCastFn') (toExpr 0)))
 
 /-- Similar to `toContextExpr`, but for semirings. -/
 private def toSContextExpr (semiringId : Nat) : RingM Expr := do
@@ -391,9 +391,12 @@ private def mkStepPrefix (declName declNameC : Name) : ProofM Expr := do
   else
     mkStepBasicPrefix declName
 
-private def getSemiringOf : RingM Semiring := do
+private def getSemiringIdOf : RingM Nat := do
   let some semiringId := (← getRing).semiringId? | throwError "`grind` internal error, semiring is not available"
-  SemiringM.run semiringId do getSemiring
+  return semiringId
+
+private def getSemiringOf : RingM Semiring := do
+  SemiringM.run (← getSemiringIdOf) do getSemiring
 
 private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
@@ -403,7 +406,7 @@ private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
 private def mkSemiringAddRightCancelPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
-  let some addRightCancelInst := semiring.addRightCancelInst?
+  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do getAddRightCancelInst?
     | throwError "`grind` internal error, `AddRightCancel` instance is not available"
   return mkApp4 (mkConst declName [semiring.u]) semiring.type semiring.semiringInst addRightCancelInst sctx
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean
index 3160fdee10..1b9fb8439a 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean
@@ -10,20 +10,20 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
-def isAddInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.addFn.appArg! inst
-def isMulInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.mulFn.appArg! inst
-def isSubInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.subFn.appArg! inst
-def isNegInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.negFn.appArg! inst
-def isPowInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.powFn.appArg! inst
-def isIntCastInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.intCastFn.appArg! inst
-def isNatCastInst (ring : Ring) (inst : Expr) : Bool :=
-  isSameExpr ring.natCastFn.appArg! inst
+def isAddInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getAddFn).appArg! inst
+def isMulInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getMulFn).appArg! inst
+def isSubInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getSubFn).appArg! inst
+def isNegInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getNegFn).appArg! inst
+def isPowInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getPowFn).appArg! inst
+def isIntCastInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getIntCastFn).appArg! inst
+def isNatCastInst (inst : Expr) : RingM Bool :=
+  return isSameExpr (← getNatCastFn).appArg! inst
 
 private def reportAppIssue (e : Expr) : GoalM Unit := do
   reportIssue! "comm ring term with unexpected instance{indentExpr e}"
@@ -49,24 +49,24 @@ partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option
   let rec go (e : Expr) : RingM RingExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
-      if isAddInst (← getRing) i then return .add (← go a) (← go b) else asVar e
+      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
     | HMul.hMul _ _ _ i a b =>
-      if isMulInst (← getRing) i then return .mul (← go a) (← go b) else asVar e
+      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
     | HSub.hSub _ _ _ i a b =>
-      if isSubInst (← getRing) i then return .sub (← go a) (← go b) else asVar e
+      if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
     | HPow.hPow _ _ _ i a b =>
       let some k ← getNatValue? b | toVar e
-      if isPowInst (← getRing) i then return .pow (← go a) k else asVar e
+      if (← isPowInst i) then return .pow (← go a) k else asVar e
     | Neg.neg _ i a =>
-      if isNegInst (← getRing) i then return .neg (← go a) else asVar e
+      if (← isNegInst i) then return .neg (← go a) else asVar e
     | IntCast.intCast _ i a =>
-      if isIntCastInst (← getRing) i then
+      if (← isIntCastInst i) then
         let some k ← getIntValue? a | toVar e
         return .num k
       else
         asVar e
     | NatCast.natCast _ i a =>
-      if isNatCastInst (← getRing) i then
+      if (← isNatCastInst i) then
         let some k ← getNatValue? a | toVar e
         return .num k
       else
@@ -85,24 +85,24 @@ partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option
     toTopVar e
   match_expr e with
   | HAdd.hAdd _ _ _ i a b =>
-    if isAddInst (← getRing) i then return some (.add (← go a) (← go b)) else asTopVar e
+    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
   | HMul.hMul _ _ _ i a b =>
-    if isMulInst (← getRing) i then return some (.mul (← go a) (← go b)) else asTopVar e
+    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
   | HSub.hSub _ _ _ i a b =>
-    if isSubInst (← getRing) i then return some (.sub (← go a) (← go b)) else asTopVar e
+    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
   | HPow.hPow _ _ _ i a b =>
     let some k ← getNatValue? b | return none
-    if isPowInst (← getRing) i then return some (.pow (← go a) k) else asTopVar e
+    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
   | Neg.neg _ i a =>
-    if isNegInst (← getRing) i then return some (.neg (← go a)) else asTopVar e
+    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
   | IntCast.intCast _ i a =>
-    if isIntCastInst (← getRing) i then
+    if (← isIntCastInst i) then
       let some k ← getIntValue? a | toTopVar e
       return some (.num k)
     else
       asTopVar e
   | NatCast.natCast _ i a =>
-    if isNatCastInst (← getRing) i then
+    if (← isNatCastInst i) then
       let some k ← getNatValue? a | toTopVar e
       return some (.num k)
     else
@@ -127,14 +127,14 @@ partial def sreify? (e : Expr) : SemiringM (Option SemiringExpr) := do
   let rec go (e : Expr) : SemiringM SemiringExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
-      if isSameExpr (← getSemiring).addFn.appArg! i then return .add (← go a) (← go b) else asVar e
+      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
     | HMul.hMul _ _ _ i a b =>
-      if isSameExpr (← getSemiring).mulFn.appArg! i then return .mul (← go a) (← go b) else asVar e
+      if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
     | HPow.hPow _ _ _ i a b =>
       let some k ← getNatValue? b | toVar e
-      if isSameExpr (← getSemiring).powFn.appArg! i then return .pow (← go a) k else asVar e
+      if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
     | NatCast.natCast _ i a =>
-      if isSameExpr (← getSemiring).natCastFn.appArg! i then
+      if isSameExpr (← getNatCastFn').appArg! i then
         let some k ← getNatValue? a | toVar e
         return .num k
       else
@@ -150,14 +150,14 @@ partial def sreify? (e : Expr) : SemiringM (Option SemiringExpr) := do
     toTopVar e
   match_expr e with
   | HAdd.hAdd _ _ _ i a b =>
-    if isSameExpr (← getSemiring).addFn.appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
+    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
   | HMul.hMul _ _ _ i a b =>
-    if isSameExpr (← getSemiring).mulFn.appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
+    if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
   | HPow.hPow _ _ _ i a b =>
     let some k ← getNatValue? b | return none
-    if isSameExpr (← getSemiring).powFn.appArg! i then return some (.pow (← go a) k) else asTopVar e
+    if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
   | NatCast.natCast _ i a =>
-    if isSameExpr (← getSemiring).natCastFn.appArg! i then
+    if isSameExpr (← getNatCastFn').appArg! i then
       let some k ← getNatValue? a | toTopVar e
       return some (.num k)
     else
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
index f1d9a492c9..92f588d4be 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
@@ -13,88 +13,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
-def denoteNumCore (u : Level) (type : Expr) (semiringInst : Expr) (negFn : Expr) (k : Int) : Expr :=
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [u]) type semiringInst n
-  let n := mkApp3 (mkConst ``OfNat.ofNat [u]) type n ofNatInst
-  if k < 0 then
-    mkApp negFn n
-  else
-    n
-
-private def internalizeFn (fn : Expr) : GoalM Expr := do
-  shareCommon (← canon fn)
-
-private def getUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
-  let inst ← synthInstance <| mkApp (mkConst instDeclName [u]) type
-  internalizeFn <| mkApp2 (mkConst declName [u]) type inst
-
-private def getBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do
-  let inst ← synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  internalizeFn <| mkApp4 (mkConst declName [u, u, u]) type type type inst
-
--- Remark: we removed consistency checks such as the one that ensures `HAdd` instance matches `Semiring.toAdd`
--- That is, we are assuming the type classes were properly setup.
-
-private def getAddFn (type : Expr) (u : Level) : GoalM Expr := do
-  getBinHomoFn type u ``HAdd ``HAdd.hAdd
-
-private def getMulFn (type : Expr) (u : Level) : GoalM Expr := do
-  getBinHomoFn type u ``HMul ``HMul.hMul
-
-private def getSubFn (type : Expr) (u : Level) : GoalM Expr := do
-  getBinHomoFn type u ``HSub ``HSub.hSub
-
-private def getDivFn (type : Expr) (u : Level) : GoalM Expr := do
-  getBinHomoFn type u ``HDiv ``HDiv.hDiv
-
-private def getNegFn (type : Expr) (u : Level) : GoalM Expr := do
-  getUnaryFn type u ``Neg ``Neg.neg
-
-private def getInvFn (type : Expr) (u : Level) : GoalM Expr := do
-  getUnaryFn type u ``Inv ``Inv.inv
-
-private def getPowFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do
-  let inst ← synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.toHPow [u]) type semiringInst
-  unless (← withDefault <| isDefEq inst inst') do
-    throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"
-  internalizeFn <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
-
-private def getIntCastFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do
-  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [u]) type ringInst
-  let instType := mkApp (mkConst ``IntCast [u]) type
-  -- Note that `Ring.intCast` is not registered as a global instance
-  -- (to avoid introducing unwanted coercions)
-  -- so merely having a `Ring α` instance
-  -- does not guarantee that an `IntCast α` will be available.
-  -- When both are present we verify that they are defeq,
-  -- and otherwise fall back to the field of the `Ring α` instance that we already have.
-  let inst ← match (← synthInstance? instType) with
-  | none => pure inst'
-  | some inst =>
-    unless (← withDefault <| isDefEq inst inst') do
-      throwError "instance for intCast{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}"
-    pure inst
-  internalizeFn <| mkApp2 (mkConst ``IntCast.intCast [u]) type inst
-
-private def getNatCastFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
-  let instType := mkApp (mkConst ``NatCast [u]) type
-  -- Note that `Semiring.natCast` is not registered as a global instance
-  -- (to avoid introducing unwanted coercions)
-  -- so merely having a `Semiring α` instance
-  -- does not guarantee that an `NatCast α` will be available.
-  -- When both are present we verify that they are defeq,
-  -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
-  let inst ← match (← synthInstance? instType) with
-  | none => pure inst'
-  | some inst =>
-    unless (← withDefault <| isDefEq inst inst') do
-      throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"
-    pure inst
-  internalizeFn <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
-
 /--
 Returns the ring id for the given type if there is a `CommRing` instance for it.
 
@@ -109,10 +27,6 @@ def getRingId? (type : Expr) : GoalM (Option Nat) := do
   else
     let id? ← go?
     modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
-    if let some id := id? then
-      -- Internalize helper constants
-      let ring := (← get').rings[id]!
-      internalize ring.one 0
     return id?
 where
   go? : GoalM (Option Nat) := do
@@ -127,24 +41,12 @@ where
     let noZeroDivInst? ← getNoZeroDivInst? u type
     trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
     let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-    let addFn ← getAddFn type u
-    let mulFn ← getMulFn type u
-    let subFn ← getSubFn type u
-    let negFn ← getNegFn type u
-    let powFn ← getPowFn type u semiringInst
-    let intCastFn ← getIntCastFn type u ringInst
-    let natCastFn ← getNatCastFn type u semiringInst
-    let invFn? ← if fieldInst?.isSome then
-      pure (some (← getInvFn type u))
-    else
-      pure none
-    let one ← shareCommon <| (← canon <| denoteNumCore u type semiringInst negFn 1)
     let semiringId? := none
     let id := (← get').rings.size
     let ring : Ring := {
       id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
       commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-      addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn, invFn?, one }
+    }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id
 
@@ -164,22 +66,12 @@ where
     let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
     let some commSemiringInst ← synthInstance? commSemiring | return none
     let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
-    let toQFn ← internalizeFn <| mkApp2 (mkConst ``Grind.Ring.OfSemiring.toQ [u]) type semiringInst
-    let addFn ← getAddFn type u
-    let mulFn ← getMulFn type u
-    let powFn ← getPowFn type u semiringInst
-    let natCastFn ← getNatCastFn type u semiringInst
-    let add := mkApp (mkConst ``Add [u]) type
-    let some addInst ← synthInstance? add | return none
-    let addRightCancel := mkApp2 (mkConst ``Grind.AddRightCancel [u]) type addInst
-    let addRightCancelInst? ← synthInstance? addRightCancel
     let q ← shareCommon (← canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
     let some ringId ← getRingId? q
       | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr q}"
     let id := (← get').semirings.size
     let semiring : Semiring := {
-      id, type, ringId, u, semiringInst, commSemiringInst,
-      addFn, mulFn, powFn, natCastFn, toQFn, addRightCancelInst?
+      id, type, ringId, u, semiringInst, commSemiringInst
     }
     modify' fun s => { s with semirings := s.semirings.push semiring }
     setSemiringId ringId id
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
index 8590389193..c2fd140749 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
@@ -165,16 +165,16 @@ structure Ring where
   noZeroDivInst? : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?     : Option Expr
-  addFn          : Expr
-  mulFn          : Expr
-  subFn          : Expr
-  negFn          : Expr
-  powFn          : Expr
-  intCastFn      : Expr
-  natCastFn      : Expr
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  subFn?         : Option Expr := none
+  negFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  intCastFn?     : Option Expr := none
+  natCastFn?     : Option Expr := none
   /-- Inverse if `fieldInst?` is `some inst` -/
-  invFn?         : Option Expr
-  one            : Expr
+  invFn?         : Option Expr := none
+  one?           : Option Expr := none
   /--
   Mapping from variables to their denotations.
   Remark each variable can be in only one ring.
@@ -230,12 +230,12 @@ structure Semiring where
   /-- `CommSemiring` instance for `type` -/
   commSemiringInst   : Expr
   /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option Expr
-  toQFn          : Expr
-  addFn          : Expr
-  mulFn          : Expr
-  powFn          : Expr
-  natCastFn      : Expr
+  addRightCancelInst? : Option (Option Expr) := none
+  toQFn?         : Option Expr := none
+  addFn?         : Option Expr := none
+  mulFn?         : Option Expr := none
+  powFn?         : Option Expr := none
+  natCastFn?     : Option Expr := none
   /-- Mapping from Lean expressions to their representations as `SemiringExpr` -/
   denote         : PHashMap ExprPtr SemiringExpr := {}
   /--
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
index ed87248faf..570deac995 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Tactic.Grind.Canon
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 
 namespace Lean.Meta.Grind.Arith.CommRing
@@ -36,14 +38,34 @@ structure RingM.Context where
   -/
   checkCoeffDvd : Bool := false
 
-class MonadGetRing (m : Type → Type) where
+class MonadRing (m : Type → Type) where
   getRing : m Ring
+  modifyRing : (Ring → Ring) → m Unit
+  /--
+  Helper function for removing dependency on `GoalM`.
+  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
+  When printing counterexamples, we are at `MetaM`, and this is just the identity function.
+  -/
+  canonExpr : Expr → m Expr
+  /--
+  Helper function for removing dependency on `GoalM`. During search we
+  want to track the instances synthesized by `grind`, and this is `Grind.synthInstance`.
+  -/
+  synthInstance? : Expr → m (Option Expr)
 
-export MonadGetRing (getRing)
+export MonadRing (getRing modifyRing canonExpr)
 
 @[always_inline]
-instance (m n) [MonadLift m n] [MonadGetRing m] : MonadGetRing n where
+instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
   getRing    := liftM (getRing : m Ring)
+  modifyRing f := liftM (modifyRing f : m Unit)
+  canonExpr e := liftM (canonExpr e : m Expr)
+  synthInstance? e := liftM (MonadRing.synthInstance? e : m (Option Expr))
+
+def MonadRing.synthInstance [Monad m] [MonadError m] [MonadRing m] (type : Expr) : m Expr := do
+  let some inst ← synthInstance? type
+    | throwError "`grind` failed to find instance{indentExpr type}"
+  return inst
 
 /-- We don't want to keep carrying the `RingId` around. -/
 abbrev RingM := ReaderT RingM.Context GoalM
@@ -62,12 +84,13 @@ protected def RingM.getRing : RingM Ring := do
   else
     throwError "`grind` internal error, invalid ringId"
 
-instance : MonadGetRing RingM where
+instance : MonadRing RingM where
   getRing := RingM.getRing
-
-@[inline] def modifyRing (f : Ring → Ring) : RingM Unit := do
-  let ringId ← getRingId
-  modify' fun s => { s with rings := s.rings.modify ringId f }
+  modifyRing f := do
+    let ringId ← getRingId
+    modify' fun s => { s with rings := s.rings.modify ringId f }
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 structure SemiringM.Context where
   semiringId : Nat
@@ -96,8 +119,13 @@ protected def SemiringM.getRing : SemiringM Ring := do
   else
     throwError "`grind` internal error, invalid ringId"
 
-instance : MonadGetRing SemiringM where
+instance : MonadRing SemiringM where
   getRing := SemiringM.getRing
+  modifyRing f := do
+    let ringId := (← getSemiring).ringId
+    modify' fun s => { s with rings := s.rings.modify ringId f }
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 @[inline] def modifySemiring (f : Semiring → Semiring) : SemiringM Unit := do
   let semiringId ← getSemiringId
@@ -132,14 +160,14 @@ def setTermSemiringId (e : Expr) : SemiringM Unit := do
   modify' fun s => { s with exprToSemiringId := s.exprToSemiringId.insert { expr := e } semiringId }
 
 /-- Returns `some c` if the current ring has a nonzero characteristic `c`. -/
-def nonzeroChar? [Monad m] [MonadGetRing m] : m (Option Nat) := do
+def nonzeroChar? [Monad m] [MonadRing m] : m (Option Nat) := do
   if let some (_, c) := (← getRing).charInst? then
     if c != 0 then
       return some c
   return none
 
 /-- Returns `some (charInst, c)` if the current ring has a nonzero characteristic `c`. -/
-def nonzeroCharInst? [Monad m] [MonadGetRing m] : m (Option (Expr × Nat)) := do
+def nonzeroCharInst? [Monad m] [MonadRing m] : m (Option (Expr × Nat)) := do
   if let some (inst, c) := (← getRing).charInst? then
     if c != 0 then
       return some (inst, c)
@@ -181,4 +209,176 @@ def getNext? : RingM (Option EqCnstr) := do
   incSteps
   return some c
 
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m]
+
+private def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : m Expr := do
+  let inst ← MonadRing.synthInstance <| mkApp (mkConst instDeclName [u]) type
+  canonExpr <| mkApp2 (mkConst declName [u]) type inst
+
+private def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : m Expr := do
+  let inst ← MonadRing.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
+  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
+
+def getAddFn : m Expr := do
+  let ring ← getRing
+  if let some addFn := ring.addFn? then return addFn
+  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd
+  modifyRing fun s => { s with addFn? := some addFn }
+  return addFn
+
+def getSubFn : m Expr := do
+  let ring ← getRing
+  if let some subFn := ring.subFn? then return subFn
+  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub
+  modifyRing fun s => { s with subFn? := some subFn }
+  return subFn
+
+def getMulFn : m Expr := do
+  let ring ← getRing
+  if let some mulFn := ring.mulFn? then return mulFn
+  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul
+  modifyRing fun s => { s with mulFn? := some mulFn }
+  return mulFn
+
+def getNegFn : m Expr := do
+  let ring ← getRing
+  if let some negFn := ring.negFn? then return negFn
+  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg
+  modifyRing fun s => { s with negFn? := some negFn }
+  return negFn
+
+def getInvFn : m Expr := do
+  let ring ← getRing
+  if ring.fieldInst?.isNone then
+    throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
+  if let some invFn := ring.invFn? then return invFn
+  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv
+  modifyRing fun s => { s with invFn? := some invFn }
+  return invFn
+
+private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let inst ← MonadRing.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
+  let inst' := mkApp2 (mkConst ``Grind.Semiring.toHPow [u]) type semiringInst
+  checkInst inst inst'
+  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
+where
+  checkInst (inst inst' : Expr) : MetaM Unit := do
+    unless (← withDefault <| isDefEq inst inst') do
+      throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"
+
+def getPowFn : m Expr := do
+  let ring ← getRing
+  if let some powFn := ring.powFn? then return powFn
+  let powFn ← mkPowFn ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with powFn? := some powFn }
+  return powFn
+
+def getIntCastFn : m Expr := do
+  let ring ← getRing
+  if let some intCastFn := ring.intCastFn? then return intCastFn
+  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
+  let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
+  -- Note that `Ring.intCast` is not registered as a global instance
+  -- (to avoid introducing unwanted coercions)
+  -- so merely having a `Ring α` instance
+  -- does not guarantee that an `IntCast α` will be available.
+  -- When both are present we verify that they are defeq,
+  -- and otherwise fall back to the field of the `Ring α` instance that we already have.
+  let inst ← match (← MonadRing.synthInstance? instType) with
+    | none => pure inst'
+    | some inst => checkInst inst inst'; pure inst
+  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
+  modifyRing fun s => { s with intCastFn? := some intCastFn }
+  return intCastFn
+where
+  checkInst (inst inst' : Expr) : MetaM Unit := do
+    unless (← withDefault <| isDefEq inst inst') do
+      throwError "instance for intCast{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}"
+
+private def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
+  let instType := mkApp (mkConst ``NatCast [u]) type
+  -- Note that `Semiring.natCast` is not registered as a global instance
+  -- (to avoid introducing unwanted coercions)
+  -- so merely having a `Semiring α` instance
+  -- does not guarantee that an `NatCast α` will be available.
+  -- When both are present we verify that they are defeq,
+  -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
+  let inst ← match (← MonadRing.synthInstance? instType) with
+  | none => pure inst'
+  | some inst => checkInst inst inst'; pure inst
+  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
+where
+  checkInst (inst inst' : Expr) : MetaM Unit := do
+    unless (← withDefault <| isDefEq inst inst') do
+      throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"
+
+def getNatCastFn : m Expr := do
+  let ring ← getRing
+  if let some natCastFn := ring.natCastFn? then return natCastFn
+  let natCastFn ← mkNatCastFn ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with natCastFn? := some natCastFn }
+  return natCastFn
+
+private def mkOne (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
+  let n := mkRawNatLit 1
+  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [u]) type semiringInst n
+  canonExpr <| mkApp3 (mkConst ``OfNat.ofNat [u]) type n ofNatInst
+
+def getOne [MonadLiftT GoalM m] : m Expr := do
+  let ring ← getRing
+  if let some one := ring.one? then return one
+  let one ← mkOne ring.u ring.type ring.semiringInst
+  modifyRing fun s => { s with one? := some one }
+  internalize one 0
+  return one
+
+def getAddFn' : SemiringM Expr := do
+  let s ← getSemiring
+  if let some addFn := s.addFn? then return addFn
+  let addFn ← mkBinHomoFn s.type s.u ``HAdd ``HAdd.hAdd
+  modifySemiring fun s => { s with addFn? := some addFn }
+  return addFn
+
+def getMulFn' : SemiringM Expr := do
+  let s ← getSemiring
+  if let some mulFn := s.mulFn? then return mulFn
+  let mulFn ← mkBinHomoFn s.type s.u ``HMul ``HMul.hMul
+  modifySemiring fun s => { s with mulFn? := some mulFn }
+  return mulFn
+
+def getPowFn' : SemiringM Expr := do
+  let s ← getSemiring
+  if let some powFn := s.powFn? then return powFn
+  let powFn ← mkPowFn s.u s.type s.semiringInst
+  modifySemiring fun s => { s with powFn? := some powFn }
+  return powFn
+
+def getNatCastFn' : SemiringM Expr := do
+  let s ← getSemiring
+  if let some natCastFn := s.natCastFn? then return natCastFn
+  let natCastFn ← mkNatCastFn s.u s.type s.semiringInst
+  modifySemiring fun s => { s with natCastFn? := some natCastFn }
+  return natCastFn
+
+def getToQFn : SemiringM Expr := do
+  let s ← getSemiring
+  if let some toQFn := s.toQFn? then return toQFn
+  let toQFn ← canonExpr <| mkApp2 (mkConst ``Grind.Ring.OfSemiring.toQ [s.u]) s.type s.semiringInst
+  modifySemiring fun s => { s with toQFn? := some toQFn }
+  return toQFn
+
+private def mkAddRightCancelInst? (u : Level) (type : Expr) : GoalM (Option Expr) := do
+  let add := mkApp (mkConst ``Add [u]) type
+  let some addInst ← synthInstance? add | return none
+  let addRightCancel := mkApp2 (mkConst ``Grind.AddRightCancel [u]) type addInst
+  synthInstance? addRightCancel
+
+def getAddRightCancelInst? : SemiringM (Option Expr) := do
+  let s ← getSemiring
+  if let some r := s.addRightCancelInst? then return r
+  let addRightCancelInst? ← mkAddRightCancelInst? s.u s.type
+  modifySemiring fun s => { s with addRightCancelInst? := some addRightCancelInst? }
+  return addRightCancelInst?
+
 end Lean.Meta.Grind.Arith.CommRing
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean
index aea8d21cb3..65725ef92a 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean
@@ -67,8 +67,13 @@ def getRing : LinearM Ring := do
     | throwNotCommRing
   return ring
 
-instance : MonadGetRing LinearM where
+instance : MonadRing LinearM where
   getRing := Linear.getRing
+  modifyRing f := do
+    let some ringId := (← getStruct).ringId? | throwNotCommRing
+    RingM.run ringId do modifyRing f
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
 
 def getZero : LinearM Expr :=
   return (← getStruct).zero
diff --git a/tests/lean/run/grind_const_pattern.lean b/tests/lean/run/grind_const_pattern.lean
index ec78f5ee80..263496f97d 100644
--- a/tests/lean/run/grind_const_pattern.lean
+++ b/tests/lean/run/grind_const_pattern.lean
@@ -18,7 +18,7 @@ h : ¬a = 10
   [eqc] False propositions
     [prop] a = 10
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 2
+    [assign] a := 1
 -/
 #guard_msgs (error) in
 example : a = 5 + 5 := by
@@ -49,8 +49,8 @@ h : ¬f a = 11
   [eqc] False propositions
     [prop] f a = 11
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 3
-    [assign] f a := 2
+    [assign] a := 2
+    [assign] f a := 1
 -/
 #guard_msgs (error) in
 example : f a = 10 + 1 := by
@@ -75,9 +75,9 @@ h : ¬f x = 11
   [ematch] E-matching patterns
     [thm] fa: [f `[a]]
   [cutsat] Assignment satisfying linear constraints
-    [assign] x := 4
-    [assign] a := 3
-    [assign] f x := 2
+    [assign] x := 3
+    [assign] a := 2
+    [assign] f x := 1
 -/
 #guard_msgs (error) in
 example : f x = 10 + 1 := by
diff --git a/tests/lean/run/grind_cutsat_diseq_2.lean b/tests/lean/run/grind_cutsat_diseq_2.lean
index 4543e2529e..bf61106b5c 100644
--- a/tests/lean/run/grind_cutsat_diseq_2.lean
+++ b/tests/lean/run/grind_cutsat_diseq_2.lean
@@ -12,7 +12,6 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by
 
 /--
 trace: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
-[grind.cutsat.assert] -1*「1」 + 1 = 0
 [grind.cutsat.assert] -1*「0」 = 0
 [grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0
 [grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean
index 69ce2674e8..5cad76a446 100644
--- a/tests/lean/run/grind_cutsat_div_1.lean
+++ b/tests/lean/run/grind_cutsat_div_1.lean
@@ -22,7 +22,6 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3 
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 0
-[grind.debug.cutsat.search.assign] 「1」 := 1
 -/
 #guard_msgs (trace) in -- finds the model without any backtracking
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -31,12 +30,10 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
   sorry
 
 /--
-trace: [grind.cutsat.assert] -1*「1」 + 1 = 0
-[grind.cutsat.assert] 2 ∣ a + 3
+trace: [grind.cutsat.assert] 2 ∣ a + 3
 [grind.cutsat.assert] 3 ∣ a + 3*b + -4
 [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 0
-[grind.debug.cutsat.search.assign] 「1」 := 1
 -/
 #guard_msgs (trace) in
 set_option trace.grind.cutsat.assert true in
@@ -48,7 +45,6 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 15
-[grind.debug.cutsat.search.assign] 「1」 := 1
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -59,7 +55,6 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 12
-[grind.debug.cutsat.search.assign] 「1」 := 1
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -70,8 +65,8 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): Fals
 /--
 trace: [grind.debug.cutsat.search.assign] f 0 := 11
 [grind.debug.cutsat.search.assign] f 1 := 2
-[grind.debug.cutsat.search.assign] 「0」 := 0
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index 3a96834747..f8c405329c 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -3,7 +3,6 @@ open Int.Linear
 
 /--
 trace: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
-[grind.cutsat.assert] -1*「1」 + 1 = 0
 [grind.cutsat.assert] -1*「0」 = 0
 [grind.cutsat.assert] 「b + f a + 1」 = 0
 -/
diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean
index 2458de0e23..1cfdfde2af 100644
--- a/tests/lean/run/grind_cutsat_nat_le.lean
+++ b/tests/lean/run/grind_cutsat_nat_le.lean
@@ -30,7 +30,6 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
 trace: [grind.cutsat.assert] -1*↑a ≤ 0
 [grind.cutsat.assert] -1*↑b ≤ 0
 [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
-[grind.cutsat.assert] -1*「1」 + 1 = 0
 [grind.cutsat.assert] -1*↑c ≤ 0
 [grind.cutsat.assert] -1*「↑a * ↑b + -1 * ↑c + 1」 + 「↑a * ↑b」 + -1*↑c + 1 = 0
 [grind.cutsat.assert] 「↑a * ↑b」 + -1*↑c + 1 ≤ 0
diff --git a/tests/lean/run/grind_split_issue.lean b/tests/lean/run/grind_split_issue.lean
index f7bda50cdf..435ab672d2 100644
--- a/tests/lean/run/grind_split_issue.lean
+++ b/tests/lean/run/grind_split_issue.lean
@@ -26,7 +26,7 @@ h_1 : ⋯ ≍ ⋯
     [cases] [1/2]: X c 0
       [cases] source: Initial goal
   [cutsat] Assignment satisfying linear constraints
-    [assign] c := 2
+    [assign] c := 1
     [assign] s := 0
 -/
 #guard_msgs (error) in