module Data.Polynomial
import Data.List
import Data.Nat
public export
(Num a) => Num (List a) where
    (+) (x::xs) (y::ys) = (x + y) :: (xs + ys)
    (+) xs ys = xs ++ ys
    (*) (x::xs) (y::ys) = (x * y) :: ([x] * ys + xs * (y::ys))
    (*) _ _ = []
    fromInteger x = [fromInteger x]
Poly = List Nat
public export
addzero : {x:Poly} -> ([] + x = x)
addzero = Refl
eqList : {x,y:ty} -> {xs, ys:List ty} -> x=y -> xs=ys -> x::xs = y::ys
eqList Refl Refl = Refl
h1 : (x:Poly) -> (x ++ [] = x)
h1 [] = Refl
h1 (x::xs) = cong (x::) (h1 xs)
h2 : (x:Poly) -> (x + [] = x ++ [])
h2 [] = Refl
h2 (x :: xs) = Refl
public export
addzero' : {x:Poly} -> (x + [] = x)
addzero' = trans (h2 x) (h1 x)
public export
addcomm : {x,y:Poly} -> (x + y = y + x)
addcomm {x = []} = sym $ addzero'
addcomm {y = []} = addzero'
addcomm {x=(x::_), y=(y::_)} = 
    eqList (plusCommutative x y) (addcomm)
public export
addassoc : {x,y,z:Poly} -> ((x + y) + z = x + (y + z))
addassoc {x = []} = Refl
addassoc {y = []} = rewrite addzero' in Refl
addassoc {z = []} = trans (addzero') $ cong (x + ) (sym $ addzero')
addassoc {x=(x::_), y=(y::_), z=(z::_)} = 
    eqList (sym $ (plusAssociative x y z)) $ addassoc
public export
mulzero : {x:Poly} -> ([] * x = [])
mulzero = Refl
public export
mulzero' : {x:Poly} -> (x * [] = [])
mulzero' {x = []} = Refl
mulzero' {x = (_ :: _)} = Refl
public export
mulone : {x:Poly} -> ([1] * x = x)
mulone {x = []} = Refl
mulone {x = (x :: xs)} = eqList (plusZeroRightNeutral x) $
    trans (cong (+ []) mulone) addzero'
public export
mulone' : {x:Poly} -> (x * [1] = x)
mulone' {x = []} = Refl
mulone' {x = (x :: xs)} = eqList (multOneRightNeutral x) mulone'
eqadd : (Num ty) => {a,b,c,d:ty} -> a=c -> b=d -> a+b=c+d
eqadd Refl Refl = Refl
eqadd2 : {a,b,c,d:Poly} -> ((a+b)+(c+d) = (a+c)+(b+d))
eqadd2 = trans addassoc
    $ trans (cong (a+)
    $ trans (sym addassoc)
    $ trans (cong (+d) addcomm) addassoc)
    $ sym addassoc 
public export
dist : {x,y,z:Poly} -> (x*(y+z) = x*y+ x*z)
dist {x = []} = Refl
dist {y = []} = cong (+ (x * z)) $ sym $ mulzero'
dist {z = []} = 
    trans (cong (x * ) addzero')
    $ trans (sym addzero')
    $ cong (x * y + ) $ sym mulzero'
dist {x = [x], y = (y :: ys), z = (z :: zs)} = 
    eqList (multDistributesOverPlusRight x y z)
    $ trans addzero' $ trans dist
    $ sym $ eqadd addzero' addzero'
dist {x = (x::xs), y = (y::ys), z = (z::zs)} = 
    eqList (multDistributesOverPlusRight x y z) 
    $ trans (eqadd dist dist)
    $ eqadd2
mulcomm' : (x,y:Poly) -> (x * y = y * x)
mulcomm' [] _ = sym mulzero' 
mulcomm' _ [] = mulzero'
mulcomm' [x] (y::ys) = 
    eqList (multCommutative x y)
    $ trans addzero' (mulcomm' [x] ys)
mulcomm' (x :: xx :: xs) [y] = sym $ mulcomm' [y] (x :: xx :: xs)
mulcomm' (x :: xx :: xs) (y :: yy :: ys) =
    eqList (multCommutative x y)
    $ trans (eqadd (mulcomm' [x] (yy::ys)) (mulcomm' (xx::xs) (y :: yy :: ys)))
    $ trans (
        eqList (trans (plusCommutative (yy * x) (y * xx))
        $ eqadd (multCommutative y xx)
        $ multCommutative yy x) 
        $ trans (sym addassoc)
        $ trans (eqadd (trans addcomm $ eqadd (mulcomm' [y] xs) (mulcomm' ys [x]))
        $ mulcomm' (yy::ys) (xx::xs))
        $ addassoc
    )
    $ sym $ eqadd (mulcomm' [y] (xx::xs)) (mulcomm' (yy::ys) (x :: xx :: xs))
public export
mulcomm : {x,y:Poly} -> (x * y = y * x)
mulcomm {x, y} = mulcomm' x y