Add more reverse properties

libs/contrib/Data/List/Reverse.idr

@@ -1,3 +1,4 @@
+||| Properties of the reverse function.
 module Data.List.Reverse
 
 %default total
@@ -33,6 +34,19 @@ reverseAppend (x :: xs) ys =
       rewrite reverseCons x xs in
         sym $ appendAssociative (reverse ys) (reverse xs) [x]
 
+||| A recursive definition of reverse.
+reverseRec : List a -> List a
+reverseRec [] = []
+reverseRec (x :: xs) = reverseRec xs ++ [x]
+
+||| The iterative and recursive defintions of reverse are the same.
+reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs
+reverseEquiv [] = Refl
+reverseEquiv (x :: xs) =
+  rewrite reverseEquiv xs in
+    rewrite reverseAppend [x] xs in
+      Refl
+
 ||| Reversing a singleton list is a no-op.
 reverseSingletonId : (x : a) -> reverse [x] = [x]
 reverseSingletonId _ = Refl
@@ -44,3 +58,42 @@ reverseReverseId (x :: xs) =
   rewrite reverseCons x xs in
     rewrite reverseAppend (reverse xs) [x] in
       cong $ reverseReverseId xs
+
+||| Reversing onto preserves list length.
+reverseOntoLength : (xs, acc : List a) ->
+  length $ reverseOnto acc xs = length acc + length xs
+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
+reverseOntoLength (x :: xs) acc =
+  rewrite reverseOntoLength xs (x :: acc) in
+    plusSuccRightSucc (length acc) (length xs)
+
+||| Reversing preserves list length.
+reverseLength : (xs : List a) -> length $ reverse xs = length xs
+reverseLength xs = reverseOntoLength xs []
+
+||| Equal reversed lists are equal.
+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
+reverseEqual xs ys prf =
+  rewrite sym $ reverseReverseId xs in
+    rewrite prf in
+      reverseReverseId ys
+
+||| Do geese see God?
+data Palindrome : (xs : List a) -> Type where
+  Empty : Palindrome []
+  Single : Palindrome [_]
+  Multi : Palindrome xs -> Palindrome $ [x] ++ xs ++ [x]
+
+||| A Palindrome reversed is itself.
+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
+palindromeReverse [] Empty = Refl
+palindromeReverse [_] Single = Refl
+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
+  rewrite reverseAppend ([x] ++ ys) [x] in
+    rewrite reverseAppend [x] ys in
+      rewrite palindromeReverse ys pf in
+        Refl
+
+||| Only Palindromes are equal to their own reverse.
+postulate  -- This is a tough one. Any takers?
+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs