Init.Grind.Ring.CommSemiringAdapter

source

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

Expr → α

Equations

Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.num k) = OfNat.ofNat k.natAbs
Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.natCast k) = OfNat.ofNat k
Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.var v) = Lean.Grind.CommRing.Var.denote ctx v
Lean.Grind.CommRing.Expr.denoteS ctx (a.add b) = Lean.Grind.CommRing.Expr.denoteS ctx a + Lean.Grind.CommRing.Expr.denoteS ctx b
Lean.Grind.CommRing.Expr.denoteS ctx (a.mul b) = Lean.Grind.CommRing.Expr.denoteS ctx a * Lean.Grind.CommRing.Expr.denoteS ctx b
Lean.Grind.CommRing.Expr.denoteS ctx (a.pow k) = Lean.Grind.CommRing.Expr.denoteS ctx a ^ k
Lean.Grind.CommRing.Expr.denoteS ctx (a.sub b) = 0
Lean.Grind.CommRing.Expr.denoteS ctx a.neg = 0
Lean.Grind.CommRing.Expr.denoteS ctx (Lean.Grind.CommRing.Expr.intCast k) = 0

Instances For

source

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

Expr → Ring.OfSemiring.Q α

Equations

Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.num k) = OfNat.ofNat k.natAbs
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.natCast k) = OfNat.ofNat k
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.var v) = ↑(Lean.Grind.CommRing.Var.denote ctx v)
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.add b) = Lean.Grind.CommRing.Expr.denoteSAsRing ctx a + Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.mul b) = Lean.Grind.CommRing.Expr.denoteSAsRing ctx a * Lean.Grind.CommRing.Expr.denoteSAsRing ctx b
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.pow k) = Lean.Grind.CommRing.Expr.denoteSAsRing ctx a ^ k
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (a.sub b) = 0
Lean.Grind.CommRing.Expr.denoteSAsRing ctx a.neg = 0
Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.intCast k) = 0

Instances For

source

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

denoteSAsRing ctx e = ↑(denoteS ctx e)

source

def Lean.Grind.CommRing.Expr.toPolyS :

Expr → Poly

Equations

(Lean.Grind.CommRing.Expr.num n).toPolyS = Lean.Grind.CommRing.Poly.num ↑n.natAbs
(Lean.Grind.CommRing.Expr.var x_1).toPolyS = Lean.Grind.CommRing.Poly.ofVar x_1
(a.add b).toPolyS = a.toPolyS.combine b.toPolyS
(a.mul b).toPolyS = a.toPolyS.mul b.toPolyS
((Lean.Grind.CommRing.Expr.num n).pow k).toPolyS = Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k)
((Lean.Grind.CommRing.Expr.var x_1).pow k).toPolyS = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := k } Lean.Grind.CommRing.Mon.unit)
(a.pow k).toPolyS = a.toPolyS.pow k
(Lean.Grind.CommRing.Expr.natCast n).toPolyS = Lean.Grind.CommRing.Poly.num ↑n
(a.sub b).toPolyS = Lean.Grind.CommRing.Poly.num 0
a.neg.toPolyS = Lean.Grind.CommRing.Poly.num 0
(Lean.Grind.CommRing.Expr.intCast k).toPolyS = Lean.Grind.CommRing.Poly.num 0

Instances For

source

def Lean.Grind.CommRing.Expr.toPolyS_nc :

Expr → Poly

Equations

(Lean.Grind.CommRing.Expr.num n).toPolyS_nc = Lean.Grind.CommRing.Poly.num ↑n.natAbs
(Lean.Grind.CommRing.Expr.var x_1).toPolyS_nc = Lean.Grind.CommRing.Poly.ofVar x_1
(a.add b).toPolyS_nc = a.toPolyS_nc.combine b.toPolyS_nc
(a.mul b).toPolyS_nc = a.toPolyS_nc.mul_nc b.toPolyS_nc
((Lean.Grind.CommRing.Expr.num n).pow k).toPolyS_nc = Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k)
((Lean.Grind.CommRing.Expr.var x_1).pow k).toPolyS_nc = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := k } Lean.Grind.CommRing.Mon.unit)
(a.pow k).toPolyS_nc = a.toPolyS_nc.pow_nc k
(Lean.Grind.CommRing.Expr.natCast n).toPolyS_nc = Lean.Grind.CommRing.Poly.num ↑n
(a.sub b).toPolyS_nc = Lean.Grind.CommRing.Poly.num 0
a.neg.toPolyS_nc = Lean.Grind.CommRing.Poly.num 0
(Lean.Grind.CommRing.Expr.intCast k).toPolyS_nc = Lean.Grind.CommRing.Poly.num 0

Instances For

source

inductive Lean.Grind.CommRing.Poly.NonnegCoeffs :

Poly → Prop

num (c : Int) : c ≥ 0 → (Poly.num c).NonnegCoeffs
add (a : Int) (m : Mon) (p : Poly) : a ≥ 0 → p.NonnegCoeffs → (Poly.add a m p).NonnegCoeffs

Instances For

source

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

Equations

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

Instances For

source

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

denoteSInt k = ↑k.toNat

source

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

Equations

Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.num k) = Lean.Grind.CommRing.denoteSInt k
Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.add k m p_2) = Lean.Grind.CommRing.denoteSInt k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denoteS ctx p_2

Instances For

source

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

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

source

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

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

source

theorem Lean.Grind.CommRing.Poly.denoteS_addConst {α : Type u_1} [Semiring α] (ctx : Context α) (p : Poly) (k : Int) :

k ≥ 0 → p.NonnegCoeffs → denoteS ctx (p.addConst k) = denoteS ctx p + ↑k.toNat

source

theorem Lean.Grind.CommRing.Poly.denoteS_insert {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) :

k ≥ 0 → p.NonnegCoeffs → denoteS ctx (insert k m p) = ↑k.toNat * Mon.denote ctx m + denoteS ctx p

source

theorem Lean.Grind.CommRing.Poly.denoteS_concat {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.concat p₂) = denoteS ctx p₁ + denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_mulConst {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (p : Poly) :

k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulConst k p) = ↑k.toNat * denoteS ctx p

source

theorem Lean.Grind.CommRing.Poly.denoteS_combine {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.combine p₂) = denoteS ctx p₁ + denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon {α : Type u_1} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) :

k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulMon k m p) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p

source

theorem Lean.Grind.CommRing.Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} :

k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.insert_Nonneg (k : Int) (m : Mon) (p : Poly) :

k ≥ 0 → p.NonnegCoeffs → (insert k m p).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon_nc_go {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) :

k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mulMon_nc.go k m p acc) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p + denoteS ctx acc

source

theorem Lean.Grind.CommRing.Poly.num_zero_NonnegCoeffs :

(num 0).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon_nc {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) :

k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulMon_nc k m p) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p

source

theorem Lean.Grind.CommRing.Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} :

k ≥ 0 → p.NonnegCoeffs → (mulConst k p).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mulMon_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) :

k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mulMon_nc_go_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) {acc : Poly} :

k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → (mulMon_nc.go k m p acc).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mulMon_nc_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) :

k ≥ 0 → p.NonnegCoeffs → (mulMon_nc k m p).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.concat_NonnegCoeffs {p₁ p₂ : Poly} :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.concat p₂).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.combine_NonnegCoeffs {p₁ p₂ : Poly} :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mul_go_NonnegCoeffs (p₁ p₂ acc : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul.go p₂ p₁ acc).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mul_NonnegCoeffs {p₁ p₂ : Poly} :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul p₂).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mul_nc_go_NonnegCoeffs (p₁ p₂ acc : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul_nc.go p₂ p₁ acc).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.mul_nc_NonnegCoeffs {p₁ p₂ : Poly} :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul_nc p₂).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.pow_NonnegCoeffs {p : Poly} (k : Nat) :

p.NonnegCoeffs → (p.pow k).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.pow_nc_NonnegCoeffs {p : Poly} (k : Nat) :

p.NonnegCoeffs → (p.pow_nc k).NonnegCoeffs

source

theorem Lean.Grind.CommRing.Poly.denoteS_mul_go {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ acc : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mul.go p₂ p₁ acc) = denoteS ctx acc + denoteS ctx p₁ * denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_mul {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.mul p₂) = denoteS ctx p₁ * denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_mul_nc_go {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ acc : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mul_nc.go p₂ p₁ acc) = denoteS ctx acc + denoteS ctx p₁ * denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_mul_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly) :

p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.mul_nc p₂) = denoteS ctx p₁ * denoteS ctx p₂

source

theorem Lean.Grind.CommRing.Poly.denoteS_pow {α : Type u_1} [CommSemiring α] (ctx : Context α) (p : Poly) (k : Nat) :

p.NonnegCoeffs → denoteS ctx (p.pow k) = denoteS ctx p ^ k

source

theorem Lean.Grind.CommRing.Poly.denoteS_pow_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p : Poly) (k : Nat) :

p.NonnegCoeffs → denoteS ctx (p.pow_nc k) = denoteS ctx p ^ k

source

theorem Lean.Grind.CommRing.Expr.toPolyS_NonnegCoeffs {e : Expr} :

e.toPolyS.NonnegCoeffs

source

theorem Lean.Grind.CommRing.Expr.toPolyS_nc_NonnegCoeffs {e : Expr} :

e.toPolyS_nc.NonnegCoeffs

source

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

Poly.denoteS ctx e.toPolyS = denoteS ctx e

source

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

Poly.denoteS ctx e.toPolyS_nc = denoteS ctx e

source

def Lean.Grind.CommRing.eq_normS_cert (lhs rhs : Expr) :

Bool

Equations

Lean.Grind.CommRing.eq_normS_cert lhs rhs = (lhs.toPolyS == rhs.toPolyS)

Instances For

source

theorem Lean.Grind.CommRing.eq_normS {α : Type u_1} [CommSemiring α] (ctx : Context α) (lhs rhs : Expr) :

eq_normS_cert lhs rhs = true → Expr.denoteS ctx lhs = Expr.denoteS ctx rhs

source

def Lean.Grind.CommRing.eq_normS_nc_cert (lhs rhs : Expr) :

Bool

Equations

Lean.Grind.CommRing.eq_normS_nc_cert lhs rhs = (lhs.toPolyS_nc == rhs.toPolyS_nc)

Instances For

source

theorem Lean.Grind.CommRing.eq_normS_nc {α : Type u_1} [Semiring α] (ctx : Context α) (lhs rhs : Expr) :

eq_normS_nc_cert lhs rhs = true → Expr.denoteS ctx lhs = Expr.denoteS ctx rhs

source

theorem Lean.Grind.Ring.OfSemiring.of_eq {α : Type u_1} [Semiring α] (ctx : CommRing.Context α) (lhs rhs : CommRing.Expr) :

CommRing.Expr.denoteS ctx lhs = CommRing.Expr.denoteS ctx rhs → CommRing.Expr.denoteSAsRing ctx lhs = CommRing.Expr.denoteSAsRing ctx rhs

source

theorem Lean.Grind.Ring.OfSemiring.of_diseq {α : Type u_1} [Semiring α] [AddRightCancel α] (ctx : CommRing.Context α) (lhs rhs : CommRing.Expr) :

CommRing.Expr.denoteS ctx lhs ≠ CommRing.Expr.denoteS ctx rhs → CommRing.Expr.denoteSAsRing ctx lhs ≠ CommRing.Expr.denoteSAsRing ctx rhs