@[reducible, inline]

abbrev Lean.Grind.CommRing.Var : Type

Equations

• Lean.Grind.CommRing.Var = Nat

inductive Lean.Grind.CommRing.Expr : Type

• num (v : 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✝ }

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

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

Equations

• Lean.Grind.CommRing.denoteInt k = bif decide (k < 0) then -OfNat.ofNat k.natAbs else OfNat.ofNat k.natAbs

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

Equations

• Lean.Grind.CommRing.Expr.denote ctx (a.add b) = Lean.Grind.CommRing.Expr.denote ctx a + Lean.Grind.CommRing.Expr.denote ctx b
• Lean.Grind.CommRing.Expr.denote ctx (a.sub b) = Lean.Grind.CommRing.Expr.denote ctx a - Lean.Grind.CommRing.Expr.denote ctx b
• Lean.Grind.CommRing.Expr.denote ctx (a.mul b) = Lean.Grind.CommRing.Expr.denote ctx a * Lean.Grind.CommRing.Expr.denote ctx b
• Lean.Grind.CommRing.Expr.denote ctx a.neg = -Lean.Grind.CommRing.Expr.denote ctx a
• Lean.Grind.CommRing.Expr.denote ctx (Lean.Grind.CommRing.Expr.num k) = Lean.Grind.CommRing.denoteInt k
• Lean.Grind.CommRing.Expr.denote ctx (Lean.Grind.CommRing.Expr.var v) = Lean.Grind.CommRing.Var.denote ctx v
• Lean.Grind.CommRing.Expr.denote ctx (a.pow k) = Lean.Grind.CommRing.Expr.denote ctx a ^ k

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

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} [CommRing α] (ctx : Context α) : Power → α

Equations

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

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

def Lean.Grind.CommRing.Mon.denote {α : Type u_1} [CommRing α] (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 a a_1) = Lean.Grind.CommRing.Power.denote ctx a * Lean.Grind.CommRing.Mon.denote ctx a_1

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 a a_1).concat m₂ = Lean.Grind.CommRing.Mon.mult a (a_1.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 a a_1).length = 1 + a_1.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 a a_1).degree = a.k + a_1.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

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₂)

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.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✝ }

instance Lean.Grind.CommRing.instLawfulBEqPoly : LawfulBEq Poly

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

Equations

• Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.num a) = ↑a
• Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.add a a_1 a_2) = ↑a * Lean.Grind.CommRing.Mon.denote ctx a_1 + Lean.Grind.CommRing.Poly.denote ctx a_2

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 a) = Lean.Grind.CommRing.Poly.num (a + k)
• Lean.Grind.CommRing.Poly.addConst.go k (Lean.Grind.CommRing.Poly.add a a_1 a_2) = Lean.Grind.CommRing.Poly.add a a_1 (Lean.Grind.CommRing.Poly.addConst.go k a_2)

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 a) = Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num a)

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

Equations

• (Lean.Grind.CommRing.Poly.num a).concat p₂ = p₂.addConst a
• (Lean.Grind.CommRing.Poly.add a a_1 a_2).concat p₂ = Lean.Grind.CommRing.Poly.add a a_1 (a_2.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 a) = Lean.Grind.CommRing.Poly.num (k * a)
• Lean.Grind.CommRing.Poly.mulConst.go k (Lean.Grind.CommRing.Poly.add a a_1 a_2) = Lean.Grind.CommRing.Poly.add (k * a) a_1 (Lean.Grind.CommRing.Poly.mulConst.go k a_2)

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 a a_1 a_2) = Lean.Grind.CommRing.Poly.add (k * a) (m.mul a_1) (Lean.Grind.CommRing.Poly.mulMon.go k m a_2)

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₂

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 a) acc = acc.combine (Lean.Grind.CommRing.Poly.mulConst a p₂)
• Lean.Grind.CommRing.Poly.mul.go p₂ (Lean.Grind.CommRing.Poly.add a a_1 a_2) acc = Lean.Grind.CommRing.Poly.mul.go p₂ a_2 (acc.combine (Lean.Grind.CommRing.Poly.mulMon a a_1 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

• (Lean.Grind.CommRing.Expr.num n).toPoly = Lean.Grind.CommRing.Poly.num n
• (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 = Lean.Grind.CommRing.Poly.num (n ^ k)
• ((Lean.Grind.CommRing.Expr.var x_1).pow k).toPoly = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := k } Lean.Grind.CommRing.Mon.unit)
• (a.pow k).toPoly = a.toPoly.pow k

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 a).addConstC k c = Lean.Grind.CommRing.Poly.num ((a + k) % ↑c)
• (Lean.Grind.CommRing.Poly.add a a_1 a_2).addConstC k c = Lean.Grind.CommRing.Poly.add a a_1 (a_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 a) = Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num a)

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 a) = Lean.Grind.CommRing.Poly.num (k * a % ↑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 a) acc = acc.combineC (Lean.Grind.CommRing.Poly.mulConstC a p₂ c) c
• Lean.Grind.CommRing.Poly.mulC.go p₂ c (Lean.Grind.CommRing.Poly.add a a_1 a_2) acc = Lean.Grind.CommRing.Poly.mulC.go p₂ c a_2 (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC a a_1 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

• Lean.Grind.CommRing.Expr.toPolyC.go c (Lean.Grind.CommRing.Expr.num n) = Lean.Grind.CommRing.Poly.num (n % ↑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) = Lean.Grind.CommRing.Poly.num (n ^ k % ↑c)
• Lean.Grind.CommRing.Expr.toPolyC.go c ((Lean.Grind.CommRing.Expr.var x_1).pow k) = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := k } Lean.Grind.CommRing.Mon.unit)
• Lean.Grind.CommRing.Expr.toPolyC.go c (a.pow k) = (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

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} [CommRing α] (ctx : Context α) (p : Power) : denote ctx p = Var.denote ctx p.x ^ p.k

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

theorem Lean.Grind.CommRing.Mon.denote_concat {α : Type u_1} [CommRing α] (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} [CommRing α] (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} [CommRing α] (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.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

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 == 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

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₁ m₁ p₁).combine (Lean.Grind.CommRing.Poly.mulMon k₂ m₂ p₂) == 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

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₁ p₁).combine (Lean.Grind.CommRing.Poly.mulMon k₂ m₂ p₂) == 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

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 p₁ == 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

• ⋯ = ⋯

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 != 0 && Lean.Grind.CommRing.Poly.mulConst k p == 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

• ⋯ = ⋯

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

Equations

• Lean.Grind.CommRing.Stepwise.unsat_eq_cert p k = (k != 0 && p == 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

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 == p₁.combine (Lean.Grind.CommRing.Poly.mulMon 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

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 == (Lean.Grind.CommRing.Poly.mulConst k₁ p₁).combine (Lean.Grind.CommRing.Poly.mulMon 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

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 == p₁ && p₂ == 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

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 != 0 && (lhs.sub rhs).toPoly == p₁ && p₂ == 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

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 == 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

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 == 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

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 == 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

• ⋯ = ⋯

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 != 0 && Lean.Grind.CommRing.Poly.mulConstC k p c == 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

• ⋯ = ⋯

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 == 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

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 != 0 && p == 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

• ⋯ = ⋯

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 == 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

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 == (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

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 == p₁ && p₂ == 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

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 != 0 && (lhs.sub rhs).toPolyC c == p₁ && p₂ == 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