@[reducible, inline]
Equations
Instances For
Equations
Instances For
Equations
Instances For
@[irreducible]
Equations
Instances For
Equations
Instances For
Equations
Instances For
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.
Equations
Instances For
A polynomial representing
q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
Equations
Instances For
Equations
Instances For
Theorems for justifying the procedure for commutative rings in grind
.
theorem
Lean.Grind.CommRing.Mon.denote_ofVar
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(x : Var)
:
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.Poly.denote_ofMon
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(m : Mon)
:
theorem
Lean.Grind.CommRing.Poly.denote_ofVar
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(x : Var)
:
theorem
Lean.Grind.CommRing.Expr.denote_toPoly
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(e : Expr)
:
theorem
Lean.Grind.CommRing.NullCert.denote_toPoly
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(nc : NullCert)
:
Equations
Instances For
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
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
Equations
Instances For
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.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
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
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
Equations
Instances For
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
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
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
{α : 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
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
Equations
Instances For
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
theorem
Lean.Grind.CommRing.Stepwise.d_init
{α : Type u_1}
[CommRing α]
(ctx : Context α)
(p : Poly)
:
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
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
Equations
Instances For
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
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
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
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.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
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_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
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
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
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
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