Poly

Poly.agda

open import Data.Nat using (ℕ; _+_; _*_ ; suc)
open import Data.List.Base using (List ; _∷_ ; [] ; map)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym; cong)

infixl 20 _⊹_
infixl 19 _⋆_

data ℙ : Set where
  X : ℙ
  #_ : ℕ -> ℙ
  _⊹_ : ℙ -> ℙ -> ℙ
  _⋆_ : ℙ -> ℙ -> ℙ

[ℙ] : Set
[ℙ] = List ℕ

_⦅_⦆ : ℙ -> ℕ ->  ℕ
X ⦅ n ⦆  = n
(# x) ⦅ _ ⦆ = x
(l ⊹ r) ⦅ n ⦆  = l ⦅ n ⦆ + r ⦅ n ⦆
(l ⋆ r) ⦅ n ⦆ = l ⦅ n ⦆ * r ⦅ n ⦆

_⟦_⟧ : [ℙ] -> ℕ -> ℕ
[] ⟦ n ⟧ = 0
(x ∷ xs) ⟦ n ⟧ = x + n * xs ⟦ n ⟧

const* : [ℙ] -> ℕ -> [ℙ]
const* xs n = map (λ i -> i * n) xs

var* : [ℙ] -> [ℙ]
var* xs = 0 ∷ xs

_+[ℙ]_ : [ℙ] -> [ℙ] -> [ℙ]
(x ∷ xs) +[ℙ] (y ∷ ys) = (x + y) ∷ xs +[ℙ] ys
[] +[ℙ] ys = ys
xs +[ℙ] [] = xs

_*[ℙ]_ : [ℙ] -> [ℙ] -> [ℙ]
[] *[ℙ] ys = []
(x ∷ xs) *[ℙ] ys = (const* ys x) +[ℙ] (xs *[ℙ] (var* ys))

ℙ→[ℙ] : ℙ -> [ℙ]
ℙ→[ℙ] (# i) = i ∷ []
ℙ→[ℙ] X = 0 ∷ 1 ∷ []
ℙ→[ℙ] (l ⊹ r) = (ℙ→[ℙ] l) +[ℙ] (ℙ→[ℙ] r)
ℙ→[ℙ] (l ⋆ r) = (ℙ→[ℙ] l) *[ℙ] (ℙ→[ℙ] r)

-- partial function for writing exponents in ℙ
_^_ : ℙ -> ℕ -> ℙ
X ^ 1 = X
X ^ (suc n) = X ⋆ (X ^ n)
_ ^ _ = # 0

p₁ : ℙ
p₁ = (# 6) ⊹ ((# 7) ⋆ X) ⊹ ((# 13) ⋆ X ^ 2)

p₂ : ℙ
p₂ = ((# 5) ⋆ X) ⊹ ((# 7) ⋆ X ^ 3)

--(6 + 7x + 13x^2) * ( 0 + 5x + 0x^2 + 7x^3) => 30x + 35x^2 + 107x^3 + 49x^4 + 91 x^5
test : ℙ
test = p₁ ⋆ p₂

_ : ℙ→[ℙ] test ≡ 0 ∷ 30 ∷ 35 ∷ 107 ∷ 49 ∷ 91 ∷ []
_ = refl

test-eval : test ⦅ 5 ⦆ ≡ (ℙ→[ℙ] test) ⟦ 5 ⟧
test-eval = refl

theorem : ∀ (p : ℙ) (n : ℕ) -> p ⦅ n ⦆ ≡ (ℙ→[ℙ] p) ⟦ n ⟧
theorem X 0 = refl
theorem X (suc n) = {!   !}
theorem _ _ = {!   !}