Documentation

Init.Data.Nat.Internal.SOM

inductive Nat.Internal.SOM.Expr :

num (i : Nat) : Expr
var (v : Linear.Var) : Expr
add (a b : Expr) : Expr
mul (a b : Expr) : Expr

Instances For

@[instance_reducible]

instance Nat.Internal.SOM.instInhabitedExpr :

Equations

Nat.Internal.SOM.instInhabitedExpr = { default := Nat.Internal.SOM.instInhabitedExpr.default }

@[inline]

noncomputable abbrev Nat.Internal.SOM.Expr.denote (ctx : Linear.Context) :

Equations

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

Instances For

@[reducible, inline]

abbrev Nat.Internal.SOM.Mon :

Equations

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

Instances For

@[inline]

noncomputable abbrev Nat.Internal.SOM.Mon.denote (ctx : Linear.Context) :

Equations

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

Instances For

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

Equations

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

Instances For

@[reducible, inline]

abbrev Nat.Internal.SOM.Poly :

Equations

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

Instances For

@[inline]

noncomputable abbrev Nat.Internal.SOM.Poly.denote (ctx : Linear.Context) :

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

Nat.Internal.SOM.Poly.insertSorted k m [] = [(k, m)]
Nat.Internal.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.Internal.SOM.Poly.insertSorted k m p_1

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

def Nat.Internal.SOM.Expr.toPoly :

Equations

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

Instances For

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

denote ctx (m₁ ++ m₂) = denote ctx m₁ * denote ctx m₂

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

denote ctx (m₁.mul m₂) = denote ctx m₁ * denote ctx m₂

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

denote ctx (p₁ ++ p₂) = denote ctx p₁ + denote ctx p₂

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

denote ctx (p₁.add p₂) = denote ctx p₁ + denote ctx p₂

theorem Nat.Internal.SOM.Poly.denote_insertSorted (ctx : Linear.Context) (k : Nat) (m : Mon) (p : Poly) :

denote ctx (insertSorted k m p) = denote ctx p + k * Mon.denote ctx m

theorem Nat.Internal.SOM.Poly.mulMon_denote (ctx : Linear.Context) (p : Poly) (k : Nat) (m : Mon) :

denote ctx (p.mulMon k m) = denote ctx p * k * Mon.denote ctx m

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

denote ctx (p₁.mul p₂) = denote ctx p₁ * denote ctx p₂

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

Poly.denote ctx e.toPoly = denote ctx e

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

denote ctx a = denote ctx b