feat: add mkEqCnstr

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

@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Eq
+import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 
@@ -25,5 +25,7 @@ builtin_initialize registerTraceClass `grind.ring.assert.unsat (inherited := tru
 builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := true)
 builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true)
 builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.simp
+
 
 end Lean

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

@@ -12,65 +12,53 @@ namespace Lean.Meta.Grind.Arith.CommRing
 Helper functions for converting reified terms back into their denotations.
 -/
 
-private def denoteNum (ring : Ring) (k : Int) : MetaM Expr := do
-  return mkApp ring.intCastFn (toExpr k)
+private def denoteNum (k : Int) : RingM Expr := do
+  return mkApp (← getRing).intCastFn (toExpr k)
 
-def _root_.Lean.Grind.CommRing.Power.denoteExpr' (ring : Ring) (pw : Power) : MetaM Expr := do
-  let x := ring.vars[pw.x]!
+def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : RingM Expr := do
+  let x := (← getRing).vars[pw.x]!
   if pw.k == 1 then
     return x
   else
-    return mkApp2 ring.powFn x (toExpr pw.k)
+    return mkApp2 (← getRing).powFn x (toExpr pw.k)
 
-def _root_.Lean.Grind.CommRing.Mon.denoteExpr' (ring : Ring) (m : Mon) : MetaM Expr := do
+def _root_.Lean.Grind.CommRing.Mon.denoteExpr (m : Mon) : RingM Expr := do
   match m with
-  | .unit => denoteNum ring 1
-  | .mult pw m => go m (← pw.denoteExpr' ring)
+  | .unit => denoteNum 1
+  | .mult pw m => go m (← pw.denoteExpr)
 where
-  go (m : Mon) (acc : Expr) : MetaM Expr := do
+  go (m : Mon) (acc : Expr) : RingM Expr := do
     match m with
     | .unit => return acc
-    | .mult pw m => go m (mkApp2 ring.mulFn acc (← pw.denoteExpr' ring))
+    | .mult pw m => go m (mkApp2 (← getRing).mulFn acc (← pw.denoteExpr))
 
-def _root_.Lean.Grind.CommRing.Poly.denoteExpr' (ring : Ring) (p : Poly) : MetaM Expr := do
+def _root_.Lean.Grind.CommRing.Poly.denoteExpr (p : Poly) : RingM Expr := do
   match p with
-  | .num k => denoteNum ring k
+  | .num k => denoteNum k
   | .add k m p => go p (← denoteTerm k m)
 where
-  denoteTerm (k : Int) (m : Mon) : MetaM Expr := do
+  denoteTerm (k : Int) (m : Mon) : RingM Expr := do
     if k == 1 then
-      m.denoteExpr' ring
+      m.denoteExpr
     else
-      return mkApp2 ring.mulFn (← denoteNum ring k) (← m.denoteExpr' ring)
+      return mkApp2 (← getRing).mulFn (← denoteNum k) (← m.denoteExpr)
 
-  go (p : Poly) (acc : Expr) : MetaM Expr := do
+  go (p : Poly) (acc : Expr) : RingM Expr := do
     match p with
     | .num 0 => return acc
-    | .num k => return mkApp2 ring.addFn acc (← denoteNum ring k)
-    | .add k m p => go p (mkApp2 ring.addFn acc (← denoteTerm k m))
+    | .num k => return mkApp2 (← getRing).addFn acc (← denoteNum k)
+    | .add k m p => go p (mkApp2 (← getRing).addFn acc (← denoteTerm k m))
 
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr' (ring : Ring) (e : RingExpr) : MetaM Expr := do
+def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : RingM Expr := do
   go e
 where
-  go : RingExpr → MetaM Expr
-  | .num k => denoteNum ring k
-  | .var x => return ring.vars[x]!
-  | .add a b => return mkApp2 ring.addFn (← go a) (← go b)
-  | .sub a b => return mkApp2 ring.subFn (← go a) (← go b)
-  | .mul a b => return mkApp2 ring.mulFn (← go a) (← go b)
-  | .pow a k => return mkApp2 ring.powFn (← go a) (toExpr k)
-  | .neg a => return mkApp ring.negFn (← go a)
-
-def _root_.Lean.Grind.CommRing.Power.denoteExpr (ringId : Nat) (pw : Power) : GoalM Expr := do
-  pw.denoteExpr' (← getRing ringId)
-
-def _root_.Lean.Grind.CommRing.Mon.denoteExpr (ringId : Nat) (m : Mon) : GoalM Expr := do
-  m.denoteExpr' (← getRing ringId)
-
-def _root_.Lean.Grind.CommRing.Poly.denoteExpr (ringId : Nat) (p : Poly) : GoalM Expr := do
-  p.denoteExpr' (← getRing ringId)
-
-def _root_.Lean.Grind.CommRing.Expr.denoteExpr (ringId : Nat) (e : RingExpr) : GoalM Expr := do
-  e.denoteExpr' (← getRing ringId)
+  go : RingExpr → RingM Expr
+  | .num k => denoteNum k
+  | .var x => return (← getRing).vars[x]!
+  | .add a b => return mkApp2 (← getRing).addFn (← go a) (← go b)
+  | .sub a b => return mkApp2 (← getRing).subFn (← go a) (← go b)
+  | .mul a b => return mkApp2 (← getRing).mulFn (← go a) (← go b)
+  | .pow a k => return mkApp2 (← getRing).powFn (← go a) (toExpr k)
+  | .neg a => return mkApp (← getRing).negFn (← go a)
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -1,72 +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
--/
-prelude
-import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
-import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-
-namespace Lean.Meta.Grind.Arith.CommRing
-
-private def toRingExpr? (ringId : Nat) (e : Expr) : GoalM (Option RingExpr) := do
-  let ring ← getRing ringId
-  if let some re := ring.denote.find? { expr := e } then
-    return some re
-  else if let some x := ring.varMap.find? { expr := e } then
-    return some (.var x)
-  else
-    reportIssue! "failed to convert to ring expression{indentExpr e}"
-    return none
-
-/-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
-private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do
-  let some ringId ← getTermRingId? a | return none
-  let some ringId' ← getTermRingId? b | return none
-  unless ringId == ringId' do return none -- This can happen when we have heterogeneous equalities
-  return ringId
-
-@[export lean_process_ring_eq]
-def processNewEqImpl (a b : Expr) : GoalM Unit := do
-  if isSameExpr a b then return () -- TODO: check why this is needed
-  let some ringId ← inSameRing? a b | return ()
-  trace[grind.ring.assert] "{← mkEq a b}"
-  let some ra ← toRingExpr? ringId a | return ()
-  let some rb ← toRingExpr? ringId b | return ()
-  let p ← (ra.sub rb).toPolyM ringId
-  if let .num k := p then
-    if k == 0 then
-      trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} = 0"
-    else if (← hasChar ringId) then
-      trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} = 0"
-      setEqUnsat ringId k a b ra rb
-    else
-      -- Remark: we currently don't do anything if the characteristic is not known.
-      trace[grind.ring.assert.discard] "{← p.denoteExpr ringId} = 0"
-    return ()
-
-  trace[grind.ring.assert.store] "{← p.denoteExpr ringId} = 0"
-  -- TODO: save equality
-
-@[export lean_process_ring_diseq]
-def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
-  let some ringId ← inSameRing? a b | return ()
-  trace[grind.ring.assert] "{mkNot (← mkEq a b)}"
-  let some ra ← toRingExpr? ringId a | return ()
-  let some rb ← toRingExpr? ringId b | return ()
-  let p ← (ra.sub rb).toPolyM ringId
-  if let .num k := p then
-    if k == 0 then
-      trace[grind.ring.assert.unsat] "{← p.denoteExpr ringId} ≠ 0"
-      setNeUnsat ringId a b ra rb
-    else
-      -- Remark: if the characteristic is known, it is trivial.
-      -- Otherwise, we don't do anything.
-      trace[grind.ring.assert.trivial] "{← p.denoteExpr ringId} ≠ 0"
-    return ()
-
-  trace[grind.ring.assert.store] "{← p.denoteExpr ringId} ≠ 0"
-  -- TODO: save disequalitys
-
-end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,125 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+/-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
+private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do
+  let some ringId ← getTermRingId? a | return none
+  let some ringId' ← getTermRingId? b | return none
+  unless ringId == ringId' do return none -- This can happen when we have heterogeneous equalities
+  return ringId
+
+def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
+  let id := (← getRing).nextId
+  let sugar := p.degree
+  modifyRing fun s => { s with nextId := s.nextId + 1 }
+  return { sugar, p, h, id }
+
+/--
+Returns the ring expression denoting the given Lean expression.
+Recall that we compute the ring expressions during internalization.
+-/
+private def toRingExpr? (e : Expr) : RingM (Option RingExpr) := do
+  let ring ← getRing
+  if let some re := ring.denote.find? { expr := e } then
+    return some re
+  else if let some x := ring.varMap.find? { expr := e } then
+    return some (.var x)
+  else
+    reportIssue! "failed to convert to ring expression{indentExpr e}"
+    return none
+
+/--
+Returns `some c`, where `c` is an equation from the basis whose leading monomial divides `m`.
+If `unitOnly` is true, only equations with a unit leading coefficient are considered.
+-/
+def _root_.Lean.Grind.CommRing.Mon.findSimp? (m : Mon) (unitOnly : Bool := false) : RingM (Option EqCnstr) :=
+  go m
+where
+  go : Mon → RingM (Option EqCnstr)
+    | .unit => return none
+    | .mult pw m' => do
+      for c in (← getRing).varToBasis[pw.x]! do
+        if !unitOnly || c.p.lc.natAbs == 1 then
+        if c.p.divides m then
+          return some c
+      go m'
+
+/--
+Returns `some c`, where `c` is an equation from the basis whose leading monomial divides some
+monomial in `p`.
+If `unitOnly` is true, only equations with a unit leading coefficient are considered.
+-/
+def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) (unitOnly : Bool := false) : RingM (Option EqCnstr) := do
+  match p with
+  | .num _ => return none
+  | .add _ m p =>
+    match (← m.findSimp? unitOnly) with
+    | some c => return some c
+    | none => p.findSimp? unitOnly
+
+/-- Simplify the given equation constraint using the current basis. -/
+def simplify (c : EqCnstr) : RingM EqCnstr := do
+  let mut c := c
+  repeat
+    checkSystem "ring"
+    let some c' ← c.p.findSimp? | return c
+    let some r := c'.p.simp? c.p | unreachable!
+    c := { c with
+      p := r.p
+      h := .simp c' c r.k₁ r.k₂ r.m
+    }
+    trace_goal[grind.ring.simp] "{← c.p.denoteExpr}"
+  return c
+
+@[export lean_process_ring_eq]
+def processNewEqImpl (a b : Expr) : GoalM Unit := do
+  if isSameExpr a b then return () -- TODO: check why this is needed
+  let some ringId ← inSameRing? a b | return ()
+  RingM.run ringId do
+    trace_goal[grind.ring.assert] "{← mkEq a b}"
+    let some ra ← toRingExpr? a | return ()
+    let some rb ← toRingExpr? b | return ()
+    let p ← (ra.sub rb).toPolyM
+    if let .num k := p then
+      if k == 0 then
+        trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} = 0"
+      else if (← hasChar) then
+        trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} = 0"
+        setEqUnsat k a b ra rb
+      else
+        -- Remark: we currently don't do anything if the characteristic is not known.
+        trace_goal[grind.ring.assert.discard] "{← p.denoteExpr} = 0"
+      return ()
+
+    trace_goal[grind.ring.assert.store] "{← p.denoteExpr} = 0"
+  -- TODO: save equality
+
+@[export lean_process_ring_diseq]
+def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
+  let some ringId ← inSameRing? a b | return ()
+  RingM.run ringId do
+    trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
+    let some ra ← toRingExpr? a | return ()
+    let some rb ← toRingExpr? b | return ()
+    let p ← (ra.sub rb).toPolyM
+    if let .num k := p then
+      if k == 0 then
+        trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} ≠ 0"
+        setNeUnsat a b ra rb
+      else
+        -- Remark: if the characteristic is known, it is trivial.
+        -- Otherwise, we don't do anything.
+        trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} ≠ 0"
+      return ()
+    trace_goal[grind.ring.assert.store] "{← p.denoteExpr} ≠ 0"
+    -- TODO: save disequalitys
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -36,10 +36,11 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
   let some ringId ← getRingId? type | return ()
-  let some re ← reify? e ringId | return ()
-  trace[grind.ring.internalize] "[{ringId}]: {e}"
-  setTermRingId e ringId
-  markAsCommRingTerm e
-  modifyRing ringId fun s => { s with denote := s.denote.insert { expr := e } re }
+  RingM.run ringId do
+    let some re ← reify? e | return ()
+    trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
+    setTermRingId e
+    markAsCommRingTerm e
+    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -110,9 +110,9 @@ structure SimpResult where
   /-- The resulting simplified polynomial after rewriting. -/
   p  : Poly := .num 0
   /-- The integer coefficient multiplied with polynomial `p₁` in the rewriting step. -/
-  c₁ : Int  := 0
+  k₁ : Int  := 0
   /-- The integer coefficient multiplied with polynomial `p₂` during rewriting. -/
-  c₂ : Int  := 0
+  k₂ : Int  := 0
   /-- The monomial factor applied to polynomial `p₁`. -/
   m  : Mon  := .unit
 
@@ -124,23 +124,43 @@ the leading monomial of `p₁`.
 -/
 def Poly.simp? (p₁ p₂ : Poly) : Option SimpResult :=
   match p₁ with
-  | .add k₁ m₁ p₁ =>
+  | .add k₁' m₁ p₁ =>
     let rec go? (p₂ : Poly) : Option SimpResult :=
       match p₂ with
-      | .add k₂ m₂ p₂ =>
+      | .add k₂' m₂ p₂ =>
         if m₁.divides m₂ then
           let m  := m₂.div m₁
-          let g  := Nat.gcd k₁.natAbs k₂.natAbs
-          let c₁ := -k₂/g
-          let c₂ := k₁/g
-          let p  := (p₁.mulMon c₁ m).combine (p₂.mulConst c₂)
-          some { p, c₁, c₂, m }
+          let g  := Nat.gcd k₁'.natAbs k₂'.natAbs
+          let k₁ := -k₂'/g
+          let k₂ := k₁'/g
+          let p  := (p₁.mulMon k₁ m).combine (p₂.mulConst k₂)
+          some { p, k₁, k₂, m }
         else if let some r := go? p₂ then
-          some { r with p := .add (k₂*r.c₂) m₂ r.p }
+          some { r with p := .add (k₂'*r.k₂) m₂ r.p }
         else
           none
       | .num _ => none
     go? p₂
   | _ => none
 
+def Poly.degree : Poly → Nat
+  | .num _ => 0
+  | .add _ m _ => m.degree
+
+/-- Returns `true` if the leading monomial of `p` divides `m`. -/
+def Poly.divides (p : Poly) (m : Mon) : Bool :=
+  match p with
+  | .num _ => true -- should be unreachable
+  | .add _ m' _ => m'.divides m
+
+/-- Returns the leading coefficient of the given polynomial -/
+def Poly.lc : Poly → Int
+ | .num k => k
+ | .add k _ _ => k
+
+/-- Returns the leading monomial of the given polynomial. -/
+def Poly.lm : Poly → Mon
+ | .num _ => .unit
+ | .add _ m _ => m
+
 end Lean.Grind.CommRing

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

@@ -14,28 +14,28 @@ namespace Lean.Meta.Grind.Arith.CommRing
 Returns a context of type `RArray α` containing the variables of the given ring.
 `α` is the type of the ring.
 -/
-def toContextExpr (ringId : Nat) : GoalM Expr := do
-  let ring ← getRing ringId
+def toContextExpr : RingM Expr := do
+  let ring ← getRing
   if h : 0 < ring.vars.size then
     RArray.toExpr ring.type id (RArray.ofFn (ring.vars[·]) h)
   else
     RArray.toExpr ring.type id (RArray.leaf (mkApp ring.natCastFn (toExpr 0)))
 
-private def mkLemmaPrefix (ringId : Nat) (declName declNameC : Name) : GoalM Expr := do
-  let ring ← getRing ringId
-  let ctx ← toContextExpr ringId
-  if let some (charInst, c) ← nonzeroCharInst? ringId then
+private def mkLemmaPrefix (declName declNameC : Name) : RingM Expr := do
+  let ring ← getRing
+  let ctx ← toContextExpr
+  if let some (charInst, c) ← nonzeroCharInst? then
     return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr c) ring.commRingInst charInst ctx
   else
     return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx
 
-def setNeUnsat (ringId : Nat) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
-  let h ← mkLemmaPrefix ringId ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
+def setNeUnsat (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
+  let h ← mkLemmaPrefix ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
   closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b)
 
-def setEqUnsat (ringId : Nat) (k : Int) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
-  let mut h ← mkLemmaPrefix ringId ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
-  let (charInst, c) ← getCharInst ringId
+def setEqUnsat (k : Int) (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
+  let mut h ← mkLemmaPrefix ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
+  let (charInst, c) ← getCharInst
   if c == 0 then
     h := mkApp h charInst
   closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b)

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

@@ -32,41 +32,40 @@ private def reportAppIssue (e : Expr) : GoalM Unit := do
 Converts a Lean expression `e` in the `CommRing` with id `ringId` into
 a `CommRing.Expr` object.
 -/
-partial def reify? (e : Expr) (ringId : Nat) : GoalM (Option RingExpr) := do
-  let ring ← getRing ringId
-  let toVar (e : Expr) : GoalM RingExpr := do
-    return .var (← mkVar e ringId)
-  let asVar (e : Expr) : GoalM RingExpr := do
+partial def reify? (e : Expr) : RingM (Option RingExpr) := do
+  let toVar (e : Expr) : RingM RingExpr := do
+    return .var (← mkVar e)
+  let asVar (e : Expr) : RingM RingExpr := do
     reportAppIssue e
-    return .var (← mkVar e ringId)
-  let rec go (e : Expr) : GoalM RingExpr := do
+    return .var (← mkVar e)
+  let rec go (e : Expr) : RingM RingExpr := do
     match_expr e with
     | HAdd.hAdd _ _ _ i a b =>
-      if isAddInst ring i then return .add (← go a) (← go b) else asVar e
+      if isAddInst (← getRing) i then return .add (← go a) (← go b) else asVar e
     | HMul.hMul _ _ _ i a b =>
-      if isMulInst ring i then return .mul (← go a) (← go b) else asVar e
+      if isMulInst (← getRing) i then return .mul (← go a) (← go b) else asVar e
     | HSub.hSub _ _ _ i a b =>
-      if isSubInst ring i then return .sub (← go a) (← go b) else asVar e
+      if isSubInst (← getRing) 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 ring i then return .pow (← go a) k else asVar e
+      if isPowInst (← getRing) i then return .pow (← go a) k else asVar e
     | Neg.neg _ i a =>
-      if isNegInst ring i then return .neg (← go a) else asVar e
+      if isNegInst (← getRing) i then return .neg (← go a) else asVar e
     | IntCast.intCast _ i e =>
-      if isIntCastInst ring i then
+      if isIntCastInst (← getRing) i then
         let some k ← getIntValue? e | toVar e
         return .num k
       else
         asVar e
     | NatCast.natCast _ i e =>
-      if isNatCastInst ring i then
+      if isNatCastInst (← getRing) i then
         let some k ← getNatValue? e | toVar e
         return .num k
       else
         asVar e
     | OfNat.ofNat _ n _ =>
       let some k ← getNatValue? n | toVar e
-      if (← withDefault <| isDefEq e (mkApp ring.natCastFn n)) then
+      if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then
         return .num k
       else
         asVar e
@@ -76,31 +75,31 @@ partial def reify? (e : Expr) (ringId : Nat) : GoalM (Option RingExpr) := do
     return none
   match_expr e with
   | HAdd.hAdd _ _ _ i a b =>
-    if isAddInst ring i then return some (.add (← go a) (← go b)) else asNone e
+    if isAddInst (← getRing) i then return some (.add (← go a) (← go b)) else asNone e
   | HMul.hMul _ _ _ i a b =>
-    if isMulInst ring i then return some (.mul (← go a) (← go b)) else asNone e
+    if isMulInst (← getRing) i then return some (.mul (← go a) (← go b)) else asNone e
   | HSub.hSub _ _ _ i a b =>
-    if isSubInst ring i then return some (.sub (← go a) (← go b)) else asNone e
+    if isSubInst (← getRing) i then return some (.sub (← go a) (← go b)) else asNone e
   | HPow.hPow _ _ _ i a b =>
     let some k ← getNatValue? b | return none
-    if isPowInst ring i then return some (.pow (← go a) k) else asNone e
+    if isPowInst (← getRing) i then return some (.pow (← go a) k) else asNone e
   | Neg.neg _ i a =>
-    if isNegInst ring i then return some (.neg (← go a)) else asNone e
+    if isNegInst (← getRing) i then return some (.neg (← go a)) else asNone e
   | IntCast.intCast _ i e =>
-    if isIntCastInst ring i then
+    if isIntCastInst (← getRing) i then
       let some k ← getIntValue? e | return none
       return some (.num k)
     else
       asNone e
   | NatCast.natCast _ i e =>
-    if isNatCastInst ring i then
+    if isNatCastInst (← getRing) i then
       let some k ← getNatValue? e | return none
       return some (.num k)
     else
       asNone e
   | OfNat.ofNat _ n _ =>
     let some k ← getNatValue? n | return none
-    if (← withDefault <| isDefEq e (mkApp ring.natCastFn n)) then
+    if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then
       return some (.num k)
     else
       asNone e

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

@@ -98,15 +98,15 @@ where
     let u ← getDecLevel type
     let ring := mkApp (mkConst ``Grind.CommRing [u]) type
     let .some commRingInst ← trySynthInstance ring | return none
-    trace[grind.ring] "new ring: {type}"
+    trace_goal[grind.ring] "new ring: {type}"
     let charInst? ← withNewMCtxDepth do
       let n ← mkFreshExprMVar (mkConst ``Nat)
       let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type commRingInst n
       let .some charInst ← trySynthInstance charType | pure none
       let n ← instantiateMVars n
       let some n ← evalNat n |>.run
-        | trace[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
-      trace[grind.ring] "characteristic: {n}"
+        | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none
+      trace_goal[grind.ring] "characteristic: {n}"
       pure <| some (charInst, n)
     let addFn ← getAddFn type u commRingInst
     let mulFn ← getMulFn type u commRingInst
@@ -116,7 +116,7 @@ where
     let intCastFn ← getIntCastFn type u commRingInst
     let natCastFn ← getNatCastFn type u commRingInst
     let id := (← get').rings.size
-    let ring : Ring := { type, u, commRingInst, charInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn }
+    let ring : Ring := { id, type, u, commRingInst, charInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id
 

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Data.PersistentArray
+import Lean.Data.RBTree
 import Lean.Meta.Tactic.Grind.ENodeKey
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
@@ -15,8 +16,39 @@ abbrev RingExpr := Grind.CommRing.Expr
 
 deriving instance Repr for Power, Mon, Poly
 
+mutual
+
+structure EqCnstr where
+  p     : Poly
+  h     : EqCnstrProof
+  sugar : Nat
+  id    : Nat
+
+inductive EqCnstrProof where
+  | core (a b : Expr)
+  | superpose (c₁ c₂ : EqCnstr)
+  | simp (c₁ c₂ : EqCnstr) (k₁ k₂ : Int) (m : Mon)
+  | mul (k : Int) (e : EqCnstr)
+  | div (k : Int) (e : EqCnstr)
+
+end
+
+instance : Inhabited EqCnstrProof where
+  default := .core default default
+
+instance : Inhabited EqCnstr where
+  default := { p := default, h := default, sugar := 0, id := 0 }
+
+protected def EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering :=
+  (compare c₁.sugar c₂.sugar) |>.then
+  (compare c₁.p.degree c₂.p.degree) |>.then
+  (compare c₁.id c₂.id)
+
+abbrev Queue : Type := RBTree EqCnstr EqCnstr.compare
+
 /-- State for each `CommRing` processed by this module. -/
 structure Ring where
+  id           : Nat
   type         : Expr
   /-- Cached `getDecLevel type` -/
   u            : Level
@@ -40,6 +72,17 @@ structure Ring where
   varMap       : PHashMap ENodeKey Var := {}
   /-- Mapping from Lean expressions to their representations as `RingExpr` -/
   denote       : PHashMap ENodeKey RingExpr := {}
+  /-- Next unique id for `EqCnstr`s. -/
+  nextId       : Nat := 0
+  /-- Number of "steps": simplification and superposition. -/
+  steps        : Nat := 0
+  /-- Equations to process. -/
+  queue        : Queue := {}
+  /--
+  Mapping from variables `x` to equations such that the smallest variable
+  in the leading monomial is `x`.
+  -/
+  varToBasis   : PArray (List EqCnstr) := {}
   deriving Inhabited
 
 /-- State for all `CommRing` types detected by `grind`. -/

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

@@ -14,51 +14,61 @@ def get' : GoalM State := do
 @[inline] def modify' (f : State → State) : GoalM Unit := do
   modify fun s => { s with arith.ring := f s.arith.ring }
 
-def getRing (ringId : Nat) : GoalM Ring := do
+/-- We don't want to keep carrying the `RingId` around. -/
+abbrev RingM := ReaderT Nat GoalM
+
+abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
+  x ringId
+
+abbrev getRingId : RingM Nat :=
+  read
+
+def getRing : RingM Ring := do
   let s ← get'
+  let ringId ← getRingId
   if h : ringId < s.rings.size then
     return s.rings[ringId]
   else
     throwError "`grind` internal error, invalid ringId"
 
-@[inline] def modifyRing (ringId : Nat) (f : Ring → Ring) : GoalM Unit := do
+@[inline] def modifyRing (f : Ring → Ring) : RingM Unit := do
+  let ringId ← getRingId
   modify' fun s => { s with rings := s.rings.modify ringId f }
 
 def getTermRingId? (e : Expr) : GoalM (Option Nat) := do
   return (← get').exprToRingId.find? { expr := e }
 
-def setTermRingId (e : Expr) (ringId : Nat) : GoalM Unit := do
+def setTermRingId (e : Expr) : RingM Unit := do
+  let ringId ← getRingId
   if let some ringId' ← getTermRingId? e then
     unless ringId' == ringId do
       reportIssue! "expression in two different rings{indentExpr e}"
     return ()
   modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
 
-/-- Returns `some c` if the given ring has a nonzero characteristic `c`. -/
-def nonzeroChar? (ringId : Nat) : GoalM (Option Nat) := do
-  let ring ← getRing ringId
-  if let some (_, c) := ring.charInst? then
+/-- Returns `some c` if the current ring has a nonzero characteristic `c`. -/
+def nonzeroChar? : RingM (Option Nat) := do
+  if let some (_, c) := (← getRing).charInst? then
     if c != 0 then
       return some c
   return none
 
-/-- Returns `some (charInst, c)` if the given ring has a nonzero characteristic `c`. -/
-def nonzeroCharInst? (ringId : Nat) : GoalM (Option (Expr × Nat)) := do
-  let ring ← getRing ringId
-  if let some (inst, c) := ring.charInst? then
+/-- Returns `some (charInst, c)` if the current ring has a nonzero characteristic `c`. -/
+def nonzeroCharInst? : RingM (Option (Expr × Nat)) := do
+  if let some (inst, c) := (← getRing).charInst? then
     if c != 0 then
       return some (inst, c)
   return none
 
-/-- Returns `true` if the ring has a `IsCharP` instance. -/
-def hasChar (ringId : Nat) : GoalM Bool := do
-  return (← getRing ringId).charInst?.isSome
+/-- Returns `true` if the current ring has a `IsCharP` instance. -/
+def hasChar  : RingM Bool := do
+  return (← getRing).charInst?.isSome
 
 /--
 Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
 -/
-def getCharInst (ringId : Nat) : GoalM (Expr × Nat) := do
-  let some c := (← getRing ringId).charInst?
+def getCharInst : RingM (Expr × Nat) := do
+  let some c := (← getRing).charInst?
     | throwError "`grind` internal error, ring does not have a characteristic"
   return c
 
@@ -66,8 +76,8 @@ def getCharInst (ringId : Nat) : GoalM (Expr × Nat) := do
 Converts the given ring expression into a multivariate polynomial.
 If the ring has a nonzero characteristic, it is used during normalization.
 -/
-def _root_.Lean.Grind.CommRing.Expr.toPolyM (ringId : Nat) (e : RingExpr) : GoalM Poly := do
-  if let some c ← nonzeroChar? ringId then
+def _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
+  if let some c ← nonzeroChar? then
     return e.toPolyC c
   else
     return e.toPoly

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

@@ -8,16 +8,17 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
-def mkVar (e : Expr) (ringId : Nat) : GoalM Var := do
-  let s ← getRing ringId
+def mkVar (e : Expr) : RingM Var := do
+  let s ← getRing
   if let some var := s.varMap.find? { expr := e } then
     return var
   let var : Var := s.vars.size
-  modifyRing ringId fun s => { s with
-    vars      := s.vars.push e
-    varMap    := s.varMap.insert { expr := e } var
+  modifyRing fun s => { s with
+    vars       := s.vars.push e
+    varMap     := s.varMap.insert { expr := e } var
+    varToBasis := s.varToBasis.push []
   }
-  setTermRingId e ringId
+  setTermRingId e
   markAsCommRingTerm e
   return var
 

tests/lean/run/grind_spoly.lean

@@ -49,7 +49,7 @@ def simp? (p₁ p₂ : Poly) : Option Poly :=
 
 partial def simp' (p₁ p₂ : Poly) : Poly :=
   if let some r := p₁.simp? p₂ then
-    assert! r.p == (p₁.mulMon r.c₁ r.m).combine (p₂.mulConst r.c₂)
+    assert! r.p == (p₁.mulMon r.k₁ r.m).combine (p₂.mulConst r.k₂)
     simp' p₁ r.p
   else
     p₂