module Data.Polynomial
import Data.List
import Data.Nat

%default total

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 x = Refl

h1 : (x:Poly) -> x ++ [] = x
h1 [] = Refl
h1 (x::xs) = rewrite (h1 xs) in Refl

public export
addzero' : (x:Poly) -> x + [] = x
addzero' [] = Refl
addzero' (x :: xs) = h1 (x :: xs)

public export
addcomm : (x,y:Poly) -> x + y = y + x
addcomm [] y = sym $ addzero' y
addcomm x [] = addzero' x
addcomm (x::xs) (y::ys) = 
    rewrite plusCommutative x y in 
    rewrite addcomm xs ys in Refl

public export
addassoc : (x,y,z:Poly) -> (x + y) + z = x + (y + z)
addassoc [] y z = Refl
addassoc x [] z = rewrite addzero' x in Refl
addassoc x y [] = rewrite addzero' (x+y) in rewrite addzero' y in Refl
addassoc (x::xs) (y::ys) (z::zs) = 
    rewrite plusAssociative x y z in
    rewrite addassoc xs ys zs in
    Refl

public export
mulzero : (x:Poly) -> [] * x = []
mulzero x = Refl

public export
mulzero' : (x:Poly) -> x * [] = []
mulzero' [] = Refl
mulzero' (x :: xs) = Refl

public export
mulone : (x:Poly) -> [1] * x = x
mulone [] = Refl
mulone (x :: xs) = 
    rewrite plusZeroRightNeutral x in 
    rewrite mulone xs in
    rewrite addzero' xs in Refl
    
public export
mulone' : (x:Poly) -> x * [1] = x
mulone' [] = Refl
mulone' (x :: xs) = 
    rewrite multOneRightNeutral x in 
    rewrite mulone' xs in Refl

eqadd : (a,b,c,d:Poly) -> (a + b) + (c + d) = (a + c) + (b + d)
eqadd a b c d = 
    rewrite addassoc a b (c + d) in 
    rewrite addassoc a c (b + d) in
    rewrite sym $ addassoc b c d in
    rewrite sym $ addassoc c b d in
    rewrite addcomm b c in Refl 

public export
dist : (x,y,z:Poly) -> x * (y + z) = x * y + x * z
dist [] _ _  = Refl
dist x [] z = rewrite mulzero' x in Refl
dist x y [] = 
    rewrite mulzero' x in 
    rewrite addzero' y in 
    rewrite addzero' (x * y) in Refl 
dist (x::xs) (y::ys) (z::zs) = 
    rewrite multDistributesOverPlusRight x y z in 
    rewrite dist xs (y::ys) (z::zs) in
    rewrite dist [x] ys zs in 
    rewrite eqadd ([x] * ys) ([x] * zs) (xs * (y::ys)) (xs * (z::zs)) in 
    Refl

lemma : (x : Nat) -> (xs : List Nat) -> (y : Nat) -> (ys : List Nat) -> [x] * ys + (y :: ys) * xs = [y] * xs + (x :: xs) * ys
public export
mulcomm : (x,y:Poly) -> x * y = y * x

lemma x [] y ys = addzero' ([x] * ys)
lemma x xs y [] = sym $ addzero' ([y] * xs)
lemma x (xx :: xs) y (yy :: ys) = 
    rewrite mulcomm (xx::xs) (yy::ys) in
    rewrite plusCommutative (x * yy) (y * xx) in
    rewrite addzero' ([x] * ys) in
    rewrite addzero' ([y] * xs) in
    rewrite eqadd [] ([x] * ys) ([y] * xs) ((yy::ys) * (xx::xs)) in 
    Refl

mulcomm [] y = sym $ mulzero' y 
mulcomm x [] = mulzero' x
mulcomm (x::xs) (y::ys) =
    rewrite mulcomm xs (y::ys) in
    rewrite mulcomm ys (x::xs) in
    rewrite multCommutative x y in
    rewrite lemma x xs y ys in Refl