Init.Grind.Ring.Poly

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.

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly → Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly → Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly → Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Poly

Equations

Instances For

source

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

Expr → Poly

Equations

Instances For

source

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

Instances For

source

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

NullCert → α

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

Equations

Instances For

source

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

Prop

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

Equations

Instances For

source

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

Poly

A polynomial representing

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

Equations

Instances For

source

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

Poly

Equations

Instances For

Theorems for justifying the procedure for commutative rings in grind.

source

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

denoteInt k = ↑k

source

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

source

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

denote' ctx m = denote ctx m

source

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

denote ctx (ofVar x) = Var.denote ctx x

source

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₂

source

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

source

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₂

source

theorem Lean.Grind.CommRing.Var.eq_of_revlex {x₁ x₂ : Var} :

x₁.revlex x₂ = Ordering.eq → x₁ = x₂

source

theorem Lean.Grind.CommRing.eq_of_powerRevlex {k₁ k₂ : Nat} :

powerRevlex k₁ k₂ = Ordering.eq → k₁ = k₂

source

theorem Lean.Grind.CommRing.Power.eq_of_revlex (p₁ p₂ : Power) :

p₁.revlex p₂ = Ordering.eq → p₁ = p₂

source

theorem Lean.Grind.CommRing.Mon.eq_of_revlexWF {m₁ m₂ : Mon} :

m₁.revlexWF m₂ = Ordering.eq → m₁ = m₂

source

theorem Lean.Grind.CommRing.Mon.eq_of_revlexFuel {fuel : Nat} {m₁ m₂ : Mon} :

revlexFuel fuel m₁ m₂ = Ordering.eq → m₁ = m₂

source

theorem Lean.Grind.CommRing.Mon.eq_of_revlex {m₁ m₂ : Mon} :

m₁.revlex m₂ = Ordering.eq → m₁ = m₂

source

theorem Lean.Grind.CommRing.Mon.eq_of_grevlex {m₁ m₂ : Mon} :

m₁.grevlex m₂ = Ordering.eq → m₁ = m₂

source

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

source

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

denote' ctx p = denote ctx p

source

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

denote ctx (ofMon m) = Mon.denote ctx m

source

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

denote ctx (ofVar x) = Var.denote ctx x

source

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

source

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

source

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₂

source

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

source

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

source

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₂

source

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₂

source

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₂

source

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

source

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

Poly.denote ctx e.toPoly = denote ctx e

source

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

source

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.

source

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

Poly.denote ctx nc.toPoly = denote ctx nc

source

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

Bool

Equations

Instances For

source

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)

source

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

source

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

source

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

Bool

Equations

Instances For

source

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)

source

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

source

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

Bool

Equations

Instances For

source

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.

source

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

source

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

source

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

source

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

source

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₂

source

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₂

source

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₂

source

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

source

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

source

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

source

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

source

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

Bool

Equations

Instances For

source

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)

source

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

source

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

Bool

Equations

Instances For

source

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)

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

↑1 * Poly.denote ctx p = Poly.denote ctx p

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

Instances For

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Equations

Instances For

source

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

Equations

Instances For

source

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

Equations

Instances For

source

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

source

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

denoteAsIntModule ctx m = denote ctx m

source

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

denoteAsIntModule ctx p = denote ctx p

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem Lean.Grind.CommRing.inv_int_eq {α : Type u_1} [Field α] [IsCharP α 0] (b : Int) :

(b != 0) = true → denoteInt b * (denoteInt b)⁻¹ = 1

source

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

source

theorem Lean.Grind.CommRing.inv_zero_eqC {α : Type u_1} {c : Nat} [Field α] [IsCharP α c] (b : Int) :

(b % ↑c == 0) = true → (denoteInt b)⁻¹ = 0

source

theorem Lean.Grind.CommRing.inv_split {α : Type u_1} [Field α] (a : α) :

if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1

source

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

Bool

Equations

Instances For

source

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

source

theorem Lean.Grind.CommRing.diseq_to_eq {α : Type u_1} [Field α] (a b : α) :

a ≠ b → (a - b) * (a - b)⁻¹ = 1

source

theorem Lean.Grind.CommRing.diseq0_to_eq {α : Type u_1} [Field α] (a : α) :

a ≠ 0 → a * a⁻¹ = 1

normEq0 helper theorems

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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

source

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

Bool

Equations

Instances For

source

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