@@ -3,13 +3,15 @@ module Data.List.Extra
3%default total
3%default total
4%access export
4%access export
6+||| The final segment of the accumulator is the final segment of the result.
7+reverseOntoAcc : (xs, ys, zs : List a) ->
8+ reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
9+reverseOntoAcc [] _ _ = Refl
10+reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs
6||| Serves as a specification for reverseOnto.
12||| Serves as a specification for reverseOnto.
7reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
13reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
8−reverseOntoSpec _ [] = Refl
14+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
9−reverseOntoSpec xs (y::ys) =
10− trans (reverseOntoSpec (y::xs) ys)
11− (trans (appendAssociative (reverse ys) [y] xs)
12− (cong {f = \l => l ++ xs} (sym (reverseOntoSpec [y] ys))))
14||| The reverse of an empty list is an empty list. Together with reverseCons,
16||| The reverse of an empty list is an empty list. Together with reverseCons,
15||| serves as a specification for reverse.
17||| serves as a specification for reverse.
@@ -26,10 +28,10 @@ reverseAppend : (xs, ys : List a) ->
26 reverse (xs ++ ys) = reverse ys ++ reverse xs
28 reverse (xs ++ ys) = reverse ys ++ reverse xs
27reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
29reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
28reverseAppend (x :: xs) ys =
30reverseAppend (x :: xs) ys =
29− trans (trans (reverseCons x (xs ++ ys))
31+ rewrite reverseCons x (xs ++ ys) in
30− (cong {f = \l => l ++ [x]} (reverseAppend xs ys)))
32+ rewrite reverseAppend xs ys in
31− (sym (trans (cong (reverseCons x xs))
33+ rewrite reverseCons x xs in
32− (appendAssociative (reverse ys) (reverse xs) [x])))
34+ sym $ appendAssociative (reverse ys) (reverse xs) [x]
34||| Reversing a singleton list is a no-op.
36||| Reversing a singleton list is a no-op.
35reverseSingletonId : (x : a) -> reverse [x] = [x]
37reverseSingletonId : (x : a) -> reverse [x] = [x]
@@ -39,6 +41,6 @@ reverseSingletonId _ = Refl
39reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
41reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
40reverseReverseId [] = Refl
42reverseReverseId [] = Refl
41reverseReverseId (x :: xs) =
43reverseReverseId (x :: xs) =
42− trans (cong (reverseCons x xs))
44+ rewrite reverseCons x xs in
43− (trans (reverseAppend (reverse xs) [x])
45+ rewrite reverseAppend (reverse xs) [x] in
44− (cong (reverseReverseId xs)))
46+ cong $ reverseReverseId xs