chore: fix tests

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

@@ -31,5 +31,6 @@ builtin_initialize registerTraceClass `grind.ring.superpose
 
 builtin_initialize registerTraceClass `grind.debug.ring.simp
 builtin_initialize registerTraceClass `grind.debug.ring.proof
+builtin_initialize registerTraceClass `grind.debug.ring.check
 
 end Lean

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

@@ -148,30 +148,49 @@ def EqCnstr.simplifyAndCheck (c : EqCnstr) : RingM (Option EqCnstr) := do
   else
     return some c
 
+def addToBasisCore (c : EqCnstr) : RingM Unit := do
+  let .add _ m _ := c.p | return ()
+  let .mult pw _ := m | return ()
+  trace_goal[grind.ring.assert.basis] "{← c.denoteExpr}"
+  modifyRing fun s => { s with
+    varToBasis := s.varToBasis.modify pw.x (c :: ·)
+    recheck := true
+  }
+
 def EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit := do
   let .add _ m _ := c.p | return ()
   let .mult pw _ := m | return ()
   let x := pw.x
   let cs := (← getRing).varToBasis[x]!
-  let cs ← cs.filterMapM fun c' => do
-    let .add _ m' _ := c'.p | return none
+  if cs.isEmpty then return ()
+  modifyRing fun s => { s with varToBasis := s.varToBasis.set x {} }
+  for c' in cs do
+    let .add _ m' _ := c'.p | pure ()
     if m.divides m' then
-      let c' ← c'.simplifyWith c'
-      if (← c'.checkConstant) then
-        return none
-      else
-        return some c'
+      let c'' ← c'.simplifyWith c
+      unless (← c''.checkConstant) do
+        addToBasisCore c''
     else
-      return some c'
-  modifyRing fun s => { s with varToBasis := s.varToBasis.set x cs }
+      addToBasisCore c'
 
 def EqCnstr.addToQueue (c : EqCnstr) : RingM Unit := do
   trace_goal[grind.ring.assert.queue] "{← c.denoteExpr}"
   modifyRing fun s => { s with queue := s.queue.insert c }
 
 def EqCnstr.superposeWith (c : EqCnstr) : RingM Unit := do
-  trace[grind.ring.superpose] "{← c.denoteExpr}"
-  return ()
+  let .add _ m _ := c.p | return ()
+  go m
+where
+  go : Mon → RingM Unit
+    | .unit => return ()
+    | .mult pw m => do
+      let x := pw.x
+      let cs := (← getRing).varToBasis[x]!
+      for c' in cs do
+        let r ← c.p.spolM c'.p
+        trace_goal[grind.ring.superpose] "{← c.denoteExpr}\nwith: {← c'.denoteExpr}\nresult: {← r.spol.denoteExpr} = 0"
+        addToQueue (← mkEqCnstr r.spol <| .superpose r.k₁ r.m₁ c r.k₂ r.m₂ c')
+      go m
 
 /--
 Tries to convert the leading monomial into a monic one.
@@ -203,10 +222,7 @@ def EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit := do
   let c ← c.toMonic
   c.simplifyBasis
   c.superposeWith
-  let .add _ m _ := c.p | return ()
-  let .mult pw _ := m | return ()
-  trace_goal[grind.ring.assert.basis] "{← c.denoteExpr}"
-  modifyRing fun s => { s with varToBasis := s.varToBasis.modify pw.x (c :: ·) }
+  addToBasisCore c
 
 def EqCnstr.addToBasis (c : EqCnstr) : RingM Unit := do
   let some c ← c.simplifyAndCheck | return ()
@@ -266,4 +282,41 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
       d := .input p
     }
 
+/--
+Returns `true` if the todo queue is not empty or the `recheck` flag is set to `true`
+-/
+private def needCheck : RingM Bool := do
+  unless (← isQueueEmpty) do return true
+  return (← getRing).recheck
+
+private def checkDiseqs : RingM Unit := do
+  let diseqs := (← getRing).diseqs
+  modifyRing fun s => { s with diseqs := {} }
+  -- No indexing simple
+  for diseq in diseqs do
+    addNewDiseq diseq
+    if (← isInconsistent) then return
+
+def checkRing : RingM Bool := do
+  unless (← needCheck) do return false
+  trace_goal[grind.debug.ring.check] "{(← getRing).type}"
+  repeat
+    checkSystem "ring"
+    let some c ← getNext? | break
+    trace_goal[grind.debug.ring.check] "{← c.denoteExpr}"
+    c.addToBasis
+    if (← isInconsistent) then return true
+  checkDiseqs
+  modifyRing fun s => { s with recheck := false }
+  return true
+
+def check : GoalM Bool := do
+  let mut progress := false
+  for ringId in [:(← get').rings.size] do
+    let r ← RingM.run ringId checkRing
+    progress := progress || r
+    if (← isInconsistent) then
+      return true
+  return progress
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -70,11 +70,11 @@ structure SPolResult where
   /-- The computed S-polynomial. -/
   spol : Poly := .num 0
   /-- Coefficient applied to polynomial `p₁`. -/
-  c₁   : Int  := 0
+  k₁   : Int  := 0
   /-- Monomial factor applied to polynomial `p₁`. -/
   m₁   : Mon  := .unit
   /-- Coefficient applied to polynomial `p₂`. -/
-  c₂   : Int  := 0
+  k₂   : Int  := 0
   /-- Monomial factor applied to polynomial `p₂`. -/
   m₂   : Mon  := .unit
 
@@ -107,7 +107,7 @@ def Poly.spol (p₁ p₂ : Poly) (char? : Option Nat := none) : SPolResult  :=
     let p₁   := p₁.mulMon' c₁ m₁ char?
     let p₂   := p₂.mulMon' c₂ m₂ char?
     let spol := p₁.combine' p₂ char?
-    { spol, c₁, m₁, c₂, m₂ }
+    { spol, m₁, m₂, k₁ := c₁, k₂ := c₂ }
   | _, _ => {}
 
 /--

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

@@ -168,6 +168,11 @@ structure Ring where
   /-- Disequalities. -/
   -- TODO: add indexing
   diseqs         : PArray DiseqCnstr := {}
+  /--
+  If `recheck` is `true`, then new equalities have been added to the basis since we checked
+  disequalities and implied equalities.
+  -/
+  recheck        : Bool := false
   deriving Inhabited
 
 /-- State for all `CommRing` types detected by `grind`. -/

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

@@ -104,4 +104,15 @@ def _root_.Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : RingM Poly := do
 def _root_.Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : RingM Poly :=
   return p₁.combine' p₂ (← nonzeroChar?)
 
+def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommRing.SPolResult := do
+  if let some c ← nonzeroChar? then return p₁.spol p₂ c else return p₁.spol p₂
+
+def isQueueEmpty : RingM Bool :=
+  return (← getRing).queue.isEmpty
+
+def getNext? : RingM (Option EqCnstr) := do
+  let some c := (← getRing).queue.min | return none
+  modifyRing fun s => { s with queue := s.queue.erase c }
+  return some c
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -555,4 +555,19 @@ def searchAssigment : GoalM Unit := do
   -- TODO: constructing a model is only worth if `grind` will **not** continue searching.
   assignElimVars
 
+/--
+Returns `true` if work/progress has been done.
+There are two kinds of progress:
+- An assignment for satisfying constraints was constructed.
+- An inconsistency was detected.
+
+The result is `false` if module already has a satisfying assignment.
+-/
+def check : GoalM Bool := do
+  if (← hasAssignment) then
+    return false
+  else
+    searchAssigment
+    return true
+
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Grind.Combinators
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
+import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 
 namespace Lean.Meta.Grind.Arith
 
@@ -38,11 +39,9 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do
 
 def check : GrindTactic := fun goal => do
   let (progress, goal) ← GoalM.run goal do
-    if (← Cutsat.hasAssignment) then
-      return false
-    else
-      Cutsat.searchAssigment
-      return true
+    let c₁ ← Cutsat.check
+    let c₂ ← CommRing.check
+    return c₁ || c₂
   unless progress do
     return none
   if goal.inconsistent then

tests/lean/run/grind_ring_2.lean

@@ -42,3 +42,12 @@ example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
 
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
   grind +ring
+
+example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
+  grind +ring
+
+example [CommRing α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
+  grind +ring
+
+example (x y : BitVec 16) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
+  grind +ring

tests/lean/run/grind_spoly.lean

@@ -30,7 +30,7 @@ def check_spoly (e₁ e₂ r : Expr) : Bool :=
   spol' p₁ p₂ == r &&
   spol' p₂ p₁ == r.mulConst (-1) &&
   s.spol == r &&
-  r == (p₁.mulMon s.c₁ s.m₁).combine (p₂.mulMon s.c₂ s.m₂)
+  r == (p₁.mulMon s.k₁ s.m₁).combine (p₂.mulMon s.k₂ s.m₂)
 
 example : check_spoly (y^2 - x + 1) (x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide
 example : check_spoly (y - z + 1) (x*y - 1) (-x*z + 1 + x) := by native_decide