feat: add checkInvariants

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

@@ -15,6 +15,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 
 namespace Lean
 

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

@@ -7,6 +7,7 @@ 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
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 
 namespace Lean.Meta.Grind.Arith.CommRing
 /-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
@@ -321,6 +322,7 @@ private def propagateEqs : 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
       -- TODO: use `isEqv` more effectively
       unless (← isEqv a b) do
@@ -350,11 +352,15 @@ def checkRing : RingM Bool := do
 def check : GoalM Bool := do
   if (← checkMaxSteps) then return false
   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
+  checkInvariants
+  try
+    for ringId in [:(← get').rings.size] do
+      let r ← RingM.run ringId checkRing
+      progress := progress || r
+      if (← isInconsistent) then
+        return true
+    return progress
+  finally
+    checkInvariants
 
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,61 @@
+/-
+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.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+private def checkVars : RingM Unit := do
+  let s ← getRing
+  let mut num := 0
+  for ({ expr }, var) in s.varMap do
+    if h : var < s.vars.size then
+      let expr' := s.vars[var]
+      assert! isSameExpr expr expr'
+    else
+      unreachable!
+    num := num + 1
+  assert! s.vars.size == num
+
+private def checkPoly (p : Poly) : RingM Unit := do
+  assert! p.isSorted
+  assert! p.checkCoeffs
+  assert! p.checkNoUnitMon
+  assert! !(p matches .num _)
+
+private def checkBasis : RingM Unit := do
+  let mut x := 0
+  for cs in (← getRing).varToBasis do
+    for c in cs do
+      checkPoly c.p
+      let .add _ m _ := c.p | unreachable!
+      let .mult pw _ := m | unreachable!
+      assert! pw.x == x
+    x := x + 1
+
+private def checkQueue : RingM Unit := do
+  for c in (← getRing).queue do
+    checkPoly c.p
+
+private def checkDiseqs : RingM Unit := do
+  for c in (← getRing).diseqs do
+    checkPoly c.d.p
+
+private def checkRingInvs : RingM Unit := do
+  checkVars
+  checkBasis
+  checkQueue
+  checkDiseqs
+
+def checkInvariants : GoalM Unit := do
+  unless grind.debug.get (← getOptions) do return ()
+  for ringId in [: (← get').rings.size] do
+    RingM.run ringId do
+      assert! (← getRingId) == ringId
+      checkRingInvs
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -186,4 +186,13 @@ def Poly.isZero : Poly → Bool
   | .num 0 => true
   | _ => false
 
+def Poly.checkCoeffs : Poly → Bool
+  | .num _ => true
+  | .add k _ p => k != 0 && checkCoeffs p
+
+def Poly.checkNoUnitMon : Poly → Bool
+  | .num _ => true
+  | .add _ .unit _ => false
+  | .add _ _ p => p.checkNoUnitMon
+
 end Lean.Grind.CommRing