@[reducible, inline]

abbrev Lean.Grind.CommRing.Var : Type

Equations

• Lean.Grind.CommRing.Var = Nat

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

instance Lean.Grind.CommRing.instInhabitedExpr : Inhabited Expr

Equations

• Lean.Grind.CommRing.instInhabitedExpr = { default := Lean.Grind.CommRing.Expr.num default }

instance Lean.Grind.CommRing.instBEqExpr : BEq Expr

Equations

• Lean.Grind.CommRing.instBEqExpr = { beq := Lean.Grind.CommRing.beqExpr✝ }

instance Lean.Grind.CommRing.instHashableExpr : Hashable Expr

Equations

• Lean.Grind.CommRing.instHashableExpr = { hash := Lean.Grind.CommRing.hashExpr✝ }

instance Lean.Grind.CommRing.instReprExpr : Repr Expr

Equations

• Lean.Grind.CommRing.instReprExpr = { reprPrec := Lean.Grind.CommRing.reprExpr✝ }

@[reducible, inline]

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

Equations

• Lean.Grind.CommRing.Context α = Lean.RArray α

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

Equations

• Lean.Grind.CommRing.Var.denote ctx v = Lean.RArray.get ctx v

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

Equations

• Lean.Grind.CommRing.denoteInt k = Bool.rec (OfNat.ofNat k.natAbs) (-OfNat.ofNat k.natAbs) (k.blt' 0)

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

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Grind.CommRing.Power : Type

• x : Var
• k : Nat

instance Lean.Grind.CommRing.instBEqPower : BEq Power

Equations

• Lean.Grind.CommRing.instBEqPower = { beq := Lean.Grind.CommRing.beqPower✝ }

instance Lean.Grind.CommRing.instReprPower : Repr Power

Equations

• Lean.Grind.CommRing.instReprPower = { reprPrec := Lean.Grind.CommRing.reprPower✝ }

instance Lean.Grind.CommRing.instInhabitedPower : Inhabited Power

Equations

• Lean.Grind.CommRing.instInhabitedPower = { default := { x := default, k := default } }

instance Lean.Grind.CommRing.instHashablePower : Hashable Power

Equations

• Lean.Grind.CommRing.instHashablePower = { hash := Lean.Grind.CommRing.hashPower✝ }

instance Lean.Grind.CommRing.instLawfulBEqPower : LawfulBEq Power

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

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• p₁.varLt p₂ = Nat.blt p₁.x p₂.x

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

Equations

• Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := 0 } = 1
• Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := 1 } = Lean.Grind.CommRing.Var.denote ctx x_1
• Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := k } = Lean.Grind.CommRing.Var.denote ctx x_1 ^ k

inductive Lean.Grind.CommRing.Mon : Type

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

instance Lean.Grind.CommRing.instBEqMon : BEq Mon

Equations

• Lean.Grind.CommRing.instBEqMon = { beq := Lean.Grind.CommRing.beqMon✝ }

instance Lean.Grind.CommRing.instReprMon : Repr Mon

Equations

• Lean.Grind.CommRing.instReprMon = { reprPrec := Lean.Grind.CommRing.reprMon✝ }

instance Lean.Grind.CommRing.instInhabitedMon : Inhabited Mon

Equations

• Lean.Grind.CommRing.instInhabitedMon = { default := Lean.Grind.CommRing.Mon.unit }

instance Lean.Grind.CommRing.instHashableMon : Hashable Mon

Equations

• Lean.Grind.CommRing.instHashableMon = { hash := Lean.Grind.CommRing.hashMon✝ }

instance Lean.Grind.CommRing.instLawfulBEqMon : LawfulBEq Mon

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• Lean.Grind.CommRing.Mon.denote ctx Lean.Grind.CommRing.Mon.unit = 1
• Lean.Grind.CommRing.Mon.denote ctx (Lean.Grind.CommRing.Mon.mult p m) = Lean.Grind.CommRing.Power.denote ctx p * Lean.Grind.CommRing.Mon.denote ctx m

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

Equations

• Lean.Grind.CommRing.Mon.denote' ctx Lean.Grind.CommRing.Mon.unit = 1
• Lean.Grind.CommRing.Mon.denote' ctx (Lean.Grind.CommRing.Mon.mult p m_1) = Lean.Grind.CommRing.Mon.denote'.go ctx m_1 (Lean.Grind.CommRing.Power.denote ctx p)

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

Equations

• Lean.Grind.CommRing.Mon.denote'.go ctx Lean.Grind.CommRing.Mon.unit acc = acc
• Lean.Grind.CommRing.Mon.denote'.go ctx (Lean.Grind.CommRing.Mon.mult p m_1) acc = Lean.Grind.CommRing.Mon.denote'.go ctx m_1 (acc * Lean.Grind.CommRing.Power.denote ctx p)

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

Equations

• Lean.Grind.CommRing.Mon.ofVar x = Lean.Grind.CommRing.Mon.mult { x := x, k := 1 } Lean.Grind.CommRing.Mon.unit

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

Equations

• Lean.Grind.CommRing.Mon.unit.concat m₂ = m₂
• (Lean.Grind.CommRing.Mon.mult p m).concat m₂ = Lean.Grind.CommRing.Mon.mult p (m.concat m₂)

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.mulPow pw Lean.Grind.CommRing.Mon.unit = Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit

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

Equations

• Lean.Grind.CommRing.Mon.unit.length = 0
• (Lean.Grind.CommRing.Mon.mult p m).length = 1 + m.length

def Lean.Grind.CommRing.hugeFuel : Nat

Equations

• Lean.Grind.CommRing.hugeFuel = 1000000

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

Equations

• m₁.mul m₂ = Lean.Grind.CommRing.Mon.mul.go Lean.Grind.CommRing.hugeFuel m₁ m₂

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.mul.go 0 m₁ m₂ = m₁.concat m₂
• Lean.Grind.CommRing.Mon.mul.go fuel_2.succ m₁ Lean.Grind.CommRing.Mon.unit = m₁
• Lean.Grind.CommRing.Mon.mul.go fuel_2.succ Lean.Grind.CommRing.Mon.unit m₂ = m₂

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

Equations

• Lean.Grind.CommRing.Mon.unit.degree = 0
• (Lean.Grind.CommRing.Mon.mult p m).degree = p.k + m.degree

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

Equations

• x.revlex y = bif Nat.blt x y then Ordering.gt else bif Nat.blt y x then Ordering.lt else Ordering.eq

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

Equations

• Lean.Grind.CommRing.powerRevlex k₁ k₂ = bif k₁.blt k₂ then Ordering.gt else bif k₂.blt k₁ then Ordering.lt else Ordering.eq

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

Equations

• Lean.Grind.CommRing.powerRevlex_k k₁ k₂ = Bool.rec (Bool.rec Ordering.eq Ordering.lt (k₂.blt k₁)) Ordering.gt (k₁.blt k₂)

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

Equations

• p₁.revlex p₂ = (p₁.x.revlex p₂.x).then (Lean.Grind.CommRing.powerRevlex p₁.k p₂.k)

@[irreducible]

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.unit.revlexWF Lean.Grind.CommRing.Mon.unit = Ordering.eq
• Lean.Grind.CommRing.Mon.unit.revlexWF (Lean.Grind.CommRing.Mon.mult p m) = Ordering.gt
• (Lean.Grind.CommRing.Mon.mult p m).revlexWF Lean.Grind.CommRing.Mon.unit = Ordering.lt

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Mon.revlexFuel 0 m₁ m₂ = m₁.revlexWF m₂
• Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit = Ordering.eq
• Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult p m) = Ordering.gt
• Lean.Grind.CommRing.Mon.revlexFuel fuel_2.succ (Lean.Grind.CommRing.Mon.mult p m) Lean.Grind.CommRing.Mon.unit = Ordering.lt

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

Equations

• m₁.revlex m₂ = Lean.Grind.CommRing.Mon.revlexFuel Lean.Grind.CommRing.hugeFuel m₁ m₂

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

Equations

• m₁.grevlex m₂ = (compare m₁.degree m₂.degree).then (m₁.revlex m₂)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• m₁.grevlex_k m₂ = Bool.rec (Bool.rec Ordering.gt Ordering.lt (m₁.degree.blt m₂.degree)) (m₁.revlex_k m₂) (m₁.degree.beq m₂.degree)

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

Equations

• Lean.Grind.CommRing.instBEqPoly = { beq := Lean.Grind.CommRing.beqPoly✝ }

instance Lean.Grind.CommRing.instReprPoly : Repr Poly

Equations

• Lean.Grind.CommRing.instReprPoly = { reprPrec := Lean.Grind.CommRing.reprPoly✝ }

instance Lean.Grind.CommRing.instInhabitedPoly : Inhabited Poly

Equations

• Lean.Grind.CommRing.instInhabitedPoly = { default := Lean.Grind.CommRing.Poly.num default }

instance Lean.Grind.CommRing.instHashablePoly : Hashable Poly

Equations

• Lean.Grind.CommRing.instHashablePoly = { hash := Lean.Grind.CommRing.hashPoly✝ }

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

instance Lean.Grind.CommRing.instLawfulBEqPoly : LawfulBEq Poly

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

Equations

• Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.num k) = ↑k
• Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.add k m p_2) = k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denote ctx p_2

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

Equations

• Lean.Grind.CommRing.Poly.denote' ctx (Lean.Grind.CommRing.Poly.num k) = ↑k
• Lean.Grind.CommRing.Poly.denote' ctx (Lean.Grind.CommRing.Poly.add k m p_2) = Lean.Grind.CommRing.Poly.denote'.go ctx p_2 (Lean.Grind.CommRing.Poly.denote'.denoteTerm ctx k m)

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

Equations

• Lean.Grind.CommRing.Poly.denote'.denoteTerm ctx k m = bif k == 1 then Lean.Grind.CommRing.Mon.denote' ctx m else k * Lean.Grind.CommRing.Mon.denote' ctx m

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

Equations

• Lean.Grind.CommRing.Poly.denote'.go ctx (Lean.Grind.CommRing.Poly.num 0) acc = acc
• Lean.Grind.CommRing.Poly.denote'.go ctx (Lean.Grind.CommRing.Poly.num k) acc = acc + ↑k
• Lean.Grind.CommRing.Poly.denote'.go ctx (Lean.Grind.CommRing.Poly.add k m p_2) acc = Lean.Grind.CommRing.Poly.denote'.go ctx p_2 (acc + Lean.Grind.CommRing.Poly.denote'.denoteTerm ctx k m)

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

Equations

• Lean.Grind.CommRing.Poly.ofMon m = Lean.Grind.CommRing.Poly.add 1 m (Lean.Grind.CommRing.Poly.num 0)

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

Equations

• Lean.Grind.CommRing.Poly.ofVar x = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.ofVar x)

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

Equations

• (Lean.Grind.CommRing.Poly.num k).isSorted = true
• (Lean.Grind.CommRing.Poly.add k v (Lean.Grind.CommRing.Poly.num k_1)).isSorted = true
• (Lean.Grind.CommRing.Poly.add k m₁ (Lean.Grind.CommRing.Poly.add k_1 m₂ p)).isSorted = (m₁.grevlex m₂ == Ordering.gt && (Lean.Grind.CommRing.Poly.add k_1 m₂ p).isSorted)

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

Equations

• p.addConst k = bif k == 0 then p else Lean.Grind.CommRing.Poly.addConst.go k p

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

Equations

• Lean.Grind.CommRing.Poly.addConst.go k (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.num (k_1 + k)
• Lean.Grind.CommRing.Poly.addConst.go k (Lean.Grind.CommRing.Poly.add k_1 m p_1) = Lean.Grind.CommRing.Poly.add k_1 m (Lean.Grind.CommRing.Poly.addConst.go k p_1)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Grind.CommRing.Poly.insert k m p = bif k == 0 then p else bif m == Lean.Grind.CommRing.Mon.unit then p.addConst k else Lean.Grind.CommRing.Poly.insert.go k m p

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.insert.go k m (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k_1)

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

Equations

• (Lean.Grind.CommRing.Poly.num k).concat p₂ = p₂.addConst k
• (Lean.Grind.CommRing.Poly.add k m p_1).concat p₂ = Lean.Grind.CommRing.Poly.add k m (p_1.concat p₂)

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

Equations

• Lean.Grind.CommRing.Poly.mulConst k p = bif k == 0 then Lean.Grind.CommRing.Poly.num 0 else bif k == 1 then p else Lean.Grind.CommRing.Poly.mulConst.go k p

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

Equations

• Lean.Grind.CommRing.Poly.mulConst.go k (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.num (k * k_1)
• Lean.Grind.CommRing.Poly.mulConst.go k (Lean.Grind.CommRing.Poly.add k_1 m p_1) = Lean.Grind.CommRing.Poly.add (k * k_1) m (Lean.Grind.CommRing.Poly.mulConst.go k p_1)

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

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.mulMon.go k m (Lean.Grind.CommRing.Poly.add k_1 m_1 p_1) = Lean.Grind.CommRing.Poly.add (k * k_1) (m.mul m_1) (Lean.Grind.CommRing.Poly.mulMon.go k m p_1)

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

Equations

• One or more equations did not get rendered due to their size.

@[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.combine (p₁ p₂ : Poly) : Poly

Equations

• p₁.combine p₂ = Lean.Grind.CommRing.Poly.combine.go Lean.Grind.CommRing.hugeFuel p₁ p₂

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.combine.go 0 p₁ p₂ = p₁.concat p₂
• Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂) = Lean.Grind.CommRing.Poly.num (k₁ + k₂)
• Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2) = (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2).addConst k₁
• Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2) (Lean.Grind.CommRing.Poly.num k₂) = (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2).addConst k₂

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

A Poly.combine optimized for the kernel.

Equations

• One or more equations did not get rendered due to their size.

@[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

Equations

• p₁.mul p₂ = Lean.Grind.CommRing.Poly.mul.go p₂ p₁ (Lean.Grind.CommRing.Poly.num 0)

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

Equations

• Lean.Grind.CommRing.Poly.mul.go p₂ (Lean.Grind.CommRing.Poly.num k) acc = acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂)
• Lean.Grind.CommRing.Poly.mul.go p₂ (Lean.Grind.CommRing.Poly.add k m p_1) acc = Lean.Grind.CommRing.Poly.mul.go p₂ p_1 (acc.combine (Lean.Grind.CommRing.Poly.mulMon k m p₂))

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

Equations

• p.pow 0 = Lean.Grind.CommRing.Poly.num 1
• p.pow 1 = p
• p.pow k_2.succ = p.mul (p.pow k_2)

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

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Grind.CommRing.Expr.num k).toPoly = Lean.Grind.CommRing.Poly.num k
• (Lean.Grind.CommRing.Expr.intCast k).toPoly = Lean.Grind.CommRing.Poly.num k
• (Lean.Grind.CommRing.Expr.natCast k).toPoly = Lean.Grind.CommRing.Poly.num ↑k
• (Lean.Grind.CommRing.Expr.var x_1).toPoly = Lean.Grind.CommRing.Poly.ofVar x_1
• (a.add b).toPoly = a.toPoly.combine b.toPoly
• (a.mul b).toPoly = a.toPoly.mul b.toPoly
• a.neg.toPoly = Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly
• (a.sub b).toPoly = a.toPoly.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly)
• ((Lean.Grind.CommRing.Expr.num n).pow k).toPoly = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (n ^ k)
• ((Lean.Grind.CommRing.Expr.intCast n).pow k).toPoly = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (n ^ k)
• ((Lean.Grind.CommRing.Expr.natCast n).pow k).toPoly = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (↑n ^ k)
• (a.pow k).toPoly = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else a.toPoly.pow k

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

Equations

• (Lean.Grind.CommRing.Poly.num k).normEq0 c = bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0 else Lean.Grind.CommRing.Poly.num k
• (Lean.Grind.CommRing.Poly.add k m p_2).normEq0 c = bif k % ↑c == 0 then p_2.normEq0 c else Lean.Grind.CommRing.Poly.add k m (p_2.normEq0 c)

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

Equations

• (Lean.Grind.CommRing.Poly.num k_1).addConstC k c = Lean.Grind.CommRing.Poly.num ((k_1 + k) % ↑c)
• (Lean.Grind.CommRing.Poly.add k_1 m p_2).addConstC k c = Lean.Grind.CommRing.Poly.add k_1 m (p_2.addConstC k c)

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

Equations

• Lean.Grind.CommRing.Poly.insertC k m p c = bif k % ↑c == 0 then p else Lean.Grind.CommRing.Poly.insertC.go m c (k % ↑c) p

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.insertC.go m c k (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k_1)

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

Equations

• Lean.Grind.CommRing.Poly.mulConstC k p c = bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0 else bif k % ↑c == 1 then p else Lean.Grind.CommRing.Poly.mulConstC.go k c p

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.mulConstC.go k c (Lean.Grind.CommRing.Poly.num k_1) = Lean.Grind.CommRing.Poly.num (k * k_1 % ↑c)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• p₁.combineC p₂ c = Lean.Grind.CommRing.Poly.combineC.go c Lean.Grind.CommRing.hugeFuel p₁ p₂

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Poly.combineC.go c 0 p₁ p₂ = p₁.concat p₂
• Lean.Grind.CommRing.Poly.combineC.go c fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂) = Lean.Grind.CommRing.Poly.num ((k₁ + k₂) % ↑c)
• Lean.Grind.CommRing.Poly.combineC.go c fuel_2.succ (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2) = (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂_2).addConstC k₁ c
• Lean.Grind.CommRing.Poly.combineC.go c fuel_2.succ (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2) (Lean.Grind.CommRing.Poly.num k₂) = (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2).addConstC k₂ c

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

Equations

• p₁.mulC p₂ c = Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ (Lean.Grind.CommRing.Poly.num 0)

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

Equations

• Lean.Grind.CommRing.Poly.mulC.go p₂ c (Lean.Grind.CommRing.Poly.num k) acc = acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c
• Lean.Grind.CommRing.Poly.mulC.go p₂ c (Lean.Grind.CommRing.Poly.add k m p_1) acc = Lean.Grind.CommRing.Poly.mulC.go p₂ c p_1 (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)

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

Equations

• p.powC 0 c = Lean.Grind.CommRing.Poly.num 1
• p.powC 1 c = p
• p.powC k_2.succ c = p.mulC (p.powC k_2 c) c

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

Equations

• e.toPolyC c = Lean.Grind.CommRing.Expr.toPolyC.go c e

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.Expr.toPolyC.go c (Lean.Grind.CommRing.Expr.num k) = Lean.Grind.CommRing.Poly.num (k % ↑c)
• Lean.Grind.CommRing.Expr.toPolyC.go c (Lean.Grind.CommRing.Expr.natCast k) = Lean.Grind.CommRing.Poly.num (↑k % ↑c)
• Lean.Grind.CommRing.Expr.toPolyC.go c (Lean.Grind.CommRing.Expr.intCast k) = Lean.Grind.CommRing.Poly.num (k % ↑c)
• Lean.Grind.CommRing.Expr.toPolyC.go c (Lean.Grind.CommRing.Expr.var x_1) = Lean.Grind.CommRing.Poly.ofVar x_1
• Lean.Grind.CommRing.Expr.toPolyC.go c (a.add b) = (Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c
• Lean.Grind.CommRing.Expr.toPolyC.go c (a.mul b) = (Lean.Grind.CommRing.Expr.toPolyC.go c a).mulC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c
• Lean.Grind.CommRing.Expr.toPolyC.go c a.neg = Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c a) c
• Lean.Grind.CommRing.Expr.toPolyC.go c (a.sub b) = (Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC (Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c b) c) c
• Lean.Grind.CommRing.Expr.toPolyC.go c ((Lean.Grind.CommRing.Expr.num n).pow k) = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (n ^ k % ↑c)
• Lean.Grind.CommRing.Expr.toPolyC.go c (a.pow k) = bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else (Lean.Grind.CommRing.Expr.toPolyC.go c a).powC k c

inductive Lean.Grind.CommRing.NullCert : Type

A Nullstellensatz certificate.

lhs₁ = rh₁ → ... → lhsₙ = rhₙ → q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ) = 0

• empty : NullCert
• add (q : Poly) (lhs rhs : Expr) (s : NullCert) : NullCert

noncomputable def Lean.Grind.CommRing.NullCert.denote {α : Type u_1} [CommRing α] (ctx : Context α) : NullCert → α

q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.NullCert.denote ctx Lean.Grind.CommRing.NullCert.empty = 0

def Lean.Grind.CommRing.NullCert.eqsImplies {α : Type u_1} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : Prop

lhs₁ = rh₁ → ... → lhsₙ = rhₙ → p

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.CommRing.NullCert.eqsImplies ctx Lean.Grind.CommRing.NullCert.empty p = p

def Lean.Grind.CommRing.NullCert.toPoly (nc : NullCert) : Poly

A polynomial representing

q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)

Equations

• Lean.Grind.CommRing.NullCert.empty.toPoly = Lean.Grind.CommRing.Poly.num 0
• (Lean.Grind.CommRing.NullCert.add q lhs rhs nc_1).toPoly = (q.mul (lhs.sub rhs).toPoly).combine nc_1.toPoly

def Lean.Grind.CommRing.NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly

Equations

• Lean.Grind.CommRing.NullCert.empty.toPolyC c = Lean.Grind.CommRing.Poly.num 0
• (Lean.Grind.CommRing.NullCert.add q lhs rhs nc_1).toPolyC c = (q.mulC ((lhs.sub rhs).toPolyC c) c).combineC (nc_1.toPolyC c) c

Theorems for justifying the procedure for commutative rings in grind.

theorem Lean.Grind.CommRing.denoteInt_eq {α : Type u_1} [CommRing α] (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_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.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) : denote'.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} [CommRing α] (ctx : Context α) (m : Mon) : denote ctx (ofMon m) = Mon.denote ctx m

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

theorem Lean.Grind.CommRing.Poly.denote_addConst {α : Type u_1} [CommRing α] (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} [CommRing α] (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} [CommRing α] (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} [CommRing α] (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_combine {α : Type u_1} [CommRing α] (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_pow {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) (k : Nat) : denote ctx (p.pow 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.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.NullCert.eqsImplies_helper {α : Type u_1} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : (denote ctx nc = 0 → p) → eqsImplies ctx nc p

Helper theorem for proving NullCert theorems.

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

def Lean.Grind.CommRing.NullCert.eq_cert (nc : NullCert) (lhs rhs : Expr) : Bool

Equations

• nc.eq_cert lhs rhs = ((lhs.sub rhs).toPoly == nc.toPoly)

theorem Lean.Grind.CommRing.NullCert.eq {α : Type u_1} [CommRing α] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr} : nc.eq_cert lhs rhs = true → eqsImplies ctx nc (Expr.denote ctx lhs = Expr.denote ctx rhs)

theorem Lean.Grind.CommRing.NullCert.eqsImplies_helper' {α : Type u_1} [CommRing α] {ctx : Context α} {nc : NullCert} {p q : Prop} : eqsImplies ctx nc p → (p → q) → eqsImplies ctx nc q

theorem Lean.Grind.CommRing.NullCert.ne_unsat {α : Type u_1} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) : nc.eq_cert lhs rhs = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → eqsImplies ctx nc False

def Lean.Grind.CommRing.NullCert.eq_nzdiv_cert (nc : NullCert) (k : Int) (lhs rhs : Expr) : Bool

Equations

• nc.eq_nzdiv_cert k lhs rhs = (decide (k ≠ 0) && Lean.Grind.CommRing.Poly.mulConst k (lhs.sub rhs).toPoly == nc.toPoly)

theorem Lean.Grind.CommRing.NullCert.eq_nzdiv {α : Type u_1} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_cert k lhs rhs = true → eqsImplies ctx nc (Expr.denote ctx lhs = Expr.denote ctx rhs)

theorem Lean.Grind.CommRing.NullCert.ne_nzdiv_unsat {α : Type u_1} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_cert k lhs rhs = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → eqsImplies ctx nc False

def Lean.Grind.CommRing.NullCert.eq_unsat_cert (nc : NullCert) (k : Int) : Bool

Equations

• nc.eq_unsat_cert k = (decide (k ≠ 0) && nc.toPoly == Lean.Grind.CommRing.Poly.num k)

theorem Lean.Grind.CommRing.NullCert.eq_unsat {α : Type u_1} [CommRing α] [IsCharP α 0] (ctx : Context α) (nc : NullCert) (k : Int) : nc.eq_unsat_cert k = true → eqsImplies ctx nc False

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} [CommRing α] [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} [CommRing α] [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} [CommRing α] [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_combineC {α : Type u_1} {c : Nat} [CommRing α] [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_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.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.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.NullCert.denote_toPolyC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) : Poly.denote ctx (nc.toPolyC c) = denote ctx nc

def Lean.Grind.CommRing.NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) : Bool

Equations

• nc.eq_certC lhs rhs c = ((lhs.sub rhs).toPolyC c == nc.toPolyC c)

theorem Lean.Grind.CommRing.NullCert.eqC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr} : nc.eq_certC lhs rhs c = true → eqsImplies ctx nc (Expr.denote ctx lhs = Expr.denote ctx rhs)

theorem Lean.Grind.CommRing.NullCert.ne_unsatC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr) : nc.eq_certC lhs rhs c = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → eqsImplies ctx nc False

def Lean.Grind.CommRing.NullCert.eq_nzdiv_certC (nc : NullCert) (k : Int) (lhs rhs : Expr) (c : Nat) : Bool

Equations

• nc.eq_nzdiv_certC k lhs rhs c = (decide (k ≠ 0) && Lean.Grind.CommRing.Poly.mulConstC k ((lhs.sub rhs).toPolyC c) c == nc.toPolyC c)

theorem Lean.Grind.CommRing.NullCert.eq_nzdivC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_certC k lhs rhs c = true → eqsImplies ctx nc (Expr.denote ctx lhs = Expr.denote ctx rhs)

theorem Lean.Grind.CommRing.NullCert.ne_nzdiv_unsatC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_certC k lhs rhs c = true → Expr.denote ctx lhs ≠ Expr.denote ctx rhs → eqsImplies ctx nc False

def Lean.Grind.CommRing.NullCert.eq_unsat_certC (nc : NullCert) (k : Int) (c : Nat) : Bool

Equations

• nc.eq_unsat_certC k c = (k % ↑c != 0 && nc.toPolyC c == Lean.Grind.CommRing.Poly.num k)

theorem Lean.Grind.CommRing.NullCert.eq_unsatC {α : Type u_1} {c : Nat} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (k : Int) : nc.eq_unsat_certC k c = true → eqsImplies ctx nc False

Theorems for stepwise proof-term construction

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

Equations

• Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = (lhs.sub rhs).toPoly_k.beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.superpose_cert k₁ m₁ p₁ k₂ m₂ p₂ p = ((Lean.Grind.CommRing.Poly.mulMon_k k₁ m₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂)).beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.simp_cert k₁ p₁ k₂ m₂ p₂ p = ((Lean.Grind.CommRing.Poly.mulConst_k k₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂)).beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.mul_cert p₁ k p = (Lean.Grind.CommRing.Poly.mulConst_k k p₁).beq' p

def 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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.div_cert p₁ k p = (!k.beq' 0).and' ((Lean.Grind.CommRing.Poly.mulConst_k k p).beq' p₁)

def 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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.unsat_eq_cert p k = (!k.beq' 0).and' (p.beq' (Lean.Grind.CommRing.Poly.num k))

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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.d_step1_cert p₁ k₂ m₂ p₂ p = p.beq' (p₁.combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂))

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

Equations

• Lean.Grind.CommRing.Stepwise.d_stepk_cert k₁ p₁ k₂ m₂ p₂ p = p.beq' ((Lean.Grind.CommRing.Poly.mulConst_k k₁ p₁).combine_k (Lean.Grind.CommRing.Poly.mulMon_k k₂ m₂ p₂))

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

Equations

• Lean.Grind.CommRing.Stepwise.imp_1eq_cert lhs rhs p₁ p₂ = ((lhs.sub rhs).toPoly_k.beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0))

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

Equations

• Lean.Grind.CommRing.Stepwise.imp_keq_cert lhs rhs k p₁ p₂ = (!k.beq' 0).and' (((lhs.sub rhs).toPoly_k.beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0)))

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

Equations

• Lean.Grind.CommRing.Stepwise.core_certC lhs rhs p c = ((lhs.sub rhs).toPolyC c).beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.superpose_certC k₁ m₁ p₁ k₂ m₂ p₂ p c = ((Lean.Grind.CommRing.Poly.mulMonC k₁ m₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c).beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.mul_certC p₁ k p c = (Lean.Grind.CommRing.Poly.mulConstC k p₁ c).beq' p

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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.div_certC p₁ k p c = (!k.beq' 0).and' ((Lean.Grind.CommRing.Poly.mulConstC k p c).beq' p₁)

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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.simp_certC k₁ p₁ k₂ m₂ p₂ p c = ((Lean.Grind.CommRing.Poly.mulConstC k₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c).beq' p

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

Equations

• Lean.Grind.CommRing.Stepwise.unsat_eq_certC p k c = (!(k % ↑c).beq' 0).and' (p.beq' (Lean.Grind.CommRing.Poly.num k))

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

Equations

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.d_step1_certC p₁ k₂ m₂ p₂ p c = p.beq' (p₁.combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c)

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

Equations

• Lean.Grind.CommRing.Stepwise.d_stepk_certC k₁ p₁ k₂ m₂ p₂ p c = p.beq' ((Lean.Grind.CommRing.Poly.mulConstC k₁ p₁ c).combineC (Lean.Grind.CommRing.Poly.mulMonC k₂ m₂ p₂ c) c)

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

Equations

• Lean.Grind.CommRing.Stepwise.imp_1eq_certC lhs rhs p₁ p₂ c = (((lhs.sub rhs).toPolyC c).beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0))

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

Equations

• Lean.Grind.CommRing.Stepwise.imp_keq_certC lhs rhs k p₁ p₂ c = (!k.beq' 0).and' ((((lhs.sub rhs).toPolyC c).beq' p₁).and' (p₂.beq' (Lean.Grind.CommRing.Poly.num 0)))

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) : α

Equations

• Lean.Grind.CommRing.Mon.denoteAsIntModule ctx Lean.Grind.CommRing.Mon.unit = One.one
• Lean.Grind.CommRing.Mon.denoteAsIntModule ctx (Lean.Grind.CommRing.Mon.mult p m_1) = Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m_1 (Lean.Grind.CommRing.Power.denote ctx p)

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

Equations

• Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx Lean.Grind.CommRing.Mon.unit acc = acc
• Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx (Lean.Grind.CommRing.Mon.mult p m_1) acc = Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m_1 (acc * Lean.Grind.CommRing.Power.denote ctx p)

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

Equations

• Lean.Grind.CommRing.Poly.denoteAsIntModule ctx (Lean.Grind.CommRing.Poly.num k) = k * One.one
• Lean.Grind.CommRing.Poly.denoteAsIntModule ctx (Lean.Grind.CommRing.Poly.add k m p_2) = k * Lean.Grind.CommRing.Mon.denoteAsIntModule ctx m + Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p_2

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.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.denoteAsIntModule ctx p ≠ 0

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

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

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

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

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

theorem Lean.Grind.CommRing.not_lt_norm' {α : Type u_1} [CommRing α] [LE α] [LT α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) : Stepwise.core_cert lhs rhs p = true → ¬Expr.denote ctx lhs < Expr.denote ctx rhs → ¬Poly.denoteAsIntModule 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.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

Equations

• Lean.Grind.CommRing.one_eq_zero_unsat_cert p = (p.beq' (Lean.Grind.CommRing.Poly.num 1) || p.beq' (Lean.Grind.CommRing.Poly.num (-1)))

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

Equations

• Lean.Grind.CommRing.eq_normEq0_cert c p₁ p₂ p = (p₁.beq' (Lean.Grind.CommRing.Poly.num ↑c) && p.beq' (p₂.normEq0 c))

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

Equations

• Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.add k v p_2) p₂ p = false
• Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.add k v p_3) p = false
• Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.num g_1) (Lean.Grind.CommRing.Poly.add k v p_4) = false
• Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.num g_1) (Lean.Grind.CommRing.Poly.num g_2) = (g_2 == a * g + b * g_1)

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

Equations

• Lean.Grind.CommRing.d_normEq0_cert c p₁ p₂ p = (p₂.beq' (Lean.Grind.CommRing.Poly.num ↑c)).and' (p.beq' (p₁.normEq0 c))

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

Equations

• Lean.Grind.CommRing.norm_int_cert e p = e.toPoly_k.beq' p

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