myReverse.idr

import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
-- myReverse {n = S k} (x :: xs) 
--          = let result = myReverse xs ++ [x] in
--                rewrite plusCommutative 1 k in result
myReverse (x :: xs) = reverseProof x xs (myReverse xs ++ [x])
  where
    reverseProof : (x : elem) -> (xs : Vect len elem) -> Vect (len + 1) elem -> Vect (S len) elem
    reverseProof {len} x xs result = rewrite plusCommutative 1 len in result

append_nil : Vect m elem -> Vect (plus m 0) elem
append_nil {m} xs = rewrite plusZeroRightNeutral m in xs

append_xs : Vect (S (m + len)) elem -> Vect (plus m (S len)) elem
append_xs {m} {len} xs = rewrite sym (plusSuccRightSucc m len) in xs

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite (plusZeroRightNeutral m) in Refl
myPlusCommutes (S k) m = rewrite (myPlusCommutes k m) in rewrite (plusSuccRightSucc m k) in Refl