missing files

This PR is an experiment using Claude to refactor the Lean code base.

src/Lean/Meta/Sym/Arith/Ring/DenoteExpr.lean

@@ -0,0 +1,86 @@
+/-
+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.Ring.Functions
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+/-!
+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 ← MonadCanon.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 denotePower (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 denoteMon (m : Mon) : M Expr := do
+  match m with
+  | .unit => denoteNum 1
+  | .mult pw m => go m (← denotePower pw)
+where
+  go (m : Mon) (acc : Expr) : M Expr := do
+    match m with
+    | .unit => return acc
+    | .mult pw m => go m (mkApp2 (← getMulFn) acc (← denotePower pw))
+
+def denotePoly (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
+      denoteMon m
+    else
+      return mkApp2 (← getMulFn) (← denoteNum k) (← denoteMon m)
+
+  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 denoteRingExpr (e : RingExpr) : M Expr := do
+  let ring ← getRing
+  denoteExprCore (fun x => ring.vars[x]!) e
+
+def denoteRingExpr' (vars : Array Expr) (e : RingExpr) : M Expr := do
+  denoteExprCore (fun x => vars[x]!) e
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Arith/Ring/Detect.lean

@@ -0,0 +1,99 @@
+/-
+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.Ring.SymExt
+import Lean.Meta.SynthInstance
+import Lean.Meta.DecLevel
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+/--
+Wrapper around `Meta.synthInstance?` that catches `isDefEqStuck` exceptions
+(which can occur when instance arguments contain metavariables or are not in normal form).
+-/
+private def synthInstance? (type : Expr) : SymM (Option Expr) :=
+  catchInternalId isDefEqStuckExceptionId
+    (Meta.synthInstance? type)
+    (fun _ => pure none)
+
+/--
+Evaluate a `Nat`-typed expression to a concrete `Nat` value.
+Handles `OfNat.ofNat`, `HPow.hPow`, `HAdd.hAdd`, `HMul.hMul`, `HSub.hSub`,
+`Nat.zero`, `Nat.succ`, and raw `Nat` literals.
+This is simpler than `Grind.Arith.evalNat?` (no threshold checks, no `Int` support)
+but sufficient for evaluating `IsCharP` characteristic values like `2^8`.
+-/
+private partial def evalNat? (e : Expr) : Option Nat :=
+  match_expr e with
+  | OfNat.ofNat _ n _ =>
+    match n with
+    | .lit (.natVal k) => some k
+    | _ => evalNat? n
+  | Nat.zero => some 0
+  | Nat.succ a => (· + 1) <$> evalNat? a
+  | HAdd.hAdd _ _ _ _ a b => (· + ·) <$> evalNat? a <*> evalNat? b
+  | HMul.hMul _ _ _ _ a b => (· * ·) <$> evalNat? a <*> evalNat? b
+  | HSub.hSub _ _ _ _ a b => (· - ·) <$> evalNat? a <*> evalNat? b
+  | HPow.hPow _ _ _ _ a b => (· ^ ·) <$> evalNat? a <*> evalNat? b
+  | _ =>
+    match e with
+    | .lit (.natVal k) => some k
+    | _ => none
+
+/--
+Detect whether `type` has a `Grind.CommRing` instance.
+Returns the shared ring id if found. The `CommRing` object is stored in
+`arithRingExt` and is shared between `Sym.simp` and `grind`.
+Results are cached in `arithRingExt.typeIdOf`.
+-/
+def detectCommRing? (type : Expr) : SymM (Option Nat) := do
+  let s ← arithRingExt.getState
+  if let some id? := s.typeIdOf.find? { expr := type } then
+    return id?
+  let some ring ← go? | do
+    arithRingExt.modifyState fun st => { st with typeIdOf := st.typeIdOf.insert { expr := type } none }
+    return none
+  let id := s.rings.size
+  let ring := { ring with toRing.id := id }
+  arithRingExt.modifyState fun st => { st with
+    rings := st.rings.push ring
+    typeIdOf := st.typeIdOf.insert { expr := type } (some id)
+  }
+  return some id
+where
+  go? : SymM (Option CommRing) := 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
+    let charInst? ← getIsCharInst? u type semiringInst
+    let noZeroDivInst? ← getNoZeroDivInst? u type
+    let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
+    return some {
+      id := 0, type, u, semiringInst, ringInst, commSemiringInst,
+      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
+      semiringId? := none,
+    }
+
+  getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : SymM (Option (Expr × Nat)) := do
+    withNewMCtxDepth do
+      let n ← mkFreshExprMVar (mkConst ``Nat)
+      let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
+      let some charInst ← synthInstance? charType | return none
+      let n ← instantiateMVars n
+      let some nVal := evalNat? n | return none
+      return some (charInst, nVal)
+
+  getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
+    let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
+    let some natModuleInst ← synthInstance? natModuleType | return none
+    let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
+    synthInstance? noZeroDivType
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Arith/Ring/Functions.lean

@@ -0,0 +1,122 @@
+/-
+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.Ring.MonadRing
+public import Lean.Meta.Basic
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+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
+
+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
+
+end
+
+end Lean.Meta.Sym.Arith.Ring

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

@@ -0,0 +1,36 @@
+/-
+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.Ring.Types
+public import Lean.Exception
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+class MonadCanon (m : Type → Type) where
+  /--
+  Canonicalize an expression (e.g., hash-cons via `shareCommon`).
+  In `SymM`-based monads, this is typically `shareCommon (← canon e)`.
+  -/
+  canonExpr : Expr → m Expr
+  /--
+  Synthesize a type class instance, returning `none` on failure.
+  -/
+  synthInstance? : Expr → m (Option Expr)
+
+export MonadCanon (canonExpr)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
+  canonExpr e := liftM (canonExpr e : m Expr)
+  synthInstance? e := liftM (MonadCanon.synthInstance? e : m (Option Expr))
+
+def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
+  let some inst ← synthInstance? type
+    | throwError "failed to find instance{indentExpr type}"
+  return inst
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Arith/Ring/MonadRing.lean

@@ -0,0 +1,23 @@
+/-
+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.Ring.MonadCanon
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+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)
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Arith/Ring/MonadSemiring.lean

@@ -0,0 +1,23 @@
+/-
+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.Ring.MonadCanon
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+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)
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Arith/Ring/SymExt.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.Sym.SymM
+public import Lean.Meta.Sym.Arith.Ring.Types
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+/-- Shared ring state, accessible from both `Sym.simp` and `grind`. -/
+builtin_initialize arithRingExt : SymExtension State ← registerSymExtension
+
+end Lean.Meta.Sym.Arith.Ring

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

@@ -0,0 +1,114 @@
+/-
+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.ExprPtr
+public import Lean.Data.PersistentHashMap
+public import Lean.Data.PersistentArray
+public import Init.Grind.Ring.CommSemiringAdapter
+public section
+namespace Lean.Meta.Sym.Arith.Ring
+
+export Lean.Grind.CommRing (Var Power Mon Poly)
+abbrev RingExpr := Grind.CommRing.Expr
+/-
+We use ring expressions to represent semiring expressions,
+and ignore non-applicable constructors.
+-/
+abbrev SemiringExpr := Grind.CommRing.Expr
+
+/-- Shared state for non-commutative and commutative semirings. -/
+structure Semiring where
+  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 := {}
+  /--
+  Mapping from variables to their denotations.
+  Each variable can be in only one ring.
+  -/
+  vars           : PArray Expr := {}
+  /-- Mapping from `Expr` to a variable representing it. -/
+  varMap         : PHashMap ExprPtr Var := {}
+  deriving Inhabited
+
+/-- Shared state for non-commutative and commutative rings. -/
+structure Ring where
+  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.
+  Each variable can be in only one ring.
+  -/
+  vars           : PArray Expr := {}
+  /-- Mapping from `Expr` to a variable representing it. -/
+  varMap         : PHashMap ExprPtr Var := {}
+  /-- Mapping from Lean expressions to their representations as `RingExpr` -/
+  denote         : PHashMap ExprPtr RingExpr := {}
+  deriving Inhabited
+
+/-- Shared state for commutative rings. -/
+structure CommRing extends Ring where
+  /--
+  If this is a `OfSemiring.Q α` ring, this field contains 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
+  invFn?             : Option Expr := none
+  /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
+  denoteEntries      : PArray (Expr × RingExpr) := {}
+  deriving Inhabited
+
+/-- Shared state for commutative semirings. -/
+structure CommSemiring extends Semiring where
+  /-- Id for `OfSemiring.Q` -/
+  ringId             : Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst   : Expr
+  /-- `AddRightCancel` instance for `type` if available. -/
+  addRightCancelInst? : Option (Option Expr) := none
+  toQFn?             : Option Expr := none
+  deriving Inhabited
+
+/-- Shared ring state, stored in `arithRingExt` and accessed by both `Sym.simp` and `grind`. -/
+structure State where
+  rings   : Array CommRing := {}
+  typeIdOf : PHashMap ExprPtr (Option Nat) := {}
+  deriving Inhabited
+
+end Lean.Meta.Sym.Arith.Ring

src/Lean/Meta/Sym/Simp.lean

@@ -23,3 +23,4 @@ public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
 public import Lean.Meta.Sym.Simp.Telescope
+public import Lean.Meta.Sym.Simp.ArithNorm

src/Lean/Meta/Sym/Simp/ArithNorm.lean

@@ -0,0 +1,204 @@
+/-
+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.Simp.SimpM
+public import Lean.Meta.Sym.Arith.Ring.DenoteExpr
+public import Lean.Meta.Sym.Arith.Ring.Detect
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Sym.LitValues
+import Lean.Meta.Sym.InferType
+public import Lean.Meta.SynthInstance
+import Lean.Data.RArray
+import Init.Grind.Ring
+public section
+namespace Lean.Meta.Sym.Simp
+
+open Arith.Ring
+
+/-!
+# Arithmetic Normalizer for Sym.simp
+
+A simproc that normalizes ring expressions to polynomial normal form.
+Given an expression like `(a + b) * (a - b)`, it normalizes to `a*a + (-1)*b*b`
+(i.e., the polynomial representation), and produces an equality proof using
+`Grind.CommRing.Expr.denote_toPoly`.
+-/
+
+/-- Monad for ring operations within the normalizer. Wraps `SimpM` with a current ring id. -/
+structure ArithRingM.Context where
+  ringId : Nat
+
+abbrev ArithRingM := ReaderT ArithRingM.Context SimpM
+
+instance : MonadCanon ArithRingM where
+  canonExpr e := shareCommonInc e
+  synthInstance? e := Meta.synthInstance? e
+
+def ArithRingM.getCommRing : ArithRingM CommRing := do
+  let s ← arithRingExt.getState
+  let ringId := (← read).ringId
+  if h : ringId < s.rings.size then
+    return s.rings[ringId]
+  else
+    throwError "arith normalizer: invalid ringId"
+
+def ArithRingM.modifyCommRing (f : CommRing → CommRing) : ArithRingM Unit := do
+  let ringId := (← read).ringId
+  arithRingExt.modifyState fun s => { s with rings := s.rings.modify ringId f }
+
+instance : MonadRing ArithRingM where
+  getRing := return (← ArithRingM.getCommRing).toRing
+  modifyRing f := ArithRingM.modifyCommRing fun s => { s with toRing := f s.toRing }
+
+/-- Check if an expression is an instance of the expected one by pointer equality. -/
+private def isExpectedInst (expected inst : Expr) : Bool :=
+  isSameExpr expected.appArg! inst
+
+/--
+Reify a Lean expression into a `RingExpr`.
+Returns `none` if the expression is not a ring term.
+-/
+private partial def reify? (e : Expr) : ArithRingM (Option RingExpr) := do
+  let mkVar (e : Expr) : ArithRingM Grind.CommRing.Var := do
+    let ring ← getRing
+    if let some var := ring.varMap.find? { expr := e } then
+      return var
+    let var : Grind.CommRing.Var := ring.vars.size
+    modifyRing fun s => { s with
+      vars   := s.vars.push e
+      varMap := s.varMap.insert { expr := e } var
+    }
+    return var
+  let toVar (e : Expr) : ArithRingM RingExpr := do
+    return .var (← mkVar e)
+  let rec go (e : Expr) : ArithRingM RingExpr := do
+    match_expr e with
+    | HAdd.hAdd _ _ _ i a b =>
+      if isExpectedInst (← getAddFn) i then return .add (← go a) (← go b) else toVar e
+    | HMul.hMul _ _ _ i a b =>
+      if isExpectedInst (← getMulFn) i then return .mul (← go a) (← go b) else toVar e
+    | HSub.hSub _ _ _ i a b =>
+      if isExpectedInst (← getSubFn) i then return .sub (← go a) (← go b) else toVar e
+    | HPow.hPow _ _ _ i a b =>
+      let some k := getNatValue? b | toVar e
+      if isExpectedInst (← getPowFn) i then return .pow (← go a) k else toVar e
+    | Neg.neg _ i a =>
+      if isExpectedInst (← getNegFn) i then return .neg (← go a) else toVar e
+    | IntCast.intCast _ i a =>
+      if isExpectedInst (← getIntCastFn) i then
+        let some k := getIntValue? a | toVar e
+        return .intCast k
+      else
+        toVar e
+    | NatCast.natCast _ i a =>
+      if isExpectedInst (← getNatCastFn) i then
+        let some k := getNatValue? a | toVar e
+        return .natCast k
+      else
+        toVar e
+    | OfNat.ofNat _ n _ =>
+      let .lit (.natVal k) := n | toVar e
+      return .num k
+    | _ => toVar e
+  -- At top level, only proceed if e is an arithmetic operation
+  match_expr e with
+  | HAdd.hAdd _ _ _ i a b =>
+    if isExpectedInst (← getAddFn) i then return some (.add (← go a) (← go b)) else return none
+  | HMul.hMul _ _ _ i a b =>
+    if isExpectedInst (← getMulFn) i then return some (.mul (← go a) (← go b)) else return none
+  | HSub.hSub _ _ _ i a b =>
+    if isExpectedInst (← getSubFn) i then return some (.sub (← go a) (← go b)) else return none
+  | HPow.hPow _ _ _ i a b =>
+    let some k := getNatValue? b | return none
+    if isExpectedInst (← getPowFn) i then return some (.pow (← go a) k) else return none
+  | Neg.neg _ i a =>
+    if isExpectedInst (← getNegFn) i then return some (.neg (← go a)) else return none
+  | _ => return none
+
+/--
+Build a `Grind.CommRing.Context α` expression (an `RArray α`) from the variable array.
+-/
+private def toContextExpr : ArithRingM Expr := do
+  let ring ← getRing
+  let vars := ring.vars.toArray
+  if h : 0 < vars.size then
+    RArray.toExpr ring.type id (RArray.ofFn (vars[·]) h)
+  else
+    RArray.toExpr ring.type id (RArray.leaf (mkApp (← getNatCastFn) (toExpr 0)))
+
+/--
+The core arithmetic normalization logic.
+Given a ring expression, normalize it to polynomial form and produce a proof.
+-/
+private def normalizeRingExpr (re : RingExpr) : ArithRingM (Option Result) := do
+  let ring ← getRing
+  let commRing ← ArithRingM.getCommRing
+  -- Normalize to polynomial
+  let p := match ring.charInst? with
+    | some (_, c) => if c != 0 then re.toPolyC c else re.toPoly
+    | none => re.toPoly
+  -- Build the denotation of the polynomial as a Lean expression
+  let e' ← denotePoly p
+  let e' ← shareCommonInc e'
+  -- Build the context (RArray of variable denotations)
+  let ctx ← toContextExpr
+  let ctx ← shareCommonInc ctx
+  -- Build the reified expression as a Lean Expr
+  let reExpr := toExpr re
+  -- Build proof: denote_toPoly ctx re : re.toPoly.denote ctx = re.denote ctx
+  -- We need: e = e', i.e., re.denote ctx = re.toPoly.denote ctx
+  -- denote_toPoly gives: re.toPoly.denote ctx = re.denote ctx, i.e., e' = e
+  -- So we use Eq.symm
+  let u := commRing.u
+  let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) ring.type commRing.commRingInst
+  -- Build `re.denote ctx` as a Lean expression (for Eq.symm argument)
+  let eOrig := mkApp4 (mkConst ``Grind.CommRing.Expr.denote [u]) ring.type ringInst ctx reExpr
+  let proof ← match ring.charInst? with
+    | some (charInst, c) =>
+      if c != 0 then
+        -- denote_toPolyC : ∀ {α c} [CommRing α] [IsCharP α c] (ctx) (e), (e.toPolyC c).denote ctx = e.denote ctx
+        let proofFwd := mkApp6 (mkConst ``Grind.CommRing.Expr.denote_toPolyC [u])
+          ring.type (toExpr c) commRing.commRingInst charInst ctx reExpr
+        pure <| mkApp4 (mkConst ``Eq.symm [u.succ]) ring.type e' eOrig proofFwd
+      else
+        let proofFwd := mkApp4 (mkConst ``Grind.CommRing.Expr.denote_toPoly [u])
+          ring.type commRing.commRingInst ctx reExpr
+        pure <| mkApp4 (mkConst ``Eq.symm [u.succ]) ring.type e' eOrig proofFwd
+    | none =>
+      let proofFwd := mkApp4 (mkConst ``Grind.CommRing.Expr.denote_toPoly [u])
+        ring.type commRing.commRingInst ctx reExpr
+      pure <| mkApp4 (mkConst ``Eq.symm [u.succ]) ring.type e' eOrig proofFwd
+  return some (.step e' proof)
+
+/--
+Create an arithmetic normalizer simproc.
+The returned simproc normalizes ring expressions to polynomial normal form.
+-/
+def mkArithNormSimproc : SymM Simproc := do
+  return fun e => do
+    -- Quick check: is this an arithmetic operation?
+    unless e.isApp do return .rfl
+    let fn := e.getAppFn
+    unless fn.isConst do return .rfl
+    let name := fn.constName!
+    unless name == ``HAdd.hAdd || name == ``HMul.hMul || name == ``HSub.hSub
+        || name == ``HPow.hPow || name == ``Neg.neg do
+      return .rfl
+    -- Infer the type of the expression
+    let type ← Sym.inferType e
+    let type ← shareCommonInc type
+    -- Try to find a CommRing instance for this type
+    let some ringId ← Arith.Ring.detectCommRing? type | return .rfl
+    -- Run normalization in the ring context
+    let ctx : ArithRingM.Context := { ringId }
+    let r ← (do
+      let some re ← reify? e | return Result.rfl
+      let some result ← normalizeRingExpr re | return Result.rfl
+      return result : ArithRingM Result) ctx
+    return r
+
+end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/SymM.lean

@@ -82,6 +82,17 @@ inductive CongrInfo where
     -/
     congrTheorem (thm : CongrTheorem)
 
+/-- Opaque extension state for `SymM`. -/
+opaque SymExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
+@[expose] def SymExtensionState : Type := SymExtensionStateSpec.fst
+instance : Inhabited SymExtensionState := SymExtensionStateSpec.snd
+
+/-- A registered extension that stores state of type `σ` in the `SymM` state. -/
+structure SymExtension (σ : Type) where
+  id        : Nat
+  mkInitial : Unit → σ
+  deriving Inhabited
+
 /-- Pre-shared expressions for commonly used terms. -/
 structure SharedExprs where
   trueExpr   : Expr
@@ -131,10 +142,52 @@ structure State where
   -/
   getLevel : PHashMap ExprPtr Level := {}
   congrInfo : PHashMap ExprPtr CongrInfo := {}
+  /-- Extension states, indexed by `SymExtension.id`. -/
+  extensions : Array SymExtensionState := #[]
   debug : Bool := false
 
 abbrev SymM := ReaderT Context <| StateRefT State MetaM
 
+private builtin_initialize symExtensionsRef : IO.Ref (Array (SymExtension SymExtensionState)) ← IO.mkRef #[]
+
+/--
+Register a `SymM` state extension. Must be called during initialization (via `builtin_initialize`).
+Returns a `SymExtension σ` handle used to access the state.
+-/
+private unsafe def registerSymExtensionImpl {σ : Type} [Inhabited σ] (mkInitial : Unit → σ := fun _ => default) : IO (SymExtension σ) := do
+  unless (← initializing) do
+    throw (IO.userError "failed to register `Sym` extension, extensions can only be registered during initialization")
+  let exts ← symExtensionsRef.get
+  let id := exts.size
+  let ext : SymExtension σ := { id, mkInitial }
+  symExtensionsRef.modify fun exts => exts.push (unsafeCast ext)
+  return ext
+
+@[implemented_by registerSymExtensionImpl]
+opaque registerSymExtension {σ : Type} [Inhabited σ] (mkInitial : Unit → σ := fun _ => default) : IO (SymExtension σ)
+
+/-- Create initial states for all registered extensions. -/
+def SymExtension.mkInitialStates : IO (Array SymExtensionState) := do
+  let exts ← symExtensionsRef.get
+  return exts.map fun ext => ext.mkInitial ()
+
+private unsafe def SymExtension.getStateCoreImpl (ext : SymExtension σ) (s : State) : IO σ :=
+  return unsafeCast s.extensions[ext.id]!
+
+@[implemented_by SymExtension.getStateCoreImpl]
+opaque SymExtension.getStateCore (ext : SymExtension σ) (s : State) : IO σ
+
+def SymExtension.getState (ext : SymExtension σ) : SymM σ := do
+  ext.getStateCore (← get)
+
+private unsafe def SymExtension.modifyStateImpl (ext : SymExtension σ) (f : σ → σ) : SymM Unit := do
+  modify fun s => { s with
+    extensions := s.extensions.modify ext.id fun st => unsafeCast (f (unsafeCast st))
+  }
+
+@[implemented_by SymExtension.modifyStateImpl]
+opaque SymExtension.modifyState (ext : SymExtension σ) (f : σ → σ) : SymM Unit
+
 private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
   let falseExpr  ← shareCommonAlphaInc <| mkConst ``False
   let trueExpr   ← shareCommonAlphaInc  <| mkConst ``True
@@ -148,7 +201,8 @@ private def mkSharedExprs : AlphaShareCommonM SharedExprs := do
 def SymM.run (x : SymM α) : MetaM α := do
   let (sharedExprs, share) := mkSharedExprs |>.run {}
   let debug := sym.debug.get (← getOptions)
-  x { sharedExprs } |>.run' { debug, share }
+  let extensions ← SymExtension.mkInitialStates
+  x { sharedExprs } |>.run' { debug, share, extensions }
 
 /-- Returns maximally shared commonly used terms -/
 def getSharedExprs : SymM SharedExprs :=

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

@@ -6,82 +6,32 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+public import Lean.Meta.Sym.Arith.Ring.DenoteExpr
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+export Sym.Arith.Ring (denoteNum denoteRingExpr denoteRingExpr')
 /-!
 Helper functions for converting reified terms back into their denotations.
+Grind-specific denotation functions are defined here; shared ones come from
+`Lean.Meta.Sym.Arith.Ring.DenoteExpr`.
 -/
 
 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 :=
+  Sym.Arith.Ring.denotePower pw
 
-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 :=
+  Sym.Arith.Ring.denoteMon m
 
-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 :=
+  Sym.Arith.Ring.denotePoly p
 
-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)
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr :=
+  Sym.Arith.Ring.denoteRingExpr e
 
-  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
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (vars : Array Expr) (e : RingExpr) : M Expr :=
+  Sym.Arith.Ring.denoteRingExpr' vars e
 
 private def mkEq (a b : Expr) : M Expr := do
   let r ← getRing

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

@@ -6,116 +6,17 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Sym.Arith.Ring.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
+export Sym.Arith.Ring (checkInst mkUnaryFn mkBinHomoFn mkPowFn mkNatCastFn
+  getAddFn getSubFn getMulFn getNegFn getPowFn getIntCastFn getNatCastFn mkOne)
+
 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

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

@@ -6,32 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Sym.Arith.Ring.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-
-class MonadCanon (m : Type → Type) where
-  /--
-  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 MonadCanon (canonExpr)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
-  canonExpr e := liftM (canonExpr e : m Expr)
-  synthInstance? e := liftM (MonadCanon.synthInstance? e : m (Option Expr))
-
-def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
-  let some inst ← synthInstance? type
-    | throwError "`grind` failed to find instance{indentExpr type}"
-  return inst
-
+export Sym.Arith.Ring (MonadCanon canonExpr)
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -6,19 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
+public import Lean.Meta.Sym.Arith.Ring.MonadRing
 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)
+export Sym.Arith.Ring (MonadRing getRing modifyRing)
 
 class MonadCommRing (m : Type → Type) where
   getCommRing : m CommRing
@@ -32,7 +23,7 @@ instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
   modifyCommRing f := liftM (modifyCommRing f : m Unit)
 
 @[always_inline]
-instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
+instance (m) [Monad m] [MonadCommRing m] : Sym.Arith.Ring.MonadRing m where
   getRing := return (← getCommRing).toRing
   modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
 

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

@@ -6,19 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
+public import Lean.Meta.Sym.Arith.Ring.MonadSemiring
 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)
+export Sym.Arith.Ring (MonadSemiring getSemiring modifySemiring)
 
 class MonadCommSemiring (m : Type → Type) where
   getCommSemiring : m CommSemiring
@@ -32,7 +23,7 @@ instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
   modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
 
 @[always_inline]
-instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
+instance (m) [Monad m] [MonadCommSemiring m] : Sym.Arith.Ring.MonadSemiring m where
   getSemiring := return (← getCommSemiring).toSemiring
   modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
 

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

@@ -7,45 +7,44 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 import Lean.Meta.Tactic.Grind.Arith.Insts
+import Lean.Meta.Sym.Arith.Ring.Detect
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 
+open Sym.Arith.Ring (detectCommRing?)
+
 /--
-Returns the ring id for the given type if there is a `CommRing` instance for it.
-
-This function will also perform sanity-checks
-(e.g., the `Add` instance for `type` must be definitionally equal to the `CommRing.toAdd` one.)
-
-It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
+Returns the shared ring id for the given type if there is a `CommRing` instance for it.
+Uses the shared state in `arithRingExt` so that ring detection results and
+lazily-computed operations (e.g., `addFn?`) are shared between the arithmetic
+normalizer and grind's ring solver.
 -/
 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 semiringId? := none
-    let id := (← get').rings.size
-    let ring : CommRing := {
-      id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-    }
-    modify' fun s => { s with rings := s.rings.push ring }
-    return some id
+  let some sharedId ← detectCommRing? type | do
+    modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } none }
+    return none
+  let shared ← Sym.Arith.Ring.arithRingExt.getState
+  let tmpl := shared.rings[sharedId]!
+  trace_goal[grind.ring] "new ring: {type}"
+  trace_goal[grind.ring] "NoNatZeroDivisors available: {tmpl.noZeroDivInst?.isSome}"
+  -- Create grind-local entry at the shared ring id index, with fresh per-context state
+  let ring : CommRing := { tmpl with
+    toRing.id := sharedId
+    toRing.vars := {}
+    toRing.varMap := {}
+    toRing.denote := {}
+    denoteEntries := {}
+  }
+  -- Pad the rings array if needed to accommodate the shared id
+  while (← get').rings.size ≤ sharedId do
+    modify' fun s => { s with rings := s.rings.push default }
+  modify' fun s => { s with
+    rings := s.rings.set! sharedId ring
+    typeIdOf := s.typeIdOf.insert { expr := type } (some sharedId)
+  }
+  return some sharedId
 
 /--
 Returns the ring id for the given type if there is a `Ring` instance for it.

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
+public import Lean.Meta.Sym.Arith.Ring.SymExt
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 
@@ -60,6 +61,39 @@ instance : MonadCommRing RingM where
   getCommRing := RingM.getCommRing
   modifyCommRing := RingM.modifyCommRing
 
+/--
+`MonadRing` for grind's `RingM`. Reads lazy ops (`addFn?`, etc.) from the shared
+`arithRingExt` state, and per-context fields (`vars`, `varMap`, `denote`) from
+grind's local `CommRing`. Writes are routed to the appropriate state.
+-/
+instance : Sym.Arith.Ring.MonadRing RingM where
+  getRing := do
+    let ringId ← getRingId
+    let s ← Sym.Arith.Ring.arithRingExt.getState
+    let sharedRing := s.rings[ringId]!.toRing
+    let localRing := (← RingM.getCommRing).toRing
+    return { sharedRing with vars := localRing.vars, varMap := localRing.varMap, denote := localRing.denote }
+  modifyRing f := do
+    let ringId ← getRingId
+    let s ← Sym.Arith.Ring.arithRingExt.getState
+    let sharedRing := s.rings[ringId]!.toRing
+    let localRing := (← RingM.getCommRing).toRing
+    let combined : Sym.Arith.Ring.Ring :=
+      { sharedRing with vars := localRing.vars, varMap := localRing.varMap, denote := localRing.denote }
+    let new := f combined
+    -- Write lazy ops to shared state
+    Sym.Arith.Ring.arithRingExt.modifyState fun s => { s with rings := s.rings.modify ringId fun r =>
+      { r with toRing := { r.toRing with
+        addFn? := new.addFn?, mulFn? := new.mulFn?, subFn? := new.subFn?,
+        negFn? := new.negFn?, powFn? := new.powFn?, intCastFn? := new.intCastFn?,
+        natCastFn? := new.natCastFn?, one? := new.one?
+      }}
+    }
+    -- Write per-context to grind local
+    RingM.modifyCommRing fun s => { s with toRing := { s.toRing with
+      vars := new.vars, varMap := new.varMap, denote := new.denote
+    }}
+
 abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
   withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
 

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

@@ -7,17 +7,13 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Sym.Arith.Ring.Types
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing
+export Sym.Arith.Ring (Ring Semiring CommSemiring RingExpr SemiringExpr)
 export Lean.Grind.CommRing (Var Power Mon Poly)
-abbrev RingExpr := Grind.CommRing.Expr
-/-
-**Note**: recall that we use ring expressions to represent semiring expressions,
-and ignore non-applicable constructors.
--/
-abbrev SemiringExpr := Grind.CommRing.Expr
 
 mutual
 structure EqCnstr where
@@ -143,79 +139,8 @@ structure DiseqCnstr where
   -/
   ofSemiring? : Option (SemiringExpr × SemiringExpr)
 
-/-- Shared state for non-commutative and commutative semirings. -/
-structure Semiring where
-  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 := {}
-  /--
-  Mapping from variables to their denotations.
-  Remark each variable can be in only one ring.
-  -/
-  vars           : PArray Expr := {}
-  /-- Mapping from `Expr` to a variable representing it. -/
-  varMap         : PHashMap ExprPtr Var := {}
-  deriving Inhabited
-
-/-- Shared state for non-commutative and commutative rings. -/
-structure Ring where
-  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.
-  -/
-  vars           : PArray Expr := {}
-  /-- Mapping from `Expr` to a variable representing it. -/
-  varMap         : PHashMap ExprPtr Var := {}
-  /-- Mapping from Lean expressions to their representations as `RingExpr` -/
-  denote         : PHashMap ExprPtr RingExpr := {}
-  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
-  /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
-  denoteEntries  : PArray (Expr × RingExpr) := {}
+structure CommRing extends Sym.Arith.Ring.CommRing where
   /-- Next unique id for `EqCnstr`s. -/
   nextId         : Nat := 0
   /-- Number of "steps": simplification and superposition. -/
@@ -246,19 +171,7 @@ structure CommRing extends Ring where
   numEq0Updated  : Bool := false
   deriving Inhabited
 
-/--
-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
-  deriving Inhabited
+-- CommSemiring is reused from Sym.Arith.Ring.CommSemiring via the export above.
 
 /-- State for all `CommRing` types detected by `grind`. -/
 structure State where

tests/lean/run/grind_9427.lean

@@ -31,7 +31,6 @@ example (x y z : BitVec 100000) : x * y - z*z = 0 → z*z = y * x := by
 
 /--
 trace: [grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
-[grind.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
 -/
 #guard_msgs in
 set_option trace.grind.issues true in

tests/lean/run/sym_simp_arith1.lean

@@ -0,0 +1,49 @@
+import Lean.Meta.Sym.Simp.ArithNorm
+import Lean.Meta.Sym.Simp.Main
+
+/-!
+# Tests for the arithmetic normalizer simproc in Sym.simp
+
+Tests that the `mkArithNormSimproc` correctly normalizes ring expressions
+to polynomial normal form.
+-/
+
+set_option maxRecDepth 4000
+
+open Lean Meta Sym Sym.Simp in
+private def runArithNorm (mkExpr : MetaM Expr) : MetaM String := do
+  SymM.run do
+    let arithNorm ← mkArithNormSimproc
+    let e ← shareCommon (← mkExpr)
+    let r ← SimpM.run' (arithNorm e) {} {}
+    match r with
+    | .step e' _ _ => return s!"{← ppExpr e'}"
+    | .rfl _ => return s!"rfl({← ppExpr e})"
+
+-- Basic arithmetic on Int
+/-- info: "5" -/
+#guard_msgs in
+open Lean Meta in
+#eval runArithNorm (mkAppM ``HAdd.hAdd #[mkIntLit 2, mkIntLit 3])
+
+/-- info: "6" -/
+#guard_msgs in
+open Lean Meta in
+#eval runArithNorm (mkAppM ``HMul.hMul #[mkIntLit 2, mkIntLit 3])
+
+/-- info: "-1" -/
+#guard_msgs in
+open Lean Meta in
+#eval runArithNorm (mkAppM ``HSub.hSub #[mkIntLit 2, mkIntLit 3])
+
+-- Symbolic: (a + b) + (a + b) normalizes to 2*a + 2*b
+/-- info: "2 * ?a + 2 * ?b" -/
+#guard_msgs in
+open Lean Meta in
+#eval show MetaM String from do
+  let a ← mkFreshExprMVar (mkConst ``Int)
+  a.mvarId!.setUserName `a
+  let b ← mkFreshExprMVar (mkConst ``Int)
+  b.mvarId!.setUserName `b
+  let ab ← mkAppM ``HAdd.hAdd #[a, b]
+  runArithNorm (mkAppM ``HAdd.hAdd #[ab, ab])