Documentation

Init.Grind.Ring.Poly

source
@[reducible, inline]
abbrev Lean.Grind.CommRing.Var :
Type
Equations
source
inductive Lean.Grind.CommRing.Expr :
Type
Instances For
source
instance Lean.Grind.CommRing.instInhabitedExpr :
Inhabited Expr
Equations
source
instance Lean.Grind.CommRing.instBEqExpr :
BEq Expr
Equations
source
instance Lean.Grind.CommRing.instHashableExpr :
Hashable Expr
Equations
source
instance Lean.Grind.CommRing.instReprExpr :
Repr Expr
Equations
source
@[reducible, inline]
abbrev Lean.Grind.CommRing.Context (α : Type u) :
Type u
Equations
source
def Lean.Grind.CommRing.Var.denote {α : Type u_1} (ctx : Context α) (v : Var) :
α
Equations
source
def Lean.Grind.CommRing.denoteInt {α : Type u_1} [Ring α] (k : Int) :
α
Equations
source
def Lean.Grind.CommRing.Expr.denote {α : Type u_1} [Ring α] (ctx : Context α) :
Expr → α
Equations
source
structure Lean.Grind.CommRing.Power :
Type
Instances For
source
instance Lean.Grind.CommRing.instBEqPower :
BEq Power
Equations
source
instance Lean.Grind.CommRing.instReprPower :
Repr Power
Equations
source
instance Lean.Grind.CommRing.instInhabitedPower :
Inhabited Power
Equations
source
instance Lean.Grind.CommRing.instHashablePower :
Hashable Power
Equations
source
instance Lean.Grind.CommRing.instLawfulBEqPower :
LawfulBEq Power
source
def Lean.Grind.CommRing.Power.varLt (p₁ p₂ : Power) :
Bool
Equations
source
def Lean.Grind.CommRing.Power.denote {α : Type u_1} [Semiring α] (ctx : Context α) :
Power → α
Equations
source
inductive Lean.Grind.CommRing.Mon :
Type
Instances For
source
instance Lean.Grind.CommRing.instBEqMon :
BEq Mon
Equations
source
instance Lean.Grind.CommRing.instReprMon :
Repr Mon
Equations
source
instance Lean.Grind.CommRing.instInhabitedMon :
Inhabited Mon
Equations
source
instance Lean.Grind.CommRing.instHashableMon :
Hashable Mon
Equations
source
instance Lean.Grind.CommRing.instLawfulBEqMon :
LawfulBEq Mon
source
def Lean.Grind.CommRing.Mon.denote {α : Type u_1} [Semiring α] (ctx : Context α) :
Mon → α
Equations
source
def Lean.Grind.CommRing.Mon.denote' {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) :
α
Equations
source
def Lean.Grind.CommRing.Mon.denote'.go {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) (acc : α) :
α
Equations
source
def Lean.Grind.CommRing.Mon.ofVar (x : Var) :
Mon
Equations
source
def Lean.Grind.CommRing.Mon.concat (m₁ m₂ : Mon) :
Mon
Equations
source
def Lean.Grind.CommRing.Mon.mulPow (pw : Power) (m : Mon) :
Mon
Equations
source
def Lean.Grind.CommRing.Mon.length :
Mon → Nat
Equations
source
def Lean.Grind.CommRing.hugeFuel :
Nat
Equations
source
def Lean.Grind.CommRing.Mon.mul (m₁ m₂ : Mon) :
Mon
Equations
source
def Lean.Grind.CommRing.Mon.mul.go (fuel : Nat) (m₁ m₂ : Mon) :
Mon
Equations
source
def Lean.Grind.CommRing.Mon.degree :
Mon → Nat
Equations
source
def Lean.Grind.CommRing.Var.revlex (x y : Var) :
Ordering
Equations
source
def Lean.Grind.CommRing.powerRevlex (k₁ k₂ : Nat) :
Ordering
Equations
source
def Lean.Grind.CommRing.Power.revlex (p₁ p₂ : Power) :
Ordering
Equations
source
@[irreducible]
def Lean.Grind.CommRing.Mon.revlexWF (m₁ m₂ : Mon) :
Ordering
Equations
source
def Lean.Grind.CommRing.Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) :
Ordering
Equations
source
def Lean.Grind.CommRing.Mon.revlex (m₁ m₂ : Mon) :
Ordering
Equations
source
def Lean.Grind.CommRing.Mon.grevlex (m₁ m₂ : Mon) :
Ordering
Equations
source
inductive Lean.Grind.CommRing.Poly :
Type
Instances For
source
instance Lean.Grind.CommRing.instBEqPoly :
BEq Poly
Equations
source
instance Lean.Grind.CommRing.instReprPoly :
Repr Poly
Equations
source
instance Lean.Grind.CommRing.instInhabitedPoly :
Inhabited Poly
Equations
source
instance Lean.Grind.CommRing.instHashablePoly :
Hashable Poly
Equations
source
instance Lean.Grind.CommRing.instLawfulBEqPoly :
LawfulBEq Poly
source
def Lean.Grind.CommRing.Poly.denote {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) :
α
Equations
source
def Lean.Grind.CommRing.Poly.denote' {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) :
α
Equations
source
def Lean.Grind.CommRing.Poly.denote'.denoteTerm {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) :
α
Equations
source
def Lean.Grind.CommRing.Poly.denote'.go {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) (acc : α) :
α
Equations
source
def Lean.Grind.CommRing.Poly.ofMon (m : Mon) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.ofVar (x : Var) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.isSorted :
Poly → Bool
Equations
source
def Lean.Grind.CommRing.Poly.addConst (p : Poly) (k : Int) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.addConst.go (k : Int) :
Poly → Poly
Equations
source
def Lean.Grind.CommRing.Poly.insert (k : Int) (m : Mon) (p : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.insert.go (k : Int) (m : Mon) :
Poly → Poly
Equations
source
def Lean.Grind.CommRing.Poly.concat (p₁ p₂ : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulConst (k : Int) (p : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulConst.go (k : Int) :
Poly → Poly
Equations
source
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.
source
def Lean.Grind.CommRing.Poly.mulMon.go (k : Int) (m : Mon) :
Poly → Poly
Equations
source
def Lean.Grind.CommRing.Poly.combine (p₁ p₂ : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.combine.go (fuel : Nat) (p₁ p₂ : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mul (p₁ p₂ : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mul.go (p₂ p₁ acc : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.pow (p : Poly) (k : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Expr.toPoly :
Expr → Poly
Equations
source
def Lean.Grind.CommRing.Poly.normEq0 (p : Poly) (c : Nat) :
Poly
Equations

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.

source
def Lean.Grind.CommRing.Poly.addConstC (p : Poly) (k : Int) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.insertC (k : Int) (m : Mon) (p : Poly) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.insertC.go (m : Mon) (c : Nat) (k : Int) :
Poly → Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulConstC (k : Int) (p : Poly) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulConstC.go (k : Int) (c : Nat) :
Poly → Poly
Equations
source
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.
source
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.
source
def Lean.Grind.CommRing.Poly.combineC (p₁ p₂ : Poly) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.combineC.go (c fuel : Nat) (p₁ p₂ : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulC (p₁ p₂ : Poly) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.mulC.go (p₂ : Poly) (c : Nat) (p₁ acc : Poly) :
Poly
Equations
source
def Lean.Grind.CommRing.Poly.powC (p : Poly) (k c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Expr.toPolyC (e : Expr) (c : Nat) :
Poly
Equations
source
def Lean.Grind.CommRing.Expr.toPolyC.go (c : Nat) :
Expr → Poly
Equations
source
inductive Lean.Grind.CommRing.NullCert :
Type

A Nullstellensatz certificate.

lhs₁ = rh₁ → ... → lhsₙ = rhₙ → q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ) = 0
Instances For
source
def Lean.Grind.CommRing.NullCert.denote {α : Type u_1} [CommRing α] (ctx : Context α) :
NullCert → α
q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
Equations
source
def Lean.Grind.CommRing.NullCert.eqsImplies {α : Type u_1} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) :
Prop
lhs₁ = rh₁ → ... → lhsₙ = rhₙ → p
Equations
source
def Lean.Grind.CommRing.NullCert.toPoly (nc : NullCert) :
Poly

A polynomial representing

q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
Equations
source
def Lean.Grind.CommRing.NullCert.toPolyC (nc : NullCert) (c : Nat) :
Poly
Equations

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
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
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
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
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
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
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
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
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
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
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
  • ⋯ = ⋯
source
def Lean.Grind.CommRing.Stepwise.div_cert (p₁ : Poly) (k : Int) (p : Poly) :
Bool
Equations
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
  • ⋯ = ⋯
source
def Lean.Grind.CommRing.Stepwise.unsat_eq_cert (p : Poly) (k : Int) :
Bool
Equations
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
  • ⋯ = ⋯
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
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
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
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
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
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
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
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
  • ⋯ = ⋯
source
def Lean.Grind.CommRing.Stepwise.div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) :
Bool
Equations
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
  • ⋯ = ⋯
source
def Lean.Grind.CommRing.Stepwise.simp_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations
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
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
  • ⋯ = ⋯
source
def Lean.Grind.CommRing.Stepwise.d_step1_certC (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations
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
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
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
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
source
def Lean.Grind.CommRing.Mon.denoteAsIntModule.go {α : Type u_1} [CommRing α] (ctx : Context α) (m : Mon) (acc : α) :
α
Equations
source
def Lean.Grind.CommRing.Poly.denoteAsIntModule {α : Type u_1} [CommRing α] (ctx : Context α) (p : Poly) :
α
Equations
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
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
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
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
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
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