feat: Nullstellensatz certificates for the comm ring procedure in grind (#8043)

This PR adds `NullCert` type for representing Nullstellensatz
certificates that will be produced by the new commutative ring procedure
in `grind`.

src/Init/Grind/CommRing/Poly.lean

@@ -449,6 +449,51 @@ where
       | .var x => Poly.ofMon (.mult {x, k} .unit)
       | _ => (go a).powC k c
 
+/--
+A Nullstellensatz certificate.
+```
+lhs₁ = rh₁ → ... → lhsₙ = rhₙ → q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ) = 0
+```
+-/
+inductive NullCert where
+  | empty
+  | add (q : Poly) (lhs : Expr) (rhs : Expr) (s : NullCert)
+
+/--
+```
+q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
+```
+-/
+def NullCert.denote {α} [CommRing α] (ctx : Context α) : NullCert → α
+  | .empty => 0
+  | .add q lhs rhs nc => (q.denote ctx)*(lhs.denote ctx - rhs.denote ctx) + nc.denote ctx
+
+/--
+```
+lhs₁ = rh₁ → ... → lhsₙ = rhₙ → p
+```
+-/
+def NullCert.eqsImplies {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : Prop :=
+  match nc with
+  | .empty           => p
+  | .add _ lhs rhs nc => lhs.denote ctx = rhs.denote ctx → eqsImplies ctx nc p
+
+/--
+A polynomial representing
+```
+q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
+```
+-/
+def NullCert.toPoly (nc : NullCert) : Poly :=
+  match nc with
+  | .empty => .num 0
+  | .add q lhs rhs nc => (q.mul (lhs.sub rhs).toPoly).combine nc.toPoly
+
+def NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly :=
+  match nc with
+  | .empty => .num 0
+  | .add q lhs rhs nc => (q.mulC ((lhs.sub rhs).toPolyC c) c).combineC (nc.toPolyC c) c
+
 /-!
 Theorems for justifying the procedure for commutative rings in `grind`.
 -/
@@ -667,6 +712,30 @@ theorem eq_unsat {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (a b : Exp
   rw [h₂, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
   assumption
 
+/-- Helper theorem for proving `NullCert` theorems. -/
+theorem NullCert.eqsImplies_helper {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : (nc.denote ctx = 0 → p) → nc.eqsImplies ctx p := by
+  induction nc <;> simp [denote, eqsImplies]
+  next ih =>
+    intro h₁ h₂
+    apply ih
+    simp [h₂, sub_self, mul_zero, zero_add] at h₁
+    assumption
+
+theorem NullCert.denote_toPoly {α} [CommRing α] (ctx : Context α) (nc : NullCert) : nc.toPoly.denote ctx = nc.denote ctx := by
+  induction nc <;> simp [toPoly, denote, Poly.denote, intCast_zero, Poly.denote_combine, Poly.denote_mul, Expr.denote_toPoly, Expr.denote, *]
+
+def NullCert.eq_cert (nc : NullCert) (lhs rhs : Expr) :=
+  (lhs.sub rhs).toPoly == nc.toPoly
+
+theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
+    : nc.eq_cert lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
+  simp [eq_cert]; intro h₁
+  apply eqsImplies_helper
+  intro h₂
+  replace h₁ := congrArg (Poly.denote ctx) h₁
+  simp [Expr.denote_toPoly, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
+  assumption
+
 /-!
 Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
 -/
@@ -814,5 +883,20 @@ theorem eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b :
   rw [h₃, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
   assumption
 
+theorem NullCert.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) : (nc.toPolyC c).denote ctx = nc.denote ctx := by
+  induction nc <;> simp [toPolyC, denote, Poly.denote, intCast_zero, Poly.denote_combineC, Poly.denote_mulC, Expr.denote_toPolyC, Expr.denote, *]
+
+def NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) :=
+  (lhs.sub rhs).toPolyC c == nc.toPoly
+
+theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
+    : nc.eq_certC lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
+  simp [eq_certC]; intro h₁
+  apply eqsImplies_helper
+  intro h₂
+  replace h₁ := congrArg (Poly.denote ctx) h₁
+  simp [Expr.denote_toPolyC, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
+  assumption
+
 end CommRing
 end Lean.Grind

tests/lean/run/grind_som1.lean

@@ -24,3 +24,17 @@ example (x y : UInt8) : (128 * x + y) * 2 = y + y :=
   let lhs : Expr := .mul (.add (.mul (.num 128) (.var 0)) (.var 1)) (.num 2)
   let rhs : Expr := .add (.var 1) (.var 1)
   Expr.eq_of_toPolyC_eq ctx lhs rhs (Eq.refl true)
+
+def q₁   : Poly := Expr.toPoly (.var 1)
+def lhs₁ : Expr := .var 0
+def rhs₁ : Expr := .var 1
+def q₂   : Poly := Expr.toPoly (.num 1)
+def lhs₂ : Expr := .add (.sub (.var 1) (.mul (.var 0) (.var 1))) (.pow (.var 1) 2)
+def rhs₂ : Expr := .num 1
+def lhs  : Expr := .var 1
+def rhs  : Expr := .num 1
+def nc   : NullCert := .add q₁ lhs₁ rhs₁ (.add q₂ lhs₂ rhs₂ .empty)
+
+example (x y : Int) : x = y → y - x*y + y^2 = 1 → y = 1 :=
+  let ctx := #R[x, y]
+  nc.eq ctx lhs rhs (Eq.refl true)