feat: ring action (#10834)

This PR implements the `ring` action for `grind`.

Author: leodemoura

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -114,7 +114,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
   evalCheck `linarith Arith.Linear.check Arith.Linear.pp?
 
 @[builtin_grind_tactic ring] def evalRing : GrindTactic := fun _ => do
-  evalCheck `ring Arith.CommRing.check Arith.CommRing.pp?
+  evalCheck `ring Arith.CommRing.check' Arith.CommRing.pp?
 
 @[builtin_grind_tactic ac] def evalAC : GrindTactic := fun _ => do
   evalCheck `ac AC.check' AC.pp?

src/Lean/Meta/Tactic/Grind/AC/Action.lean

@@ -10,12 +10,7 @@ import Lean.Meta.Tactic.Grind.AC.Eq
 namespace Lean.Meta.Grind.Action
 
 /-- Associative-Commutative solver action. -/
-public def ac : Action := fun goal kna kp => do
-  let (result, goal') ← GoalM.run goal AC.check
-  match result with
-  | .none       => kna goal'
-  | .progress   => kp goal'
-  | .propagated => concatTactic (← kp goal') `(grind| ac)
-  | .closed     => closeWith `(grind| ac)
+public def ac : Action :=
+  solverAction AC.check `(grind| ac)
 
 end Lean.Meta.Grind.Action

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+public import Lean.Meta.Tactic.Grind.CheckResult
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -257,6 +258,22 @@ def terminalAction (check : GoalM Bool) (mkTac : GrindM (TSyntax `grind)) : Acti
   else
     kna goal'
 
+/--
+Helper action for satellite solvers that use `CheckResult`.
+-/
+def solverAction (check : GoalM CheckResult) (mkTac : GrindM (TSyntax `grind)) : Action := fun goal kna kp => do
+  let (result, goal') ← GoalM.run goal check
+  match result with
+  | .none       => kna goal'
+  | .progress   => kp goal'
+  | .propagated =>
+    let goal' ← GoalM.run' goal' processNewFacts
+    if goal'.inconsistent then
+      closeWith mkTac
+    else
+      concatTactic (← kp goal') mkTac
+  | .closed     => closeWith mkTac
+
 /--
 Helper action that checks whether the resulting tactic script produced by its continuation
 can close the original goal.

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

@@ -25,6 +25,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 builtin_initialize registerTraceClass `grind.ring
@@ -52,7 +53,7 @@ builtin_initialize
     (internalize := CommRing.internalize)
     (newEq       := CommRing.processNewEq)
     (newDiseq    := CommRing.processNewDiseq)
-    (check       := CommRing.check)
+    (check       := CommRing.check')
     (checkInv    := CommRing.checkInvariants)
     (mkTactic?   := return some (← `(grind| ring)))
 

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

@@ -0,0 +1,16 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Action
+import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
+namespace Lean.Meta.Grind.Action
+
+/-- Ring solver action. -/
+public def ring : Action :=
+  solverAction Arith.CommRing.check `(grind| ring)
+
+end Lean.Meta.Grind.Action

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+public import Lean.Meta.Tactic.Grind.CheckResult
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util
@@ -485,29 +486,31 @@ abbrev PropagateEqMap := Std.HashMap (Int × Poly) (Expr × RingExpr)
 /--
 Propagates implied equalities.
 -/
-private def propagateEqs : RingM Unit := do
-  if (← isInconsistent) then return ()
+private def propagateEqs : RingM Bool := do
+  if (← isInconsistent) then return false
   /-
   This is a very simple procedure that does not use any indexing data-structure.
   We don't even cache the simplified polynomials.
   TODO: optimize
   TODO: support for semiring
   -/
-  let mut map : PropagateEqMap := {}
-  for a in (← getRing).vars do
-    if (← checkMaxSteps) then return ()
-    let some ra ← toRingExpr? a | unreachable!
-    map ← process map a ra
-  for (a, ra) in (← getCommRing).denoteEntries do
-    if (← checkMaxSteps) then return ()
-    map ← process map a ra
+  let go : StateT (Bool × PropagateEqMap) RingM Unit := do
+    for a in (← getRing).vars do
+      if (← checkMaxSteps) then return ()
+      let some ra ← toRingExpr? a | unreachable!
+      process a ra
+    for (a, ra) in (← getCommRing).denoteEntries do
+      if (← checkMaxSteps) then return ()
+      process a ra
+  let (_, (propagated, _)) ← go.run (false, {})
+  return propagated
 where
-  process (map : PropagateEqMap) (a : Expr) (ra : RingExpr) : RingM PropagateEqMap := do
+  process (a : Expr) (ra : RingExpr) : StateT (Bool × PropagateEqMap) RingM Unit := do
     let d : PolyDerivation := .input (← ra.toPolyM)
     let d ← d.simplify
     let k := d.getMultiplier
     trace_goal[grind.debug.ring.impEq] "{a}, {k}, {← d.p.denoteExpr}"
-    if let some (b, rb) := map[(k, d.p)]? then
+    if let some (b, rb) :=  (← get).2[(k, d.p)]? then
       -- TODO: use `isEqv` more effectively
       unless (← isEqv a b) do
         let p ← (ra.sub rb).toPolyM
@@ -518,40 +521,44 @@ where
             -- Given the multiplier `k' = d.getMultiplier`, we have that `k*(a - b) = 0`,
             -- but we cannot eliminate the `k` because we don't have `noZeroDivisors`.
             trace_goal[grind.ring.impEq] "skip: {← mkEq a b}, k: {k}, noZeroDivisors: false"
-            return map.insert (k, d.p) (a, ra)
+            modify fun (propagated, map) => (propagated, map.insert (k, d.p) (a, ra))
+            return ()
         trace_goal[grind.ring.impEq] "{← mkEq a b}, {k}, {← p.denoteExpr}"
         propagateEq a b ra rb d
-      return map
+        modify fun s => (true, s.2)
     else
-      return map.insert (k, d.p) (a, ra)
+      modify fun (propagated, map) => (propagated, map.insert (k, d.p) (a, ra))
 
-def checkRing : RingM Bool := do
-  unless (← needCheck) do return false
+def checkRing : RingM CheckResult := do
+  unless (← needCheck) do return .none
   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
-    if (← checkMaxSteps) then return true
+    if (← isInconsistent) then return .closed
+    if (← checkMaxSteps) then return .progress
   checkDiseqs
-  propagateEqs
+  if (← propagateEqs) then return .propagated
   modifyCommRing fun s => { s with recheck := false }
-  return true
+  return .progress
 
-def check : GoalM Bool := do profileitM Exception "grind ring" (← getOptions) do
-  if (← checkMaxSteps) then return false
-  let mut progress := false
+def check : GoalM CheckResult := do profileitM Exception "grind ring" (← getOptions) do
+  if (← checkMaxSteps) then return .none
+  let mut result : CheckResult := .none
   checkInvariants
   try
     for ringId in *...(← get').rings.size do
       let r ← RingM.run ringId checkRing
-      progress := progress || r
+      result := result.join r
       if (← isInconsistent) then
-        return true
-    return progress
+        return .closed
+    return result
   finally
     checkInvariants
 
+def check' : GoalM Bool :=
+  return (← check) != .none
+
 end Lean.Meta.Grind.Arith.CommRing