IdrisDoc: Data.List.Reverse

Data.List.Reverse

Properties of the reverse function.

data Palindrome : (xs : List a) -> Type

Do geese see God?

Empty : Palindrome []
Single : Palindrome [x]
Multi : Palindrome xs -> Palindrome ([x] ++ xs ++ [x])
palindromeReverse : (xs : List a) -> Palindrome xs -> reverse xs = xs

A Palindrome reversed is itself.

reverseAppend : (xs : List a) -> (ys : List a) -> reverse (xs ++ ys) = reverse ys ++ reverse xs

Reversing an append is appending reversals backwards.

reverseCons : (x : a) -> (xs : List a) -> reverse (x :: xs) = reverse xs ++ [x]

The reverse of a cons is the reverse of the tail followed by the head.
Together with reverseNil serves as a specification for reverse.

reverseEqual : (xs : List a) -> (ys : List a) -> (reverse xs = reverse ys) -> xs = ys

Equal reversed lists are equal.

reverseEquiv : (xs : List a) -> reverseRec xs = reverse xs

The iterative and recursive defintions of reverse are the same.

reverseLength : (xs : List a) -> length (reverse xs) = length xs

Reversing preserves list length.

reverseNil : reverse [] = []

The reverse of an empty list is an empty list. Together with reverseCons,
serves as a specification for reverse.

reverseOntoAcc : (xs : List a) -> (ys : List a) -> (zs : List a) -> reverseOnto (ys ++ zs) xs = reverseOnto ys xs ++ zs

The final segment of the accumulator is the final segment of the result.

reverseOntoLength : (xs : List a) -> (acc : List a) -> length (reverseOnto acc xs) = length acc + length xs

Reversing onto preserves list length.

reverseOntoSpec : (xs : List a) -> (ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

Serves as a specification for reverseOnto.

reversePalindrome : (xs : List a) -> (reverse xs = xs) -> Palindrome xs

Only Palindromes are equal to their own reverse.

reverseRec : List a -> List a

A recursive definition of reverse.

reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs

Reversing a reverse gives the original.

reverseSingletonId : (x : a) -> reverse [x] = [x]

Reversing a singleton list is a no-op.