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

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

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

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

@[reducible, inline]

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

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

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

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

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

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) : α

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) : α

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

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