@@ -3,13 +3,15 @@ module Data.List.Extra
33%default total
44%access export
55
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
11+
612||| Serves as a specification for reverseOnto.
713reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
8−reverseOntoSpec _ [] = Refl
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+reverseOntoSpec xs ys = reverseOntoAcc ys [] xs
1315
1416||| The reverse of an empty list is an empty list. Together with reverseCons,
1517||| serves as a specification for reverse.
@@ -26,10 +28,10 @@ reverseAppend : (xs, ys : List a) ->
2628 reverse (xs ++ ys) = reverse ys ++ reverse xs
2729reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
2830reverseAppend (x :: xs) ys =
29− trans (trans (reverseCons x (xs ++ ys))
30− (cong {f = \l => l ++ [x]} (reverseAppend xs ys)))
31− (sym (trans (cong (reverseCons x xs))
32− (appendAssociative (reverse ys) (reverse xs) [x])))
31+ rewrite reverseCons x (xs ++ ys) in
32+ rewrite reverseAppend xs ys in
33+ rewrite reverseCons x xs in
34+ sym $ appendAssociative (reverse ys) (reverse xs) [x]
3335
3436||| Reversing a singleton list is a no-op.
3537reverseSingletonId : (x : a) -> reverse [x] = [x]
@@ -39,6 +41,6 @@ reverseSingletonId _ = Refl
3941reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
4042reverseReverseId [] = Refl
4143reverseReverseId (x :: xs) =
42− trans (cong (reverseCons x xs))
43− (trans (reverseAppend (reverse xs) [x])
44− (cong (reverseReverseId xs)))
44+ rewrite reverseCons x xs in
45+ rewrite reverseAppend (reverse xs) [x] in
46+ cong $ reverseReverseId xs