+ 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