Data-structures, definitions and theorems for implementing the `grind` solver and normalizer for commutative rings and its extensions (e.g., fields, commutative semirings, etc.)

The solver uses proof-by-reflection.

source
@[reducible, inline]
abbrev Lean.Grind.CommRing.Var :
Type
Equations

- Lean.Grind.CommRing.Var = Nat

Instances For

source
inductive Lean.Grind.CommRing.Expr :
Type

- num (k : Int) : Expr
- natCast (k : Nat) : Expr
- intCast (k : Int) : Expr
- var (i : Var) : Expr
- neg (a : Expr) : Expr
- add (a b : Expr) : Expr
- sub (a b : Expr) : Expr
- mul (a b : Expr) : Expr
- pow (a : Expr) (k : Nat) : Expr

Instances For

source
def Lean.Grind.CommRing.instInhabitedExpr.default :
Expr
Equations

- Lean.Grind.CommRing.instInhabitedExpr.default = Lean.Grind.CommRing.Expr.num default

Instances For

source
instance Lean.Grind.CommRing.instInhabitedExpr :
Inhabited Expr
Equations

- Lean.Grind.CommRing.instInhabitedExpr = { default := Lean.Grind.CommRing.instInhabitedExpr.default }

source
instance Lean.Grind.CommRing.instBEqExpr :
BEq Expr
Equations

- Lean.Grind.CommRing.instBEqExpr = { beq := Lean.Grind.CommRing.instBEqExpr.beq }

source
def Lean.Grind.CommRing.instBEqExpr.beq :
Expr → Expr → Bool
Equations

- Lean.Grind.CommRing.instBEqExpr.beq (Lean.Grind.CommRing.Expr.num a) (Lean.Grind.CommRing.Expr.num b) = (a == b)
- Lean.Grind.CommRing.instBEqExpr.beq (Lean.Grind.CommRing.Expr.natCast a) (Lean.Grind.CommRing.Expr.natCast b) = (a == b)
- Lean.Grind.CommRing.instBEqExpr.beq (Lean.Grind.CommRing.Expr.intCast a) (Lean.Grind.CommRing.Expr.intCast b) = (a == b)
- Lean.Grind.CommRing.instBEqExpr.beq (Lean.Grind.CommRing.Expr.var a) (Lean.Grind.CommRing.Expr.var b) = (a == b)
- Lean.Grind.CommRing.instBEqExpr.beq a.neg b.neg = Lean.Grind.CommRing.instBEqExpr.beq a b
- Lean.Grind.CommRing.instBEqExpr.beq (a.add a_1) (b.add b_1) = (Lean.Grind.CommRing.instBEqExpr.beq a b && Lean.Grind.CommRing.instBEqExpr.beq a_1 b_1)
- Lean.Grind.CommRing.instBEqExpr.beq (a.sub a_1) (b.sub b_1) = (Lean.Grind.CommRing.instBEqExpr.beq a b && Lean.Grind.CommRing.instBEqExpr.beq a_1 b_1)
- Lean.Grind.CommRing.instBEqExpr.beq (a.mul a_1) (b.mul b_1) = (Lean.Grind.CommRing.instBEqExpr.beq a b && Lean.Grind.CommRing.instBEqExpr.beq a_1 b_1)
- Lean.Grind.CommRing.instBEqExpr.beq (a.pow a_1) (b.pow b_1) = (Lean.Grind.CommRing.instBEqExpr.beq a b && a_1 == b_1)
- Lean.Grind.CommRing.instBEqExpr.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Grind.CommRing.instHashableExpr :
Hashable Expr
Equations

- Lean.Grind.CommRing.instHashableExpr = { hash := Lean.Grind.CommRing.instHashableExpr.hash }

source
def Lean.Grind.CommRing.instHashableExpr.hash :
Expr → UInt64
Equations

- Lean.Grind.CommRing.instHashableExpr.hash (Lean.Grind.CommRing.Expr.num a) = mixHash 0 (hash a)
- Lean.Grind.CommRing.instHashableExpr.hash (Lean.Grind.CommRing.Expr.natCast a) = mixHash 1 (hash a)
- Lean.Grind.CommRing.instHashableExpr.hash (Lean.Grind.CommRing.Expr.intCast a) = mixHash 2 (hash a)
- Lean.Grind.CommRing.instHashableExpr.hash (Lean.Grind.CommRing.Expr.var a) = mixHash 3 (hash a)
- Lean.Grind.CommRing.instHashableExpr.hash a.neg = mixHash 4 (Lean.Grind.CommRing.instHashableExpr.hash a)
- Lean.Grind.CommRing.instHashableExpr.hash (a.add a_1) = mixHash (mixHash 5 (Lean.Grind.CommRing.instHashableExpr.hash a)) (Lean.Grind.CommRing.instHashableExpr.hash a_1)
- Lean.Grind.CommRing.instHashableExpr.hash (a.sub a_1) = mixHash (mixHash 6 (Lean.Grind.CommRing.instHashableExpr.hash a)) (Lean.Grind.CommRing.instHashableExpr.hash a_1)
- Lean.Grind.CommRing.instHashableExpr.hash (a.mul a_1) = mixHash (mixHash 7 (Lean.Grind.CommRing.instHashableExpr.hash a)) (Lean.Grind.CommRing.instHashableExpr.hash a_1)
- Lean.Grind.CommRing.instHashableExpr.hash (a.pow a_1) = mixHash (mixHash 8 (Lean.Grind.CommRing.instHashableExpr.hash a)) (hash a_1)

Instances For

source
instance Lean.Grind.CommRing.instReprExpr :
Repr Expr
Equations

- Lean.Grind.CommRing.instReprExpr = { reprPrec := Lean.Grind.CommRing.instReprExpr.repr }

source
def Lean.Grind.CommRing.instReprExpr.repr :
Expr → Nat → Std.Format
Equations

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

Instances For

source
@[reducible, inline]
abbrev Lean.Grind.CommRing.Context (α : Type u) :
Type u
Equations

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

source
structure Lean.Grind.CommRing.Power :
Type

- x : Var
- k : Nat

Instances For

source
instance Lean.Grind.CommRing.instBEqPower :
BEq Power
Equations

- Lean.Grind.CommRing.instBEqPower = { beq := Lean.Grind.CommRing.instBEqPower.beq }

source
def Lean.Grind.CommRing.instBEqPower.beq :
Power → Power → Bool
Equations

- Lean.Grind.CommRing.instBEqPower.beq { x := a, k := a_1 } { x := b, k := b_1 } = (a == b && a_1 == b_1)
- Lean.Grind.CommRing.instBEqPower.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Grind.CommRing.instReflBEqPower :
ReflBEq Power
source
instance Lean.Grind.CommRing.instLawfulBEqPower :
LawfulBEq Power
source
def Lean.Grind.CommRing.instReprPower.repr :
Power → Nat → Std.Format
Equations

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

Instances For

source
instance Lean.Grind.CommRing.instReprPower :
Repr Power
Equations

- Lean.Grind.CommRing.instReprPower = { reprPrec := Lean.Grind.CommRing.instReprPower.repr }

source
def Lean.Grind.CommRing.instInhabitedPower.default :
Power
Equations

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

Instances For

source
instance Lean.Grind.CommRing.instInhabitedPower :
Inhabited Power
Equations

- Lean.Grind.CommRing.instInhabitedPower = { default := Lean.Grind.CommRing.instInhabitedPower.default }

source
instance Lean.Grind.CommRing.instHashablePower :
Hashable Power
Equations

- Lean.Grind.CommRing.instHashablePower = { hash := Lean.Grind.CommRing.instHashablePower.hash }

source
def Lean.Grind.CommRing.instHashablePower.hash :
Power → UInt64
Equations

- Lean.Grind.CommRing.instHashablePower.hash { x := a, k := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Power.beq'_eq (pw₁ pw₂ : Power) :
(pw₁.beq' pw₂ = true) = (pw₁ = pw₂)
source
def Lean.Grind.CommRing.Power.varLt (p₁ p₂ : Power) :
Bool
Equations

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

Instances For

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

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

Instances For

source
inductive Lean.Grind.CommRing.Mon :
Type

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

Instances For

source
instance Lean.Grind.CommRing.instBEqMon :
BEq Mon
Equations

- Lean.Grind.CommRing.instBEqMon = { beq := Lean.Grind.CommRing.instBEqMon.beq }

source
def Lean.Grind.CommRing.instBEqMon.beq :
Mon → Mon → Bool
Equations

- Lean.Grind.CommRing.instBEqMon.beq Lean.Grind.CommRing.Mon.unit Lean.Grind.CommRing.Mon.unit = true
- Lean.Grind.CommRing.instBEqMon.beq (Lean.Grind.CommRing.Mon.mult a a_1) (Lean.Grind.CommRing.Mon.mult b b_1) = (a == b && Lean.Grind.CommRing.instBEqMon.beq a_1 b_1)
- Lean.Grind.CommRing.instBEqMon.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Grind.CommRing.instReflBEqMon :
ReflBEq Mon
source
instance Lean.Grind.CommRing.instLawfulBEqMon :
LawfulBEq Mon
source
def Lean.Grind.CommRing.instReprMon.repr :
Mon → Nat → Std.Format
Equations

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

Instances For

source
instance Lean.Grind.CommRing.instReprMon :
Repr Mon
Equations

- Lean.Grind.CommRing.instReprMon = { reprPrec := Lean.Grind.CommRing.instReprMon.repr }

source
instance Lean.Grind.CommRing.instInhabitedMon :
Inhabited Mon
Equations

- Lean.Grind.CommRing.instInhabitedMon = { default := Lean.Grind.CommRing.instInhabitedMon.default }

source
def Lean.Grind.CommRing.instInhabitedMon.default :
Mon
Equations

- Lean.Grind.CommRing.instInhabitedMon.default = Lean.Grind.CommRing.Mon.unit

Instances For

source
instance Lean.Grind.CommRing.instHashableMon :
Hashable Mon
Equations

- Lean.Grind.CommRing.instHashableMon = { hash := Lean.Grind.CommRing.instHashableMon.hash }

source
def Lean.Grind.CommRing.instHashableMon.hash :
Mon → UInt64
Equations

- Lean.Grind.CommRing.instHashableMon.hash Lean.Grind.CommRing.Mon.unit = 0
- Lean.Grind.CommRing.instHashableMon.hash (Lean.Grind.CommRing.Mon.mult a a_1) = mixHash (mixHash 1 (hash a)) (Lean.Grind.CommRing.instHashableMon.hash a_1)

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Mon.beq'_eq (m₁ m₂ : Mon) :
(m₁.beq' m₂ = true) = (m₁ = m₂)
source
def Lean.Grind.CommRing.Mon.denote {α : Type u_1} [Semiring α] (ctx : Context α) :
Mon → α
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

source
def Lean.Grind.CommRing.Mon.mulPow_nc (pw : Power) (m : Mon) :
Mon
Equations

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

Instances For

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

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

Instances For

source
def Lean.Grind.CommRing.hugeFuel :
Nat
Equations

- Lean.Grind.CommRing.hugeFuel = 1000000

Instances For

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

Instances For

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

Instances For

source
def Lean.Grind.CommRing.Mon.mul_nc (m₁ m₂ : Mon) :
Mon
Equations

- Lean.Grind.CommRing.Mon.unit.mul_nc m₂ = m₂
- (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit).mul_nc m₂ = Lean.Grind.CommRing.Mon.mulPow_nc pw m₂
- (Lean.Grind.CommRing.Mon.mult pw m₁_2).mul_nc m₂ = Lean.Grind.CommRing.Mon.mult pw (m₁_2.mul_nc m₂)

Instances For

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

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

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

source
theorem Lean.Grind.CommRing.powerRevlex_k_eq_powerRevlex (k₁ k₂ : Nat) :
powerRevlex_k k₁ k₂ = powerRevlex k₁ k₂
source
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)

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
theorem Lean.Grind.CommRing.Mon.revlex_k_eq_revlex (m₁ m₂ : Mon) :
m₁.revlex_k m₂ = m₁.revlex m₂
source
theorem Lean.Grind.CommRing.Mon.grevlex_k_eq_grevlex (m₁ m₂ : Mon) :
m₁.grevlex_k m₂ = m₁.grevlex m₂
source
inductive Lean.Grind.CommRing.Poly :
Type

- num (k : Int) : Poly
- add (k : Int) (v : Mon) (p : Poly) : Poly

Instances For

source
def Lean.Grind.CommRing.instBEqPoly.beq :
Poly → Poly → Bool
Equations

- Lean.Grind.CommRing.instBEqPoly.beq (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b) = (a == b)
- Lean.Grind.CommRing.instBEqPoly.beq (Lean.Grind.CommRing.Poly.add a a_1 a_2) (Lean.Grind.CommRing.Poly.add b b_1 b_2) = (a == b && (a_1 == b_1 && Lean.Grind.CommRing.instBEqPoly.beq a_2 b_2))
- Lean.Grind.CommRing.instBEqPoly.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Grind.CommRing.instBEqPoly :
BEq Poly
Equations

- Lean.Grind.CommRing.instBEqPoly = { beq := Lean.Grind.CommRing.instBEqPoly.beq }

source
instance Lean.Grind.CommRing.instReflBEqPoly :
ReflBEq Poly
source
instance Lean.Grind.CommRing.instLawfulBEqPoly :
LawfulBEq Poly
source
instance Lean.Grind.CommRing.instReprPoly :
Repr Poly
Equations

- Lean.Grind.CommRing.instReprPoly = { reprPrec := Lean.Grind.CommRing.instReprPoly.repr }

source
def Lean.Grind.CommRing.instReprPoly.repr :
Poly → Nat → Std.Format
Equations

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

Instances For

source
def Lean.Grind.CommRing.instInhabitedPoly.default :
Poly
Equations

- Lean.Grind.CommRing.instInhabitedPoly.default = Lean.Grind.CommRing.Poly.num default

Instances For

source
instance Lean.Grind.CommRing.instInhabitedPoly :
Inhabited Poly
Equations

- Lean.Grind.CommRing.instInhabitedPoly = { default := Lean.Grind.CommRing.instInhabitedPoly.default }

source
instance Lean.Grind.CommRing.instHashablePoly :
Hashable Poly
Equations

- Lean.Grind.CommRing.instHashablePoly = { hash := Lean.Grind.CommRing.instHashablePoly.hash }

source
def Lean.Grind.CommRing.instHashablePoly.hash :
Poly → UInt64
Equations

- Lean.Grind.CommRing.instHashablePoly.hash (Lean.Grind.CommRing.Poly.num a) = mixHash 0 (hash a)
- Lean.Grind.CommRing.instHashablePoly.hash (Lean.Grind.CommRing.Poly.add a a_1 a_2) = mixHash (mixHash (mixHash 1 (hash a)) (hash a_1)) (Lean.Grind.CommRing.instHashablePoly.hash a_2)

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Poly.beq'_eq (p₁ p₂ : Poly) :
(p₁.beq' p₂ = true) = (p₁ = p₂)
source
def Lean.Grind.CommRing.Poly.denote {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) :
α
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

source
theorem Lean.Grind.CommRing.Poly.addConst_k_eq_addConst (p : Poly) (k : Int) :
p.addConst_k k = p.addConst k
source
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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Poly.mulConst_k_eq_mulConst (k : Int) (p : Poly) :
mulConst_k k p = mulConst k p
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.

Instances For

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

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

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Poly.mulMon_k_eq_mulMon (k : Int) (m : Mon) (p : Poly) :
mulMon_k k m p = mulMon k m p
source
def Lean.Grind.CommRing.Poly.mulMon_nc (k : Int) (m : Mon) (p : Poly) :
Poly
Equations

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

Instances For

source
def Lean.Grind.CommRing.Poly.mulMon_nc.go (k : Int) (m : Mon) (p acc : Poly) :
Poly
Equations

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

Instances For

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

Instances For

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

Instances For

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

A `Poly.combine` optimized for the kernel.

Equations

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Poly.combine_k_eq_combine (p₁ p₂ : Poly) :
p₁.combine_k p₂ = p₁.combine p₂
source
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)

Instances For

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

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

Instances For

source
def Lean.Grind.CommRing.Poly.mul_nc (p₁ p₂ : Poly) :
Poly
Equations

- p₁.mul_nc p₂ = Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ (Lean.Grind.CommRing.Poly.num 0)

Instances For

source
def Lean.Grind.CommRing.Poly.mul_nc.go (p₂ p₁ acc : Poly) :
Poly
Equations

- Lean.Grind.CommRing.Poly.mul_nc.go p₂ (Lean.Grind.CommRing.Poly.num k) acc = acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂)
- Lean.Grind.CommRing.Poly.mul_nc.go p₂ (Lean.Grind.CommRing.Poly.add k m p_1) acc = Lean.Grind.CommRing.Poly.mul_nc.go p₂ p_1 (acc.combine (Lean.Grind.CommRing.Poly.mulMon_nc k m p₂))

Instances For

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

Instances For

source
def Lean.Grind.CommRing.Poly.pow_nc (p : Poly) (k : Nat) :
Poly
Equations

- p.pow_nc 0 = Lean.Grind.CommRing.Poly.num 1
- p.pow_nc 1 = p
- p.pow_nc k_2.succ = (p.pow_nc k_2).mul_nc p

Instances For

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

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

Instances For

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

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

Instances For

source
@[simp]
theorem Lean.Grind.CommRing.Expr.toPoly_k_eq_toPoly (e : Expr) :
e.toPoly_k = e.toPoly
source
def Lean.Grind.CommRing.Expr.toPoly_nc :
Expr → Poly
Equations

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

Instances For

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

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

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.

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

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

Instances For

source
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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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.

Instances For

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.

Instances For

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

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

Instances For

source
def Lean.Grind.CommRing.Poly.mulMonC_nc.go (k : Int) (m : Mon) (c : Nat) (p acc : Poly) :
Poly
Equations

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

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

Instances For

source
def Lean.Grind.CommRing.Poly.mulC_nc (p₁ p₂ : Poly) (c : Nat) :
Poly
Equations

- p₁.mulC_nc p₂ c = Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ (Lean.Grind.CommRing.Poly.num 0)

Instances For

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

- Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c (Lean.Grind.CommRing.Poly.num k) acc = acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c
- Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c (Lean.Grind.CommRing.Poly.add k m p_1) acc = Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p_1 (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC_nc k m p₂ c) c)

Instances For

source
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

Instances For

source
def Lean.Grind.CommRing.Poly.powC_nc (p : Poly) (k c : Nat) :
Poly
Equations

- p.powC_nc 0 c = Lean.Grind.CommRing.Poly.num 1
- p.powC_nc 1 c = p
- p.powC_nc k_2.succ c = (p.powC_nc k_2 c).mulC_nc p c

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Grind.CommRing.Expr.toPolyC_nc (e : Expr) (c : Nat) :
Poly
Equations

- e.toPolyC_nc c = Lean.Grind.CommRing.Expr.toPolyC_nc.go c e

Instances For

source
def Lean.Grind.CommRing.Expr.toPolyC_nc.go (c : Nat) :
Expr → Poly
Equations

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

Instances For

Theorems for justifying the procedure for commutative rings in `grind`.

source
theorem Lean.Grind.CommRing.denoteInt_eq {α : Type u_1} [Ring α] (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_mulPow_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p : Power) (m : Mon) :
denote ctx (mulPow_nc 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.Mon.denote_mul_nc {α : Type u_1} [Semiring α] (ctx : Context α) (m₁ m₂ : Mon) :
denote ctx (m₁.mul_nc 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} [Ring α] (ctx : Context α) (m : Mon) :
denote ctx (ofMon m) = Mon.denote ctx m
source
theorem Lean.Grind.CommRing.Poly.denote_ofVar {α : Type u_1} [Ring α] (ctx : Context α) (x : Var) :
denote ctx (ofVar x) = Var.denote ctx x
source
theorem Lean.Grind.CommRing.Poly.denote_addConst {α : Type u_1} [Ring α] (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} [Ring α] (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} [Ring α] (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} [Ring α] (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_mulMon_nc_go {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) :
denote ctx (mulMon_nc.go k m p acc) = ↑k * Mon.denote ctx m * denote ctx p + denote ctx acc
source
theorem Lean.Grind.CommRing.Poly.denote_mulMon_nc {α : Type u_1} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) :
denote ctx (mulMon_nc k m p) = ↑k * Mon.denote ctx m * denote ctx p
source
theorem Lean.Grind.CommRing.Poly.denote_combine {α : Type u_1} [Ring α] (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_mul_nc_go {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ acc : Poly) :
denote ctx (mul_nc.go p₂ p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂
source
theorem Lean.Grind.CommRing.Poly.denote_mul_nc {α : Type u_1} [Ring α] (ctx : Context α) (p₁ p₂ : Poly) :
denote ctx (p₁.mul_nc 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.Poly.denote_pow_nc {α : Type u_1} [Ring α] (ctx : Context α) (p : Poly) (k : Nat) :
denote ctx (p.pow_nc 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.denote_toPoly_nc {α : Type u_1} [Ring α] (ctx : Context α) (e : Expr) :
Poly.denote ctx e.toPoly_nc = 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.Expr.eq_of_toPoly_nc_eq {α : Type u_1} [Ring α] (ctx : Context α) (a b : Expr) (h : (a.toPoly_nc == b.toPoly_nc) = true) :
denote ctx a = denote ctx b

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} [Ring α] [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} [Ring α] [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} [Ring α] [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_mulMonC_nc_go {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) :
denote ctx (mulMonC_nc.go k m c p acc) = ↑k * Mon.denote ctx m * denote ctx p + denote ctx acc
source
theorem Lean.Grind.CommRing.Poly.denote_mulMonC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) :
denote ctx (mulMonC_nc 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} [Ring α] [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_mulC_nc_go {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly) :
denote ctx (mulC_nc.go p₂ c p₁ acc) = denote ctx acc + denote ctx p₁ * denote ctx p₂
source
theorem Lean.Grind.CommRing.Poly.denote_mulC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly) :
denote ctx (p₁.mulC_nc 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.Poly.denote_powC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat) :
denote ctx (p.powC_nc 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.denote_toPolyC_nc {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (e : Expr) :
Poly.denote ctx (e.toPolyC_nc 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.Expr.eq_of_toPolyC_nc_eq {α : Type u_1} {c : Nat} [Ring α] [IsCharP α c] (ctx : Context α) (a b : Expr) (h : (a.toPolyC_nc c == b.toPolyC_nc c) = true) :
denote ctx a = denote ctx b

Theorems for stepwise proof-term construction

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

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.superpose_cert (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.simp_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.mul_cert (p₁ : Poly) (k : Int) (p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.div_cert (p₁ : Poly) (k : Int) (p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.unsat_eq_cert (p : Poly) (k : Int) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.d_step1_cert (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.d_stepk_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.imp_1eq_cert (lhs rhs : Expr) (p₁ p₂ : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.imp_keq_cert (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.core_certC (lhs rhs : Expr) (p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.superpose_certC (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.mul_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.simp_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.unsat_eq_certC (p : Poly) (k : Int) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.d_step1_certC (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.d_stepk_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ p : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.imp_1eq_certC (lhs rhs : Expr) (p₁ p₂ : Poly) (c : Nat) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.Stepwise.imp_keq_certC (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) (c : Nat) :
Bool
Equations

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

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

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

Instances For

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

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

Instances For

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

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

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 α] [LE α] [LT α] [Std.IsPreorder α] [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 α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [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 α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [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 α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] [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 α] [LE α] [LT α] [Std.IsPreorder α] [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 α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [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
noncomputable def Lean.Grind.CommRing.one_eq_zero_unsat_cert (p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) :
Bool
Equations

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

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

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

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
noncomputable def Lean.Grind.CommRing.d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) :
Bool
Equations

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

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
noncomputable def Lean.Grind.CommRing.norm_int_cert (e : Expr) (p : Poly) :
Bool
Equations

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

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

Helper theorems for normalizing ring constraints in the `grind order` module.

source
noncomputable def Lean.Grind.CommRing.norm_cnstr_cert (lhs rhs lhs' rhs' : Expr) :
Bool
Equations

- Lean.Grind.CommRing.norm_cnstr_cert lhs rhs lhs' rhs' = (rhs.sub lhs).toPoly_k.beq' (rhs'.sub lhs').toPoly_k

Instances For

source
theorem Lean.Grind.CommRing.le_norm_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_cnstr_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')
source
theorem Lean.Grind.CommRing.lt_norm_expr {α : Type u_1} [CommRing α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_cnstr_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')
source
noncomputable def Lean.Grind.CommRing.norm_eq_cert (lhs rhs lhs' rhs' : Expr) :
Bool
Equations

- Lean.Grind.CommRing.norm_eq_cert lhs rhs lhs' rhs' = (lhs.sub rhs).toPoly_k.beq' (lhs'.sub rhs').toPoly_k

Instances For

source
theorem Lean.Grind.CommRing.eq_norm_expr {α : Type u_1} [CommRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_eq_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')
source
noncomputable def Lean.Grind.CommRing.norm_cnstr_nc_cert (lhs rhs lhs' rhs' : Expr) :
Bool
Equations

- Lean.Grind.CommRing.norm_cnstr_nc_cert lhs rhs lhs' rhs' = (rhs.sub lhs).toPoly_nc.beq' (rhs'.sub lhs').toPoly_nc

Instances For

source
theorem Lean.Grind.CommRing.le_norm_expr_nc {α : Type u_1} [Ring α] [LE α] [LT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_cnstr_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs ≤ Expr.denote ctx rhs) = (Expr.denote ctx lhs' ≤ Expr.denote ctx rhs')
source
theorem Lean.Grind.CommRing.lt_norm_expr_nc {α : Type u_1} [Ring α] [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_cnstr_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs < Expr.denote ctx rhs) = (Expr.denote ctx lhs' < Expr.denote ctx rhs')
source
noncomputable def Lean.Grind.CommRing.norm_eq_nc_cert (lhs rhs lhs' rhs' : Expr) :
Bool
Equations

- Lean.Grind.CommRing.norm_eq_nc_cert lhs rhs lhs' rhs' = (lhs.sub rhs).toPoly_nc.beq' (lhs'.sub rhs').toPoly_nc

Instances For

source
theorem Lean.Grind.CommRing.eq_norm_expr_nc {α : Type u_1} [Ring α] (ctx : Context α) (lhs rhs lhs' rhs' : Expr) :
norm_eq_nc_cert lhs rhs lhs' rhs' = true → (Expr.denote ctx lhs = Expr.denote ctx rhs) = (Expr.denote ctx lhs' = Expr.denote ctx rhs')

Helper theorems for quick normalization

source
theorem Lean.Grind.CommRing.le_norm0 {α : Type u_1} [Ring α] [LE α] (lhs rhs : α) :
(lhs ≤ rhs) = (lhs ≤ rhs + ↑0)
source
theorem Lean.Grind.CommRing.lt_norm0 {α : Type u_1} [Ring α] [LT α] (lhs rhs : α) :
(lhs < rhs) = (lhs < rhs + ↑0)
source
theorem Lean.Grind.CommRing.eq_norm0 {α : Type u_1} [Ring α] (lhs rhs : α) :
(lhs = rhs) = (lhs = rhs + ↑0)