list.bend checks

The empty list is a right identity for append: xs ++ [] = xs.

The empty list is a left identity for append: [] ++ xs = xs.

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).

The length of an append is the sum of the lengths.

The reverse accumulator loop appends the reversed list to the accumulator.

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.

Reversing twice gives the list back.

Reversing preserves the length.

A right fold over an append folds the first part onto the fold of the second.

Taking n elements and appending the rest after dropping n gives the list back.

Mapping preserves the length.

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.

Taking zero elements gives the empty list.

Dropping zero elements gives the list back.

Taking from the empty list gives the empty list.

Dropping from the empty list gives the empty list.

Taking n elements leaves min(n, length) of them.

Dropping n elements leaves length - n of them.

Taking as many elements as the list has gives the list back.

Dropping as many elements as the list has gives the empty list.

Taking m from the first n is taking min(n, m).

Dropping m after dropping n is dropping n + m.

Reversing the empty list gives the empty list.

Reversing a one-element list gives it back.

Replicating x n times gives a list of length n.

Range(n) has length n.

Zipping two lists gives the length of the shorter one.

Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).

The empty list has length zero.

A cons is one longer than its tail.

Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.

A left fold over an append folds the second part from the fold of the first.

Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).

All over an append is all over each part, joined by and.

Any over an append is any over each part, joined by or.

Filtering an append filters each part.

An append contains x iff either part does.

Filtering never makes a list longer.

The head of a cons is a member of it.

Membership is preserved when a new head is prepended.

Nothing is a member of the empty list.

Membership on the left of an append.

Membership on the right of an append.

The empty list is sorted by any comparator.

A singleton list is sorted by any comparator.

A sorted tail with an in-order head is sorted.

The head pair of a sorted cons-cons list is in order.

The tail of a sorted cons-cons list is sorted.

A sorted list has a sorted tail.

Taking the length of the first part of an append gives the first part back.

Dropping the length of the first part of an append gives the second part.

Taking past the first part of an append keeps it and takes the rest from the second part.

Dropping past the first part of an append drops the rest from the second part.

Taking at most the length of the first part of an append only sees the first part.

Dropping at most the length of the first part of an append drops only from the first part.

Mapping commutes with taking: map f (take n xs) = take n (map f xs).

Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs).

Taking m from n copies of x gives min(m, n) copies of x.

Dropping m from n copies of x gives n - m copies of x.

Taking n elements gives at most n of them.

The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1.

Mapping the identity gives the list back.

A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs.

A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs.

Replicating m + n times appends m copies to n copies.

Reversing n copies of x gives them back.

Filtering with an always-true predicate gives the list back.

Filtering with an always-false predicate gives the empty list.

Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs.

All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs.

Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs.

All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs.

Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs.

Reversing does not change whether all elements satisfy a predicate.

Reversing does not change whether some element satisfies a predicate.

Reversing does not change whether a list contains x.

The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.

The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.

The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.

The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.

Reversing twice gives the list back, reversed to rewrite toward the simple side.

Reversing preserves the length, reversed to rewrite toward the simple side.

A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.

Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.

Mapping preserves the length, reversed to rewrite toward the simple side.

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.

Taking zero elements gives the empty list, reversed to rewrite toward the simple side.

Dropping zero elements gives the list back, reversed to rewrite toward the simple side.

Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.

Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.

Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.

Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.

Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.

Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.

Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.

Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.

Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.

Reversing a one-element list gives it back, reversed to rewrite toward the simple side.

Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.

Range(n) has length n, reversed to rewrite toward the simple side.

Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side.

Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.

The empty list has length zero, reversed to rewrite toward the simple side.

A cons is one longer than its tail, reversed to rewrite toward the simple side.

Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.

A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.

Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.

All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.

Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.

Filtering an append filters each part, reversed to rewrite toward the simple side.

An append contains x iff either part does, reversed to rewrite toward the simple side.

Filtering never makes a list longer, reversed to rewrite toward the simple side.

Taking the length of the first part of an append gives the first part back, reversed to rewrite toward the simple side.

Dropping the length of the first part of an append gives the second part, reversed to rewrite toward the simple side.

Taking past the first part of an append keeps it and takes the rest from the second part, reversed to rewrite toward the simple side.

Dropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side.

Taking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side.

Dropping at most the length of the first part of an append drops only from the first part, reversed to rewrite toward the simple side.

Mapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side.

Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side.

Taking m from n copies of x gives min(m, n) copies of x, reversed to rewrite toward the simple side.

Dropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side.

The tail is one shorter than the list, or empty: length (tail xs) = length xs - 1, reversed to rewrite toward the simple side.

Mapping the identity gives the list back, reversed to rewrite toward the simple side.

A right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g . f) z xs, reversed to rewrite toward the simple side.

A left fold over a map folds with the mapped function: foldl g z (map f xs) = foldl (fun acc x => g acc (f x)) z xs, reversed to rewrite toward the simple side.

Replicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side.

Reversing n copies of x gives them back, reversed to rewrite toward the simple side.

Filtering with an always-true predicate gives the list back, reversed to rewrite toward the simple side.

Filtering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side.

Filtering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs, reversed to rewrite toward the simple side.

All over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs, reversed to rewrite toward the simple side.

Any over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs, reversed to rewrite toward the simple side.

All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs, reversed to rewrite toward the simple side.

Any over a map checks the composed predicate: any p (map f xs) = any (p . f) xs, reversed to rewrite toward the simple side.

Reversing does not change whether all elements satisfy a predicate, reversed to rewrite toward the simple side.

Reversing does not change whether some element satisfies a predicate, reversed to rewrite toward the simple side.

Reversing does not change whether a list contains x, reversed to rewrite toward the simple side.

Membership in a list, as a reusable proposition.

A list is sorted by a comparator when every adjacent pair is in order.