Proofs surrounding the list reverse function

Reverse.idr

import Data.Nat
import Prelude

%hide reverse

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

testRev1 : reverse (reverse [1, 2, 3]) = [1, 2, 3]
testRev1 = Refl

testRev2 : reverse (reverse ['a', 'b', 'c']) = ['a', 'b', 'c']
testRev2 = Refl

testRev3 : reverse (reverse [1.0, 2.0, 3.0]) = [1.0, 2.0, 3.0]
testRev3 = Refl

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

||| `reverse` is distrubutive over `++`
reverseDistributive : (xs : List a) -> (ys : List a) -> reverse (xs ++ ys) = reverse ys ++ reverse xs
reverseDistributive xs [] = rewrite nilIdentity xs in Refl
reverseDistributive xs (y :: ys) = rewrite reverseDistributive xs (y ::ys) in Refl

||| The `reverse` function is its own inverse
reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
reverseInvolutive [] = Refl
reverseInvolutive (x :: xs) =
  let p = reverseDistributive (reverse xs) [x]
      iH = reverseInvolutive xs in
    rewrite p in rewrite iH in Refl

applyRev : Nat -> List a -> List a
applyRev 0 xs = xs
applyRev (S k) xs = applyRev k (reverse xs)  
  
applyRevEven' : {n : Nat} -> (xs : List a) -> applyRev (n + n) xs = xs
applyRevEven' {n=Z} xs = Refl
applyRevEven' {n=(S k)} xs =
  let s = plusSuccRightSucc k k
      base = reverseInvolutive xs
      iH = applyRevEven' xs
      in rewrite sym s
      in rewrite base in iH
         
applyRevOdd' : {n : Nat} -> (xs : List a) -> applyRev (S (n + n)) xs = reverse xs
applyRevOdd' {n =Z} xs = Refl
applyRevOdd' {n=(S k)} xs =
  let s = plusSuccRightSucc k k
      base = reverseInvolutive xs
      iH = applyRevOdd' xs
  in rewrite sym s
  in rewrite base in iH
 
{- 
  Data types representing even and odd natural numbers. Using
  these two constructors `MkEven` and `MkOdd` we can create all
  natural numbers. Here `MkEven 0` represents the first even natural
  number `0` and `MkOdd 0` represents the first odd natural number `1`.
-}

data Even : Nat -> Type where
  MkEven : (half : Nat) -> (k = half + half) -> Even k
  
data Odd : Nat -> Type where
  MkOdd : (half : Nat) -> (k = S (half + half)) -> Odd k

||| Applying `reverse` an even amount of times to a list `xs` is equal to `xs`
applyRevEven : Even n -> (xs : List a) -> applyRev n xs = xs
applyRevEven (MkEven half p) xs =
  let s = applyRevEven' xs in rewrite p in s

||| Applying `reverse` an odd amount of times to a list `xs` is equal to `reverse xs`
applyRevOdd : Odd n -> (xs : List a) -> applyRev n xs = reverse xs
applyRevOdd (MkOdd half p) xs =
  let s = applyRevOdd' xs in rewrite p in s