Formal verification of ++ and reverse

Reverse.idr

module Test

%hide reverse
%hide (++)
%default total

infixr 7 ++
(++) : List a -> List a -> List a
(++) [] ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]

-- # Formal verifications?

-- ## (++)
nonEuxaustive : (x : a) -> (xx : a) -> (y : a) -> (yy : a) ->
        [x,xx] ++ [y,yy] = [x,xx,y,yy]
nonEuxaustive x xx y yy = Refl

lenghtsAdd : (xs : List a) -> (ys : List a) ->
              length (xs ++ ys) = length xs + length ys
lenghtsAdd [] ys = Refl
lenghtsAdd (x :: xs) ys = 
  rewrite lenghtsAdd xs ys in Refl

emptyListIsLeftNullElement : (xs : List a) -> [] ++ xs = xs
emptyListIsLeftNullElement xs = Refl

emptyListIsRightNullElement : (xs : List a) -> xs ++ [] = xs
emptyListIsRightNullElement [] = Refl
emptyListIsRightNullElement (x :: xs) =
  rewrite emptyListIsRightNullElement xs in Refl

concatIsAssociative : (xs : List a) -> (ys : List a) -> (zs : List a) ->
                      (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
concatIsAssociative [] ys zs = Refl
concatIsAssociative (x :: xs) ys zs = 
   rewrite concatIsAssociative xs ys zs in Refl

-- ## reverse
reverseAppend : (xs : List a) -> (ys : List a) ->
                reverse (xs ++ ys) = reverse ys ++ reverse xs
reverseAppend [] ys = 
  rewrite emptyListIsRightNullElement (reverse ys) in Refl
reverseAppend (x :: xs) ys = 
  rewrite reverseAppend xs ys
  in
  rewrite concatIsAssociative (reverse ys) (reverse xs) [x] in Refl

reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
  rewrite reverseAppend (reverse xs) [x]
  in
  rewrite reverseReverse xs in Refl