Data-structures, definitions and theorems for implementing the grind solver and normalizer for commutative rings and its extensions (e.g., fields, commutative semirings, etc.)

The solver uses proof-by-reflection.

@[reducible, inline]

abbrev Lean.Grind.CommRing.Var : Type

inductive Lean.Grind.CommRing.Expr : Type

• num (k : Int) : Expr
• natCast (k : Nat) : Expr
• intCast (k : Int) : Expr
• var (i : Var) : Expr
• neg (a : Expr) : Expr
• add (a b : Expr) : Expr
• sub (a b : Expr) : Expr
• mul (a b : Expr) : Expr
• pow (a : Expr) (k : Nat) : Expr

def Lean.Grind.CommRing.instInhabitedExpr.default : Expr

instance Lean.Grind.CommRing.instInhabitedExpr : Inhabited Expr

instance Lean.Grind.CommRing.instBEqExpr : BEq Expr

def Lean.Grind.CommRing.instBEqExpr.beq : Expr → Expr → Bool

instance Lean.Grind.CommRing.instHashableExpr : Hashable Expr

def Lean.Grind.CommRing.instHashableExpr.hash : Expr → UInt64

instance Lean.Grind.CommRing.instReprExpr : Repr Expr

def Lean.Grind.CommRing.instReprExpr.repr : Expr → Nat → Std.Format

@[reducible, inline]

abbrev Lean.Grind.CommRing.Context (α : Type u) : Type u

@[inline]

abbrev Lean.Grind.CommRing.Var.denote {α : Type u_1} (ctx : Context α) (v : Var) : α

@[inline]

noncomputable abbrev Lean.Grind.CommRing.denoteInt {α : Type u_1} [Ring α] (k : Int) : α

@[inline]

noncomputable abbrev Lean.Grind.CommRing.Expr.denote {α : Type u_1} [Ring α] (ctx : Context α) (e : Expr) : α

structure Lean.Grind.CommRing.Power : Type

• x : Var
• k : Nat

def Lean.Grind.CommRing.instBEqPower.beq : Power → Power → Bool

instance Lean.Grind.CommRing.instBEqPower : BEq Power

instance Lean.Grind.CommRing.instReflBEqPower : ReflBEq Power

instance Lean.Grind.CommRing.instLawfulBEqPower : LawfulBEq Power

instance Lean.Grind.CommRing.instReprPower : Repr Power

def Lean.Grind.CommRing.instReprPower.repr : Power → Nat → Std.Format

def Lean.Grind.CommRing.instInhabitedPower.default : Power

instance Lean.Grind.CommRing.instInhabitedPower : Inhabited Power

instance Lean.Grind.CommRing.instHashablePower : Hashable Power

def Lean.Grind.CommRing.instHashablePower.hash : Power → UInt64

noncomputable def Lean.Grind.CommRing.Power.beq' (pw₁ pw₂ : Power) : Bool

@[simp]

theorem Lean.Grind.CommRing.Power.beq'_eq (pw₁ pw₂ : Power) : (pw₁.beq' pw₂ = true) = (pw₁ = pw₂)

def Lean.Grind.CommRing.Power.varLt (p₁ p₂ : Power) : Bool

@[inline]

abbrev Lean.Grind.CommRing.Power.denote {α : Type u_1} [Semiring α] (ctx : Context α) : Power → α

inductive Lean.Grind.CommRing.Mon : Type

• unit : Mon
• mult (p : Power) (m : Mon) : Mon

def Lean.Grind.CommRing.instBEqMon.beq : Mon → Mon → Bool

instance Lean.Grind.CommRing.instBEqMon : BEq Mon

instance Lean.Grind.CommRing.instReflBEqMon : ReflBEq Mon

instance Lean.Grind.CommRing.instLawfulBEqMon : LawfulBEq Mon

def Lean.Grind.CommRing.instReprMon.repr : Mon → Nat → Std.Format

instance Lean.Grind.CommRing.instReprMon : Repr Mon

def Lean.Grind.CommRing.instInhabitedMon.default : Mon

instance Lean.Grind.CommRing.instInhabitedMon : Inhabited Mon

instance Lean.Grind.CommRing.instHashableMon : Hashable Mon

def Lean.Grind.CommRing.instHashableMon.hash : Mon → UInt64

noncomputable def Lean.Grind.CommRing.Mon.beq' (m₁ : Mon) : Mon → Bool

@[simp]

theorem Lean.Grind.CommRing.Mon.beq'_eq (m₁ m₂ : Mon) : (m₁.beq' m₂ = true) = (m₁ = m₂)

@[inline]

abbrev Lean.Grind.CommRing.Mon.denote {α : Type u_1} [Semiring α] (ctx : Context α) : Mon → α

@[inline]

abbrev Lean.Grind.CommRing.Mon.denote'.go {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) (acc : α) : α

@[inline]

abbrev Lean.Grind.CommRing.Mon.denote' {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) : α

def Lean.Grind.CommRing.Mon.ofVar (x : Var) : Mon

def Lean.Grind.CommRing.Mon.concat (m₁ m₂ : Mon) : Mon

def Lean.Grind.CommRing.Mon.mulPow (pw : Power) (m : Mon) : Mon

def Lean.Grind.CommRing.Mon.mulPow_nc (pw : Power) (m : Mon) : Mon

def Lean.Grind.CommRing.Mon.length : Mon → Nat

def Lean.Grind.CommRing.hugeFuel : Nat

def Lean.Grind.CommRing.Mon.mul (m₁ m₂ : Mon) : Mon

def Lean.Grind.CommRing.Mon.mul.go (fuel : Nat) (m₁ m₂ : Mon) : Mon

noncomputable def Lean.Grind.CommRing.Mon.mul_k : Mon → Mon → Mon

theorem Lean.Grind.CommRing.Mon.mul_k_eq_mul {m₁ m₂ : Mon} : m₁.mul_k m₂ = m₁.mul m₂

def Lean.Grind.CommRing.Mon.mul_nc (m₁ m₂ : Mon) : Mon

def Lean.Grind.CommRing.Mon.degree : Mon → Nat

noncomputable def Lean.Grind.CommRing.Mon.degree_k : Mon → Nat

theorem Lean.Grind.CommRing.Mon.degree_k_eq_degree {m : Mon} : m.degree_k = m.degree

def Lean.Grind.CommRing.Var.revlex (x y : Var) : Ordering

def Lean.Grind.CommRing.powerRevlex (k₁ k₂ : Nat) : Ordering

noncomputable def Lean.Grind.CommRing.powerRevlex_k (k₁ k₂ : Nat) : Ordering

theorem Lean.Grind.CommRing.powerRevlex_k_eq_powerRevlex (k₁ k₂ : Nat) : powerRevlex_k k₁ k₂ = powerRevlex k₁ k₂

def Lean.Grind.CommRing.Power.revlex (p₁ p₂ : Power) : Ordering

@[irreducible]

def Lean.Grind.CommRing.Mon.revlexWF (m₁ m₂ : Mon) : Ordering

def Lean.Grind.CommRing.Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering

def Lean.Grind.CommRing.Mon.revlex (m₁ m₂ : Mon) : Ordering

def Lean.Grind.CommRing.Mon.grevlex (m₁ m₂ : Mon) : Ordering

noncomputable def Lean.Grind.CommRing.Mon.revlex_k : Mon → Mon → Ordering

noncomputable def Lean.Grind.CommRing.Mon.grevlex_k (m₁ m₂ : Mon) : Ordering

theorem Lean.Grind.CommRing.Mon.revlex_k_eq_revlex (m₁ m₂ : Mon) : m₁.revlex_k m₂ = m₁.revlex m₂

theorem Lean.Grind.CommRing.Mon.grevlex_k_eq_grevlex (m₁ m₂ : Mon) : m₁.grevlex_k m₂ = m₁.grevlex m₂

inductive Lean.Grind.CommRing.Poly : Type

• num (k : Int) : Poly
• add (k : Int) (v : Mon) (p : Poly) : Poly

instance Lean.Grind.CommRing.instBEqPoly : BEq Poly

def Lean.Grind.CommRing.instBEqPoly.beq : Poly → Poly → Bool

instance Lean.Grind.CommRing.instReflBEqPoly : ReflBEq Poly

instance Lean.Grind.CommRing.instLawfulBEqPoly : LawfulBEq Poly

instance Lean.Grind.CommRing.instReprPoly : Repr Poly

def Lean.Grind.CommRing.instReprPoly.repr : Poly → Nat → Std.Format

def Lean.Grind.CommRing.instInhabitedPoly.default : Poly

instance Lean.Grind.CommRing.instInhabitedPoly : Inhabited Poly

def Lean.Grind.CommRing.instHashablePoly.hash : Poly → UInt64

instance Lean.Grind.CommRing.instHashablePoly : Hashable Poly

noncomputable def Lean.Grind.CommRing.Poly.beq' (p₁ : Poly) : Poly → Bool

@[simp]

theorem Lean.Grind.CommRing.Poly.beq'_eq (p₁ p₂ : Poly) : (p₁.beq' p₂ = true) = (p₁ = p₂)

@[inline]

abbrev Lean.Grind.CommRing.Poly.denote {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) : α

@[inline]

abbrev Lean.Grind.CommRing.denoteTerm {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : α

@[inline]

abbrev Lean.Grind.CommRing.Poly.denote'.go {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) (acc : α) : α

@[inline]

abbrev Lean.Grind.CommRing.Poly.denote' {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) : α

def Lean.Grind.CommRing.Poly.ofMon (m : Mon) : Poly

def Lean.Grind.CommRing.Poly.ofVar (x : Var) : Poly

def Lean.Grind.CommRing.Poly.isSorted : Poly → Bool

def Lean.Grind.CommRing.Poly.addConst (p : Poly) (k : Int) : Poly

def Lean.Grind.CommRing.Poly.addConst.go (k : Int) : Poly → Poly

noncomputable def Lean.Grind.CommRing.Poly.addConst_k (p : Poly) (k : Int) : Poly

theorem Lean.Grind.CommRing.Poly.addConst_k_eq_addConst (p : Poly) (k : Int) : p.addConst_k k = p.addConst k

def Lean.Grind.CommRing.Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly

def Lean.Grind.CommRing.Poly.insert.go (k : Int) (m : Mon) : Poly → Poly

def Lean.Grind.CommRing.Poly.concat (p₁ p₂ : Poly) : Poly

def Lean.Grind.CommRing.Poly.mulConst (k : Int) (p : Poly) : Poly

def Lean.Grind.CommRing.Poly.mulConst.go (k : Int) : Poly → Poly

noncomputable def Lean.Grind.CommRing.Poly.mulConst_k (k : Int) (p : Poly) : Poly

@[simp]

theorem Lean.Grind.CommRing.Poly.mulConst_k_eq_mulConst (k : Int) (p : Poly) : mulConst_k k p = mulConst k p

def Lean.Grind.CommRing.Poly.mulMon (k : Int) (m : Mon) (p : Poly) : Poly

def Lean.Grind.CommRing.Poly.mulMon.go (k : Int) (m : Mon) : Poly → Poly

noncomputable def Lean.Grind.CommRing.Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly

@[simp]

theorem Lean.Grind.CommRing.Poly.mulMon_k_eq_mulMon (k : Int) (m : Mon) (p : Poly) : mulMon_k k m p = mulMon k m p

def Lean.Grind.CommRing.Poly.mulMon_nc (k : Int) (m : Mon) (p : Poly) : Poly

def Lean.Grind.CommRing.Poly.mulMon_nc.go (k : Int) (m : Mon) (p acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.combine (p₁ p₂ : Poly) : Poly

def Lean.Grind.CommRing.Poly.combine.go (fuel : Nat) (p₁ p₂ : Poly) : Poly

noncomputable def Lean.Grind.CommRing.Poly.combine_k : Poly → Poly → Poly

A Poly.combine optimized for the kernel.

@[simp]

theorem Lean.Grind.CommRing.Poly.combine_k_eq_combine (p₁ p₂ : Poly) : p₁.combine_k p₂ = p₁.combine p₂

def Lean.Grind.CommRing.Poly.mul (p₁ p₂ : Poly) : Poly

def Lean.Grind.CommRing.Poly.mul.go (p₂ p₁ acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.mul_nc (p₁ p₂ : Poly) : Poly

def Lean.Grind.CommRing.Poly.mul_nc.go (p₂ p₁ acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.pow (p : Poly) (k : Nat) : Poly

def Lean.Grind.CommRing.Poly.pow_nc (p : Poly) (k : Nat) : Poly

def Lean.Grind.CommRing.Expr.toPoly : Expr → Poly

noncomputable def Lean.Grind.CommRing.Expr.toPoly_k (e : Expr) : Poly

def Lean.Grind.CommRing.Mon.degreeOf (m : Mon) (x : Var) : Nat

def Lean.Grind.CommRing.Mon.cancelVar (m : Mon) (x : Var) : Mon

def Lean.Grind.CommRing.Poly.cancelVar' (c : Int) (x : Var) (p acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly

@[simp]

theorem Lean.Grind.CommRing.Expr.toPoly_k_eq_toPoly (e : Expr) : e.toPoly_k = e.toPoly

def Lean.Grind.CommRing.Expr.toPoly_nc : Expr → Poly

def Lean.Grind.CommRing.Poly.normEq0 (p : Poly) (c : Nat) : Poly

Definitions for the IsCharP case

We considered using a single set of definitions parameterized by Option c or simply set c = 0 since n % 0 = n in Lean, but decided against it to avoid unnecessary kernel‑reduction overhead. Once we can specialize definitions before they reach the kernel, we can merge the two versions. Until then, the IsCharP definitions will carry the C suffix. We use them whenever we can infer the characteristic using type class instance synthesis.

def Lean.Grind.CommRing.Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.insertC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.insertC.go (m : Mon) (c : Nat) (k : Int) : Poly → Poly

def Lean.Grind.CommRing.Poly.mulConstC (k : Int) (p : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulConstC.go (k : Int) (c : Nat) : Poly → Poly

def Lean.Grind.CommRing.Poly.mulMonC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulMonC.go (k : Int) (m : Mon) (c : Nat) : Poly → Poly

def Lean.Grind.CommRing.Poly.mulMonC_nc (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulMonC_nc.go (k : Int) (m : Mon) (c : Nat) (p acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.combineC (p₁ p₂ : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulC (p₁ p₂ : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulC.go (p₂ : Poly) (c : Nat) (p₁ acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.mulC_nc (p₁ p₂ : Poly) (c : Nat) : Poly

def Lean.Grind.CommRing.Poly.mulC_nc.go (p₂ : Poly) (c : Nat) (p₁ acc : Poly) : Poly

def Lean.Grind.CommRing.Poly.powC (p : Poly) (k c : Nat) : Poly

def Lean.Grind.CommRing.Poly.powC_nc (p : Poly) (k c : Nat) : Poly

def Lean.Grind.CommRing.Expr.toPolyC (e : Expr) (c : Nat) : Poly

def Lean.Grind.CommRing.Expr.toPolyC.go (c : Nat) : Expr → Poly

def Lean.Grind.CommRing.Expr.toPolyC_nc (e : Expr) (c : Nat) : Poly

def Lean.Grind.CommRing.Expr.toPolyC_nc.go (c : Nat) : Expr → Poly

Theorems for justifying the procedure for commutative rings in grind.

theorem Lean.Grind.CommRing.denoteInt_eq {α : Type u_1} [Ring α] (k : Int) : denoteInt k = ↑k

theorem Lean.Grind.CommRing.Power.denote_eq {α : Type u_1} [Semiring α] (ctx : Context α) (p : Power) : denote ctx p = Var.denote ctx p.x ^ p.k

theorem Lean.Grind.CommRing.Mon.denote'_eq_denote {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) : denote' ctx m = denote ctx m

theorem Lean.Grind.CommRing.Mon.denote_ofVar {α : Type u_1} [Semiring α] (ctx : Context α) (x : Var) : denote ctx (ofVar x) = Var.denote ctx x

theorem Lean.Grind.CommRing.Mon.denote_concat {α : Type u_1} [Semiring α] (ctx : Context α) (m₁ m₂ : Mon) : denote ctx (m₁.concat m₂) = denote ctx m₁ * denote ctx m₂

theorem Lean.Grind.CommRing.Mon.denote_mulPow {α : Type u_1} [CommSemiring α] (ctx : Context α) (p : Power) (m : Mon) : denote ctx (mulPow p m) = Power.denote ctx p * denote ctx m

theorem Lean.Grind.CommRing.Mon.denote_mulPow_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p : Power) (m : Mon) : denote ctx (mulPow_nc p m) = Power.denote ctx p * denote ctx m

theorem Lean.Grind.CommRing.Mon.denote_mul {α : Type u_1} [CommSemiring α] (ctx : Context α) (m₁ m₂ : Mon) : denote ctx (m₁.mul m₂) = denote ctx m₁ * denote ctx m₂

theorem Lean.Grind.CommRing.Mon.denote_mul_nc {α : Type u_1} [Semiring α] (ctx : Context α) (m₁ m₂ : Mon) : denote ctx (m₁.mul_nc m₂) = denote ctx m₁ * denote ctx m₂

theorem Lean.Grind.CommRing.Var.eq_of_revlex {x₁ x₂ : Var} : x₁.revlex x₂ = Ordering.eq → x₁ = x₂

theorem Lean.Grind.CommRing.eq_of_powerRevlex {k₁ k₂ : Nat} : powerRevlex k₁ k₂ = Ordering.eq → k₁ = k₂

theorem Lean.Grind.CommRing.Power.eq_of_revlex (p₁ p₂ : Power) : p₁.revlex p₂ = Ordering.eq → p₁ = p₂

theorem Lean.Grind.CommRing.Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = Ordering.eq → m₁ = m₂

theorem Lean.Grind.CommRing.Mon.eq_of_revlexFuel {fuel : Nat} {m₁ m₂ : Mon} : revlexFuel fuel m₁ m₂ = Ordering.eq → m₁ = m₂

theorem Lean.Grind.CommRing.Mon.eq_of_revlex {m₁ m₂ : Mon} : m₁.revlex m₂ = Ordering.eq → m₁ = m₂

theorem Lean.Grind.CommRing.Mon.eq_of_grevlex {m₁ m₂ : Mon} : m₁.grevlex m₂ = Ordering.eq → m₁ = m₂

theorem Lean.Grind.CommRing.Poly.denoteTerm_eq {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denoteTerm ctx k m = ↑k * Mon.denote ctx m

theorem Lean.Grind.CommRing.Poly.denote'_eq_denote {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) : denote' ctx p = denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_ofMon {α : Type u_1} [Ring α] (ctx : Context α) (m : Mon) : denote ctx (ofMon m) = Mon.denote ctx m

theorem Lean.Grind.CommRing.Poly.denote_ofVar {α : Type u_1} [Ring α] (ctx : Context α) (x : Var) : denote ctx (ofVar x) = Var.denote ctx x

theorem Lean.Grind.CommRing.Poly.denote_addConst {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) (k : Int) : denote ctx (p.addConst k) = denote ctx p + ↑k

theorem Lean.Grind.CommRing.Poly.denote_insert {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (insert k m p) = ↑k * Mon.denote ctx m + denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_concat {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.concat p₂) = denote ctx p₁ + denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mulConst {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (p : Poly) : denote ctx (mulConst k p) = ↑k * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_mulMon {α : Type u_1} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (mulMon k m p) = ↑k * Mon.denote ctx m * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_mulMon_nc_go {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) : denote ctx (mulMon_nc.go k m p acc) = ↑k * Mon.denote ctx m * denote ctx p + denote ctx acc

theorem Lean.Grind.CommRing.Poly.denote_mulMon_nc {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (mulMon_nc k m p) = ↑k * Mon.denote ctx m * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_combine {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.combine p₂) = denote ctx p₁ + denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mul_go {α : Type u_1} [CommRing α] (ctx : Context α) (p₁ p₂ acc : Poly) : denote ctx (mul.go p₂ p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mul {α : Type u_1} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.mul p₂) = denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mul_nc_go {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ acc : Poly) : denote ctx (mul_nc.go p₂ p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mul_nc {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.mul_nc p₂) = denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_pow {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (k : Nat) : denote ctx (p.pow k) = denote ctx p ^ k

theorem Lean.Grind.CommRing.Poly.denote_pow_nc {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) (k : Nat) : denote ctx (p.pow_nc k) = denote ctx p ^ k

theorem Lean.Grind.CommRing.Expr.denote_toPoly {α : Type u_1} [CommRing α] (ctx : Context α) (e : Expr) : Poly.denote ctx e.toPoly = denote ctx e

theorem Lean.Grind.CommRing.Expr.denote_toPoly_nc {α : Type u_1} [Ring α] (ctx : Context α) (e : Expr) : Poly.denote ctx e.toPoly_nc = denote ctx e

theorem Lean.Grind.CommRing.Expr.eq_of_toPoly_eq {α : Type u_1} [CommRing α] (ctx : Context α) (a b : Expr) (h : (a.toPoly == b.toPoly) = true) : denote ctx a = denote ctx b

theorem Lean.Grind.CommRing.Expr.eq_of_toPoly_nc_eq {α : Type u_1} [Ring α] (ctx : Context α) (a b : Expr) (h : (a.toPoly_nc == b.toPoly_nc) = true) : denote ctx a = denote ctx b

theorem Lean.Grind.CommRing.Mon.denote_cancelVar {α : Type u_1} [CommSemiring α] (ctx : Context α) (m : Mon) (x : Var) : denote ctx m = Var.denote ctx x ^ m.degreeOf x * denote ctx (m.cancelVar x)

theorem Lean.Grind.CommRing.Poly.denote_cancelVar' {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) (acc : Poly) : c ≠ 0 → ↑c * Var.denote ctx x = 1 → denote ctx (cancelVar' c x p acc) = denote ctx p + denote ctx acc

theorem Lean.Grind.CommRing.Poly.denote_cancelVar {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) : c ≠ 0 → ↑c * Var.denote ctx x = 1 → denote ctx (cancelVar c x p) = denote ctx p

noncomputable def Lean.Grind.CommRing.cancel_var_cert (c : Int) (x : Var) (p₁ p₂ : Poly) : Bool

theorem Lean.Grind.CommRing.eq_cancel_var {α : Type u_1} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) : cancel_var_cert c x p₁ p₂ = true → ↑c * Var.denote ctx x = 1 → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0

theorem Lean.Grind.CommRing.diseq_cancel_var {α : Type u_1} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) : cancel_var_cert c x p₁ p₂ = true → ↑c * Var.denote ctx x = 1 → Poly.denote ctx p₁ ≠ 0 → Poly.denote ctx p₂ ≠ 0

theorem Lean.Grind.CommRing.le_cancel_var {α : Type u_1} [CommRing α] [LE α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) : cancel_var_cert c x p₁ p₂ = true → ↑c * Var.denote ctx x = 1 → Poly.denote ctx p₁ ≤ 0 → Poly.denote ctx p₂ ≤ 0

theorem Lean.Grind.CommRing.lt_cancel_var {α : Type u_1} [CommRing α] [LT α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly) : cancel_var_cert c x p₁ p₂ = true → ↑c * Var.denote ctx x = 1 → Poly.denote ctx p₁ < 0 → Poly.denote ctx p₂ < 0

Theorems for justifying the procedure for commutative rings with a characteristic in grind.

theorem Lean.Grind.CommRing.Poly.denote_addConstC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : denote ctx (p.addConstC k c) = denote ctx p + ↑k

theorem Lean.Grind.CommRing.Poly.denote_insertC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (insertC k m p c) = ↑k * Mon.denote ctx m + denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_mulConstC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (p : Poly) : denote ctx (mulConstC k p c) = ↑k * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_mulMonC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (mulMonC k m p c) = ↑k * Mon.denote ctx m * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_mulMonC_nc_go {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) : denote ctx (mulMonC_nc.go k m c p acc) = ↑k * Mon.denote ctx m * denote ctx p + denote ctx acc

theorem Lean.Grind.CommRing.Poly.denote_mulMonC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : denote ctx (mulMonC_nc k m p c) = ↑k * Mon.denote ctx m * denote ctx p

theorem Lean.Grind.CommRing.Poly.denote_combineC {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.combineC p₂ c) = denote ctx p₁ + denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mulC_go {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly) : denote ctx (mulC.go p₂ c p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mulC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.mulC p₂ c) = denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mulC_nc_go {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly) : denote ctx (mulC_nc.go p₂ c p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_mulC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly) : denote ctx (p₁.mulC_nc p₂ c) = denote ctx p₁ * denote ctx p₂

theorem Lean.Grind.CommRing.Poly.denote_powC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat) : denote ctx (p.powC k c) = denote ctx p ^ k

theorem Lean.Grind.CommRing.Poly.denote_powC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat) : denote ctx (p.powC_nc k c) = denote ctx p ^ k

theorem Lean.Grind.CommRing.Expr.denote_toPolyC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (e : Expr) : Poly.denote ctx (e.toPolyC c) = denote ctx e

theorem Lean.Grind.CommRing.Expr.denote_toPolyC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (e : Expr) : Poly.denote ctx (e.toPolyC_nc c) = denote ctx e

theorem Lean.Grind.CommRing.Expr.eq_of_toPolyC_eq {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (h : (a.toPolyC c == b.toPolyC c) = true) : denote ctx a = denote ctx b

theorem Lean.Grind.CommRing.Expr.eq_of_toPolyC_nc_eq {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (a b : Expr) (h : (a.toPolyC_nc c == b.toPolyC_nc c) = true) : denote ctx a = denote ctx b

Theorems for stepwise proof-term construction

noncomputable def Lean.Grind.CommRing.Stepwise.core_cert (lhs rhs : Expr) (p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.core {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_cert lhs rhs p = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.superpose_cert (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.superpose {α : Type u_1} [CommRing α] (ctx : Context α) (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : superpose_cert k₁ m₁ p₁ k₂ m₂ p₂ p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.simp_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.simp {α : Type u_1} [CommRing α] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : simp_cert k₁ p₁ k₂ m₂ p₂ p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.mul_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.mul {α : Type u_1} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_cert p₁ k p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

theorem Lean.Grind.CommRing.Stepwise.eq_mul {α : Type u_1} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_cert p₁ k p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.mul_ne_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.diseq_mul {α : Type u_1} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_ne_cert p₁ k p = true → Poly.denote ctx p₁ ≠ 0 → Poly.denote ctx p ≠ 0

theorem Lean.Grind.CommRing.Stepwise.inv {α : Type u_1} [CommRing α] (ctx : Context α) (p₁ p : Poly) : mul_cert p₁ (-1) p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.div {α : Type u_1} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly) : div_cert p₁ k p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.unsat_eq_cert (p : Poly) (k : Int) : Bool

def Lean.Grind.CommRing.Stepwise.unsat_eq {α : Type u_1} [CommRing α] (ctx : Context α) [IsCharP α 0] (p : Poly) (k : Int) : unsat_eq_cert p k = true → Poly.denote ctx p = 0 → False

theorem Lean.Grind.CommRing.Stepwise.d_init {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) : ↑1 * Poly.denote ctx p = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.Stepwise.d_step1_cert (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.d_step1 {α : Type u_1} [CommRing α] (ctx : Context α) (k : Int) (init p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : d_step1_cert p₁ k₂ m₂ p₂ p = true → ↑k * Poly.denote ctx init = Poly.denote ctx p₁ → Poly.denote ctx p₂ = 0 → ↑k * Poly.denote ctx init = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.Stepwise.d_stepk_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.d_stepk {α : Type u_1} [CommRing α] (ctx : Context α) (k₁ k : Int) (init p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : d_stepk_cert k₁ p₁ k₂ m₂ p₂ p = true → ↑k * Poly.denote ctx init = Poly.denote ctx p₁ → Poly.denote ctx p₂ = 0 → ↑(k₁ * k) * Poly.denote ctx init = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.Stepwise.imp_1eq_cert (lhs rhs : Expr) (p₁ p₂ : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.imp_1eq {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p₁ p₂ : Poly) : imp_1eq_cert lhs rhs p₁ p₂ = true → ↑1 * Poly.denote ctx p₁ = Poly.denote ctx p₂ → Expr.denote ctx lhs = Expr.denote ctx rhs

noncomputable def Lean.Grind.CommRing.Stepwise.imp_keq_cert (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) : Bool

theorem Lean.Grind.CommRing.Stepwise.imp_keq {α : Type u_1} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (k : Int) (lhs rhs : Expr) (p₁ p₂ : Poly) : imp_keq_cert lhs rhs k p₁ p₂ = true → ↑k * Poly.denote ctx p₁ = Poly.denote ctx p₂ → Expr.denote ctx lhs = Expr.denote ctx rhs

noncomputable def Lean.Grind.CommRing.Stepwise.core_certC (lhs rhs : Expr) (p : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.coreC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : core_certC lhs rhs p c = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.superpose_certC (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.superposeC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : superpose_certC k₁ m₁ p₁ k₂ m₂ p₂ p c = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.mul_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool

def Lean.Grind.CommRing.Stepwise.mulC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_certC p₁ k p c = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool

def Lean.Grind.CommRing.Stepwise.divC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly) : div_certC p₁ k p c = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.simp_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.simpC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : simp_certC k₁ p₁ k₂ m₂ p₂ p c = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.Stepwise.unsat_eq_certC (p : Poly) (k : Int) (c : Nat) : Bool

def Lean.Grind.CommRing.Stepwise.unsat_eqC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : unsat_eq_certC p k c = true → Poly.denote ctx p = 0 → False

noncomputable def Lean.Grind.CommRing.Stepwise.d_step1_certC (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.d_step1C {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (init p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : d_step1_certC p₁ k₂ m₂ p₂ p c = true → ↑k * Poly.denote ctx init = Poly.denote ctx p₁ → Poly.denote ctx p₂ = 0 → ↑k * Poly.denote ctx init = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.Stepwise.d_stepk_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.d_stepkC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ k : Int) (init p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) : d_stepk_certC k₁ p₁ k₂ m₂ p₂ p c = true → ↑k * Poly.denote ctx init = Poly.denote ctx p₁ → Poly.denote ctx p₂ = 0 → ↑(k₁ * k) * Poly.denote ctx init = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.Stepwise.imp_1eq_certC (lhs rhs : Expr) (p₁ p₂ : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.imp_1eqC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (lhs rhs : Expr) (p₁ p₂ : Poly) : imp_1eq_certC lhs rhs p₁ p₂ c = true → ↑1 * Poly.denote ctx p₁ = Poly.denote ctx p₂ → Expr.denote ctx lhs = Expr.denote ctx rhs

noncomputable def Lean.Grind.CommRing.Stepwise.imp_keq_certC (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) (c : Nat) : Bool

theorem Lean.Grind.CommRing.Stepwise.imp_keqC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (k : Int) (lhs rhs : Expr) (p₁ p₂ : Poly) : imp_keq_certC lhs rhs k p₁ p₂ c = true → ↑k * Poly.denote ctx p₁ = Poly.denote ctx p₂ → Expr.denote ctx lhs = Expr.denote ctx rhs

IntModule interface

def Lean.Grind.CommRing.Mon.denoteAsIntModule {α : Type u_1} [CommRing α] (ctx : Context α) (m : Mon) : α

def Lean.Grind.CommRing.Mon.denoteAsIntModule.go {α : Type u_1} [CommRing α] (ctx : Context α) (m : Mon) (acc : α) : α

def Lean.Grind.CommRing.Poly.denoteAsIntModule {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) : α

theorem Lean.Grind.CommRing.Mon.denoteAsIntModule_go_eq_denote {α : Type u_1} [CommRing α] (ctx : Context α) (m : Mon) (acc : α) : denoteAsIntModule.go ctx m acc = acc * denote ctx m

theorem Lean.Grind.CommRing.Mon.denoteAsIntModule_eq_denote {α : Type u_1} [CommRing α] (ctx : Context α) (m : Mon) : denoteAsIntModule ctx m = denote ctx m

theorem Lean.Grind.CommRing.Poly.denoteAsIntModule_eq_denote {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) : denoteAsIntModule ctx p = denote ctx p

theorem Lean.Grind.CommRing.eq_norm {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert lhs rhs p = true → Expr.denote ctx lhs = Expr.denote ctx rhs → Poly.denote ctx p = 0

theorem Lean.Grind.CommRing.eq_int_module {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) : Poly.denote ctx p = 0 → Poly.denoteAsIntModule ctx p = 0

theorem Lean.Grind.CommRing.diseq_norm {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert lhs rhs p = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → Poly.denote ctx p ≠ 0

theorem Lean.Grind.CommRing.diseq_int_module {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) : Poly.denote ctx p ≠ 0 → Poly.denoteAsIntModule ctx p ≠ 0

theorem Lean.Grind.CommRing.le_norm {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert lhs rhs p = true → Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote ctx p ≤ 0

theorem Lean.Grind.CommRing.le_int_module {α : Type u_1} [CommRing α] [LE α] (ctx : Context α) (p : Poly) : Poly.denote ctx p ≤ 0 → Poly.denoteAsIntModule ctx p ≤ 0

noncomputable def Lean.Grind.CommRing.mul_ineq_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool

theorem Lean.Grind.CommRing.le_mul {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_ineq_cert p₁ k p = true → Poly.denote ctx p₁ ≤ 0 → Poly.denote ctx p ≤ 0

theorem Lean.Grind.CommRing.lt_norm {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert lhs rhs p = true → Expr.denote ctx lhs < Expr.denote ctx rhs → Poly.denote ctx p < 0

theorem Lean.Grind.CommRing.lt_int_module {α : Type u_1} [CommRing α] [LT α] (ctx : Context α) (p : Poly) : Poly.denote ctx p < 0 → Poly.denoteAsIntModule ctx p < 0

theorem Lean.Grind.CommRing.lt_mul {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_ineq_cert p₁ k p = true → Poly.denote ctx p₁ < 0 → Poly.denote ctx p < 0

theorem Lean.Grind.CommRing.not_le_norm {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert rhs lhs p = true → ¬Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Poly.denote ctx p < 0

theorem Lean.Grind.CommRing.not_lt_norm {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert rhs lhs p = true → ¬Expr.denote ctx lhs < Expr.denote ctx rhs → Poly.denote ctx p ≤ 0

theorem Lean.Grind.CommRing.inv_int_eq {α : Type u_1} [Field α] [IsCharP α 0] (b : Int) : (b != 0) = true → denoteInt b * (denoteInt b)⁻¹ = 1

theorem Lean.Grind.CommRing.intCast_eq_denoteInt {α : Type u_1} [Field α] (b : Int) : IntCast.intCast b = denoteInt b

theorem Lean.Grind.CommRing.inv_int_eq' {α : Type u_1} [Field α] [IsCharP α 0] (b : Int) : (b != 0) = true → IntCast.intCast b * (denoteInt b)⁻¹ = 1

theorem Lean.Grind.CommRing.inv_int_eqC {α : Type u_1} {c : Nat} [Field α] [IsCharP α c] (b : Int) : (b % ↑c != 0) = true → denoteInt b * (denoteInt b)⁻¹ = 1

theorem Lean.Grind.CommRing.inv_zero_eqC {α : Type u_1} {c : Nat} [Field α] [IsCharP α c] (b : Int) : (b % ↑c == 0) = true → (denoteInt b)⁻¹ = 0

theorem Lean.Grind.CommRing.inv_split {α : Type u_1} [Field α] (a : α) : if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1

noncomputable def Lean.Grind.CommRing.one_eq_zero_unsat_cert (p : Poly) : Bool

theorem Lean.Grind.CommRing.one_eq_zero_unsat {α : Type u_1} [Field α] (ctx : Context α) (p : Poly) : one_eq_zero_unsat_cert p = true → Poly.denote ctx p = 0 → False

theorem Lean.Grind.CommRing.diseq_to_eq {α : Type u_1} [Field α] (a b : α) : a ≠ b → (a - b) * (a - b)⁻¹ = 1

theorem Lean.Grind.CommRing.diseq0_to_eq {α : Type u_1} [Field α] (a : α) : a ≠ 0 → a * a⁻¹ = 1

normEq0 helper theorems

theorem Lean.Grind.CommRing.Poly.normEq0_eq {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (c : Nat) (h : ↑↑c = 0) : denote ctx (p.normEq0 c) = denote ctx p

noncomputable def Lean.Grind.CommRing.eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.eq_normEq0 {α : Type u_1} [CommRing α] (ctx : Context α) (c : Nat) (p₁ p₂ p : Poly) : eq_normEq0_cert c p₁ p₂ p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

theorem Lean.Grind.CommRing.gcd_eq_0 {α : Type u_1} [CommRing α] (g n m a b : Int) (h : g = a * n + b * m) (h₁ : ↑n = 0) (h₂ : ↑m = 0) : ↑g = 0

def Lean.Grind.CommRing.eq_gcd_cert (a b : Int) (p₁ p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.eq_gcd {α : Type u_1} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p : Poly) : eq_gcd_cert a b p₁ p₂ p = true → Poly.denote ctx p₁ = 0 → Poly.denote ctx p₂ = 0 → Poly.denote ctx p = 0

noncomputable def Lean.Grind.CommRing.d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool

theorem Lean.Grind.CommRing.d_normEq0 {α : Type u_1} [CommRing α] (ctx : Context α) (k : Int) (c : Nat) (init p₁ p₂ p : Poly) : d_normEq0_cert c p₁ p₂ p = true → ↑k * Poly.denote ctx init = Poly.denote ctx p₁ → Poly.denote ctx p₂ = 0 → ↑k * Poly.denote ctx init = Poly.denote ctx p

noncomputable def Lean.Grind.CommRing.norm_int_cert (e : Expr) (p : Poly) : Bool

theorem Lean.Grind.CommRing.norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p = true → Expr.denote ctx e = Poly.denote' ctx p

Helper theorems for normalizing ring constraints in the grind order module.

noncomputable def Lean.Grind.CommRing.norm_cnstr_cert (lhs rhs lhs' rhs' : Expr) : Bool

theorem Lean.Grind.CommRing.le_norm_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_cnstr_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.lt_norm_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_cnstr_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')

noncomputable def Lean.Grind.CommRing.norm_eq_cert (lhs rhs lhs' rhs' : Expr) : Bool

theorem Lean.Grind.CommRing.eq_norm_expr {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_eq_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

noncomputable def Lean.Grind.CommRing.norm_cnstr_nc_cert (lhs rhs lhs' rhs' : Expr) : Bool

theorem Lean.Grind.CommRing.le_norm_expr_nc {α : Type u_1} [Ring α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_cnstr_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')

theorem Lean.Grind.CommRing.lt_norm_expr_nc {α : Type u_1} [Ring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_cnstr_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')

noncomputable def Lean.Grind.CommRing.norm_eq_nc_cert (lhs rhs lhs' rhs' : Expr) : Bool

theorem Lean.Grind.CommRing.eq_norm_expr_nc {α : Type u_1} [Ring α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) : norm_eq_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

Helper theorems for quick normalization

theorem Lean.Grind.CommRing.le_norm0 {α : Type u_1} [Ring α] [LE α] (lhs rhs : α) : (lhs ≤ rhs) = (lhs ≤ rhs + ↑0)

theorem Lean.Grind.CommRing.lt_norm0 {α : Type u_1} [Ring α] [LT α] (lhs rhs : α) : (lhs < rhs) = (lhs < rhs + ↑0)

theorem Lean.Grind.CommRing.eq_norm0 {α : Type u_1} [Ring α] (lhs rhs : α) : (lhs = rhs) = (lhs = rhs + ↑0)