checkpoint

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -44,6 +44,26 @@ private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) :=
   let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
   Sym.synthInstance? noZeroDivType
 
+private def getPowIdentityInst? (u : Level) (type : Expr) : SymM (Option (Expr × Expr × Nat)) := do withNewMCtxDepth do
+  -- We use a fresh metavar for `CommSemiring` (unlike `getIsCharInst?` which pins the semiring)
+  -- because `PowIdentity` instances may be declared against a canonical `CommSemiring` instance
+  -- that is not definitionally equal to `CommRing.toCommSemiring`. The synthesized `csInst` is
+  -- stored and used in proof terms to ensure type-correctness.
+  let csInst ← mkFreshExprMVar (mkApp (mkConst ``Grind.CommSemiring [u]) type)
+  let p ← mkFreshExprMVar (mkConst ``Nat)
+  let powIdentityType := mkApp3 (mkConst ``Grind.PowIdentity [u]) type csInst p
+  let some inst ← synthInstance? powIdentityType | return none
+  let csInst ← instantiateMVars csInst
+  let p ← instantiateMVars p
+  let some pVal ← evalNat? p | return none
+  return some (inst, csInst, pVal)
+
+private def mkAddRightCancelInst? (u : Level) (type : Expr) : SymM (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
+
 /-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
 private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
   let u ← getDecLevel type
@@ -55,11 +75,12 @@ private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
   let charInst? ← getIsCharInst? u type semiringInst
   let noZeroDivInst? ← getNoZeroDivInst? u type
   let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+  let powIdentityInst? ← getPowIdentityInst? u type
   let semiringId? := none
   let id := (← getArithState).rings.size
   let ring : CommRing := {
     id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-    commRingInst, charInst?, noZeroDivInst?, fieldInst?,
+    commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?
   }
   modifyArithState fun s => { s with rings := s.rings.push ring }
   return some id
@@ -96,13 +117,14 @@ private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
   let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
   let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
   let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
+  let addRightCancelInst? ← mkAddRightCancelInst? u type
   let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
   -- The envelope `Q` type must be classifiable as a CommRing.
   let some ringId ← tryCacheAndCommRing? q
     | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
   let id := (← getArithState).semirings.size
   let semiring : CommSemiring := {
-    id, type, ringId, u, semiringInst, commSemiringInst
+    id, type, ringId, u, semiringInst, commSemiringInst, addRightCancelInst?
   }
   modifyArithState fun s => { s with semirings := s.semirings.push semiring }
   -- Link the envelope ring back to this semiring

src/Lean/Meta/Sym/Arith/MonadCanon.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Arith.Types
+public import Lean.Meta.Sym.Canon
+public import Lean.Meta.Sym.SynthInstance
 public section
 namespace Lean.Meta.Sym.Arith
 
@@ -33,4 +35,8 @@ def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Exp
     | throwError "failed to find instance{indentExpr type}"
   return inst
 
+instance : MonadCanon SymM where
+  canonExpr := canon
+  synthInstance? := Sym.synthInstance?
+
 end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -21,12 +21,12 @@ instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
 
 /-- Create or lookup a variable for a Lean expression. Used by reification. -/
 class MonadMkVar (m : Type → Type) where
-  mkVar : Expr → m Var
+  mkVar : Expr → (gen : Nat) → m Var
 
 export MonadMkVar (mkVar)
 
 @[always_inline]
 instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
-  mkVar e := liftM (mkVar e : m Var)
+  mkVar e gen := liftM (mkVar e gen : m Var)
 
 end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -57,12 +57,12 @@ If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
 (used for equalities/disequalities). If `false`, treats non-interpreted terms
 as variables (used for inequalities).
 -/
-partial def reifyRing? (e : Expr) (skipVar : Bool := true) : m (Option RingExpr) := do
+partial def reifyRing? (e : Expr) (skipVar : Bool := true) (gen : Nat) : m (Option RingExpr) := do
   let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let asVar (e : Expr) : m RingExpr := do
     reportRingAppIssue e
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let rec go (e : Expr) : m RingExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
@@ -151,12 +151,12 @@ private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
 Converts a Lean expression `e` into a `SemiringExpr`.
 Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
 -/
-partial def reifySemiring? (e : Expr) : m (Option SemiringExpr) := do
+partial def reifySemiring? (e : Expr) (gen : Nat) : m (Option SemiringExpr) := do
   let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let asVar (e : Expr) : m SemiringExpr := do
     reportSemiringAppIssue e
-    return .var (← mkVar e)
+    return .var (← mkVar e gen)
   let rec go (e : Expr) : m SemiringExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>

src/Lean/Meta/Sym/Arith/Types.lean

@@ -71,6 +71,8 @@ structure CommRing extends Ring where
   noZeroDivInst?     : Option Expr
   /-- `Field` instance for `type` if available. -/
   fieldInst?         : Option Expr
+  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
+  powIdentityInst? : Option (Expr × Expr × Nat) := none
   deriving Inhabited
 
 /--
@@ -79,12 +81,12 @@ Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelop
 -/
 structure CommSemiring extends Semiring where
   /-- Id of the envelope ring `OfSemiring.Q type` -/
-  ringId             : Nat
+  ringId              : Nat
   /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
+  commSemiringInst    : Expr
   /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option (Option Expr) := none
-  toQFn?             : Option Expr := none
+  addRightCancelInst? : Option Expr := none
+  toQFn?              : Option Expr := none
   deriving Inhabited
 
 /-- Result of classifying a type's algebraic structure. -/
@@ -96,6 +98,11 @@ inductive ClassifyResult where
   | /-- No algebraic structure found. -/ none
   deriving Inhabited
 
+def ClassifyResult.toOption : ClassifyResult → Option Nat
+ | .commRing id | .nonCommRing id
+ | .commSemiring id | .nonCommSemiring id => some id
+ | .none => .none
+
 /-- Arith type classification state, stored as a `SymExtension`. -/
 structure State where
   /-- Exponent threshold for `HPow` evaluation. -/
@@ -134,4 +141,20 @@ def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
   setExpThreshold exp
   try k finally setExpThreshold oldExp
 
+def getCommRingOfId (id : Nat) : SymM CommRing := do
+  let s ← getArithState
+  return s.rings[id]!
+
+def getNonCommRingOfId (id : Nat) : SymM Ring := do
+  let s ← getArithState
+  return s.ncRings[id]!
+
+def getCommSemiringOfId (id : Nat) : SymM CommSemiring := do
+  let s ← getArithState
+  return s.semirings[id]!
+
+def getNonCommSemiringOfId (id : Nat) : SymM Semiring := do
+  let s ← getArithState
+  return s.ncSemirings[id]!
+
 end Lean.Meta.Sym.Arith

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

@@ -12,17 +12,12 @@ 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.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
-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
-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.PP
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Power
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 builtin_initialize registerTraceClass `grind.ring

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

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2026 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.Types
+public import Lean.Meta.Sym.Arith.DenoteExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+open Sym.Arith
+/-!
+Helper functions for converting reified terms back into their denotations.
+-/
+
+variable [Monad M] [MonadGetVar M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
+
+def mkEq (a b : Expr) : M Expr := do
+  let r ← getRing
+  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
+
+public def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
+  mkEq (← denotePoly c.p) (← denoteNum 0)
+
+public def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
+  denotePoly d.p
+
+public def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
+  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -1,100 +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.Functions
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
-/-!
-Helper functions for converting reified terms back into their denotations.
--/
-
-variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]
-
-def denoteNum (k : Int) : M Expr := do
-  let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst ← if let some inst ← synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
-    pure inst
-  else
-    pure <| 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 (← getPowFn) x (toExpr pw.k)
-
-def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : M Expr := do
-  match m with
-  | .unit => denoteNum 1
-  | .mult pw m => go m (← pw.denoteExpr)
-where
-  go (m : Mon) (acc : Expr) : M Expr := do
-    match m with
-    | .unit => return acc
-    | .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
-  | .num k => denoteNum k
-  | .add k m p => go p (← denoteTerm k m)
-where
-  denoteTerm (k : Int) (m : Mon) : M Expr := do
-    if k == 1 then
-      m.denoteExpr
-    else
-      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 (← getAddFn) acc (← denoteNum k)
-    | .add k m p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k m))
-
-@[specialize]
-private def denoteExprCore (getVar : Nat → Expr) (e : RingExpr) : M Expr := do
-  go e
-where
-  go : RingExpr → M Expr
-  | .num k => denoteNum k
-  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
-  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return getVar x
-  | .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)
-
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
-  let ring ← getRing
-  denoteExprCore (fun x => ring.vars[x]!) e
-
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (vars : Array Expr) (e : RingExpr) : M Expr := do
-  denoteExprCore (fun x => vars[x]!) e
-
-private def mkEq (a b : Expr) : M Expr := do
-  let r ← getRing
-  return mkApp3 (mkConst ``Eq [r.u.succ]) r.type a b
-
-def EqCnstr.denoteExpr (c : EqCnstr) : M Expr := do
-  mkEq (← c.p.denoteExpr) (← denoteNum 0)
-
-def PolyDerivation.denoteExpr (d : PolyDerivation) : M Expr := do
-  d.p.denoteExpr
-
-def DiseqCnstr.denoteExpr (c : DiseqCnstr) : M Expr := do
-  return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -9,9 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

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

@@ -1,143 +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.MonadRing
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
-
-section
-variable [MonadRing m]
-
-def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
-  unless (← isDefEqI inst inst') do
-    throwError "error while initializing `grind ring` operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
-
-def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp2 (mkConst declName [u]) type inst
-
-def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
-
-def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
-  checkInst ``HPow.hPow inst inst'
-  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type 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 (← MonadCanon.synthInstance? instType) with
-  | none => pure inst'
-  | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
-  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
-
-def getAddFn : m Expr := do
-  let ring ← getRing
-  if let some addFn := ring.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [ring.u]) ring.type ring.semiringInst
-  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd expectedInst
-  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 expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
-  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
-  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 expectedInst := mkApp2 (mkConst ``instHMul [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [ring.u]) ring.type ring.semiringInst
-  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul expectedInst
-  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 expectedInst := mkApp2 (mkConst ``Grind.Ring.toNeg [ring.u]) ring.type ring.ringInst
-  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg expectedInst
-  modifyRing fun s => { s with negFn? := some negFn }
-  return negFn
-
-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 (← MonadCanon.synthInstance? instType) with
-    | none => pure inst'
-    | some inst => checkInst ``Int.cast 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
-
-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
-
-section
-variable [MonadCommRing m]
-
-def getInvFn : m Expr := do
-  let ring ← getCommRing
-  let some fieldInst := ring.fieldInst?
-    | throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
-  if let some invFn := ring.invFn? then return invFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
-  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
-  modifyCommRing fun s => { s with invFn? := some invFn }
-  return invFn
-end
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -6,12 +6,16 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Sym.Arith.Reify
+import Lean.Meta.Sym.Arith.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Util
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+open Sym Arith
 
 /-- If `e` is a function application supported by the `CommRing` module, return its type. -/
 private def getType? (e : Expr) : Option Expr :=
@@ -80,8 +84,8 @@ private def processInv (e inst a : Expr) : RingM Unit := do
   unless (← isInvInst inst) do return ()
   let ring ← getCommRing
   let some fieldInst := ring.fieldInst? | return ()
-  if (← getCommRing).invSet.contains a then return ()
-  modifyCommRing fun s => { s with invSet := s.invSet.insert a }
+  if (← getCommRingEntry).invSet.contains a then return ()
+  modifyCommRingEntry fun s => { s with invSet := s.invSet.insert a }
   if let some k ← toInt? a then
     if k == 0 then
       /-
@@ -119,8 +123,9 @@ push the equation `x ^ p = x` as a new fact into grind.
 private def processPowIdentityVars : RingM Unit := do
   let ring ← getCommRing
   let some (powIdentityInst, csInst, p) := ring.powIdentityInst? | return ()
-  let startIdx := ring.powIdentityVarCount
-  let vars := ring.toRing.vars
+  let ringEntry ← getCommRingEntry
+  let startIdx := ringEntry.powIdentityVarCount
+  let vars := ringEntry.vars
   if startIdx >= vars.size then return ()
   for i in [startIdx:vars.size] do
     let x := vars[i]!
@@ -129,7 +134,7 @@ private def processPowIdentityVars : RingM Unit := do
     let proof := mkApp5 (mkConst ``Grind.PowIdentity.pow_eq [ring.u])
       ring.type csInst (mkNatLit p) powIdentityInst x
     pushNewFact proof
-  modifyCommRing fun s => { s with powIdentityVarCount := vars.size }
+  modifyCommRingEntry fun s => { s with powIdentityVarCount := vars.size }
 
 /-- Returns `true` if `e` is a term `a⁻¹`. -/
 private def internalizeInv (e : Expr) : GoalM Bool := do
@@ -148,33 +153,34 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if (← internalizeInv e) then return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
+  let gen ← getGeneration e
   if let some ringId ← getCommRingId? type then RingM.run ringId do
-    let some re ← reify? e | return ()
+    let some re ← reifyRing? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
     setTermRingId e
     ringExt.markTerm e
-    modifyCommRing fun s => { s with
+    modifyCommRingEntry fun s => { s with
       denote := s.denote.insert { expr := e } re
       denoteEntries := s.denoteEntries.push (e, re)
     }
     processPowIdentityVars
   else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
-    let some re ← sreify? e | return ()
+    let some re ← reifySemiring? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"
     setTermSemiringId e
     ringExt.markTerm e
-    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyCommSemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncRingId ← getNonCommRingId? type then NonCommRingM.run ncRingId do
-    let some re ← ncreify? e | return ()
+    let some re ← reifyRing? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "(non-comm) ring [{ncRingId}]: {e}"
     setTermNonCommRingId e
     ringExt.markTerm e
-    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifyRingEntry fun s => { s with denote := s.denote.insert { expr := e } re }
   else if let some ncSemiringId ← getNonCommSemiringId? type then NonCommSemiringM.run ncSemiringId do
-    let some re ← ncsreify? e | return ()
+    let some re ← reifySemiring? e (gen := gen) | return ()
     trace_goal[grind.ring.internalize] "(non-comm) semiring [{ncSemiringId}]: {e}"
     setTermNonCommSemiringId e
     ringExt.markTerm e
-    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
+    modifySemiringEntry fun s => { s with denote := s.denote.insert { expr := e } re }
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Sym.Arith.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-
+/-
 private def checkVars : RingM Unit := do
   let s ← getRing
   let mut num := 0
@@ -42,11 +42,14 @@ private def checkDiseqs : RingM Unit := do
   for c in (← getCommRing).diseqs do
     checkPoly c.d.p
 
+-/
+
 private def checkRingInvs : RingM Unit := do
-  checkVars
-  checkBasis
-  checkQueue
-  checkDiseqs
+  -- checkVars
+  -- checkBasis
+  -- checkQueue
+  -- checkDiseqs
+  return ()
 
 def checkInvariants : GoalM Unit := do
   if (← isDebugEnabled) then

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

@@ -1,40 +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.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-
-class MonadRing (m : Type → Type) where
-  getRing : m Ring
-  modifyRing : (Ring → Ring) → m Unit
-
-export MonadRing (getRing modifyRing)
-
-@[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)
-
-class MonadCommRing (m : Type → Type) where
-  getCommRing : m CommRing
-  modifyCommRing : (CommRing → CommRing) → m Unit
-
-export MonadCommRing (getCommRing modifyCommRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
-  getCommRing      := liftM (getCommRing : m CommRing)
-  modifyCommRing f := liftM (modifyCommRing f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
-  getRing := return (← getCommRing).toRing
-  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -1,40 +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.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-
-class MonadSemiring (m : Type → Type) where
-  getSemiring : m Semiring
-  modifySemiring : (Semiring → Semiring) → m Unit
-
-export MonadSemiring (getSemiring modifySemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadSemiring m] : MonadSemiring n where
-  getSemiring    := liftM (getSemiring : m Semiring)
-  modifySemiring f := liftM (modifySemiring f : m Unit)
-
-class MonadCommSemiring (m : Type → Type) where
-  getCommSemiring : m CommSemiring
-  modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit
-
-export MonadCommSemiring (getCommSemiring modifyCommSemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
-  getCommSemiring      := liftM (getCommSemiring : m CommSemiring)
-  modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
-  getSemiring := return (← getCommSemiring).toSemiring
-  modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -9,30 +9,30 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
+
 structure NonCommRingM.Context where
   ringId : Nat
+  symRingId : Nat
 
 /-- We don't want to keep carrying the `RingId` around. -/
 abbrev NonCommRingM := ReaderT NonCommRingM.Context GoalM
 
-abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α :=
-  x { ringId }
-
-instance : MonadCanon NonCommRingM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α := do
+  let s ← get'
+  let symRingId := s.ncRings[ringId]!.symId
+  x { ringId, symRingId }
 
 protected def NonCommRingM.getRing : NonCommRingM Ring := do
-  let s ← get'
-  let ringId := (← read).ringId
+  let s ← getArithState
+  let ringId := (← read).symRingId
   if h : ringId < s.ncRings.size then
     return s.ncRings[ringId]
   else
     throwError "`grind` internal error, invalid ringId"
 
 protected def NonCommRingM.modifyRing (f : Ring → Ring) : NonCommRingM Unit := do
-  let ringId := (← read).ringId
-  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
+  let ringId := (← read).symRingId
+  modifyArithState fun s => { s with ncRings := s.ncRings.modify ringId f }
 
 instance : MonadRing NonCommRingM where
   getRing := NonCommRingM.getRing
@@ -49,7 +49,37 @@ def setTermNonCommRingId (e : Expr) : NonCommRingM Unit := do
     return ()
   modify' fun s => { s with exprToNCRingId := s.exprToNCRingId.insert { expr := e } ringId }
 
-instance : MonadSetTermId NonCommRingM where
-  setTermId e := setTermNonCommRingId e
+def getRingEntry : NonCommRingM RingEntry := do
+  let s ← get'
+  let ringId := (← read).ringId
+  if h : ringId < s.ncRings.size then
+    return s.ncRings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+def modifyRingEntry (f : RingEntry → RingEntry) : NonCommRingM Unit := do
+  let ringId := (← read).ringId
+  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
+
+def mkNonCommVar (e : Expr) (gen : Nat) : NonCommRingM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getRingEntry
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifyRingEntry fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermNonCommRingId e
+  ringExt.markTerm e
+  return var
+
+instance : MonadMkVar NonCommRingM where
+  mkVar := mkNonCommVar
+
+instance : MonadGetVar NonCommRingM where
+  getVar x := return (← getRingEntry).vars[x]!
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -8,21 +8,36 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
+open Sym.Arith
 
 structure NonCommSemiringM.Context where
   semiringId : Nat
+  symSemiringId : Nat
 
 abbrev NonCommSemiringM := ReaderT NonCommSemiringM.Context GoalM
 
-abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α :=
-  x { semiringId }
-
-instance : MonadCanon NonCommSemiringM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+abbrev NonCommSemiringM.run (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α := do
+  let s ← get'
+  let symSemiringId := s.ncSemirings[semiringId]!.symId
+  x { semiringId, symSemiringId }
 
 protected def NonCommSemiringM.getSemiring : NonCommSemiringM Semiring := do
+  let s ← getArithState
+  let semiringId := (← read).symSemiringId
+  if h : semiringId < s.ncSemirings.size then
+    return s.ncSemirings[semiringId]
+  else
+    throwError "`grind` internal error, invalid semiringId"
+
+protected def NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit := do
+  let semiringId := (← read).symSemiringId
+  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
+
+instance : MonadSemiring NonCommSemiringM where
+  getSemiring := NonCommSemiringM.getSemiring
+  modifySemiring := NonCommSemiringM.modifySemiring
+
+def getSemiringEntry : NonCommSemiringM SemiringEntry := do
   let s ← get'
   let semiringId := (← read).semiringId
   if h : semiringId < s.ncSemirings.size then
@@ -30,14 +45,10 @@ protected def NonCommSemiringM.getSemiring : NonCommSemiringM Semiring := do
   else
     throwError "`grind` internal error, invalid semiringId"
 
-protected def NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit := do
+def modifySemiringEntry (f : SemiringEntry → SemiringEntry) : NonCommSemiringM Unit := do
   let semiringId := (← read).semiringId
   modify' fun s => { s with ncSemirings := s.ncSemirings.modify semiringId f }
 
-instance : MonadSemiring NonCommSemiringM where
-  getSemiring := NonCommSemiringM.getSemiring
-  modifySemiring := NonCommSemiringM.modifySemiring
-
 def getTermNonCommSemiringId? (e : Expr) : GoalM (Option Nat) := do
     return (← get').exprToNCSemiringId.find? { expr := e }
 
@@ -49,7 +60,25 @@ def setTermNonCommSemiringId (e : Expr) : NonCommSemiringM Unit := do
     return ()
   modify' fun s => { s with exprToNCSemiringId := s.exprToNCSemiringId.insert { expr := e } semiringId }
 
-instance : MonadSetTermId NonCommSemiringM where
-  setTermId e := setTermNonCommSemiringId e
+def mkNonCommSVar (e : Expr) (gen : Nat) : NonCommSemiringM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getSemiringEntry
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifySemiringEntry fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermNonCommSemiringId e
+  ringExt.markTerm e
+  return var
+
+instance : MonadMkVar NonCommSemiringM where
+  mkVar := mkNonCommSVar
+
+instance : MonadGetVar NonCommSemiringM where
+  getVar x := return (← getSemiringEntry).vars[x]!
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -6,21 +6,26 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
+import Lean.Meta.Sym.Arith.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
 
-private abbrev M := StateT CommRing MetaM
+private abbrev M := StateT (CommRing × CommRingEntry) MetaM
 
 private instance : MonadCanon M where
   canonExpr e := return e
   synthInstance? e := Meta.synthInstance? e none
 
 private instance : MonadCommRing M where
-  getCommRing := get
-  modifyCommRing := modify
+  getCommRing := return (← get).1
+  modifyCommRing f := modify fun (r, e) => (f r, e)
+
+private instance : MonadGetVar M where
+  getVar x := return (← get).2.vars[x]!
 
 private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array MessageData) : Option MessageData :=
   if msgs.isEmpty then
@@ -31,15 +36,18 @@ 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
 
+private def getCommRingEntry : M CommRingEntry :=
+  return (← get).2
+
 private def ppBasis? : M (Option MessageData) := do
   let mut basis := #[]
-  for c in (← getCommRing).basis do
+  for c in (← getCommRingEntry).basis do
     basis := basis.push (toTraceElem (← c.denoteExpr))
   return toOption `basis "Basis" basis
 
 private def ppDiseqs? : M (Option MessageData) := do
   let mut diseqs := #[]
-  for d in (← getCommRing).diseqs do
+  for d in (← getCommRingEntry).diseqs do
     diseqs := diseqs.push (toTraceElem (← d.denoteExpr))
   return toOption `diseqs "Disequalities" diseqs
 
@@ -51,9 +59,12 @@ private def ppRing? : M (Option MessageData) := do
 
 def pp? (goal : Goal) : MetaM (Option MessageData) := do
   let mut msgs := #[]
-  for ring in (← ringExt.getStateCore goal).rings do
-    let some msg ← ppRing? |>.run' ring | pure ()
-    msgs := msgs.push msg
+  for ringEntry in (← ringExt.getStateCore goal).rings do
+    -- let ring ← getCommRingOfId ringEntry.symId
+    -- let some msg ← ppRing? |>.run' (_, ringEntry) | pure ()
+    -- msgs := msgs.push msg
+    -- TODO: fix
+    pure ()
   if msgs.isEmpty then
     return none
   else if h : msgs.size = 1 then

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

@@ -8,17 +8,18 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Denote
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Sym.Arith.DenoteExpr
 import Lean.Meta.Sym.Arith.ToExpr
 import Lean.Meta.Sym.Arith.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
+open Sym.Arith
 
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
@@ -57,7 +58,7 @@ private def throwNoNatZeroDivisors : RingM α := do
 
 private def getPolyConst (p : Poly) : RingM Int := do
   let .num k := p
-    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
+    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← denotePoly p)}"
   return k
 
 structure ProofM.State where
@@ -135,6 +136,9 @@ private def getSemiringIdOf : RingM Nat := do
 private def getSemiringOf : RingM CommSemiring := do
   SemiringM.run (← getSemiringIdOf) do getCommSemiring
 
+private def getSemiringEntryOf : RingM CommSemiringEntry := do
+  SemiringM.run (← getSemiringIdOf) do getCommSemiringEntry
+
 private def mkSemiringPrefix (declName : Name) : ProofM Expr := do
   let sctx ← getSContext
   let semiring ← getSemiringOf
@@ -143,7 +147,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 ← SemiringM.run (← getSemiringIdOf) do getAddRightCancelInst?
+  let some addRightCancelInst ← SemiringM.run (← getSemiringIdOf) do return (← getCommSemiring).addRightCancelInst?
     | throwError "`grind` internal error, `AddRightCancel` instance is not available"
   return mkApp4 (mkConst declName [semiring.u]) semiring.type semiring.semiringInst addRightCancelInst sctx
 
@@ -241,7 +245,7 @@ private def mkContext (h : Expr) : ProofM Expr := do
     collectMapVars (← get).exprDecls (·.collectVars) <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getRing).vars
+  let vars         := (← getCommRingEntry).vars
   let vars         := vars'.map fun x => vars[x]!
   let h := mkLetOfMap (← get).polyDecls h `p (mkConst ``Grind.CommRing.Poly) fun p => toExpr <| p.renameVars varRename
   let h := mkLetOfMap (← get).monDecls h `m (mkConst ``Grind.CommRing.Mon) fun m => toExpr <| m.renameVars varRename
@@ -258,11 +262,12 @@ private def mkContext (h : Expr) : ProofM Expr := do
 private def mkSemiringContext (h : Expr) : ProofM Expr := do
   let some sctx := (← read).sctx? | return h
   let some semiringId := (← getCommRing).semiringId? | return h
-  let semiring ← getSemiringOf
+  let semiring      ← getSemiringOf
+  let semiringEntry ← getSemiringEntryOf
   let usedVars     := collectMapVars (← get).sexprDecls (·.collectVars) {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := vars'.map fun x => semiring.vars[x]!
+  let vars         := vars'.map fun x => semiringEntry.vars[x]!
   let h := mkLetOfMap (← get).sexprDecls h `s (mkConst ``Grind.CommRing.Expr) fun s => toExpr <| s.renameVars varRename
   let h := h.abstract #[sctx]
   if h.hasLooseBVars then
@@ -327,7 +332,7 @@ def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit :
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := (← getSemiring).vars
+  let vars         := (← getCommSemiringEntry).vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -342,11 +347,12 @@ terms s.t. `ra.toPoly_nc == rb.toPoly_nc`, close the goal.
 -/
 def setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) : NonCommRingM Unit := do
   let ring ← getRing
+  let ringEntry ← getRingEntry
   let hne ← mkDiseqProof a b
   let usedVars     := ra.collectVars >> rb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := ring.vars
+  let vars         := ringEntry.vars
   let vars         := vars'.map fun x => vars[x]!
   let ra           := ra.renameVars varRename
   let rb           := rb.renameVars varRename
@@ -364,11 +370,12 @@ terms s.t. `sa.toPolyS_nc == sb.toPolyS_nc`, close the goal.
 -/
 def setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : NonCommSemiringM Unit := do
   let semiring ← getSemiring
+  let semiringEntry ← getSemiringEntry
   let hne ← mkDiseqProof a b
   let usedVars     := sa.collectVars >> sb.collectVars <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'
-  let vars         := semiring.vars
+  let vars         := semiringEntry.vars
   let vars         := vars'.map fun x => vars[x]!
   let sa           := sa.renameVars varRename
   let sb           := sb.renameVars varRename
@@ -397,7 +404,8 @@ private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResul
 
 def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -409,7 +417,8 @@ def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs
 
 def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -421,7 +430,8 @@ def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst :
 
 def mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getCommRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -436,7 +446,8 @@ Given `e` and `e'` s.t. `e.toPoly == e'.toPoly`, returns a proof that `e.denote
 -/
 def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
   let ring ← getCommRing
-  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
+  let ringEntry ← getCommRingEntry
+  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_eq [ring.u]) ring.type ring.commRingInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue
@@ -446,7 +457,8 @@ def mkTermEqProof (e e' : RingExpr) : RingM Expr := do
 
 def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -458,7 +470,8 @@ def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (l
 
 def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -470,7 +483,8 @@ def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRin
 
 def mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ringEntry ← getRingEntry
+  let { lhs, rhs, lhs', rhs', vars } := norm ringEntry.vars lhs rhs lhs' rhs'
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
   let h := mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
@@ -485,7 +499,8 @@ Given `e` and `e'` s.t. `e.toPoly_nc == e'.toPoly_nc`, returns a proof that `e.d
 -/
 def mkNonCommTermEqProof (e e' : RingExpr) : NonCommRingM Expr := do
   let ring ← getRing
-  let { lhs, lhs', vars, .. } := norm ring.vars e (.num 0) e' (.num 0)
+  let ringEntry ← getRingEntry
+  let { lhs, lhs', vars, .. } := norm ringEntry.vars e (.num 0) e' (.num 0)
   let ctx ← toContextExpr vars
   let h := mkApp2 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst
   let h := mkApp4 h ctx (toExpr lhs) (toExpr lhs') eagerReflBoolTrue

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

@@ -1,203 +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.NonCommRingM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
-public section
-namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
-
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
-
-def isAddInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getAddFn).appArg! inst
-def isMulInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getMulFn).appArg! inst
-def isSubInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getSubFn).appArg! inst
-def isNegInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNegFn).appArg! inst
-def isPowInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getPowFn).appArg! inst
-def isIntCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getIntCastFn).appArg! inst
-def isNatCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNatCastFn).appArg! inst
-
-private def reportAppIssue (e : Expr) : GoalM Unit := do
-  reportIssue! "ring term with unexpected instance{indentExpr e}"
-
-variable [MonadLiftT GoalM m] [MonadSetTermId m]
-
-/--
-Converts a Lean expression `e` in the `CommRing` into a `CommRing.Expr` object.
-
-If `skipVar` is `true`, then the result is `none` if `e` is not an interpreted `CommRing` term.
-We use `skipVar := false` when processing inequalities, and `skipVar := true` for equalities and disequalities
--/
-partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingExpr) := do
-  let mkVar (e : Expr) : m Var := do
-    if (← alreadyInternalized e) then
-      mkVarCore e
-    else
-      internalize e gen
-      mkVarCore e
-  let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m RingExpr := do
-    reportAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m RingExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
-    | HSub.hSub _ _ _ i a b =>
-      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 i) then return .pow (← go a) k else asVar e
-    | Neg.neg _ i a =>
-      if (← isNegInst i) then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i a =>
-      if (← isIntCastInst i) then
-        let some k ← getIntValue? a | toVar e
-        return .intCast k
-      else
-        asVar e
-    | NatCast.natCast _ i a =>
-      if (← isNatCastInst i) then
-        let some k ← getNatValue? a | toVar e
-        return .natCast k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      let some k ← getNatValue? n | toVar e
-      return .num k
-    | BitVec.ofNat _ n =>
-      let some k ← getNatValue? n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option RingExpr) := do
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option RingExpr) := do
-    reportAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HSub.hSub _ _ _ i a b =>
-    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k ← getNatValue? b | asTopVar e
-    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
-  | Neg.neg _ i a =>
-    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
-  | IntCast.intCast _ i a =>
-    if (← isIntCastInst i) then
-      let some k ← getIntValue? a | toTopVar e
-      return some (.intCast k)
-    else
-      asTopVar e
-  | NatCast.natCast _ i a =>
-    if (← isNatCastInst i) then
-      let some k ← getNatValue? a | toTopVar e
-      return some (.natCast k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let some k ← getNatValue? n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-/-- Reify ring expression. -/
-def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option RingExpr) := do
-  reifyCore? e skipVar gen
-
-/-- Reify non-commutative ring expression. -/
-def ncreify? (e : Expr) (skipVar := true) (gen : Nat := 0) : NonCommRingM (Option RingExpr) := do
-  reifyCore? e skipVar gen
-
-private def reportSAppIssue (e : Expr) : GoalM Unit := do
-  reportIssue! "semiring term with unexpected instance{indentExpr e}"
-
-section
-variable [MonadLiftT GoalM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadSetTermId m]
-
-/--
-Similar to `reify?` but for `CommSemiring`
--/
-partial def sreifyCore? (e : Expr) : m (Option SemiringExpr) := do
-  let mkVar (e : Expr) : m Var := do
-    unless (← alreadyInternalized e) do
-      internalize e 0
-    mkSVarCore e
-  let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m SemiringExpr := do
-    reportSAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m SemiringExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      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 (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
-    | NatCast.natCast _ i a =>
-      if isSameExpr (← getNatCastFn').appArg! i then
-        let some k ← getNatValue? a | toVar e
-        return .num k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      let some k ← getNatValue? n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option SemiringExpr) := do
-    return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option SemiringExpr) := do
-    reportSAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    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 (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
-  | NatCast.natCast _ i a =>
-    if isSameExpr (← getNatCastFn').appArg! i then
-      let some k ← getNatValue? a | toTopVar e
-      return some (.num k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let some k ← getNatValue? n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end
-
-/-- Reify semiring expression. -/
-def sreify? (e : Expr) : SemiringM (Option SemiringExpr) := do
-  sreifyCore? e
-
-/-- Reify non-commutative semiring expression. -/
-def ncsreify? (e : Expr) : NonCommSemiringM (Option SemiringExpr) := do
-  sreifyCore? e
-
-end  Lean.Meta.Grind.Arith.CommRing

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

@@ -7,9 +7,10 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Tactic.Grind.Arith.Insts
+import Lean.Meta.Sym.Arith.Classify
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-
+open Sym Arith
 /--
 Returns the ring id for the given type if there is a `CommRing` instance for it.
 
@@ -19,104 +20,75 @@ This function will also perform sanity-checks
 It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
 -/
 def getCommRingId? (type : Expr) : GoalM (Option Nat) := do
-  if let some id? := (← get').typeIdOf.find? { expr := type } then
-    return id?
-  else
-    let id? ← go?
-    modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
-    return id?
-where
-  go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
-    let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
-    let some commRingInst ← synthInstance? commRing | return none
-    let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
-    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-    let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
-    trace_goal[grind.ring] "new ring: {type}"
-    let charInst? ← getIsCharInst? u type semiringInst
-    let noZeroDivInst? ← getNoZeroDivInst? u type
-    trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}"
-    let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-    let powIdentityInst? ← getPowIdentityInst? u type
-    trace_goal[grind.ring] "PowIdentity available: {powIdentityInst?.isSome}"
-    let semiringId? := none
-    let id := (← get').rings.size
-    let ring : CommRing := {
-      id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-      commRingInst, charInst?, noZeroDivInst?, fieldInst?, powIdentityInst?,
-    }
-    modify' fun s => { s with rings := s.rings.push ring }
+  if let some result := (← get').typeClassify.find? { expr := type } then
+    let .commRing id := result | return none
     return some id
+  else
+    let result ← go?
+    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+    return result.toOption
+where
+  go? : GoalM ClassifyResult := do
+    let .commRing symId ← classify? type | return .none
+    let id := (← get').rings.size
+    modify' fun s => { s with rings := s.rings.push { symId, id } }
+    return .commRing id
 
 /--
 Returns the ring id for the given type if there is a `Ring` instance for it.
 This function is invoked only when `getCommRingId?` returns `none`.
 -/
 def getNonCommRingId? (type : Expr) : GoalM (Option Nat) := do
-  if let some id? := (← get').nctypeIdOf.find? { expr := type } then
-    return id?
-  else
-    let id? ← go?
-    modify' fun s => { s with nctypeIdOf := s.nctypeIdOf.insert { expr := type } id? }
-    return id?
-where
-  go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
-    let ring := mkApp (mkConst ``Grind.Ring [u]) type
-    let some ringInst ← synthInstance? ring | return none
-    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-    trace_goal[grind.ring] "new ring: {type}"
-    let charInst? ← getIsCharInst? u type semiringInst
-    let id := (← get').ncRings.size
-    let ring : Ring := {
-      id, type, u, semiringInst, ringInst, charInst?
-    }
-    modify' fun s => { s with ncRings := s.ncRings.push ring }
+  if let some result := (← get').typeClassify.find? { expr := type } then
+    let .nonCommRing id := result | return none
     return some id
+  else
+    let result ← go?
+    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+    return result.toOption
+where
+  go? : GoalM ClassifyResult := do
+    let .nonCommRing symId ← classify? type | return .none
+    let id := (← get').ncRings.size
+    modify' fun s => { s with ncRings := s.ncRings.push { symId, id } }
+    return .nonCommRing id
 
 private def setCommSemiringId (ringId : Nat) (semiringId : Nat) : GoalM Unit := do
   RingM.run ringId do modifyCommRing fun s => { s with semiringId? := some semiringId }
 
 def getCommSemiringId? (type : Expr) : GoalM (Option Nat) := do
-  if let some id? := (← get').stypeIdOf.find? { expr := type } then
-    return id?
-  else
-    let id? ← go?
-    modify' fun s => { s with stypeIdOf := s.stypeIdOf.insert { expr := type } id? }
-    return id?
-where
-  go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
-    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 q ← shareCommon (← canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
-    let some ringId ← getCommRingId? q
-      | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr q}"
-    let id := (← get').semirings.size
-    let semiring : CommSemiring := {
-      id, type, ringId, u, semiringInst, commSemiringInst
-    }
-    modify' fun s => { s with semirings := s.semirings.push semiring }
-    setCommSemiringId ringId id
+  if let some result := (← get').typeClassify.find? { expr := type } then
+    let .commSemiring id := result | return .none
     return some id
+  else
+    let result ← go?
+    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+    return result.toOption
+where
+  go? : GoalM ClassifyResult := do
+    let .commSemiring symId ← classify? type | return .none
+    let s ← getCommSemiringOfId symId
+    let r ← getCommRingOfId s.ringId
+    let some ringId ← getCommRingId? r.type
+      | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr r.type}"
+    let id := (← get').semirings.size
+    modify' fun s => { s with semirings := s.semirings.push { symId, id, ringId } }
+    setCommSemiringId ringId id
+    return .commSemiring id
 
 def getNonCommSemiringId? (type : Expr) : GoalM (Option Nat) := do
-  if let some id? := (← get').ncstypeIdOf.find? { expr := type } then
-    return id?
-  else
-    let id? ← go?
-    modify' fun s => { s with ncstypeIdOf := s.ncstypeIdOf.insert { expr := type } id? }
-    return id?
-where
-  go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
-    let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-    let some semiringInst ← synthInstance? semiring | return none
-    let id := (← get').ncSemirings.size
-    let semiring : Semiring := { id, type, u, semiringInst }
-    modify' fun s => { s with ncSemirings := s.ncSemirings.push semiring }
+  if let some result := (← get').typeClassify.find? { expr := type } then
+    let .nonCommSemiring id := result | return .none
     return some id
+  else
+    let result ← go?
+    modify' fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
+    return result.toOption
+where
+  go? : GoalM ClassifyResult := do
+    let .nonCommSemiring symId ← classify? type | return .none
+    let id := (← get').ncSemirings.size
+    modify' fun s => { s with ncSemirings := s.ncSemirings.push { symId, id } }
+    return .nonCommSemiring id
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -5,8 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.SynthInstance
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Sym.Arith.MonadRing
+public import Lean.Meta.Sym.Arith.MonadVar
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
@@ -19,6 +22,7 @@ def incSteps (n : Nat := 1) : GoalM Unit := do
 
 structure RingM.Context where
   ringId : Nat
+  symRingId : Nat
   /--
   If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p`
   to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF
@@ -35,17 +39,34 @@ structure RingM.Context where
 /-- 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 RingM.run (ringId : Nat) (x : RingM α) : GoalM α := do
+  let s ← get'
+  let symRingId := s.rings[ringId]!.symId
+  x { ringId, symRingId }
 
 abbrev getRingId : RingM Nat :=
   return (← read).ringId
 
-instance : MonadCanon RingM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+abbrev getSymRingId : RingM Nat :=
+  return (← read).symRingId
 
 protected def RingM.getCommRing : RingM CommRing := do
+  let s ← getArithState
+  let symRingId ← getSymRingId
+  if h : symRingId < s.rings.size then
+    return s.rings[symRingId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+protected def RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit := do
+  let symRingId ← getSymRingId
+  modifyArithState fun s => { s with rings := s.rings.modify symRingId f }
+
+instance : MonadCommRing RingM where
+  getCommRing := RingM.getCommRing
+  modifyCommRing := RingM.modifyCommRing
+
+def getCommRingEntry : RingM CommRingEntry := do
   let s ← get'
   let ringId ← getRingId
   if h : ringId < s.rings.size then
@@ -53,14 +74,10 @@ protected def RingM.getCommRing : RingM CommRing := do
   else
     throwError "`grind` internal error, invalid ringId"
 
-protected def RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit := do
+def modifyCommRingEntry (f : CommRingEntry → CommRingEntry) : RingM Unit := do
   let ringId ← getRingId
   modify' fun s => { s with rings := s.rings.modify ringId f }
 
-instance : MonadCommRing RingM where
-  getCommRing := RingM.getCommRing
-  modifyCommRing := RingM.modifyCommRing
-
 abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
   withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
 
@@ -112,17 +129,14 @@ def isField : RingM Bool :=
   return (← getCommRing).fieldInst?.isSome
 
 def isQueueEmpty : RingM Bool :=
-  return (← getCommRing).queue.isEmpty
+  return (← getCommRingEntry).queue.isEmpty
 
 def getNext? : RingM (Option EqCnstr) := do
-  let some c := (← getCommRing).queue.min? | return none
-  modifyCommRing fun s => { s with queue := s.queue.erase c }
+  let some c := (← getCommRingEntry).queue.min? | return none
+  modifyCommRingEntry fun s => { s with queue := s.queue.erase c }
   incSteps
   return some c
 
-class MonadSetTermId (m : Type → Type) where
-  setTermId : Expr → m Unit
-
 def setTermRingId (e : Expr) : RingM Unit := do
   let ringId ← getRingId
   if let some ringId' ← getTermRingId? e then
@@ -131,23 +145,25 @@ def setTermRingId (e : Expr) : RingM Unit := do
     return ()
   modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
 
-def mkVarCore [MonadLiftT GoalM m] [Monad m] [MonadRing m] [MonadSetTermId m] (e : Expr) : m Var := do
-  let s ← getRing
+def mkVar (e : Expr) (gen : Nat) : RingM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getCommRingEntry
   if let some var := s.varMap.find? { expr := e } then
     return var
   let var : Var := s.vars.size
-  modifyRing fun s => { s with
+  modifyCommRingEntry fun s => { s with
     vars       := s.vars.push e
     varMap     := s.varMap.insert { expr := e } var
   }
-  MonadSetTermId.setTermId e
+  setTermRingId e
   ringExt.markTerm e
   return var
 
-instance : MonadSetTermId RingM where
-  setTermId e := setTermRingId e
+instance : MonadMkVar RingM where
+  mkVar := CommRing.mkVar
 
-def mkVar (e : Expr) : RingM Var :=
-  mkVarCore e
+instance : MonadGetVar RingM where
+  getVar x := return (← getCommRingEntry).vars[x]!
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -121,7 +121,7 @@ def _root_.Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) : RingM (Option
   match m with
   | .unit => return none
   | .mult pw m =>
-    let e := (← getRing).vars[pw.x]!
+    let e := (← getCommRingEntry).vars[pw.x]!
     let_expr Inv.inv _ _ a := e | m.findInvNumeralVar?
     let_expr OfNat.ofNat _ n _ := a | m.findInvNumeralVar?
     let some n ← getNatValue? n | m.findInvNumeralVar?

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

@@ -6,46 +6,44 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+public import Lean.Meta.Sym.Arith.MonadSemiring
+public import Lean.Meta.Sym.Arith.MonadVar
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 open Sym.Arith
 
 structure SemiringM.Context where
-  semiringId : Nat
+  semiringId    : Nat
+  symSemiringId : Nat
 
 abbrev SemiringM := ReaderT SemiringM.Context GoalM
 
-abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α :=
-  x { semiringId }
+abbrev SemiringM.run (semiringId : Nat) (x : SemiringM α) : GoalM α := do
+  let s ← get'
+  let symSemiringId := s.semirings[semiringId]!.symId
+  x { semiringId, symSemiringId }
 
 abbrev getSemiringId : SemiringM Nat :=
   return (← read).semiringId
 
-instance : MonadCanon SemiringM where
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
-
 protected def SemiringM.getCommSemiring : SemiringM CommSemiring := do
-  let s ← get'
-  let semiringId ← getSemiringId
+  let s ← getArithState
+  let semiringId := (← read).symSemiringId
   if h : semiringId < s.semirings.size then
     return s.semirings[semiringId]
   else
     throwError "`grind` internal error, invalid semiringId"
 
 @[inline] protected def SemiringM.modifyCommSemiring (f : CommSemiring → CommSemiring) : SemiringM Unit := do
-  let semiringId ← getSemiringId
-  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
+  let semiringId := (← read).symSemiringId
+  modifyArithState fun s => { s with semirings := s.semirings.modify semiringId f }
 
 instance : MonadCommSemiring SemiringM where
   getCommSemiring := SemiringM.getCommSemiring
   modifyCommSemiring := SemiringM.modifyCommSemiring
 
 protected def SemiringM.getCommRing : SemiringM CommRing := do
-  let s ← get'
+  let s ← getArithState
   let ringId := (← getCommSemiring).ringId
   if h : ringId < s.rings.size then
     return s.rings[ringId]
@@ -54,12 +52,59 @@ protected def SemiringM.getCommRing : SemiringM CommRing := do
 
 protected def SemiringM.modifyCommRing (f : CommRing → CommRing) : SemiringM Unit := do
   let ringId := (← getCommSemiring).ringId
-  modify' fun s => { s with rings := s.rings.modify ringId f }
+  modifyArithState fun s => { s with rings := s.rings.modify ringId f }
 
 instance : MonadCommRing SemiringM where
  getCommRing := SemiringM.getCommRing
  modifyCommRing := SemiringM.modifyCommRing
 
+def getCommSemiringEntry : SemiringM CommSemiringEntry := do
+  let s ← get'
+  let semiringId := (← read).semiringId
+  if h : semiringId < s.semirings.size then
+    return s.semirings[semiringId]
+  else
+    throwError "`grind` internal error, invalid semiringId"
+
+def modifyCommSemiringEntry (f : CommSemiringEntry → CommSemiringEntry) : SemiringM Unit := do
+  let semiringId := (← read).semiringId
+  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
+
+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 `mkVarCore` but for `Semiring`s -/
+def mkSVar (e : Expr) (gen : Nat) : SemiringM Var := do
+  unless (← alreadyInternalized e) do
+    internalize e gen
+  let s ← getCommSemiringEntry
+  if let some var := s.varMap.find? { expr := e } then
+    return var
+  let var : Var := s.vars.size
+  modifyCommSemiringEntry fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+  }
+  setTermSemiringId e
+  ringExt.markTerm e
+  return var
+
+instance : MonadMkVar SemiringM where
+  mkVar := mkSVar
+
+instance : MonadGetVar SemiringM where
+  getVar x := return (← getCommSemiringEntry).vars[x]!
+
+
+/-
 def getToQFn : SemiringM Expr := do
   let s ← getCommSemiring
   if let some toQFn := s.toQFn? then return toQFn
@@ -115,37 +160,6 @@ def getNatCastFn' : m Expr := do
 
 end
 
-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 }
-
-instance : MonadSetTermId SemiringM where
-  setTermId e := setTermSemiringId e
-
-/-- Similar to `mkVarCore` but for `Semiring`s -/
-def mkSVarCore [MonadLiftT GoalM m] [Monad m] [MonadSemiring m] [MonadSetTermId m] (e : Expr) : m 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
-  }
-  MonadSetTermId.setTermId e
-  ringExt.markTerm e
-  return var
-
-def mkSVar (e : Expr) : SemiringM Var := do
-  mkSVarCore e
-
 def _root_.Lean.Grind.CommRing.Expr.denoteAsRingExpr (e : SemiringExpr) : SemiringM Expr := do
   shareCommon (← go e)
 where
@@ -158,4 +172,6 @@ where
   | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
   | .neg .. | .sub .. | .intCast .. => unreachable!
 
+-/
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.Arith.Types
 import Lean.Meta.Sym.Arith.Poly
 public section
 
@@ -144,17 +145,9 @@ structure DiseqCnstr where
   ofSemiring? : Option (SemiringExpr × SemiringExpr)
 
 /-- Shared state for non-commutative and commutative semirings. -/
-structure Semiring where
+structure SemiringEntry where
+  symId          : Nat
   id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  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 := {}
   /--
@@ -167,25 +160,9 @@ structure Semiring where
   deriving Inhabited
 
 /-- Shared state for non-commutative and commutative rings. -/
-structure Ring where
+structure RingEntry where
+  symId          : Nat
   id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Ring` instance for `type` -/
-  ringInst       : Expr
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  /-- `IsCharP` instance for `type` if available. -/
-  charInst?      : Option (Expr × Nat)
-  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
-  one?           : Option Expr := none
   /--
   Mapping from variables to their denotations.
   Remark each variable can be in only one ring.
@@ -198,24 +175,7 @@ structure Ring where
   deriving Inhabited
 
 /-- State for each `CommRing` processed by this module. -/
-structure CommRing extends Ring where
-  /-- Inverse if `fieldInst?` is `some inst` -/
-  invFn?         : Option Expr := none
-  /--
-  If this is a `OfSemiring.Q α` ring, this field contain the
-  `semiringId` for `α`.
-  -/
-  semiringId?    : Option Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `CommRing` instance for `type` -/
-  commRingInst   : Expr
-  /-- `NoNatZeroDivisors` instance for `type` if available. -/
-  noZeroDivInst? : Option Expr
-  /-- `Field` instance for `type` if available. -/
-  fieldInst?     : Option Expr
-  /-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available. -/
-  powIdentityInst? : Option (Expr × Expr × Nat) := none
+structure CommRingEntry extends RingEntry where
   /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
   denoteEntries  : PArray (Expr × RingExpr) := {}
   /-- Next unique id for `EqCnstr`s. -/
@@ -254,62 +214,36 @@ structure CommRing extends Ring where
 State for each `CommSemiring` processed by this module.
 Recall that `CommSemiring` are processed using the envelop `OfCommSemiring.Q`
 -/
-structure CommSemiring extends Semiring where
-  /-- Id for `OfCommSemiring.Q` -/
-  ringId         : Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option (Option Expr) := none
-  toQFn?         : Option Expr := none
+structure CommSemiringEntry extends SemiringEntry where
+  /-- Id for `CommRingEntry` associated with `OfCommSemiring.Q` -/
+  ringId : Nat
   deriving Inhabited
 
+export Sym.Arith (ClassifyResult)
+
 /-- State for all `CommRing` types detected by `grind`. -/
 structure State where
   /--
   Commutative rings.
   We expect to find a small number of rings in a given goal. Thus, using `Array` is fine here.
   -/
-  rings : Array CommRing := {}
-  /--
-  Mapping from types to its "ring id". We cache failures using `none`.
-  `typeIdOf[type]` is `some id`, then `id < rings.size`. -/
-  typeIdOf : PHashMap ExprPtr (Option Nat) := {}
+  rings : Array CommRingEntry := {}
+  /-- Commutative semirings. We support them using the envelope `OfCommRing.Q` -/
+  semirings : Array CommSemiringEntry := {}
+  /-- Non commutative rings. -/
+  ncRings : Array RingEntry := {}
+  /-- Non commutative semirings. -/
+  ncSemirings : Array SemiringEntry := {}
+  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
+  typeClassify : PHashMap ExprPtr ClassifyResult := {}
   /- Mapping from expressions/terms to their ring ids. -/
   exprToRingId : PHashMap ExprPtr Nat := {}
-  /-- Commutative semirings. We support them using the envelope `OfCommRing.Q` -/
-  semirings : Array CommSemiring := {}
-  /--
-  Mapping from types to its "semiring id". We cache failures using `none`.
-  `stypeIdOf[type]` is `some id`, then `id < semirings.size`.
-  If a type is in this map, it is not in `typeIdOf`.
-  -/
-  stypeIdOf : PHashMap ExprPtr (Option Nat) := {}
-  /-
-  Mapping from expressions/terms to their semiring ids.
-  If an expression is in this map, it is not in `exprToRingId`.
-  -/
+  /- Mapping from expressions/terms to their semiring ids. -/
   exprToSemiringId : PHashMap ExprPtr Nat := {}
-  /--
-  Non commutative rings.
-  -/
-  ncRings : Array Ring := {}
   /- Mapping from expressions/terms to their (non-commutative) ring ids. -/
   exprToNCRingId : PHashMap ExprPtr Nat := {}
-  /--
-  Mapping from types to its "ring id". We cache failures using `none`.
-  `nctypeIdOf[type]` is `some id`, then `id < ncRings.size`. -/
-  nctypeIdOf : PHashMap ExprPtr (Option Nat) := {}
-  /--
-  Non commutative semirings.
-  -/
-  ncSemirings : Array Semiring := {}
   /- Mapping from expressions/terms to their (non-commutative) semiring ids. -/
   exprToNCSemiringId : PHashMap ExprPtr Nat := {}
-  /--
-  Mapping from types to its "semiring id". We cache failures using `none`.
-  `ncstypeIdOf[type]` is `some id`, then `id < ncSemirings.size`. -/
-  ncstypeIdOf : PHashMap ExprPtr (Option Nat) := {}
   steps := 0
   deriving Inhabited
 

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

@@ -10,11 +10,12 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
+import Lean.Meta.Sym.Arith.Reify
+import Lean.Meta.Sym.Arith.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat
+open Sym Arith
 /-!
 CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
 -/
@@ -45,9 +46,9 @@ def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.Ri
     -- Internalized operators instead of `mkIntMul` and `mkIntAdd`
     let e ← shareCommon (← canon e)
     let gen ← p.getGeneration
-    let some re ← CommRing.reify? e (gen := gen) | return none
+    let some re ← reifyRing? e (gen := gen) | return none
     let some p' ← re.toPolyM? | return none
-    let e' ← p'.denoteExpr
+    let e' ← denotePoly p'
     let e' ← preprocessLight e'
     /-
     **Note**: We are reusing the `IntModule` virtual parent.

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

@@ -174,7 +174,7 @@ private def mkContext
 private def mkRingContext (h : Expr) : ProofM Expr := do
   unless (← get').usedCommRing do return h
   let some ringId ← getIntRingId? | return h
-  let vars ← CommRing.RingM.run ringId do return (← CommRing.getRing).vars
+  let vars ← CommRing.RingM.run ringId do return (← CommRing.getCommRingEntry).vars
   let usedVars     := collectMapVars (← get).ringPolyDecls (·.collectVars) >> collectMapVars (← get).ringExprDecls (·.collectVars) <| {}
   let vars'        := usedVars.toArray
   let varRename    := mkVarRename vars'

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

@@ -8,7 +8,7 @@ prelude
 import Lean.Meta.Tactic.Grind.Arith.Util
 public import Lean.Meta.Tactic.Grind.Arith.Linear.Util
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Sym.Arith.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.Linear
 /-!
@@ -69,7 +69,9 @@ private def denoteNum (k : Int) : LinearM Expr := do
 def _root_.Lean.Grind.CommRing.Poly.denoteAsIntModuleExpr (p : Grind.CommRing.Poly) : LinearM Expr := do
   match p with
   | .num k => denoteNum k
-  | .add k m p => return mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
+  | .add _k _m _p =>
+    -- TODO: FIX
+    return default -- mkApp2 (← getStruct).addFn (mkApp2 (← getStruct).zsmulFn (mkIntLit k) (← m.denoteExpr)) (← denoteAsIntModuleExpr p)
 
 def _root_.Lean.Grind.CommRing.Poly.toIntModuleExpr (p : Grind.CommRing.Poly) (generation := 0) : LinearM Expr := do
   let e ← p.denoteAsIntModuleExpr

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

@@ -6,12 +6,13 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Den
 import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
+import Lean.Meta.Sym.Arith.Reify
 namespace Lean.Meta.Grind.Arith.Linear
+open Sym Arith
 
 def isInstOf (fn? : Option Expr) (inst : Expr) : Bool :=
   if let some fn := fn? then
@@ -39,8 +40,9 @@ public def IneqCnstr.assert (c : IneqCnstr) : LinearM Unit := do
       resetAssignmentFrom x
 
 def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : Bool) : LinearM Unit := do
-  let some lhs ← withRingM <| CommRing.reify? lhs (skipVar := false) | return ()
-  let some rhs ← withRingM <| CommRing.reify? rhs (skipVar := false) | return ()
+  let gen ← getGeneration e
+  let some lhs ← withRingM <| reifyRing? lhs (skipVar := false) (gen := gen) | return ()
+  let some rhs ← withRingM <| reifyRing? rhs (skipVar := false) (gen := gen) | return ()
   let generation ← getGeneration e
   if eqTrue then
     let p := (lhs.sub rhs).toPoly

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

@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym.Arith (MonadCanon)
+open Sym.Arith (MonadCanon MonadRing)
 
 def get' : GoalM State := do
   linearExt.getState
@@ -52,8 +52,10 @@ instance : MonadGetStruct LinearM where
 open CommRing
 
 def getRingCore? (ringId? : Option Nat) : GoalM (Option Ring) := do
-  let some ringId := ringId? | return none
-  RingM.run ringId do return some (← getRing)
+  let some _ringId := ringId? | return none
+  -- TODO: FIX
+  -- RingM.run ringId do return some (← getRing)
+  return none
 
 def throwNotRing : LinearM α :=
   throwError "`grind linarith` internal error, structure is not a ring"
@@ -75,9 +77,10 @@ def LinearM.getRing : LinearM Ring := do
 
 instance : MonadRing LinearM where
   getRing := LinearM.getRing
-  modifyRing f := do
-    let some ringId := (← getStruct).ringId? | throwNotCommRing
-    RingM.run ringId do modifyRing f
+  modifyRing _f := do
+    let some _ringId := (← getStruct).ringId? | throwNotCommRing
+    -- RingM.run ringId do modifyRing f
+    -- TODO: FIX
 
 def withRingM (x : RingM α) : LinearM α := do
   let some ringId := (← getStruct).ringId?

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

@@ -123,6 +123,8 @@ private def mkContext (h : Expr) : ProofM Expr := do
 
 private def mkRingContext (h : Expr) : ProofM Expr := do
   unless (← isCommRing) do return h
+  throwError "NIY"
+/-
   let ring ← withRingM do CommRing.getRing
   let vars := ring.vars
   let ringVarDecls := (← get).ringVarDecls
@@ -144,6 +146,7 @@ private def mkRingContext (h : Expr) : ProofM Expr := do
     return .letE `rctx ctxType ctxVal h (nondep := false)
   else
     return h
+-/
 
 private abbrev withProofContext (x : ProofM Expr) : LinearM Expr := do
   let ctx := mkFVar (← mkFreshFVarId)

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

@@ -6,13 +6,14 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.Den
-import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
 import Lean.Meta.Tactic.Grind.Arith.Linear.IneqCnstr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Proof
+import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
+import Lean.Meta.Sym.Arith.Reify
 public section
 namespace Lean.Meta.Grind.Arith.Linear
+open Sym Arith
 
 private def _root_.Lean.Grind.Linarith.Poly.substVar (p : Poly) : LinearM (Option (Var × EqCnstr × Poly)) := do
   let some (a, x, c) ← p.findVarToSubst | return none
@@ -47,8 +48,8 @@ private def inSameStruct? (a b : Expr) : GoalM (Option Nat) := do
   return structId
 
 private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do
-  let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
-  let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
+  let some lhs ← withRingM <| reifyRing? a (skipVar := false) (gen := (← getGeneration a)) | return ()
+  let some rhs ← withRingM <| reifyRing? b (skipVar := false) (gen := (← getGeneration a)) | return ()
   let generation := max (← getGeneration a) (← getGeneration b)
   let p := (lhs.sub rhs).toPoly
   let c : RingEqCnstr := { p, h := .core a b lhs rhs }
@@ -294,8 +295,8 @@ def processNewEq (a b : Expr) : GoalM Unit := do
       processNewNatModuleEq a b
 
 private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do
-  let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
-  let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
+  let some lhs ← withRingM <| reifyRing? a (skipVar := false) (← getGeneration a) | return ()
+  let some rhs ← withRingM <| reifyRing? b (skipVar := false) (← getGeneration b) | return ()
   let p := (lhs.sub rhs).toPoly
   let c : RingDiseqCnstr := { p, h := .core a b lhs rhs }
   let c ← c.cleanupDenominators

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Arith.Insts
 import Init.Grind.Module.Envelope
 public section
 namespace Lean.Meta.Grind.Arith.Linear
+open Sym Arith
 
 private def preprocess (e : Expr) : GoalM Expr := do
   shareCommon (← canon e)
@@ -66,7 +67,7 @@ private def isCutsatType (type : Expr) : GoalM Bool := do
 
 private def getCommRingInst? (ringId? : Option Nat) : GoalM (Option Expr) := do
   let some ringId := ringId? | return none
-  return some (← CommRing.RingM.run ringId do return (← CommRing.getCommRing).commRingInst)
+  return some (← CommRing.RingM.run ringId do return (← getCommRing).commRingInst)
 
 private def mkRingInst? (u : Level) (type : Expr) (commRingInst? : Option Expr) : GoalM (Option Expr) := do
   if let some commRingInst := commRingInst? then

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

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public import Lean.Meta.Tactic.Grind.PropagatorAttr
 public section
 namespace Lean.Meta.Grind.Arith
-
+open Sym Arith
 /-!
 This file defines propagators for `Nat` operators that have simprocs associated with them, but do not
 have support in satellite solvers. The goal is to workaround a nasty interaction between

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

@@ -10,8 +10,6 @@ import Init.Data.Int.OfNat
 import Init.Grind.Module.Envelope
 import Init.Grind.Order
 import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Order.StructId

src/Lean/Meta/Tactic/Grind/Order/StructId.lean

@@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public section
 namespace Lean.Meta.Grind.Order
+open Sym Arith
 
 private def preprocess (e : Expr) : GoalM Expr := do
   shareCommon (← canon e)