feat: AC module invariants

src/Init/Grind/AC.lean

@@ -478,6 +478,13 @@ theorem eq_erase_dup {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_ : S
       (lhs rhs lhs' rhs' : Seq) : eq_erase_dup_cert lhs rhs lhs' rhs' → lhs.denote ctx = rhs.denote ctx → lhs'.denote ctx = rhs'.denote ctx := by
   simp [eq_erase_dup_cert]; intro _ _; subst lhs' rhs'; simp
 
+noncomputable def eq_erase0_cert (lhs rhs lhs' rhs' : Seq) : Bool :=
+  lhs.erase0.beq' lhs' |>.and' (rhs.erase0.beq' rhs')
+
+theorem eq_erase0 {α} (ctx : Context α) {_ : Std.Associative ctx.op} {_ : Std.LawfulIdentity ctx.op (Var.denote ctx 0)}
+      (lhs rhs lhs' rhs' : Seq) : eq_erase0_cert lhs rhs lhs' rhs' → lhs.denote ctx = rhs.denote ctx → lhs'.denote ctx = rhs'.denote ctx := by
+  simp [eq_erase0_cert]; intro _ _; subst lhs' rhs'; simp
+
 theorem diseq_norm_a {α} (ctx : Context α) {_ : Std.Associative ctx.op} (lhs rhs : Expr) (lhs' rhs' : Seq)
     : eq_norm_a_cert lhs rhs lhs' rhs' → lhs.denote ctx ≠ rhs.denote ctx → lhs'.denote ctx ≠ rhs'.denote ctx := by
   simp [eq_norm_a_cert]; intro _ _; subst lhs' rhs'; simp

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

@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.AC.Util
 import Lean.Meta.Tactic.Grind.AC.DenoteExpr
 import Lean.Meta.Tactic.Grind.AC.Proof
 import Lean.Meta.Tactic.Grind.AC.Seq
+import Lean.Meta.Tactic.Grind.AC.Inv
 public section
 namespace Lean.Meta.Grind.AC
 open Lean.Grind
@@ -79,6 +80,18 @@ def EqCnstr.eraseDup (c : EqCnstr) : ACM EqCnstr := do
   else
     return { c with lhs, rhs, h := .erase_dup c }
 
+def EqCnstr.erase0 (c : EqCnstr) : ACM EqCnstr := do
+  unless (← hasNeutral) do return c
+  let lhs := c.lhs.erase0
+  let rhs := c.rhs.erase0
+  if c.lhs == lhs && c.rhs == rhs then
+    return c
+  else
+    return { c with lhs, rhs, h := .erase0 c }
+
+def EqCnstr.cleanup (c : EqCnstr) : ACM EqCnstr := do
+  (← c.eraseDup).erase0
+
 def EqCnstr.orient (c : EqCnstr) : EqCnstr :=
   if compare c.rhs c.lhs == .gt then
     { c with lhs := c.rhs, rhs := c.lhs, h := .swap c }
@@ -127,16 +140,16 @@ private def simplifyRhsWithA (c : EqCnstr) (c' : EqCnstr) (r : AC.SubseqResult)
 
 /-- Simplifies `c` using the basis when `(← isCommutative)` is `false` -/
 private def EqCnstr.simplifyA (c : EqCnstr) : ACM EqCnstr := do
-  let mut c ← c.eraseDup
+  let mut c ← c.cleanup
   repeat
     incSteps
     if (← checkMaxSteps) then return c
     if let some (c', r) ← c.lhs.findSimpA? then
       c := simplifyLhsWithA c c' r
-      c ← c.eraseDup
+      c ← c.cleanup
     else if let some (c', r) ← c.rhs.findSimpA? then
       c := simplifyRhsWithA c c' r
-      c ← c.eraseDup
+      c ← c.cleanup
     else
       trace[grind.debug.ac.simplify] "{← c.denoteExpr}"
       return c
@@ -178,16 +191,16 @@ private def simplifyWithAC' (c : EqCnstr) (c' : EqCnstr) : Option EqCnstr := do
 
 /-- Simplify `c` using the basis when `(← isCommutative)` is `true` -/
 private def EqCnstr.simplifyAC (c : EqCnstr) : ACM EqCnstr := do
-  let mut c ← c.eraseDup
+  let mut c ← c.cleanup
   repeat
     incSteps
     if (← checkMaxSteps) then return c
     if let some (c', r) ← c.lhs.findSimpAC? then
       c := simplifyLhsWithAC c c' r
-      c ← c.eraseDup
+      c ← c.cleanup
     else if let some (c', r) ← c.rhs.findSimpAC? then
       c := simplifyRhsWithAC c c' r
-      c ← c.eraseDup
+      c ← c.cleanup
     else
       trace[grind.debug.ac.simplify] "{← c.denoteExpr}"
       return c
@@ -273,4 +286,21 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := withExprs a b do
   let rhs ← norm eb
   { lhs, rhs, h := .core a b ea eb : DiseqCnstr }.assert
 
+def checkStruct : ACM Bool := do
+  -- TODO
+  return false
+
+def check : GoalM Bool := do profileitM Exception "grind ac" (← getOptions) do
+  if (← checkMaxSteps) then return false
+  let mut progress := false
+  checkInvariants
+  try
+    for opId in *...(← get').structs.size do
+      let r ← ACM.run opId checkStruct
+      progress := progress || r
+      if (← isInconsistent) then return true
+    return progress
+  finally
+    checkInvariants
+
 end Lean.Meta.Grind.AC

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

@@ -0,0 +1,60 @@
+/-
+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.AC.Util
+import Lean.Meta.Tactic.Grind.AC.Seq
+namespace Lean.Meta.Grind.AC
+open Lean.Grind
+
+def checkVars : ACM Unit := do
+  let s ← getStruct
+  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
+
+def checkSeq (s : AC.Seq) : ACM Unit := do
+  if (← isCommutative) then
+    assert! s.isSorted
+  if (← hasNeutral) then
+    assert! !s.contains 0 || s == .var 0
+  if (← isIdempotent) then
+    assert! s.noAdjacentDuplicates
+
+def checkLhsRhs (lhs rhs : AC.Seq) : ACM Unit := do
+  checkSeq lhs; checkSeq rhs
+
+def checkBasis : ACM Unit := do
+  for c in (← getStruct).basis do
+    assert! compare c.lhs c.rhs == .gt
+    checkLhsRhs c.lhs c.rhs
+
+def checkQueue : ACM Unit := do
+  for c in (← getStruct).queue do
+    checkLhsRhs c.lhs c.rhs
+
+def checkDiseqs : ACM Unit := do
+  for c in (← getStruct).diseqs do
+    checkLhsRhs c.lhs c.rhs
+
+def checkStructInvs : ACM Unit := do
+  checkVars
+  checkBasis
+  checkQueue
+  checkDiseqs
+
+public def checkInvariants : GoalM Unit := do
+  unless grind.debug.get (← getOptions) do return ()
+  for opId in *...(← get').structs.size do
+    ACM.run opId checkStructInvs
+
+end Lean.Meta.Grind.AC

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

@@ -190,4 +190,33 @@ example : Seq.subset (2::2) (0::1::2::2::3::4) = .strict (0::1::3::4) := rfl
 example : Seq.subset (1::2) (0::1::1::1::2::2::3::4) = .strict (0::1::1::2::3::4) := rfl
 example : Seq.subset (1::1::2) (0::1::1::1::2::2::3::4) = .strict (0::1::2::3::4) := rfl
 
+def Seq.isSorted (s : Seq) : Bool :=
+  match s with
+  | .var _ => true
+  | .cons x s => go x s
+where
+  go (x : Var) (s : Seq) : Bool :=
+    match s with
+    | .var y => x ≤ y
+    | .cons y s => x ≤ y && go y s
+
+def Seq.contains (s : Seq) (x : Var) : Bool :=
+  match s with
+  | .var y => x == y
+  | .cons y s => x == y || s.contains x
+
+def Seq.noAdjacentDuplicates (s : Seq) : Bool :=
+  match s with
+  | .var _ => true
+  | .cons x s => go x s
+where
+  go (x : Var) (s : Seq) : Bool :=
+    match s with
+    | .var y => x != y
+    | .cons y s => x != y && go y s
+
+example : Seq.erase0 (1::0) = 1 := rfl
+example : Seq.erase0 (0::1) = 1 := rfl
+example : Seq.erase0 (0::1::2) = 1::2 := rfl
+
 end Lean.Grind.AC

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

@@ -28,6 +28,7 @@ structure EqCnstr where
 inductive EqCnstrProof where
   | core (a b : Expr) (ea eb : AC.Expr)
   | erase_dup (c : EqCnstr)
+  | erase0 (c : EqCnstr)
   | swap (c : EqCnstr)
   | simp_exact (lhs : Bool) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : EqCnstr) (c₂ : EqCnstr)
@@ -59,6 +60,7 @@ structure DiseqCnstr where
 inductive DiseqCnstrProof where
   | core (a b : Expr) (ea eb : AC.Expr)
   | erase_dup (c : DiseqCnstr)
+  | erase0 (c : DiseqCnstr)
   | simp_ac (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
   | simp_suffix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)
   | simp_prefix (lhs : Bool) (s : AC.Seq) (c₁ : DiseqCnstr) (c₂ : EqCnstr)

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

@@ -0,0 +1,18 @@
+/-
+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.Types
+import Lean.Meta.Tactic.Grind.Arith.Main
+import Lean.Meta.Tactic.Grind.AC.Eq
+namespace Lean.Meta.Grind
+/--
+Checks whether satellite solvers can make progress (e.g., detect unsatisfiability, propagate equations, etc)
+-/
+public def check : GoalM Bool := do
+  Arith.check <||> AC.check
+
+namespace Lean.Meta.Grind

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

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

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

@@ -4,22 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Proof
-public import Lean.Meta.Tactic.Grind.MatchCond
-public import Lean.Meta.Tactic.Grind.Arith.Inv
-
-public section
-
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.Arith.Inv
+import Lean.Meta.Tactic.Grind.AC.Inv
 namespace Lean.Meta.Grind
-
 /-!
 Debugging support code for checking basic invariants.
 -/
 
-private def checkEqc (root : ENode) : GoalM Unit := do
+def checkEqc (root : ENode) : GoalM Unit := do
   let mut size := 0
   let mut curr := root.self
   repeat
@@ -55,7 +51,7 @@ def checkChild (e : Expr) (child : Expr) : GoalM Bool := do
   let some childRoot ← getRoot? child | return false
   return isSameExpr childRoot e
 
-private def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
+def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
   let_expr Grind.MatchCond parent ← parent | return false
   let mut curr := parent
   repeat
@@ -68,7 +64,7 @@ private def checkMatchCondParent (e : Expr) (parent : Expr) : GoalM Bool := do
     curr := b
   return false
 
-private def checkParents (e : Expr) : GoalM Unit := do
+def checkParents (e : Expr) : GoalM Unit := do
   if (← isRoot e) then
     for parent in (← getParents e) do
       if isMatchCond parent then
@@ -97,7 +93,7 @@ private def checkParents (e : Expr) : GoalM Unit := do
     -- All the parents are stored in the root of the equivalence class.
     assert! (← getParents e).isEmpty
 
-private def checkPtrEqImpliesStructEq : GoalM Unit := do
+def checkPtrEqImpliesStructEq : GoalM Unit := do
   let exprs ← getExprs
   for h₁ : i in *...exprs.size do
     let e₁ := exprs[i]
@@ -108,7 +104,7 @@ private def checkPtrEqImpliesStructEq : GoalM Unit := do
       -- and the two expressions must not be structurally equal
       assert! !Expr.equal e₁ e₂
 
-private def checkProofs : GoalM Unit := do
+def checkProofs : GoalM Unit := do
   let eqcs ← getEqcs
   for eqc in eqcs do
     for a in eqc do
@@ -119,10 +115,8 @@ private def checkProofs : GoalM Unit := do
           check p
           trace_goal[grind.debug.proofs] "checked: {← inferType p}"
 
-/--
-Checks basic invariants if `grind.debug` is enabled.
--/
-def checkInvariants (expensive := false) : GoalM Unit := do
+/-- Checks invariants if `grind.debug` is enabled. -/
+public def checkInvariants (expensive := false) : GoalM Unit := do
   if grind.debug.get (← getOptions) then
     for e in (← getExprs) do
       let node ← getENode e
@@ -132,10 +126,12 @@ def checkInvariants (expensive := false) : GoalM Unit := do
     if expensive then
       checkPtrEqImpliesStructEq
     Arith.checkInvariants
+    AC.checkInvariants
   if expensive && grind.debug.proofs.get (← getOptions) then
     checkProofs
 
-def Goal.checkInvariants (goal : Goal) (expensive := false) : GrindM Unit :=
+@[inherit_doc Grind.checkInvariants]
+public def Goal.checkInvariants (goal : Goal) (expensive := false) : GrindM Unit :=
   discard <| GoalM.run' goal <| Grind.checkInvariants expensive
 
 end Lean.Meta.Grind

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

@@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Intro
-public import Lean.Meta.Tactic.Grind.Arith
-public import Lean.Meta.Tactic.Grind.Split
-public import Lean.Meta.Tactic.Grind.EMatch
-public import Lean.Meta.Tactic.Grind.SearchM
-
+import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.Split
+import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.SearchM
+import Lean.Meta.Tactic.Grind.Check
 public section
-
 namespace Lean.Meta.Grind
 
 private partial def solve (generation : Nat) : SearchM Bool := withIncRecDepth do
@@ -22,7 +19,7 @@ private partial def solve (generation : Nat) : SearchM Bool := withIncRecDepth d
     return false -- `splitNext` should have been configured to not create choice points
   if (← getGoal).inconsistent then
     return true
-  if (← intros' generation <||> assertAll <||> Arith.check <||> splitNext <||> ematch) then
+  if (← intros' generation <||> assertAll <||> check <||> splitNext <||> ematch) then
     solve generation
   else
     return false