feat: enable ring if ringNull is used

src/Init/Grind/CommRing/Poly.lean

@@ -25,7 +25,7 @@ inductive Expr where
   | sub  (a b : Expr)
   | mul (a b : Expr)
   | pow (a : Expr) (k : Nat)
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Hashable
 
 abbrev Context (α : Type u) := RArray α
 
@@ -950,5 +950,115 @@ theorem NullCert.eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α
   simp [h₂] at this
   contradiction
 
+namespace Stepwise
+/-!
+Theorems for stepwise proof-term construction
+-/
+def core_cert (lhs rhs : Expr) (p : Poly) : Bool :=
+  (lhs.sub rhs).toPoly == p
+
+theorem core {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote ctx = 0 := by
+  simp [core_cert]; intro; subst p
+  simp [Expr.denote_toPoly, Expr.denote]
+  simp [sub_eq_zero_iff]
+
+def superpose_cert (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
+  (p₁.mulMon k₁ m₁).combine (p₂.mulMon k₂ m₂) == p
+
+theorem superpose {α} [CommRing α] (ctx : Context α) (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly)
+    : superpose_cert k₁ m₁ p₁ k₂ m₂ p₂ p → p₁.denote ctx = 0 → p₂.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [superpose_cert]; intro _ h₁ h₂; subst p
+  simp [Poly.denote_combine, Poly.denote_mulMon, h₁, h₂, mul_zero, add_zero]
+
+def simp_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
+  (p₁.mulConst k₁).combine (p₂.mulMon k₂ m₂) == p
+
+theorem simp {α} [CommRing α] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly)
+    : simp_cert k₁ p₁ k₂ m₂ p₂ p → p₁.denote ctx = 0 → p₂.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [simp_cert]; intro _ h₁ h₂; subst p
+  simp [Poly.denote_combine, Poly.denote_mulMon, Poly.denote_mulConst, h₁, h₂, mul_zero, add_zero]
+
+def mul_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
+  p₁.mulConst k == p
+
+def mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [mul_cert]; intro _ h; subst p
+  simp [Poly.denote_mulConst, *, mul_zero]
+
+def div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
+  k != 0 && p.mulConst k == p₁
+
+def div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
+    : div_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [div_cert]; intro hnz _ h; subst p₁
+  simp [Poly.denote_mulConst] at h
+  exact no_int_zero_divisors hnz h
+
+def unsat_eq_cert (p : Poly) (k : Int) : Bool :=
+  k != 0 && p == .num k
+
+def unsat_eq {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (p : Poly) (k : Int)
+    : unsat_eq_cert p k → p.denote ctx = 0 → False := by
+  simp [unsat_eq_cert]; intro h _; subst p; simp [Poly.denote]
+  have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
+  simp [h] at this
+  assumption
+
+def core_certC (lhs rhs : Expr) (p : Poly) (c : Nat) : Bool :=
+  (lhs.sub rhs).toPolyC c == p
+
+theorem coreC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_certC lhs rhs p c → lhs.denote ctx = rhs.denote ctx → p.denote ctx = 0 := by
+  simp [core_certC]; intro; subst p
+  simp [Expr.denote_toPolyC, Expr.denote]
+  simp [sub_eq_zero_iff]
+
+def superpose_certC (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
+  (p₁.mulMonC k₁ m₁ c).combineC (p₂.mulMonC k₂ m₂ c) c == p
+
+theorem superposeC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly)
+    : superpose_certC k₁ m₁ p₁ k₂ m₂ p₂ p c → p₁.denote ctx = 0 → p₂.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [superpose_certC]; intro _ h₁ h₂; subst p
+  simp [Poly.denote_combineC, Poly.denote_mulMonC, h₁, h₂, mul_zero, add_zero]
+
+def mul_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool :=
+  p₁.mulConstC k c == p
+
+def mulC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_certC p₁ k p c → p₁.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [mul_certC]; intro _ h; subst p
+  simp [Poly.denote_mulConstC, *, mul_zero]
+
+def div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool :=
+  k != 0 && p.mulConstC k c == p₁
+
+def divC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
+    : div_certC p₁ k p c → p₁.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [div_certC]; intro hnz _ h; subst p₁
+  simp [Poly.denote_mulConstC] at h
+  exact no_int_zero_divisors hnz h
+
+def simp_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
+  (p₁.mulConstC k₁ c).combineC (p₂.mulMonC k₂ m₂ c) c == p
+
+theorem simpC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly)
+    : simp_certC k₁ p₁ k₂ m₂ p₂ p c → p₁.denote ctx = 0 → p₂.denote ctx = 0 → p.denote ctx = 0 := by
+  simp [simp_certC]; intro _ h₁ h₂; subst p
+  simp [Poly.denote_combineC, Poly.denote_mulMonC, Poly.denote_mulConstC, h₁, h₂, mul_zero, add_zero]
+
+def unsat_eq_certC (p : Poly) (k : Int) (c : Nat) : Bool :=
+  k % c != 0 && p == .num k
+
+def unsat_eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int)
+    : unsat_eq_certC p k c → p.denote ctx = 0 → False := by
+  simp [unsat_eq_certC]; intro h _; subst p; simp [Poly.denote]
+  have := IsCharP.intCast_eq_zero_iff (α := α) c k
+  simp [h] at this
+  assumption
+
+end Stepwise
+
 end CommRing
 end Lean.Grind

src/Init/Grind/Tactics.lean

@@ -119,6 +119,11 @@ structure Config where
   -/
   ring := false
   ringSteps := 10000
+  /--
+  When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise
+  proof terms, instead of a single-step Nullstellensatz certificate
+  -/
+  ringNull := false
   deriving Inhabited, BEq
 
 end Lean.Grind

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Util
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.Types
 import Lean.Meta.Tactic.Grind.Arith.Main
 import Lean.Meta.Tactic.Grind.Arith.Offset

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

@@ -32,7 +32,7 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
     false
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
-  unless (← getConfig).ring do return ()
+  if !(← getConfig).ring && !(← getConfig).ringNull then return ()
   let some type := getType? e | return ()
   if isForbiddenParent parent? then return ()
   let some ringId ← getRingId? type | return ()

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
@@ -22,6 +23,19 @@ def toContextExpr : RingM Expr := do
   else
     RArray.toExpr ring.type id (RArray.leaf (mkApp ring.natCastFn (toExpr 0)))
 
+def throwNoNatZeroDivisors : RingM α := do
+  throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
+
+def getPolyConst (p : Poly) : RingM Int := do
+  let .num k := p
+    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
+  return k
+
+namespace Null
+/-!
+Proof term for a Nullstellensatz certificate.
+-/
+
 /--
 A "pre" Nullstellensatz certificate.
 Recall that, given the hypotheses `h₁ : lhs₁ = rhs₁` ... `hₙ : lhsₙ = rhsₙ`,
@@ -122,6 +136,14 @@ private abbrev caching (c : α) (k : ProofM PreNullCert) : ProofM PreNullCert :=
     modify fun s => { s with cache := s.cache.insert addr h }
     return h
 
+structure NullCertExt where
+  d   : Int
+  qhs : Array (Poly × NullCertHypothesis)
+
+end Null
+
+section
+open Null
 partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching c do
   match c.h with
   | .core a b lhs rhs =>
@@ -151,10 +173,6 @@ where
     | .input _ => acc
     | .step _ k₁ d .. => go d (k₁ * acc)
 
-structure NullCertExt where
-  d   : Int
-  qhs : Array (Poly × NullCertHypothesis)
-
 def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do
   let (nc, s) ← c.toPreNullCert.run {}
   return { d := nc.d, qhs := nc.qs.zip s.hyps }
@@ -165,7 +183,9 @@ def PolyDerivation.mkNullCertExt (d : PolyDerivation) : RingM NullCertExt := do
 
 def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt :=
   c.d.mkNullCertExt
+end
 
+namespace Null
 def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do
   let mut p : Poly := .num 0
   for (q, h) in nc.qhs do
@@ -206,14 +226,12 @@ private def getNoZeroDivInstIfNeeded? (k : Int) : RingM (Option Expr) := do
   if k == 1 then
     return none
   else
-    let some inst ← noZeroDivisorsInst?
-      | throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
+    let some inst ← noZeroDivisorsInst? | throwNoNatZeroDivisors
     return some inst
 
-def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
+def setEqUnsat (c : EqCnstr) : RingM Unit := do
   trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
-  let .num k := c.p
-    | throwError "`grind` internal error, constant polynomial expected {indentExpr (← c.p.denoteExpr)}"
+  let k ← getPolyConst c.p
   let ncx ← c.mkNullCertExt
   trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
   let ring ← getRing
@@ -228,7 +246,7 @@ def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
   let h := mkApp6 h ring.commRingInst charInst ctx nc (toExpr k) reflBoolTrue
   closeGoal <| ncx.applyEqs h
 
-def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
+def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do
   trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
   let ncx ← c.mkNullCertExt
   trace_goal[grind.ring.assert.unsat] "multiplier: {c.d.getMultiplier}, {ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
@@ -268,4 +286,121 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni
   let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
   pushEq a b <| mkExpectedPropHint (ncx.applyEqs h) eq
 
+end Null
+
+namespace Stepwise
+/-!
+Alternative proof term construction where we generate a sub-term for each step in
+the derivation.
+-/
+
+structure ProofM.State where
+  cache       : Std.HashMap UInt64 Expr := {}
+  polyMap     : Std.HashMap Poly Expr := {}
+  exprMap     : Std.HashMap RingExpr Expr := {}
+
+structure ProofM.Context where
+  ctx : Expr
+
+abbrev ProofM := ReaderT ProofM.Context (StateRefT ProofM.State RingM)
+
+/-- Returns a Lean expression representing the variable context used to construct `CommRing` proof steps. -/
+private abbrev getContext : ProofM Expr := do
+  return (← read).ctx
+
+private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
+  let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2
+  if let some h := (← get).cache[addr]? then
+    return h
+  else
+    let h ← k
+    modify fun s => { s with cache := s.cache.insert addr h }
+    return h
+
+def mkPolyDecl (p : Poly) : ProofM Expr := do
+  if let some x := (← get).polyMap[p]? then
+    return x
+  let x := mkFVar (← mkFreshFVarId)
+  modify fun s => { s with polyMap := s.polyMap.insert p x }
+  return x
+
+def mkExprDecl (e : RingExpr) : ProofM Expr := do
+  if let some x := (← get).exprMap[e]? then
+    return x
+  let x := mkFVar (← mkFreshFVarId)
+  modify fun s => { s with exprMap := s.exprMap.insert e x }
+  return x
+
+private def mkStepPrefix (declName declNameC : Name) : ProofM Expr := do
+  let ctx ← getContext
+  let ring ← getRing
+  if let some (charInst, char) ← nonzeroCharInst? then
+    return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx
+  else
+    return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx
+
+open Lean.Grind.CommRing in
+partial def _root_.Lean.Meta.Grind.Arith.CommRing.EqCnstr.toExprProof (c : EqCnstr) : ProofM Expr := caching c do
+  match c.h with
+  | .core a b lhs rhs =>
+    let h ← mkStepPrefix ``Stepwise.core ``Stepwise.coreC
+    return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c.p) reflBoolTrue (← mkEqProof a b)
+  | .superpose k₁ m₁ c₁ k₂ m₂ c₂ =>
+    let h ← mkStepPrefix ``Stepwise.superpose ``Stepwise.superposeC
+    return mkApp10 h
+      (toExpr k₁) (toExpr m₁) (← mkPolyDecl c₁.p)
+      (toExpr k₂) (toExpr m₂) (← mkPolyDecl c₂.p)
+      (← mkPolyDecl c.p) reflBoolTrue (← toExprProof c₁) (← toExprProof c₂)
+  | .simp k₁ c₁ k₂ m₂ c₂ =>
+    let h ← mkStepPrefix ``Stepwise.simp ``Stepwise.simpC
+    return mkApp9 h
+      (toExpr k₁) (← mkPolyDecl c₁.p)
+      (toExpr k₂) (toExpr m₂) (← mkPolyDecl c₂.p)
+      (← mkPolyDecl c.p) reflBoolTrue (← toExprProof c₁) (← toExprProof c₂)
+  | .mul k c₁ =>
+    let h ← mkStepPrefix ``Stepwise.mul ``Stepwise.mulC
+    return mkApp5 h (← mkPolyDecl c₁.p) (toExpr k) (← mkPolyDecl c.p) reflBoolTrue (← toExprProof c₁)
+  | .div k c₁ =>
+    let h ← mkStepPrefix ``Stepwise.div ``Stepwise.divC
+    let some nzInst ← noZeroDivisorsInst?
+      | throwNoNatZeroDivisors
+    return mkApp6 h nzInst (← mkPolyDecl c₁.p) (toExpr k) (← mkPolyDecl c.p) reflBoolTrue (← toExprProof c₁)
+
+private abbrev withProofContext (x : ProofM Expr) : RingM Expr := do
+  let ring ← getRing
+  withLetDecl `ctx (mkApp (mkConst ``RArray [ring.u]) ring.type) (← toContextExpr) fun ctx =>
+  go { ctx } |>.run' {}
+where
+  go : ProofM Expr := do
+    let h ← x
+    let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.CommRing.Poly) toExpr
+    let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.CommRing.Expr) toExpr
+    mkLetFVars #[(← getContext)] h
+
+open Lean.Grind.CommRing in
+def setEqUnsat (c : EqCnstr) : RingM Expr := do
+  withProofContext do
+    let mut h ← mkStepPrefix ``Stepwise.unsat_eq ``Stepwise.unsat_eqC
+    let (charInst, char) ← getCharInst
+    if char == 0 then
+      h := mkApp h charInst
+    let k ← getPolyConst c.p
+    return mkApp4 h (← mkPolyDecl c.p) (toExpr k) reflBoolTrue (← c.toExprProof)
+
+end Stepwise
+
+def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
+  if (← getConfig).ringNull then
+    Null.setEqUnsat c
+  else
+    closeGoal (← Stepwise.setEqUnsat c)
+
+def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
+  Null.setDiseqUnsat c
+  -- TODO: stepwise support
+
+def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do
+  Null.propagateEq a b ra rb d
+  -- TODO: stepwise support
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Diseq
+import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 

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

@@ -0,0 +1,24 @@
+/-
+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.Types
+
+namespace Lean.Meta.Grind.Arith
+
+def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
+    (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do
+  if m.isEmpty then
+    return e
+  else
+    let as := m.toArray
+    let mut e := e.abstract <| as.map (·.2)
+    let mut i := as.size
+    for (p, _) in as.reverse do
+      e := mkLet (varPrefix.appendIndexAfter i) varType (toExpr p) e
+      i := i - 1
+    return e
+
+end Lean.Meta.Grind.Arith

tests/lean/run/grind_ring_2.lean

@@ -41,9 +41,15 @@ example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y
 example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
   grind +ring
 
+example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
+  grind +ringNull
+
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
   grind +ring
 
+example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
+  grind +ringNull
+
 example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
   grind +ring