Init.Data.Nat.SOM

source

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

source

instance Nat.SOM.instInhabitedExpr:

Inhabited Nat.SOM.Expr

Equations

Nat.SOM.instInhabitedExpr = { default := Nat.SOM.Expr.num default }

source

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

Nat.SOM.Expr → Nat

Equations

Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.num n) = n
Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.var v) = Nat.Linear.Var.denote ctx v
Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.add a b) = Nat.add (Nat.SOM.Expr.denote ctx a) (Nat.SOM.Expr.denote ctx b)
Nat.SOM.Expr.denote ctx (Nat.SOM.Expr.mul a b) = Nat.mul (Nat.SOM.Expr.denote ctx a) (Nat.SOM.Expr.denote ctx b)

source

@[inline]

abbrev Nat.SOM.Mon:

Type

Equations

Nat.SOM.Mon = List Nat.Linear.Var

source

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.mul (Nat.Linear.Var.denote ctx v) (Nat.SOM.Mon.denote ctx vs)

source

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

Nat.SOM.Mon

Equations

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

source

def Nat.SOM.Mon.mul.go (fuel : Nat) (m₁ : Nat.SOM.Mon) (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₂

source

@[inline]

abbrev Nat.SOM.Poly:

Type

Equations

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

source

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

Nat.SOM.Poly → Nat

Equations

Nat.SOM.Poly.denote ctx [] = 0
Nat.SOM.Poly.denote ctx ((k, m) :: p) = Nat.add (Nat.mul k (Nat.SOM.Mon.denote ctx m)) (Nat.SOM.Poly.denote ctx p)

source

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

Nat.SOM.Poly

Equations

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

source

def Nat.SOM.Poly.add.go (fuel : Nat) (p₁ : Nat.SOM.Poly) (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₂

source

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

Nat.SOM.Poly

Equations

Nat.SOM.Poly.insertSorted k m [] = [(k, m)]
Nat.SOM.Poly.insertSorted k m ((k_1, m_1) :: p_1) = bif decide (m < m_1) then (k, m) :: (k_1, m_1) :: p_1 else (k_1, m_1) :: Nat.SOM.Poly.insertSorted k m p_1

source

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

Nat.SOM.Poly

Equations

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

source

def Nat.SOM.Poly.mulMon.go (k : Nat) (m : Nat.SOM.Mon) (p : Nat.SOM.Poly) (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) (Nat.SOM.Mon.mul m m_1) acc)

source

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

Nat.SOM.Poly

Equations

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

source

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

Nat.SOM.Poly

Equations

Nat.SOM.Poly.mul.go p₂ [] acc = acc
Nat.SOM.Poly.mul.go p₂ ((k, m) :: p) acc = Nat.SOM.Poly.mul.go p₂ p (Nat.SOM.Poly.add acc (Nat.SOM.Poly.mulMon p₂ k m))

source

def Nat.SOM.Expr.toPoly:

Nat.SOM.Expr → Nat.SOM.Poly

Equations

Nat.SOM.Expr.toPoly (Nat.SOM.Expr.num n) = bif n == 0 then [] else [(n, [])]
Nat.SOM.Expr.toPoly (Nat.SOM.Expr.var v) = [(1, [v])]
Nat.SOM.Expr.toPoly (Nat.SOM.Expr.add a b) = Nat.SOM.Poly.add (Nat.SOM.Expr.toPoly a) (Nat.SOM.Expr.toPoly b)
Nat.SOM.Expr.toPoly (Nat.SOM.Expr.mul a b) = Nat.SOM.Poly.mul (Nat.SOM.Expr.toPoly a) (Nat.SOM.Expr.toPoly b)

source

theorem Nat.SOM.Mon.append_denote (ctx : Nat.Linear.Context) (m₁ : Nat.SOM.Mon) (m₂ : Nat.SOM.Mon) :

Nat.SOM.Mon.denote ctx (m₁ ++ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂

source

theorem Nat.SOM.Mon.mul_denote (ctx : Nat.Linear.Context) (m₁ : Nat.SOM.Mon) (m₂ : Nat.SOM.Mon) :

Nat.SOM.Mon.denote ctx (Nat.SOM.Mon.mul m₁ m₂) = Nat.SOM.Mon.denote ctx m₁ * Nat.SOM.Mon.denote ctx m₂

source

theorem Nat.SOM.Mon.mul_denote.go (ctx : Nat.Linear.Context) (fuel : Nat) (m₁ : Nat.SOM.Mon) (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₂

source

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

Nat.SOM.Poly.denote ctx (p₁ ++ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂

source

theorem Nat.SOM.Poly.add_denote (ctx : Nat.Linear.Context) (p₁ : Nat.SOM.Poly) (p₂ : Nat.SOM.Poly) :

Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.add p₁ p₂) = Nat.SOM.Poly.denote ctx p₁ + Nat.SOM.Poly.denote ctx p₂

source

theorem Nat.SOM.Poly.add_denote.go (ctx : Nat.Linear.Context) (fuel : Nat) (p₁ : Nat.SOM.Poly) (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₂

source

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

source

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 (Nat.SOM.Poly.mulMon p k m) = Nat.SOM.Poly.denote ctx p * k * Nat.SOM.Mon.denote ctx m

source

theorem Nat.SOM.Poly.mulMon_denote.go (ctx : Nat.Linear.Context) (k : Nat) (m : Nat.SOM.Mon) (p : Nat.SOM.Poly) (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

source

theorem Nat.SOM.Poly.mul_denote (ctx : Nat.Linear.Context) (p₁ : Nat.SOM.Poly) (p₂ : Nat.SOM.Poly) :

Nat.SOM.Poly.denote ctx (Nat.SOM.Poly.mul p₁ p₂) = Nat.SOM.Poly.denote ctx p₁ * Nat.SOM.Poly.denote ctx p₂

source

theorem Nat.SOM.Poly.mul_denote.go (ctx : Nat.Linear.Context) (p₂ : Nat.SOM.Poly) (p₁ : Nat.SOM.Poly) (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₂

source

theorem Nat.SOM.Expr.toPoly_denote (ctx : Nat.Linear.Context) (e : Nat.SOM.Expr) :

Nat.SOM.Poly.denote ctx (Nat.SOM.Expr.toPoly e) = Nat.SOM.Expr.denote ctx e

source

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

Nat.SOM.Expr.denote ctx a = Nat.SOM.Expr.denote ctx b