Helper definitions and theorems for converting Semiring expressions into Ring ones. We use them to implement grind

@[reducible, inline]

abbrev Lean.Grind.Ring.OfSemiring.Var : Type

Equations

• Lean.Grind.Ring.OfSemiring.Var = Nat

inductive Lean.Grind.Ring.OfSemiring.Expr : Type

• num (v : Nat) : Expr
• var (i : Var) : Expr
• add (a b : Expr) : Expr
• mul (a b : Expr) : Expr
• pow (a : Expr) (k : Nat) : Expr

instance Lean.Grind.Ring.OfSemiring.instInhabitedExpr : Inhabited Expr

Equations

• Lean.Grind.Ring.OfSemiring.instInhabitedExpr = { default := Lean.Grind.Ring.OfSemiring.Expr.num default }

instance Lean.Grind.Ring.OfSemiring.instBEqExpr : BEq Expr

Equations

• Lean.Grind.Ring.OfSemiring.instBEqExpr = { beq := Lean.Grind.Ring.OfSemiring.beqExpr✝ }

instance Lean.Grind.Ring.OfSemiring.instHashableExpr : Hashable Expr

Equations

• Lean.Grind.Ring.OfSemiring.instHashableExpr = { hash := Lean.Grind.Ring.OfSemiring.hashExpr✝ }

@[reducible, inline]

abbrev Lean.Grind.Ring.OfSemiring.Context (α : Type u) : Type u

Equations

• Lean.Grind.Ring.OfSemiring.Context α = Lean.RArray α

def Lean.Grind.Ring.OfSemiring.Var.denote {α : Type u_1} (ctx : Context α) (v : Var) : α

Equations

• Lean.Grind.Ring.OfSemiring.Var.denote ctx v = Lean.RArray.get ctx v

def Lean.Grind.Ring.OfSemiring.Expr.denote {α : Type u_1} [Semiring α] (ctx : Context α) : Expr → α

Equations

• Lean.Grind.Ring.OfSemiring.Expr.denote ctx (Lean.Grind.Ring.OfSemiring.Expr.num a) = OfNat.ofNat a
• Lean.Grind.Ring.OfSemiring.Expr.denote ctx (Lean.Grind.Ring.OfSemiring.Expr.var a) = Lean.Grind.Ring.OfSemiring.Var.denote ctx a
• Lean.Grind.Ring.OfSemiring.Expr.denote ctx (a.add a_1) = Lean.Grind.Ring.OfSemiring.Expr.denote ctx a + Lean.Grind.Ring.OfSemiring.Expr.denote ctx a_1
• Lean.Grind.Ring.OfSemiring.Expr.denote ctx (a.mul a_1) = Lean.Grind.Ring.OfSemiring.Expr.denote ctx a * Lean.Grind.Ring.OfSemiring.Expr.denote ctx a_1
• Lean.Grind.Ring.OfSemiring.Expr.denote ctx (a.pow a_1) = Lean.Grind.Ring.OfSemiring.Expr.denote ctx a ^ a_1

def Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing {α : Type u_1} [Semiring α] (ctx : Context α) : Expr → Q α

Equations

• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx (Lean.Grind.Ring.OfSemiring.Expr.num a) = OfNat.ofNat a
• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx (Lean.Grind.Ring.OfSemiring.Expr.var a) = ↑(Lean.Grind.Ring.OfSemiring.Var.denote ctx a)
• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx (a.add a_1) = Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx a + Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx a_1
• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx (a.mul a_1) = Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx a * Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx a_1
• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx (a.pow a_1) = Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing ctx a ^ a_1

theorem Lean.Grind.Ring.OfSemiring.Expr.denoteAsRing_eq {α : Type u_1} [Semiring α] (ctx : Context α) (e : Expr) : denoteAsRing ctx e = ↑(denote ctx e)

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

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

def Lean.Grind.Ring.OfSemiring.Expr.toPoly : Expr → CommRing.Poly

Equations

• (Lean.Grind.Ring.OfSemiring.Expr.num a).toPoly = Lean.Grind.CommRing.Poly.num ↑a
• (Lean.Grind.Ring.OfSemiring.Expr.var a).toPoly = Lean.Grind.CommRing.Poly.ofVar a
• (a.add a_1).toPoly = a.toPoly.combine a_1.toPoly
• (a.mul a_1).toPoly = a.toPoly.mul a_1.toPoly
• ((Lean.Grind.Ring.OfSemiring.Expr.num n).pow a_1).toPoly = Lean.Grind.CommRing.Poly.num (↑n ^ a_1)
• ((Lean.Grind.Ring.OfSemiring.Expr.var x_1).pow a_1).toPoly = Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x_1, k := a_1 } Lean.Grind.CommRing.Mon.unit)
• (a.pow a_1).toPoly = a.toPoly.pow a_1

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

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

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

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

theorem Lean.Grind.CommRing.Poly.denoteS_ofMon {α : Type u_1} [CommSemiring α] (ctx : Context α) (m : Mon) : denoteS ctx (ofMon m) = Mon.denote ctx m

theorem Lean.Grind.CommRing.Poly.denoteS_ofVar {α : Type u_1} [CommSemiring α] (ctx : Context α) (x : Var) : denoteS ctx (ofVar x) = Var.denote ctx x

theorem Lean.Grind.CommRing.Poly.denoteS_addConst {α : Type u_1} [CommSemiring α] (ctx : Context α) (p : Poly) (k : Int) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (p.addConst k) = denoteS ctx p + ↑k.toNat

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

theorem Lean.Grind.CommRing.Poly.denoteS_concat {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.concat p₂) = denoteS ctx p₁ + denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_mulConst {α : Type u_1} [CommSemiring α] (ctx : Context α) (k : Int) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulConst k p) = ↑k.toNat * denoteS ctx p

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

theorem Lean.Grind.CommRing.Poly.denoteS_combine {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.combine p₂) = denoteS ctx p₁ + denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (mulConst k p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mulMon_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.concat_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.concat p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.combine_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_go_NonnegCoeffs (p₁ p₂ acc : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul.go p₂ p₁ acc).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul p₂).NonnegCoeffs

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

theorem Lean.Grind.CommRing.Poly.num_zero_NonnegCoeffs : (num 0).NonnegCoeffs

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₂

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₂

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

theorem Lean.Grind.Ring.OfSemiring.Expr.toPoly_NonnegCoeffs {e : Expr} : e.toPoly.NonnegCoeffs

theorem Lean.Grind.Ring.OfSemiring.Expr.denoteS_toPoly {α : Type u_1} [CommSemiring α] (ctx : Context α) (e : Expr) : CommRing.Poly.denoteS ctx e.toPoly = denote ctx e

def Lean.Grind.Ring.OfSemiring.eq_normS_cert (lhs rhs : Expr) : Bool

Equations

• Lean.Grind.Ring.OfSemiring.eq_normS_cert lhs rhs = (lhs.toPoly == rhs.toPoly)

theorem Lean.Grind.Ring.OfSemiring.eq_normS {α : Type u_1} [CommSemiring α] (ctx : Context α) (lhs rhs : Expr) : eq_normS_cert lhs rhs = true → Expr.denote ctx lhs = Expr.denote ctx rhs