refined PreNullCert

src/Init/Grind/CommRing/Poly.lean

@@ -387,6 +387,8 @@ def Poly.mulMonC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
   let k := k % c
   bif k == 0 then
     .num 0
+  else bif m == .unit then
+    p.mulConstC k c
   else
     go p
 where
@@ -802,24 +804,28 @@ theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context
     rw [← IsCharP.intCast_emod (p := c)]
     simp [denote, *, intCast_zero, zero_mul]
   next =>
-    fun_induction mulMonC.go <;> simp [mulMonC.go, denote, *, cond_eq_if]
+    split
     next h =>
-      simp +zetaDelta at h; simp [*, denote]
-      rw [mul_assoc, mul_left_comm, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c), h]
-      simp [intCast_zero, mul_zero]
-    next h =>
-      simp +zetaDelta at h; simp [*, denote, IsCharP.intCast_emod]
-      simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
-    next h _ =>
-      simp +zetaDelta at h; simp [*, denote, left_distrib]
-      rw [mul_left_comm]
-      conv => rhs; rw [← mul_assoc, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (p := c)]
-      rw [Int.mul_comm] at h
-      simp [h, intCast_zero, zero_mul, zero_add]
-    next h _ =>
-      simp +zetaDelta at h
-      simp [*, denote, IsCharP.intCast_emod, Mon.denote_mul, intCast_mul, left_distrib,
-        mul_comm, mul_left_comm, mul_assoc]
+      simp at h; simp [*, Mon.denote, mul_one, denote_mulConstC, IsCharP.intCast_emod]
+    next =>
+      fun_induction mulMonC.go <;> simp [mulMonC.go, denote, *, cond_eq_if]
+      next h =>
+        simp +zetaDelta at h; simp [*, denote]
+        rw [mul_assoc, mul_left_comm, ← intCast_mul, ← IsCharP.intCast_emod (x := k * _) (p := c), h]
+        simp [intCast_zero, mul_zero]
+      next h =>
+        simp +zetaDelta at h; simp [*, denote, IsCharP.intCast_emod]
+        simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
+      next h _ =>
+        simp +zetaDelta at h; simp [*, denote, left_distrib]
+        rw [mul_left_comm]
+        conv => rhs; rw [← mul_assoc, ← mul_assoc, ← intCast_mul, ← IsCharP.intCast_emod (p := c)]
+        rw [Int.mul_comm] at h
+        simp [h, intCast_zero, zero_mul, zero_add]
+      next h _ =>
+        simp +zetaDelta at h
+        simp [*, denote, IsCharP.intCast_emod, Mon.denote_mul, intCast_mul, left_distrib,
+          mul_comm, mul_left_comm, mul_assoc]
 
 theorem Poly.denote_combineC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
     : (combineC p₁ p₂ c).denote ctx = p₁.denote ctx + p₂.denote ctx := by

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

@@ -23,9 +23,12 @@ builtin_initialize registerTraceClass `grind.ring.internalize
 builtin_initialize registerTraceClass `grind.ring.assert
 builtin_initialize registerTraceClass `grind.ring.assert.unsat (inherited := true)
 builtin_initialize registerTraceClass `grind.ring.assert.trivial (inherited := true)
-builtin_initialize registerTraceClass `grind.ring.assert.store (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.queue (inherited := true)
+builtin_initialize registerTraceClass `grind.ring.assert.basis (inherited := true)
 builtin_initialize registerTraceClass `grind.ring.assert.discard (inherited := true)
 builtin_initialize registerTraceClass `grind.ring.simp
+builtin_initialize registerTraceClass `grind.ring.superpose
 
+builtin_initialize registerTraceClass `grind.debug.ring.simp
 
 end Lean

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

@@ -68,4 +68,7 @@ where
   | .pow a k => return mkApp2 (← getRing).powFn (← go a) (toExpr k)
   | .neg a => return mkApp (← getRing).negFn (← go a)
 
+def EqCnstr.denoteExpr (c : EqCnstr) : RingM Expr := do
+  mkEq (← c.p.denoteExpr) (← denoteNum 0)
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -65,20 +65,131 @@ def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) (unitOnly : Bool := fal
     | 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
+/-- Simplifies `c` using `c'`. -/
+def EqCnstr.simplify1 (c c' : EqCnstr) : RingM (Option EqCnstr) := do
+  let some r := c'.p.simp? c.p (← nonzeroChar?) | return none
+  let 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 some c
+
+/-- Keep simplifying `c` with `c'` until it is not applicable anymore. -/
+def EqCnstr.simplifyWith (c 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}"
+    let some r ← c.simplify1 c' | return c
+    trace_goal[grind.debug.ring.simp] "simplifying{indentD (← c.denoteExpr)}\nwith{indentD (← c'.denoteExpr)}"
+    c := r
   return c
 
+/-- Simplify the given equation constraint using the current basis. -/
+def EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr := do
+  let mut c := c
+  repeat
+    let some c' ← c.p.findSimp? |
+      trace_goal[grind.debug.ring.simp] "simplified{indentD (← c.denoteExpr)}"
+      return c
+    c ← c.simplifyWith c'
+  return c
+
+/-- Returns `true` if `c.p` is the constant polynomial. -/
+def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do
+  let .num k := c.p | return false
+  if k == 0 then
+    trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}"
+  else if (← hasChar) then
+    setInconsistent c
+  else
+    -- Remark: we currently don't do anything if the characteristic is not known.
+    trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}"
+  return true
+
+/--
+Simplifies and checks whether the resulting constraint is trivial (i.e., `0 = 0`),
+or inconsistent (i.e., `k = 0` where `k % c != 0` for a comm-ring with characteristic `c`),
+and returns `none`. Otherwise, returns the simplified constraint.
+-/
+def EqCnstr.simplifyAndCheck (c : EqCnstr) : RingM (Option EqCnstr) := do
+  let c ← c.simplify
+  if (← c.checkConstant) then
+    return none
+  else
+    return some c
+
+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 m.divides m' then
+      let c' ← c'.simplifyWith c'
+      if (← c'.checkConstant) then
+        return none
+      else
+        return some c'
+    else
+      return some c'
+  modifyRing fun s => { s with varToBasis := s.varToBasis.set x cs }
+
+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 ()
+
+/--
+Tries to convert the leading monomial into a monic one.
+
+It exploits the fact that given a polynomial with leading coefficient `k`,
+if the ring has a nonzero characteristic `p` and `gcd k p = 1`, then
+`k` has an inverse.
+
+It also handles the easy case where `k` is `-1`.
+-/
+def EqCnstr.toMonic (c : EqCnstr) : RingM EqCnstr := do
+  let k := c.p.lc
+  if k == 1 then return c
+  if let some p ← nonzeroChar? then
+    let (g, α, _β) := gcdExt k p
+    if g == 1 then
+      -- `α*k + β*p = 1`
+      -- `α*k = 1 (mod p)`
+      let α := if α < 0 then α % p else α
+      return { c with p := c.p.mulConstC α p, h := .mul α c }
+    else
+      return c
+  else if k == -1 then
+    return { c with p := c.p.mulConst (-1), h := .mul (-1) c }
+  else
+    return c
+
+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 :: ·) }
+
+def EqCnstr.addToBasis (c : EqCnstr) : RingM Unit := do
+  let some c ← c.simplifyAndCheck | return ()
+  c.addToBasisAfterSimp
+
+def addNewEq (c : EqCnstr) : RingM Unit := do
+  let some c ← c.simplifyAndCheck | return ()
+  if c.p.degree == 1 then
+    c.addToBasisAfterSimp
+  else
+    c.addToQueue
+
 @[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
@@ -88,6 +199,7 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     let some ra ← toRingExpr? a | return ()
     let some rb ← toRingExpr? b | return ()
     let p ← (ra.sub rb).toPolyM
+    -- TODO: delete this `if` after simplifier is fully integrated
     if let .num k := p then
       if k == 0 then
         trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} = 0"
@@ -98,9 +210,7 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
         -- 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
+    addNewEq (← mkEqCnstr p (.core a b ra rb))
 
 @[export lean_process_ring_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do

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

@@ -78,14 +78,24 @@ structure SPolResult where
   /-- Monomial factor applied to polynomial `p₂`. -/
   m₂   : Mon  := .unit
 
+def Poly.mulConst' (p : Poly) (k : Int) (char? : Option Nat := none) : Poly :=
+  if let some char := char? then p.mulConstC k char else p.mulConst k
+
+def Poly.mulMon' (p : Poly) (k : Int) (m : Mon) (char? : Option Nat := none) : Poly :=
+  if let some char := char? then p.mulMonC k m char else p.mulMon k m
+
+def Poly.combine' (p₁ p₂ : Poly) (char? : Option Nat := none) : Poly :=
+  if let some char := char? then p₁.combineC p₂ char else p₁.combine p₂
+
 /--
 Returns the S-polynomial of polynomials `p₁` and `p₂`, and coefficients&terms used to construct it.
 Given polynomials with leading terms `k₁*m₁` and `k₂*m₂`, the S-polynomial is defined as:
 ```
 S(p₁, p₂) = (k₂/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₁) * p₁ - (k₁/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₂) * p₂
 ```
+Remark: if `char? = some c`, then `c` is the characteristic of the ring.
 -/
-def Poly.spol (p₁ p₂ : Poly) : SPolResult  :=
+def Poly.spol (p₁ p₂ : Poly) (char? : Option Nat := none) : SPolResult  :=
   match p₁, p₂ with
   | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
     let m    := m₁.lcm m₂
@@ -94,9 +104,9 @@ def Poly.spol (p₁ p₂ : Poly) : SPolResult  :=
     let g    := Nat.gcd k₁.natAbs k₂.natAbs
     let c₁   := k₂/g
     let c₂   := -k₁/g
-    let p₁   := p₁.mulMon c₁ m₁
-    let p₂   := p₂.mulMon c₂ m₂
-    let spol := p₁.combine p₂
+    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₂ }
   | _, _ => {}
 
@@ -121,8 +131,10 @@ Simplifies polynomial `p₂` using polynomial `p₁` by rewriting.
 
 This function attempts to rewrite `p₂` by eliminating the first occurrence of
 the leading monomial of `p₁`.
+
+Remark: if `char? = some c`, then `c` is the characteristic of the ring.
 -/
-def Poly.simp? (p₁ p₂ : Poly) : Option SimpResult :=
+def Poly.simp? (p₁ p₂ : Poly) (char? : Option Nat := none) : Option SimpResult :=
   match p₁ with
   | .add k₁' m₁ p₁ =>
     let rec go? (p₂ : Poly) : Option SimpResult :=
@@ -133,10 +145,17 @@ def Poly.simp? (p₁ p₂ : Poly) : Option SimpResult :=
           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₂)
+          let p  := (p₁.mulMon' k₁ m char?).combine' (p₂.mulConst' k₂ char?) char?
           some { p, k₁, k₂, m }
         else if let some r := go? p₂ then
-          some { r with p := .add (k₂'*r.k₂) m₂ r.p }
+          if let some char := char? then
+            let k := (k₂'*r.k₂) % char
+            if k == 0 then
+              some r
+            else
+              some { r with p := .add k m₂ r.p }
+          else
+            some { r with p := .add (k₂'*r.k₂) m₂ r.p }
         else
           none
       | .num _ => none
@@ -163,4 +182,8 @@ def Poly.lm : Poly → Mon
  | .num _ => .unit
  | .add _ m _ => m
 
+def Poly.isZero : Poly → Bool
+  | .num 0 => true
+  | _ => false
+
 end Lean.Grind.CommRing

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 
 namespace Lean.Meta.Grind.Arith.CommRing
@@ -21,6 +22,88 @@ def toContextExpr : RingM Expr := do
   else
     RArray.toExpr ring.type id (RArray.leaf (mkApp ring.natCastFn (toExpr 0)))
 
+/--
+A "pre" Nullstellensatz certificate.
+Recall that, given the hypotheses `h₁ : lhs₁ = rhs₁` ... `hₙ : lhsₙ = rhsₙ`,
+a Nullstellensatz certificate is of the form
+```
+q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
+```
+Each hypothesis is an `EqCnstr` justified by a `.core ..` `EqnCnstrProof`.
+We dynamically associate them with unique indices based on the order we find them
+during traversal.
+For the other `EqCnstr`s we compute a "pre" certificate as a dense array
+containing `q₁` ... `qₙ` needed to create the `EqCnstr`.
+
+We are assuming the number of hypotheses used to derive a conclusion is small
+and a dense array is a reasonable representation.
+-/
+structure PreNullCert where
+  qs : Array Poly
+  /--
+  We don't use rational coefficients in the polynomials.
+  Thus, we need to track a denominator to justify the proof step `div`.
+  -/
+  d  : Int := 1
+
+def PreNullCert.unit (i : Nat) (n : Nat) : PreNullCert :=
+  let qs := Array.replicate n (.num 0)
+  let qs := qs.set! i (.num 1)
+  { qs }
+
+def PreNullCert.mul (c : PreNullCert) (k : Int) (char? : Option Nat) : PreNullCert :=
+  if k == 1 then c
+  else
+    let g := Int.gcd k c.d
+    let k := k / g
+    let d := c.d / g
+    if k == 1 then
+      { c with d }
+    else
+      let qs := c.qs.map fun q => if q.isZero then q else q.mulConst' k char?
+      { qs, d }
+
+def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : Int) (m₂ : Mon) (c₂ : PreNullCert) (char? : Option Nat) : PreNullCert := Id.run do
+  let d₁    := c₁.d
+  let d₂    := c₂.d
+  let k₁_d₂ := k₁*d₂
+  let k₂_d₁ := k₂*d₁
+  let d₁_d₂ := d₁*d₂
+  let g     := Int.gcd (Int.gcd k₁_d₂ k₂_d₁) d₁_d₂
+  let k₁    := k₁_d₂ / g
+  let k₂    := k₂_d₁ / g
+  let d     := d₁_d₂ / g
+  let qs₁   := c₁.qs
+  let qs₂   := c₂.qs
+  let n := Nat.max qs₁.size qs₂.size
+  let mut qs : Vector Poly n := Vector.replicate n (.num 0)
+  for h : i in [:n] do
+    if h₁ : i < qs₁.size then
+      let q₁ := qs₁[i].mulMon' k₁ m₁ char?
+      if h₂ : i < qs₂.size then
+        let q₂ := qs₂[i].mulMon' k₂ m₂ char?
+        qs := qs.set i (q₁.combine' q₂ char?)
+      else
+        qs := qs.set i q₁
+    else
+      have : i < n := h.upper
+      have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta [Nat.max_def]; split <;> simp [*]
+      have : i < qs₂.size := by omega
+      let q₂ := qs₂[i].mulMon' k₂ m₂ char?
+      qs := qs.set i q₂
+  return { qs := qs.toArray, d }
+
+structure NullCertHypothesis where
+  h   : Expr
+  lhs : RingExpr
+  rhs : RingExpr
+
+structure ProofM.State where
+  /-- Mapping from `EqCnstr` to `PreNullCert` -/
+  cache       : Std.HashMap UInt64 PreNullCert := {}
+  hypToId     : Std.HashMap UInt64 Nat := {}
+  hyps        : Array NullCertHypothesis := #[]
+
 private def mkLemmaPrefix (declName declNameC : Name) : RingM Expr := do
   let ring ← getRing
   let ctx ← toContextExpr
@@ -40,4 +123,8 @@ def setEqUnsat (k : Int) (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
     h := mkApp h charInst
   closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b)
 
+def setInconsistent (c : EqCnstr) : RingM Unit := do
+  trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
+  -- TODO
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -25,7 +25,7 @@ structure EqCnstr where
   id    : Nat
 
 inductive EqCnstrProof where
-  | core (a b : Expr)
+  | core (a b : Expr) (ra rb : RingExpr)
   | superpose (c₁ c₂ : EqCnstr)
   | simp (c₁ c₂ : EqCnstr) (k₁ k₂ : Int) (m : Mon)
   | mul (k : Int) (e : EqCnstr)
@@ -34,7 +34,7 @@ inductive EqCnstrProof where
 end
 
 instance : Inhabited EqCnstrProof where
-  default := .core default default
+  default := .core default default default default
 
 instance : Inhabited EqCnstr where
   default := { p := default, h := default, sugar := 0, id := 0 }
@@ -46,6 +46,75 @@ protected def EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering :=
 
 abbrev Queue : Type := RBTree EqCnstr EqCnstr.compare
 
+/--
+A simplification chain.
+From an input polynomial `p`, we use equations (i.e., `EqCnstr`) as rewriting rules.
+For example, consider the following sequence of rewrites for the input polynomial `x^2 + x*y`
+using the equations `x - 1 = 0` (`c₁`) and `y - 2 = 0` (`c₂`).
+```
+2*x^2 + x*y                  | s₁ := .input (2*x^2 + x*y)
+=           - 2*x*(x - 1)
+(2*x + x*y)                  | s₂ := .simp (2*x + x*y) c₁ 1 (-2) x s₁
+=           - 2*1*(x - 1)
+(x*y + 2)                    | s₃ := .simp (x*y + 2) c₁ 1 (-2) 1 s₂
+=           - 1*y*(x - 1)
+(y + 2)                      | s₄ := .simp (y+2) c₁ 1 (-1) y s₃
+=           - 1*1*(y - 2)
+4                            | s₅ := .simp 4 c₂ 1 1 1 s₄
+```
+From the chain above, we build the certificate
+```
+(-2*x - y - 2)*(x-1) + (-1)*(y-2)
+```
+for
+```
+4 = (2*x^2 + x*y)
+```
+because `x-1 = 0` and `y-2=0`
+-/
+inductive SimpChain where
+  | input (p : Poly)
+  | /--
+    ```
+    p = k₁*s.getPoly + k₂*m*c.p
+    ```
+    The coefficient `k₁` is used because the leading monomial in `c` may not be monic.
+    Thus, if we follow the chain back to the input polynomial, we have that
+    `p = C * input_p` for a `C` that is equal to the product of all `k₁`s in the chain.
+    Here is a small example where we simplify `x+y` using the equations
+    `2*x - 1 = 0` (`c₁`), `3*y - 1 = 0` (`c₂`), and `6*z + 5 = 0` (`c₃`)
+    ```
+    x + y + z            | s₁ := .input (x + y + z)
+    *2
+    =   - 1*1*(2*x - 1)
+    2*y + 2*z + 1        | s₂ := .simp (2*y + 2*z + 1) c₁ 2 (-1) 1 s₁
+    *3
+    =   - 2*1*(3*y - 1)
+    6*z + 5              | s₃ := .simp (6*z + 5) c₂ 3 (-2) 1 s₂
+    =   - 1*1*(6*z + 5)
+    0                    | s₄ := .simp (0) c₃ 1 (-1) 1 s₃
+    ```
+    For this chain, we build the certificate
+    ```
+    (-3)*(2*x - 1) + (-2)*(3*y - 1) + (-1)*(6*z + 5)
+    ```
+    for
+    ```
+    0 = 6*(x + y + z)
+    ```
+    If we have a commutative ring where
+    ```
+    ∀ (k : Int) (a b : α), k ≠ 0 → (intCast k) * a = 0 → a = 0
+    ```
+    grind can deduce that `x+y+z = 0`
+    -/
+    simp (p : Poly) (c : EqCnstr) (k₁ : Int) (k₂ : Int) (m : Mon) (s : SimpChain)
+
+def SimpChain.getPoly : SimpChain → Poly
+  | .input p   => p
+  | .simp p .. => p
+
+
 /-- State for each `CommRing` processed by this module. -/
 structure Ring where
   id           : Nat

tests/lean/run/grind_ring_1.lean

@@ -44,9 +44,9 @@ example [CommRing α] [IsCharP α 0] (x : α) : (x + 1)*(x - 1) = x^2 → False
 example [CommRing α] [IsCharP α 8] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
   grind +ring
 
-/-- info: [grind.ring.assert.store] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/
+/-- info: [grind.ring.assert.queue] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/
 #guard_msgs (info) in
-set_option trace.grind.ring.assert.store true in
+set_option trace.grind.ring.assert.queue true in
 example (x y : Int) : x + 16*y^2 - 7*x^2 = 0 → False := by
   fail_if_success grind +ring
   sorry