%default total

addzero : {x:Poly} -> ([] + x = x)
addzero = Refl

addzero : (x:Poly) -> [] + x = x
addzero x = 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 : (x:Poly) -> x ++ [] = x

h1 (x::xs) = cong (x::) (h1 xs)
h2 : (x:Poly) -> (x + [] = x ++ [])
h2 [] = Refl
h2 (x :: xs) = Refl

h1 (x::xs) = rewrite (h1 xs) in Refl

addzero' : {x:Poly} -> (x + [] = x)
addzero' = trans (h2 x) (h1 x)

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

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)

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

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

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

mulzero : {x:Poly} -> ([] * x = [])
mulzero = Refl

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

mulzero' : {x:Poly} -> (x * [] = [])
mulzero' {x = []} = Refl
mulzero' {x = (_ :: _)} = Refl

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

mulone : {x:Poly} -> ([1] * x = x)
mulone {x = []} = Refl
mulone {x = (x :: xs)} = eqList (plusZeroRightNeutral x) $
    trans (cong (+ []) mulone) addzero'

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

mulone' : {x:Poly} -> (x * [1] = x)
mulone' {x = []} = Refl
mulone' {x = (x :: xs)} = eqList (multOneRightNeutral x) mulone'

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

eqadd : (Num ty) => {a,b,c,d:ty} -> a=c -> b=d -> a+b=c+d
eqadd Refl Refl = 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 

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 [] _ _  = 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

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' : (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))

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

public export
mulcomm : {x,y:Poly} -> (x * y = y * x)
mulcomm {x, y} = mulcomm' x y

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