def Lean.Grind.Linarith.Expr.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) : Expr → α

Equations

• Lean.Grind.Linarith.Expr.denoteN ctx (a.sub b) = 0
• Lean.Grind.Linarith.Expr.denoteN ctx a.neg = 0
• Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.intMul k a) = 0
• Lean.Grind.Linarith.Expr.denoteN ctx Lean.Grind.Linarith.Expr.zero = 0
• Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.var v) = Lean.Grind.Linarith.Var.denote ctx v
• Lean.Grind.Linarith.Expr.denoteN ctx (a.add b) = Lean.Grind.Linarith.Expr.denoteN ctx a + Lean.Grind.Linarith.Expr.denoteN ctx b
• Lean.Grind.Linarith.Expr.denoteN ctx (Lean.Grind.Linarith.Expr.natMul k a) = k • Lean.Grind.Linarith.Expr.denoteN ctx a

inductive Lean.Grind.Linarith.Poly.NonnegCoeffs : Poly → Prop

• nil : Poly.nil.NonnegCoeffs
• add (a : Int) (x : Var) (p : Poly) : a ≥ 0 → p.NonnegCoeffs → (Poly.add a x p).NonnegCoeffs

def Lean.Grind.Linarith.Poly.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) : α

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Poly.denoteN ctx Lean.Grind.Linarith.Poly.nil = 0

def Lean.Grind.Linarith.Poly.denoteN_nil {α : Type u_1} [NatModule α] (ctx : Context α) : denoteN ctx nil = 0

Equations

• ⋯ = ⋯

def Lean.Grind.Linarith.Poly.denoteN_add {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) : k ≥ 0 → denoteN ctx (add k x p) = k.toNat • Var.denote ctx x + denoteN ctx p

Equations

• ⋯ = ⋯

theorem Lean.Grind.Linarith.instAssociativeHAdd_1 {α : Type u_1} [NatModule α] : Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.instCommutativeHAdd_1 {α : Type u_1} [NatModule α] : Std.Commutative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.Poly.denoteN_insert {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteN ctx (insert k x p) = k.toNat • Var.denote ctx x + denoteN ctx p

theorem Lean.Grind.Linarith.Poly.denoteN_append {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.append p₂) = denoteN ctx p₁ + denoteN ctx p₂

theorem Lean.Grind.Linarith.Poly.denoteN_combine' {α : Type u_1} [NatModule α] (ctx : Context α) (fuel : Nat) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (combine' fuel p₁ p₂) = denoteN ctx p₁ + denoteN ctx p₂

theorem Lean.Grind.Linarith.Poly.denoteN_combine {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.combine p₂) = denoteN ctx p₁ + denoteN ctx p₂

theorem Lean.Grind.Linarith.Poly.denoteN_mul' {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteN ctx (p.mul' ↑k) = k • denoteN ctx p

theorem Lean.Grind.Linarith.Poly.denoteN_mul {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteN ctx (p.mul ↑k) = k • denoteN ctx p

def Lean.Grind.Linarith.Expr.toPolyN : Expr → Poly

Equations

• (a.sub b).toPolyN = Lean.Grind.Linarith.Poly.nil
• a.neg.toPolyN = Lean.Grind.Linarith.Poly.nil
• (Lean.Grind.Linarith.Expr.intMul k a).toPolyN = Lean.Grind.Linarith.Poly.nil
• Lean.Grind.Linarith.Expr.zero.toPolyN = Lean.Grind.Linarith.Poly.nil
• (Lean.Grind.Linarith.Expr.var v).toPolyN = Lean.Grind.Linarith.Poly.add 1 v Lean.Grind.Linarith.Poly.nil
• (a.add b).toPolyN = a.toPolyN.combine b.toPolyN
• (Lean.Grind.Linarith.Expr.natMul k a).toPolyN = a.toPolyN.mul ↑k

theorem Lean.Grind.Linarith.Poly.mul'_Nonneg (p : Poly) (k : Nat) : p.NonnegCoeffs → (p.mul' ↑k).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.mul_Nonneg (p : Poly) (k : Nat) : p.NonnegCoeffs → (p.mul ↑k).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.append_Nonneg (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.append p₂).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.combine'_Nonneg (fuel : Nat) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (combine' fuel p₁ p₂).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.combine_Nonneg (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs

theorem Lean.Grind.Linarith.Expr.toPolyN_Nonneg (e : Expr) : e.toPolyN.NonnegCoeffs

theorem Lean.Grind.Linarith.Expr.denoteN_toPolyN {α : Type u_1} [NatModule α] (ctx : Context α) (e : Expr) : Poly.denoteN ctx e.toPolyN = denoteN ctx e

def Lean.Grind.Linarith.eq_normN_cert (lhs rhs : Expr) : Bool

Equations

• Lean.Grind.Linarith.eq_normN_cert lhs rhs = (lhs.toPolyN == rhs.toPolyN)

theorem Lean.Grind.Linarith.eq_normN {α : Type u_1} [NatModule α] (ctx : Context α) (lhs rhs : Expr) : eq_normN_cert lhs rhs = true → Expr.denoteN ctx lhs = Expr.denoteN ctx rhs