0 | ||| Properties of the reverse function.
 1 | module Data.List.Reverse
 2 |
 3 | import Data.Nat
 4 | import Data.List
 5 |
 6 | -- Additional properties coming out of base's Data.List
 7 | --  - revAppend (i.e. reverse xs ++ reverse ys = reverse (ys ++ xs)
 8 | --  - reverseInvolutive (i.e. reverse (reverse xs) = xs)
 9 |
10 | %default total
11 |
12 | export
13 | reverseOntoAcc : (xs, ys, zs : List a) ->
14 |   reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
15 | reverseOntoAcc [] _ _ = Refl
16 | reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs
17 |
18 | ||| Serves as a specification for reverseOnto.
19 | export
20 | reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
21 | reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
22 |
23 | ||| The reverse of an empty list is an empty list.  Together with reverseCons,
24 | ||| serves as a specification for reverse.
25 | export
26 | reverseNil : reverse [] = []
27 | reverseNil = Refl
28 |
29 | ||| The reverse of a cons is the reverse of the tail followed by the head.
30 | ||| Together with reverseNil serves as a specification for reverse.
31 | export
32 | reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs `snoc` x
33 | reverseCons x xs = reverseOntoSpec [x] xs
34 |
35 | ||| A slow recursive definition of reverse.
36 | public export
37 | 0 slowReverse : List a -> List a
38 | slowReverse [] = []
39 | slowReverse (x :: xs) = slowReverse xs `snoc` x
40 |
41 | ||| The iterative and recursive definitions of reverse are the same.
42 | export
43 | reverseEquiv : (xs : List a) -> slowReverse xs = reverse xs
44 | reverseEquiv [] = Refl
45 | reverseEquiv (x :: xs) =
46 |   rewrite reverseEquiv xs in
47 |     rewrite revAppend [x] xs in
48 |       Refl
49 |
50 | ||| Reversing a singleton list is a no-op.
51 | export
52 | reverseSingletonId : (x : a) -> reverse [x] = [x]
53 | reverseSingletonId _ = Refl
54 |
55 | ||| Reversing onto preserves list length.
56 | export
57 | reverseOntoLength : (xs, acc : List a) ->
58 |   length (reverseOnto acc xs) = length acc + length xs
59 | reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
60 | reverseOntoLength (x :: xs) acc =
61 |   rewrite reverseOntoLength xs (x :: acc) in
62 |     plusSuccRightSucc (length acc) (length xs)
63 |
64 | ||| Reversing preserves list length.
65 | export
66 | reverseLength : (xs : List a) -> length (reverse xs) = length xs
67 | reverseLength xs = reverseOntoLength xs []
68 |
69 | ||| Equal reversed lists are equal.
70 | export
71 | reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
72 | reverseEqual xs ys prf =
73 |   rewrite sym $ reverseInvolutive xs in
74 |     rewrite prf in
75 |       reverseInvolutive ys
76 |