@@ -1,3 +1,4 @@
1+||| Properties of the reverse function.
1module Data.List.Reverse
2module Data.List.Reverse
3%default total
4%default total
@@ -33,6 +34,19 @@ reverseAppend (x :: xs) ys =
33 rewrite reverseCons x xs in
34 rewrite reverseCons x xs in
34 sym $ appendAssociative (reverse ys) (reverse xs) [x]
35 sym $ appendAssociative (reverse ys) (reverse xs) [x]
37+||| A recursive definition of reverse.
38+reverseRec : List a -> List a
40+reverseRec (x :: xs) = reverseRec xs ++ [x]
42+||| The iterative and recursive defintions of reverse are the same.
43+reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs
44+reverseEquiv [] = Refl
45+reverseEquiv (x :: xs) =
46+ rewrite reverseEquiv xs in
47+ rewrite reverseAppend [x] xs in
36||| Reversing a singleton list is a no-op.
50||| Reversing a singleton list is a no-op.
37reverseSingletonId : (x : a) -> reverse [x] = [x]
51reverseSingletonId : (x : a) -> reverse [x] = [x]
38reverseSingletonId _ = Refl
52reverseSingletonId _ = Refl
@@ -44,3 +58,42 @@ reverseReverseId (x :: xs) =
44 rewrite reverseCons x xs in
58 rewrite reverseCons x xs in
45 rewrite reverseAppend (reverse xs) [x] in
59 rewrite reverseAppend (reverse xs) [x] in
46 cong $ reverseReverseId xs
60 cong $ reverseReverseId xs
62+||| Reversing onto preserves list length.
63+reverseOntoLength : (xs, acc : List a) ->
64+ length $ reverseOnto acc xs = length acc + length xs
65+reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
66+reverseOntoLength (x :: xs) acc =
67+ rewrite reverseOntoLength xs (x :: acc) in
68+ plusSuccRightSucc (length acc) (length xs)
70+||| Reversing preserves list length.
71+reverseLength : (xs : List a) -> length $ reverse xs = length xs
72+reverseLength xs = reverseOntoLength xs []
74+||| Equal reversed lists are equal.
75+reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
76+reverseEqual xs ys prf =
77+ rewrite sym $ reverseReverseId xs in
82+data Palindrome : (xs : List a) -> Type where
83+ Empty : Palindrome []
84+ Single : Palindrome [_]
85+ Multi : Palindrome xs -> Palindrome $ [x] ++ xs ++ [x]
87+||| A Palindrome reversed is itself.
88+palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs
89+palindromeReverse [] Empty = Refl
90+palindromeReverse [_] Single = Refl
91+palindromeReverse ([x] ++ ys ++ [x]) (Multi pf) =
92+ rewrite reverseAppend ([x] ++ ys) [x] in
93+ rewrite reverseAppend [x] ys in
94+ rewrite palindromeReverse ys pf in
97+||| Only Palindromes are equal to their own reverse.
98+postulate -- This is a tough one. Any takers?
99+reversePalindrome : (xs : List a) -> reverse xs = xs -> Palindrome xs