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 Nat list is a member of it (membership by Nat.is_eq).

A member of a Nat list stays a member when a head is prepended.

No Nat is a member of the empty list.

A member of xs is a member of xs ++ ys (Nat lists).

A member of ys is a member of xs ++ ys (Nat lists).

The empty Nat list is sorted by Nat.is_le.

A one-element Nat list is sorted by Nat.is_le.

A Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element.

The first two elements of a Nat list sorted by Nat.is_le are in order.

The tail of a Nat list of two or more elements sorted by Nat.is_le is sorted.

The tail of a nonempty Nat list sorted by Nat.is_le is sorted.

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.

Zipping the empty list with anything gives the empty list.

Zipping anything with the empty list gives the empty list.

The head of a cons is its first element.

The head of an append is the head of the first part, or else of the second.

The head of a map is the mapped head.

The tail of a map is the map of the tail.

The element at index zero of a cons is its head.

The element at index n + 1 of a cons is the element at index n of its tail.

Indexing a map is mapping the indexed element.

Setting an element does not change the length.

Reading the index just set gives the new value wherever the index is in range.

The last element of xs ++ [x] is x.

The head of the reverse is the last element.

The last element of the reverse is the head.

A list is empty exactly when its length is zero.

An append is empty exactly when both parts are.

The reverse is empty exactly when the list is.

A map is empty exactly when the list is.

Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs).

Folding cons from the right, starting from the empty list, rebuilds the list.

A left fold over the reverse is a right fold with the arguments flipped.

A right fold over the reverse is a left fold with the arguments flipped.

Range(n + 1) is range(n) followed by n.

Finding in an append finds in the first part, or else in the second.

All elements satisfy f exactly when no element fails it.

Some element satisfies f exactly when not all elements fail it.

A one-element list has length one.

Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x].

Taking n + 1 elements of a cons keeps its head and takes n from its tail.

Dropping n + 1 elements of a cons drops its head and n from its tail.

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.

Zipping the empty list with anything gives the empty list, reversed to rewrite toward the simple side.

Zipping anything with the empty list gives the empty list, reversed to rewrite toward the simple side.

The head of a cons is its first element, reversed to rewrite toward the simple side.

The head of an append is the head of the first part, or else of the second, reversed to rewrite toward the simple side.

The head of a map is the mapped head, reversed to rewrite toward the simple side.

The tail of a map is the map of the tail, reversed to rewrite toward the simple side.

The element at index zero of a cons is its head, reversed to rewrite toward the simple side.

The element at index n + 1 of a cons is the element at index n of its tail, reversed to rewrite toward the simple side.

Indexing a map is mapping the indexed element, reversed to rewrite toward the simple side.

Setting an element does not change the length, reversed to rewrite toward the simple side.

Reading the index just set gives the new value wherever the index is in range, reversed to rewrite toward the simple side.

The last element of xs ++ [x] is x, reversed to rewrite toward the simple side.

The head of the reverse is the last element, reversed to rewrite toward the simple side.

The last element of the reverse is the head, reversed to rewrite toward the simple side.

A list is empty exactly when its length is zero, reversed to rewrite toward the simple side.

An append is empty exactly when both parts are, reversed to rewrite toward the simple side.

The reverse is empty exactly when the list is, reversed to rewrite toward the simple side.

A map is empty exactly when the list is, reversed to rewrite toward the simple side.

Filtering commutes with reversing: filter p (reverse xs) = reverse (filter p xs), reversed to rewrite toward the simple side.

Folding cons from the right, starting from the empty list, rebuilds the list, reversed to rewrite toward the simple side.

A left fold over the reverse is a right fold with the arguments flipped, reversed to rewrite toward the simple side.

A right fold over the reverse is a left fold with the arguments flipped, reversed to rewrite toward the simple side.

Range(n + 1) is range(n) followed by n, reversed to rewrite toward the simple side.

Finding in an append finds in the first part, or else in the second, reversed to rewrite toward the simple side.

All elements satisfy f exactly when no element fails it, reversed to rewrite toward the simple side.

Some element satisfies f exactly when not all elements fail it, reversed to rewrite toward the simple side.

A one-element list has length one, reversed to rewrite toward the simple side.

Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x], reversed to rewrite toward the simple side.

Taking n + 1 elements of a cons keeps its head and takes n from its tail, reversed to rewrite toward the simple side.

Dropping n + 1 elements of a cons drops its head and n from its tail, 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.