- 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
Equations
- Nat.SOM.instInhabitedExpr = { default := Nat.SOM.Expr.num default }
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)
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)
Equations
- Nat.SOM.Mon.mul m₁ m₂ = Nat.SOM.Mon.mul.go Nat.Linear.hugeFuel m₁ m₂
Equations
- Nat.SOM.Mon.mul.go 0 m₁ m₂ = m₁ ++ m₂
- Nat.SOM.Mon.mul.go (Nat.succ fuel_2) m₁ [] = m₁
- Nat.SOM.Mon.mul.go (Nat.succ fuel_2) [] m₂ = m₂
- Nat.SOM.Mon.mul.go (Nat.succ fuel_2) (v₁ :: m₁_2) (v₂ :: m₂_2) = cond (Nat.blt v₁ v₂) (v₁ :: Nat.SOM.Mon.mul.go fuel_2 m₁_2 (v₂ :: m₂_2)) (cond (Nat.blt v₂ v₁) (v₂ :: Nat.SOM.Mon.mul.go fuel_2 (v₁ :: m₁_2) m₂_2) (v₁ :: v₂ :: Nat.SOM.Mon.mul.go fuel_2 m₁_2 m₂_2))
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)
Equations
- Nat.SOM.Poly.add p₁ p₂ = Nat.SOM.Poly.add.go Nat.Linear.hugeFuel p₁ p₂
Equations
- Nat.SOM.Poly.add.go 0 p₁ p₂ = p₁ ++ p₂
- Nat.SOM.Poly.add.go (Nat.succ fuel_2) p₁ [] = p₁
- Nat.SOM.Poly.add.go (Nat.succ fuel_2) [] p₂ = p₂
- Nat.SOM.Poly.add.go (Nat.succ fuel_2) ((k₁, m₁) :: p₁_2) ((k₂, m₂) :: p₂_2) = cond (decide (m₁ < m₂)) ((k₁, m₁) :: Nat.SOM.Poly.add.go fuel_2 p₁_2 ((k₂, m₂) :: p₂_2)) (cond (decide (m₂ < m₁)) ((k₂, m₂) :: Nat.SOM.Poly.add.go fuel_2 ((k₁, m₁) :: p₁_2) p₂_2) (cond (k₁ + k₂ == 0) (Nat.SOM.Poly.add.go fuel_2 p₁_2 p₂_2) ((k₁ + k₂, m₁) :: Nat.SOM.Poly.add.go fuel_2 p₁_2 p₂_2)))
Equations
- Nat.SOM.Poly.insertSorted k m [] = [(k, m)]
- Nat.SOM.Poly.insertSorted k m ((k_1, m_1) :: p_1) = cond (decide (m < m_1)) ((k, m) :: (k_1, m_1) :: p_1) ((k_1, m_1) :: Nat.SOM.Poly.insertSorted k m p_1)
Equations
- Nat.SOM.Poly.mulMon p k m = Nat.SOM.Poly.mulMon.go k m p []
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)
Equations
- Nat.SOM.Poly.mul p₁ p₂ = Nat.SOM.Poly.mul.go p₂ p₁ []
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))
Equations
- Nat.SOM.Expr.toPoly (Nat.SOM.Expr.num n) = cond (n == 0) [] [(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)
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₂
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₂
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₂
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₂
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₂
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₂
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 (Nat.SOM.Poly.mulMon p 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 : 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
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₂
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₂
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
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