inductive Nat.SOM.Expr : Type

• num: Nat → Nat.SOM.Expr
• var: Nat.Linear.Var → Nat.SOM.Expr
• add: Nat.SOM.Expr → Nat.SOM.Expr → Nat.SOM.Expr
• mul: Nat.SOM.Expr → Nat.SOM.Expr → Nat.SOM.Expr

instance Nat.SOM.instInhabitedExpr : Inhabited Nat.SOM.Expr

def Nat.SOM.Expr.denote (ctx : Nat.Linear.Context) : Nat.SOM.Expr → Nat

@[reducible, inline]

abbrev Nat.SOM.Mon : Type

def Nat.SOM.Mon.denote (ctx : Nat.Linear.Context) : Nat.SOM.Mon → Nat

Equations

• Nat.SOM.Mon.denote ctx [] = 1
• Nat.SOM.Mon.denote ctx (v :: vs) = (Nat.Linear.Var.denote ctx v).mul (Nat.SOM.Mon.denote ctx vs)

def Nat.SOM.Mon.mul (m₁ m₂ : Nat.SOM.Mon) : Nat.SOM.Mon

Equations

• m₁.mul m₂ = Nat.SOM.Mon.mul.go Nat.Linear.hugeFuel m₁ m₂

def Nat.SOM.Mon.mul.go (fuel : Nat) (m₁ m₂ : Nat.SOM.Mon) : Nat.SOM.Mon

Equations

• One or more equations did not get rendered due to their size.
• Nat.SOM.Mon.mul.go 0 m₁ m₂ = m₁ ++ m₂
• Nat.SOM.Mon.mul.go fuel_2.succ m₁ [] = m₁
• Nat.SOM.Mon.mul.go fuel_2.succ [] m₂ = m₂

@[reducible, inline]

abbrev Nat.SOM.Poly : Type

Equations

• Nat.SOM.Poly = List (Nat × Nat.SOM.Mon)

def Nat.SOM.Poly.denote (ctx : Nat.Linear.Context) : Nat.SOM.Poly → Nat

def Nat.SOM.Poly.add (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly

Equations

• p₁.add p₂ = Nat.SOM.Poly.add.go Nat.Linear.hugeFuel p₁ p₂

def Nat.SOM.Poly.add.go (fuel : Nat) (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly

Equations

• One or more equations did not get rendered due to their size.
• Nat.SOM.Poly.add.go 0 p₁ p₂ = p₁ ++ p₂
• Nat.SOM.Poly.add.go fuel_2.succ p₁ [] = p₁
• Nat.SOM.Poly.add.go fuel_2.succ [] p₂ = p₂

def Nat.SOM.Poly.insertSorted (k : Nat) (m : Nat.SOM.Mon) (p : Nat.SOM.Poly) : Nat.SOM.Poly

def Nat.SOM.Poly.mulMon (p : Nat.SOM.Poly) (k : Nat) (m : Nat.SOM.Mon) : Nat.SOM.Poly

Equations

• p.mulMon k m = Nat.SOM.Poly.mulMon.go k m p []

def Nat.SOM.Poly.mulMon.go (k : Nat) (m : Nat.SOM.Mon) (p acc : Nat.SOM.Poly) : Nat.SOM.Poly

Equations

• Nat.SOM.Poly.mulMon.go k m [] acc = acc
• Nat.SOM.Poly.mulMon.go k m ((k_1, m_1) :: p_1) acc = Nat.SOM.Poly.mulMon.go k m p_1 (Nat.SOM.Poly.insertSorted (k * k_1) (m.mul m_1) acc)

def Nat.SOM.Poly.mul (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly

Equations

• p₁.mul p₂ = Nat.SOM.Poly.mul.go p₂ p₁ []

def Nat.SOM.Poly.mul.go (p₂ p₁ acc : Nat.SOM.Poly) : Nat.SOM.Poly

def Nat.SOM.Expr.toPoly : Nat.SOM.Expr → Nat.SOM.Poly

theorem Nat.SOM.Mon.append_denote (ctx : Nat.Linear.Context) (m₁ m₂ : Nat.SOM.Mon) : Nat.SOM.Mon.denote ctx (m₁ ++ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂

theorem Nat.SOM.Mon.mul_denote (ctx : Nat.Linear.Context) (m₁ m₂ : Nat.SOM.Mon) : Nat.SOM.Mon.denote ctx (m₁.mul m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂

theorem Nat.SOM.Mon.mul_denote.go (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ m₂ : Nat.SOM.Mon) : Nat.SOM.Mon.denote ctx (Nat.SOM.Mon.mul.go fuel m₁ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂

theorem Nat.SOM.Poly.append_denote (ctx : Nat.Linear.Context) (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (p₁ ++ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂

theorem Nat.SOM.Poly.add_denote (ctx : Nat.Linear.Context) (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (p₁.add p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂

theorem Nat.SOM.Poly.add_denote.go (ctx : Nat.Linear.Context) (fuel : Nat) (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.add.go fuel p₁ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂

theorem Nat.SOM.Poly.denote_insertSorted (ctx : Nat.Linear.Context) (k : Nat) (m : Nat.SOM.Mon) (p : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.insertSorted k m p) = Nat.SOM.Poly.denote ctx p + k * Nat.SOM.Mon.denote ctx m

theorem Nat.SOM.Poly.mulMon_denote (ctx : Nat.Linear.Context) (p : Nat.SOM.Poly) (k : Nat) (m : Nat.SOM.Mon) : Nat.SOM.Poly.denote ctx (p.mulMon k m) = Nat.SOM.Poly.denote ctx p * k * Nat.SOM.Mon.denote ctx m

theorem Nat.SOM.Poly.mulMon_denote.go (ctx : Nat.Linear.Context) (k : Nat) (m : Nat.SOM.Mon) (p acc : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.mulMon.go k m p acc) = Nat.SOM.Poly.denote ctx acc + Nat.SOM.Poly.denote ctx p * k * Nat.SOM.Mon.denote ctx m

theorem Nat.SOM.Poly.mul_denote (ctx : Nat.Linear.Context) (p₁ p₂ : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (p₁.mul p₂) = Nat.SOM.Poly.denote ctx p₁ * Nat.SOM.Poly.denote ctx p₂

theorem Nat.SOM.Poly.mul_denote.go (ctx : Nat.Linear.Context) (p₂ p₁ acc : Nat.SOM.Poly) : Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.mul.go p₂ p₁ acc) = Nat.SOM.Poly.denote ctx acc + Nat.SOM.Poly.denote ctx p₁ * Nat.SOM.Poly.denote ctx p₂

theorem Nat.SOM.Expr.toPoly_denote (ctx : Nat.Linear.Context) (e : Nat.SOM.Expr) : Nat.SOM.Poly.denote ctx e.toPoly = Nat.SOM.Expr.denote ctx e

theorem Nat.SOM.Expr.eq_of_toPoly_eq (ctx : Nat.Linear.Context) (a b : Nat.SOM.Expr) (h : (a.toPoly == b.toPoly) = true) : Nat.SOM.Expr.denote ctx a = Nat.SOM.Expr.denote ctx b