chore: dep

src/Lean/Meta/Match/Basic.lean

@@ -364,4 +364,15 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
           let fields ← fields.mapM toPattern
           return Pattern.ctor v.name us params.toList fields.toList
 
+/-! Match congruence equational theorem names helper declarations and functions -/
+
+def congrEqnThmSuffixBase := "congr_eq"
+def congrEqnThmSuffixBasePrefix := congrEqnThmSuffixBase ++ "_"
+def congrEqn1ThmSuffix := congrEqnThmSuffixBasePrefix ++ "1"
+example : congrEqn1ThmSuffix = "congr_eq_1" := rfl
+
+/-- Returns `true` if `s` is of the form `congr_eq_<idx>` -/
+def isCongrEqnReservedNameSuffix (s : String) : Bool :=
+  congrEqnThmSuffixBasePrefix.isPrefixOf s && (s.drop congrEqnThmSuffixBasePrefix.length).isNat
+
 end Lean.Meta.Match

src/Lean/Meta/Match/MatchEqs.lean

@@ -834,15 +834,6 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
       let result := { eqnNames, splitterName, splitterAltNumParams }
       registerMatchEqns matchDeclName result
 
-def congrEqnThmSuffixBase := "congr_eq"
-def congrEqnThmSuffixBasePrefix := congrEqnThmSuffixBase ++ "_"
-def congrEqn1ThmSuffix := congrEqnThmSuffixBasePrefix ++ "1"
-example : congrEqn1ThmSuffix = "congr_eq_1" := rfl
-
-/-- Returns `true` if `s` is of the form `congr_eq_<idx>` -/
-def isCongrEqnReservedNameSuffix (s : String) : Bool :=
-  congrEqnThmSuffixBasePrefix.isPrefixOf s && (s.drop congrEqnThmSuffixBasePrefix.length).isNat
-
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchCongrEqnsExt : EnvExtension (PHashMap Name (Array Name)) ←
   -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`.

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

@@ -12,7 +12,9 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof

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

@@ -4,15 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.OfSemiring
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 /-!
 Helper functions for converting reified terms back into their denotations.
@@ -91,14 +88,4 @@ def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
 def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
   return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
 
-def _root_.Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr (e : SemiringExpr) : SemiringM Expr := do
-  shareCommon (← go e)
-where
-  go : SemiringExpr → SemiringM Expr
-  | .num k => denoteNum 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

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

@@ -12,6 +12,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 
 public section
 

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

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m]
+
+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
+
+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 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.npow [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 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'}"
+
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m]
+
+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
+
+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'}"
+
+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
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+def get' : GoalM State := do
+  return (← get).arith.ring
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  modify fun s => { s with arith.ring := f s.arith.ring }
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -10,6 +10,7 @@ public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 
 public section
 

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

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 
 public section

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

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+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 MonadRing (getRing modifyRing canonExpr)
+
+@[always_inline]
+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
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
 
 private abbrev M := StateT Ring MetaM

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

@@ -13,8 +13,10 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 
 public section
 

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

@@ -7,9 +7,9 @@ module
 
 prelude
 public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
-
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing

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

@@ -11,7 +11,7 @@ public import Init.Grind.Ring.Envelope
 public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.Insts
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 
 public section
 

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

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+def checkMaxSteps : GoalM Bool := do
+  return (← get').steps >= (← getConfig).ringSteps
+
+def incSteps : GoalM Unit := do
+  modify' fun s => { s with steps := s.steps + 1 }
+
+structure RingM.Context where
+  ringId : Nat
+  /--
+  If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p`
+  to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF
+  - `k` divides `k'`, OR
+  - Ring implements `NoNatZeroDivisors`.
+
+  We need this check when simplifying disequalities. In this case, if we perform
+  the simplification anyway, we may end up with a proof that `k * q = 0`, but
+  we cannot deduce `q = 0` since the ring does not implement `NoNatZeroDivisors`
+  See comment at `PolyDerivation`.
+  -/
+  checkCoeffDvd : Bool := false
+
+/-- We don't want to keep carrying the `RingId` around. -/
+abbrev RingM := ReaderT RingM.Context GoalM
+
+abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
+  x { ringId }
+
+abbrev getRingId : RingM Nat :=
+  return (← read).ringId
+
+protected def RingM.getRing : RingM Ring := do
+  let s ← get'
+  let ringId ← getRingId
+  if h : ringId < s.rings.size then
+    return s.rings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+protected def modifyRing (f : Ring → Ring) : RingM Unit := do
+  let ringId ← getRingId
+  modify' fun s => { s with rings := s.rings.modify ringId f }
+
+instance : MonadRing RingM where
+  getRing := RingM.getRing
+  modifyRing := CommRing.modifyRing
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
+abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
+  withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
+
+def checkCoeffDvd : RingM Bool :=
+  return (← read).checkCoeffDvd
+
+def getTermRingId? (e : Expr) : GoalM (Option Nat) := do
+  return (← get').exprToRingId.find? { expr := e }
+
+def setTermRingId (e : Expr) : RingM Unit := do
+  let ringId ← getRingId
+  if let some ringId' ← getTermRingId? e then
+    unless ringId' == ringId do
+      reportIssue! "expression in two different rings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
+
+/-- Returns `some c` if the current ring has a nonzero characteristic `c`. -/
+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] [MonadRing m] : m (Option (Expr × Nat)) := do
+  if let some (inst, c) := (← getRing).charInst? then
+    if c != 0 then
+      return some (inst, c)
+  return none
+
+def noZeroDivisorsInst? : RingM (Option Expr) := do
+  return (← getRing).noZeroDivInst?
+
+/--
+Returns `true` if the current ring satisfies the property
+```
+∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
+```
+-/
+def noZeroDivisors : RingM Bool := do
+  return (← getRing).noZeroDivInst?.isSome
+
+/-- Returns `true` if the current ring has a `IsCharP` instance. -/
+def hasChar  : RingM Bool := do
+  return (← getRing).charInst?.isSome
+
+/--
+Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
+-/
+def getCharInst : RingM (Expr × Nat) := do
+  let some c := (← getRing).charInst?
+    | throwError "`grind` internal error, ring does not have a characteristic"
+  return c
+
+def isField : RingM Bool :=
+  return (← getRing).fieldInst?.isSome
+
+def isQueueEmpty : RingM Bool :=
+  return (← getRing).queue.isEmpty
+
+def getNext? : RingM (Option EqCnstr) := do
+  let some c := (← getRing).queue.min? | return none
+  modifyRing fun s => { s with queue := s.queue.erase c }
+  incSteps
+  return some c
+
+def mkVar (e : Expr) : RingM Var := do
+  let s ← getRing
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifyRing fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermRingId e
+  markAsCommRingTerm e
+  return var
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -4,19 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
-
 namespace Lean.Meta.Grind.Arith.CommRing
-
 /-!
 The polynomial functions at `Poly.lean` are used for constructing proofs-by-reflection,
 but they do not provide mechanisms for aborting expensive computations.
 -/
-
 private def applyChar (a : Int) : RingM Int := do
   if let some c ← nonzeroChar? then
     return a % c

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

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Grind.Ring.OfSemiring
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.SynthInstance
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.GetSet
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+structure SemiringM.Context where
+  semiringId : Nat
+
+abbrev SemiringM := ReaderT SemiringM.Context GoalM
+
+abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α :=
+  x { semiringId }
+
+abbrev getSemiringId : SemiringM Nat :=
+  return (← read).semiringId
+
+def getSemiring : SemiringM Semiring := do
+  let s ← get'
+  let semiringId ← getSemiringId
+  if h : semiringId < s.semirings.size then
+    return s.semirings[semiringId]
+  else
+    throwError "`grind` internal error, invalid semiringId"
+
+protected def SemiringM.getRing : SemiringM Ring := do
+  let s ← get'
+  let ringId := (← getSemiring).ringId
+  if h : ringId < s.rings.size then
+    return s.rings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+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
+  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
+
+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?
+
+def getTermSemiringId? (e : Expr) : GoalM (Option Nat) := do
+  return (← get').exprToSemiringId.find? { expr := e }
+
+def setTermSemiringId (e : Expr) : SemiringM Unit := do
+  let semiringId ← getSemiringId
+  if let some semiringId' ← getTermSemiringId? e then
+    unless semiringId' == semiringId do
+      reportIssue! "expression in two different semirings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToSemiringId := s.exprToSemiringId.insert { expr := e } semiringId }
+
+/-- Similar to `mkVar` but for `Semiring`s -/
+def mkSVar (e : Expr) : SemiringM Var := do
+  let s ← getSemiring
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifySemiring fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermSemiringId e
+  markAsCommRingTerm e
+  return var
+
+def _root_.Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr (e : SemiringExpr) : SemiringM Expr := do
+  shareCommon (← go e)
+where
+  go : SemiringExpr → SemiringM Expr
+  | .num k => denoteNum 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

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

@@ -1,388 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Meta.Tactic.Grind.Canon
-public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
-
-public section
-
-namespace Lean.Meta.Grind.Arith.CommRing
-
-def get' : GoalM State := do
-  return (← get).arith.ring
-
-@[inline] def modify' (f : State → State) : GoalM Unit := do
-  modify fun s => { s with arith.ring := f s.arith.ring }
-
-def checkMaxSteps : GoalM Bool := do
-  return (← get').steps >= (← getConfig).ringSteps
-
-def incSteps : GoalM Unit := do
-  modify' fun s => { s with steps := s.steps + 1 }
-
-structure RingM.Context where
-  ringId : Nat
-  /--
-  If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p`
-  to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF
-  - `k` divides `k'`, OR
-  - Ring implements `NoNatZeroDivisors`.
-
-  We need this check when simplifying disequalities. In this case, if we perform
-  the simplification anyway, we may end up with a proof that `k * q = 0`, but
-  we cannot deduce `q = 0` since the ring does not implement `NoNatZeroDivisors`
-  See comment at `PolyDerivation`.
-  -/
-  checkCoeffDvd : Bool := false
-
-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 MonadRing (getRing modifyRing canonExpr)
-
-@[always_inline]
-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
-
-abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
-  x { ringId }
-
-abbrev getRingId : RingM Nat :=
-  return (← read).ringId
-
-protected def RingM.getRing : RingM Ring := do
-  let s ← get'
-  let ringId ← getRingId
-  if h : ringId < s.rings.size then
-    return s.rings[ringId]
-  else
-    throwError "`grind` internal error, invalid ringId"
-
-instance : MonadRing RingM where
-  getRing := RingM.getRing
-  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
-
-abbrev SemiringM := ReaderT SemiringM.Context GoalM
-
-abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α :=
-  x { semiringId }
-
-abbrev getSemiringId : SemiringM Nat :=
-  return (← read).semiringId
-
-def getSemiring : SemiringM Semiring := do
-  let s ← get'
-  let semiringId ← getSemiringId
-  if h : semiringId < s.semirings.size then
-    return s.semirings[semiringId]
-  else
-    throwError "`grind` internal error, invalid semiringId"
-
-protected def SemiringM.getRing : SemiringM Ring := do
-  let s ← get'
-  let ringId := (← getSemiring).ringId
-  if h : ringId < s.rings.size then
-    return s.rings[ringId]
-  else
-    throwError "`grind` internal error, invalid ringId"
-
-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
-  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
-
-abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
-  withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
-
-def checkCoeffDvd : RingM Bool :=
-  return (← read).checkCoeffDvd
-
-def getTermRingId? (e : Expr) : GoalM (Option Nat) := do
-  return (← get').exprToRingId.find? { expr := e }
-
-def setTermRingId (e : Expr) : RingM Unit := do
-  let ringId ← getRingId
-  if let some ringId' ← getTermRingId? e then
-    unless ringId' == ringId do
-      reportIssue! "expression in two different rings{indentExpr e}"
-    return ()
-  modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
-
-def getTermSemiringId? (e : Expr) : GoalM (Option Nat) := do
-  return (← get').exprToSemiringId.find? { expr := e }
-
-def setTermSemiringId (e : Expr) : SemiringM Unit := do
-  let semiringId ← getSemiringId
-  if let some semiringId' ← getTermSemiringId? e then
-    unless semiringId' == semiringId do
-      reportIssue! "expression in two different semirings{indentExpr e}"
-    return ()
-  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] [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] [MonadRing m] : m (Option (Expr × Nat)) := do
-  if let some (inst, c) := (← getRing).charInst? then
-    if c != 0 then
-      return some (inst, c)
-  return none
-
-def noZeroDivisorsInst? : RingM (Option Expr) := do
-  return (← getRing).noZeroDivInst?
-
-/--
-Returns `true` if the current ring satisfies the property
-```
-∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0
-```
--/
-def noZeroDivisors : RingM Bool := do
-  return (← getRing).noZeroDivInst?.isSome
-
-/-- Returns `true` if the current ring has a `IsCharP` instance. -/
-def hasChar  : RingM Bool := do
-  return (← getRing).charInst?.isSome
-
-/--
-Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
--/
-def getCharInst : RingM (Expr × Nat) := do
-  let some c := (← getRing).charInst?
-    | throwError "`grind` internal error, ring does not have a characteristic"
-  return c
-
-def isField : RingM Bool :=
-  return (← getRing).fieldInst?.isSome
-
-def isQueueEmpty : RingM Bool :=
-  return (← getRing).queue.isEmpty
-
-def getNext? : RingM (Option EqCnstr) := do
-  let some c := (← getRing).queue.min? | return none
-  modifyRing fun s => { s with queue := s.queue.erase c }
-  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.npow [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

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

@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
-
-public section
-
-namespace Lean.Meta.Grind.Arith.CommRing
-
-def mkVar (e : Expr) : RingM Var := do
-  let s ← getRing
-  if let some var := s.varMap.find? { expr := e } then
-    return var
-  let var : Var := s.vars.size
-  modifyRing fun s => { s with
-    vars       := s.vars.push e
-    varMap     := s.varMap.insert { expr := e } var
-  }
-  setTermRingId e
-  markAsCommRingTerm e
-  return var
-
-/-- Similar to `mkVar` but for `Semiring`s -/
-def mkSVar (e : Expr) : SemiringM Var := do
-  let s ← getSemiring
-  if let some var := s.varMap.find? { expr := e } then
-    return var
-  let var : Var := s.vars.size
-  modifySemiring fun s => { s with
-    vars       := s.vars.push e
-    varMap     := s.varMap.insert { expr := e } var
-  }
-  setTermSemiringId e
-  markAsCommRingTerm e
-  return var
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -10,8 +10,8 @@ public import Lean.Meta.Tactic.Grind.ProveEq
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 public section
 
 /-!

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

@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Simp.Arith.Int
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Simp.Arith.Int
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 
 public section
 

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

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Canon
 public import Lean.Meta.Tactic.Grind.MBTC
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 

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

@@ -4,21 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Poly
-public import Lean.Meta.Tactic.Grind.Diseq
-public import Lean.Meta.Tactic.Grind.Arith.Util
-public import Lean.Meta.Tactic.Grind.Arith.ProofUtil
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
-public import Lean.Meta.Tactic.Grind.Arith.VarRename
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
+import Lean.Meta.Tactic.Grind.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public section
 
 namespace Lean.Meta.Grind.Arith.Cutsat

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

@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.ProveEq
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Var
-
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 
 namespace Lean.Meta.Grind.Arith.Linear

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

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Canon
 public import Lean.Meta.Tactic.Grind.MBTC
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Model
 public import Lean.Meta.Tactic.Grind.Arith.Linear.PropagateEq

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

@@ -4,14 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.Tactic.Grind.Arith.Util
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
-public import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
-public import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.Linear.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 

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

@@ -11,7 +11,7 @@ public import Lean.Meta.Tactic.Grind.Simp
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Var
 

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

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 
 public section
 

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -74,7 +74,7 @@ private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do
 Helper function for canonicalizing `e` occurring as the `i`th argument of an `f`-application.
 If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false
 -/
-def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do
+private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do
   let s ← get'
   if let some c := s.canon.find? e then
     return c
@@ -111,9 +111,9 @@ def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBou
   modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
   return e
 
-abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
-abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true)
-abbrev canonImplicit (parent f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore parent f i e (useIsDefEqBounded := true)
+private abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
+private abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true)
+private abbrev canonImplicit (parent f : Expr) (i : Nat) (e : Expr) := withReducible <| canonElemCore parent f i e (useIsDefEqBounded := true)
 
 /--
 Return type for the `shouldCanon` function.
@@ -195,8 +195,8 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       return some <| args.set 0 Int.mkType
   return none
 
-/-- Canonicalizes nested types, type formers, and instances in `e`. -/
-partial def canon (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
+@[export lean_grind_canon]
+partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"
   visit e |>.run' {}
 where
@@ -261,6 +261,4 @@ where
 
 end Canon
 
-export Canon (canon)
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -15,7 +15,9 @@ public import Lean.Meta.Basic
 public import Lean.Meta.InferType
 public import Lean.Meta.Eqns
 public import Lean.Meta.Tactic.Grind.Util
-import Lean.Meta.Match.MatchEqs
+import Lean.Message
+import Lean.Meta.Tactic.FVarSubst
+import Lean.Meta.Match.Basic
 
 public section
 
@@ -310,7 +312,7 @@ def Origin.key : Origin → Name
 
 def Origin.pp [Monad m] [MonadEnv m] [MonadError m] (o : Origin) : m MessageData := do
   match o with
-  | .decl declName => return MessageData.ofConst (← mkConstWithLevelParams declName)
+  | .decl declName => return MessageData.ofConstName declName
   | .fvar fvarId   => return mkFVar fvarId
   | .stx _ ref     => return ref
   | .local id      => return id

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

@@ -15,7 +15,6 @@ public import Lean.Meta.Match.MatchEqs
 public import Lean.Util.CollectLevelParams
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Util
-public import Lean.Meta.Tactic.Grind.Canon
 public import Lean.Meta.Tactic.Grind.Beta
 public import Lean.Meta.Tactic.Grind.MatchCond
 public import Lean.Meta.Tactic.Grind.Arith.Internalize

src/Lean/Meta/Tactic/Grind/MBTC.lean

@@ -4,13 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Canon
-
 public section
-
 namespace Lean.Meta.Grind
 
 /--

src/Lean/Meta/Tactic/Grind/Simp.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Assert
@@ -13,10 +12,7 @@ public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 public import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
-public import Lean.Meta.Tactic.Grind.Canon
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Simplifies the given expression using the `grind` simprocs and normalization theorems. -/

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -1579,4 +1579,8 @@ def withoutModifyingState (x : GoalM α) : GoalM α := do
   finally
     set saved
 
+/-- Canonicalizes nested types, type formers, and instances in `e`. -/
+@[extern "lean_grind_canon"] -- Forward definition
+opaque canon (e : Expr) : GoalM Expr
+
 end Lean.Meta.Grind