chore: remove NullCert leftovers

src/Init/Grind/Ring/Poly.lean

@@ -833,55 +833,6 @@ 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ₙ)
-```
--/
-@[expose]
-noncomputable 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
-```
--/
-@[expose]
-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ₙ)
-```
--/
-@[expose]
-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
-
-@[expose]
-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`.
 -/
@@ -1107,78 +1058,6 @@ theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr)
   simp [denote_toPoly] at h
   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, *]
-
-@[expose]
-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
-
-theorem NullCert.eqsImplies_helper' {α} [CommRing α] {ctx : Context α} {nc : NullCert} {p q : Prop} : nc.eqsImplies ctx p → (p → q) → nc.eqsImplies ctx q := by
-  induction nc <;> simp [eqsImplies]
-  next => intro h₁ h₂; exact h₂ h₁
-  next ih => intro h₁ h₂ h₃; exact ih (h₁ h₃) h₂
-
-theorem NullCert.ne_unsat {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
-    : nc.eq_cert lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
-  intro h₁ h₂
-  exact eqsImplies_helper' (eq ctx nc h₁) h₂
-
-@[expose]
-def NullCert.eq_nzdiv_cert (nc : NullCert) (k : Int) (lhs rhs : Expr) : Bool :=
-  k ≠ 0 && (lhs.sub rhs).toPoly.mulConst k == nc.toPoly
-
-theorem NullCert.eq_nzdiv {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
-    : nc.eq_nzdiv_cert k lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
-  simp [eq_nzdiv_cert]
-  intro h₁ h₂
-  apply eqsImplies_helper
-  intro h₃
-  replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₃, Expr.denote, ← zsmul_eq_intCast_mul] at h₂
-  replace h₂ := no_int_zero_divisors h₁ h₂
-  rw [sub_eq_zero_iff] at h₂
-  assumption
-
-theorem NullCert.ne_nzdiv_unsat {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
-    : nc.eq_nzdiv_cert k lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
-  intro h₁ h₂
-  exact eqsImplies_helper' (eq_nzdiv ctx nc k lhs rhs h₁) h₂
-
-@[expose]
-def NullCert.eq_unsat_cert (nc : NullCert) (k : Int) : Bool :=
-  k ≠ 0 && nc.toPoly == .num k
-
-theorem NullCert.eq_unsat {α} [CommRing α] [IsCharP α 0] (ctx : Context α) (nc : NullCert) (k : Int)
-    : nc.eq_unsat_cert k → nc.eqsImplies ctx False := by
-  simp [eq_unsat_cert]
-  intro h₁ h₂
-  apply eqsImplies_helper
-  intro h₃
-  replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [denote_toPoly, h₃, Poly.denote] at h₂
-  have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
-  simp [← h₂] at this
-  contradiction
-
 /-!
 Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
 -/
@@ -1306,64 +1185,6 @@ theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context
   simp [denote_toPolyC] at h
   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, *]
-
-@[expose]
-def NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) :=
-  (lhs.sub rhs).toPolyC c == nc.toPolyC c
-
-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_toPolyC, h₂, Expr.denote, sub_eq_zero_iff] at h₁
-  assumption
-
-theorem NullCert.ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
-    : nc.eq_certC lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
-  intro h₁ h₂
-  exact eqsImplies_helper' (eqC ctx nc h₁) h₂
-
-@[expose]
-def NullCert.eq_nzdiv_certC (nc : NullCert) (k : Int) (lhs rhs : Expr) (c : Nat) : Bool :=
-  k ≠ 0 && ((lhs.sub rhs).toPolyC c).mulConstC k c == nc.toPolyC c
-
-theorem NullCert.eq_nzdivC {α c} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
-    : nc.eq_nzdiv_certC k lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
-  simp [eq_nzdiv_certC]
-  intro h₁ h₂
-  apply eqsImplies_helper
-  intro h₃
-  replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Expr.denote, ← zsmul_eq_intCast_mul] at h₂
-  replace h₂ := no_int_zero_divisors h₁ h₂
-  rw [sub_eq_zero_iff] at h₂
-  assumption
-
-theorem NullCert.ne_nzdiv_unsatC {α c} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
-    : nc.eq_nzdiv_certC k lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
-  intro h₁ h₂
-  exact eqsImplies_helper' (eq_nzdivC ctx nc k lhs rhs h₁) h₂
-
-@[expose]
-def NullCert.eq_unsat_certC (nc : NullCert) (k : Int) (c : Nat) : Bool :=
-  k % c != 0 && nc.toPolyC c == .num k
-
-theorem NullCert.eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (k : Int)
-    : nc.eq_unsat_certC k c → nc.eqsImplies ctx False := by
-  simp [eq_unsat_certC]
-  intro h₁ h₂
-  apply eqsImplies_helper
-  intro h₃
-  replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp [denote_toPolyC, h₃, Poly.denote] at h₂
-  have := IsCharP.intCast_eq_zero_iff (α := α) c k
-  simp [h₂] at this
-  contradiction
-
 namespace Stepwise
 /-!
 Theorems for stepwise proof-term construction

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

@@ -61,15 +61,6 @@ instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr
   toTypeExpr := mkConst ``CommRing.Expr
 
-def ofNullCert (nc : NullCert) : Expr :=
-  match nc with
-  | .empty => mkConst ``CommRing.NullCert.empty
-  | .add q lhs rhs nc => mkApp4 (mkConst ``CommRing.NullCert.add) (toExpr q) (toExpr lhs) (toExpr rhs) (ofNullCert nc)
-
-instance : ToExpr CommRing.NullCert where
-  toExpr := ofNullCert
-  toTypeExpr := mkConst ``CommRing.NullCert
-
 def ofSemiringExpr (e : Ring.OfSemiring.Expr) : Expr :=
   match e with
   | .num k => mkApp (mkConst ``Ring.OfSemiring.Expr.num) (toExpr k)

tests/lean/run/grind_som1.lean

@@ -24,17 +24,3 @@ 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 := lhs) (rhs := rhs) (Eq.refl true)