bend-mathlib

Search uses release 0.8.1.0 · 1,126 definitions

Releases (15)

0.8.1.0 indexed
0.8.0.0 unindexed
0.7.5.0 unindexed
0.7.4.0 unindexed
0.7.3.0 unindexed
0.7.2.0 unindexed
0.7.1.0 unindexed
0.7.0.0 unindexed
0.6.0.0 unindexed
0.5.0.0 unindexed
0.4.0.0 unindexed
0.3.0.0 unindexed
0.2.0.0 unindexed
0.1.0.1 unindexed
0.1.0.0 unindexed

Definitions (1,126)

list.bend

law all_eq_not_any_notAll elements satisfy f exactly when no element fails it.
def internal_or_not_eq_not_and_not
def internal_any_eq_not_all_not
law any_eq_not_all_notSome element satisfies f exactly when not all elements fail it.
law length_singletonA one-element list has length one.
law reverse_consReversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x].
law take_succTaking n + 1 elements of a cons keeps its head and takes n from its tail.
law drop_succDropping n + 1 elements of a cons drops its head and n from its tail.
law append_nil_symThe empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.
law nil_append_symThe empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.
law append_assoc_symAppend is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.
law length_append_symThe length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
law reverse_go_spec_symThe reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.
law reverse_append_symReversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
law reverse_reverse_symReversing twice gives the list back, reversed to rewrite toward the simple side.
law length_reverse_symReversing preserves the length, reversed to rewrite toward the simple side.
law foldr_append_symA right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.
law take_append_drop_symTaking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.
law length_map_symMapping preserves the length, reversed to rewrite toward the simple side.
law map_append_symMapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
law map_map_symMapping twice is mapping the composition: map g (map f xs) = map (g .
law take_zero_symTaking zero elements gives the empty list, reversed to rewrite toward the simple side.
law drop_zero_symDropping zero elements gives the list back, reversed to rewrite toward the simple side.
law take_nil_symTaking from the empty list gives the empty list, reversed to rewrite toward the simple side.
law drop_nil_symDropping from the empty list gives the empty list, reversed to rewrite toward the simple side.
law length_take_symTaking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.
law length_drop_symDropping n elements leaves length - n of them, reversed to rewrite toward the simple side.
law take_length_symTaking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.
law drop_length_symDropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.
law take_take_symTaking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.
law drop_drop_symDropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.
law reverse_nil_symReversing the empty list gives the empty list, reversed to rewrite toward the simple side.
law reverse_singleton_symReversing a one-element list gives it back, reversed to rewrite toward the simple side.
law length_replicate_symReplicating x n times gives a list of length n, reversed to rewrite toward the simple side.
law length_range_symRange(n) has length n, reversed to rewrite toward the simple side.
law length_zip_symA zip is as long as the shorter of the two lists, reversed to rewrite toward the simple side.
law append_cons_symAppending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.
law length_nil_symThe empty list has length zero, reversed to rewrite toward the simple side.
law length_cons_symA cons is one longer than its tail, reversed to rewrite toward the simple side.
law concat_append_symConcatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
law foldl_append_symA left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
law map_reverse_symMapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
law all_append_symAll over an append is all over each part, joined by and, reversed to rewrite toward the simple side.
law any_append_symAny over an append is any over each part, joined by or, reversed to rewrite toward the simple side.
law filter_append_symFiltering an append filters each part, reversed to rewrite toward the simple side.
law contains_append_symAn append contains x iff either part does, reversed to rewrite toward the simple side.
law length_filter_le_symFiltering never makes a list longer, reversed to rewrite toward the simple side.
law take_left_symTaking the length of the first part of an append gives the first part back, reversed to rewrite toward the simple side.
law drop_left_symDropping the length of the first part of an append gives the second part, reversed to rewrite toward the simple side.
law take_append_symTaking past the first part of an append keeps it and takes the rest from the second part, reversed to rewrite toward the simple side.
law drop_append_symDropping past the first part of an append drops the rest from the second part, reversed to rewrite toward the simple side.
law take_append_of_le_length_symTaking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side.
law drop_append_of_le_length_symDropping at most the length of the first part of an append drops only from the first part, reversed to rewrite toward the simple side.
law map_take_symMapping commutes with taking: map f (take n xs) = take n (map f xs), reversed to rewrite toward the simple side.
law map_drop_symMapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side.
law take_replicate_symTaking m from n copies of x gives min(m, n) copies of x, reversed to rewrite toward the simple side.
law drop_replicate_symDropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side.
law length_tail_symThe tail is one shorter than the list, or empty: length (tail xs) = length xs - 1, reversed to rewrite toward the simple side.
law map_id_symMapping the identity gives the list back, reversed to rewrite toward the simple side.
law foldr_map_symA right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g .
law foldl_map_symA 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.
law replicate_add_symReplicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side.
law reverse_replicate_symReversing n copies of x gives them back, reversed to rewrite toward the simple side.
law filter_true_symFiltering with an always-true predicate gives the list back, reversed to rewrite toward the simple side.
law filter_false_symFiltering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side.
law filter_filter_symFiltering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs, reversed to rewrite toward the simple side.
law all_filter_symAll 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.
law any_filter_symAny 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.
law all_map_symAll over a map checks the composed predicate: all p (map f xs) = all (p .
law any_map_symAny over a map checks the composed predicate: any p (map f xs) = any (p .
law all_reverse_symReversing does not change whether all elements satisfy a predicate, reversed to rewrite toward the simple side.
law any_reverse_symReversing does not change whether some element satisfies a predicate, reversed to rewrite toward the simple side.
law contains_reverse_symReversing does not change whether a list contains x, reversed to rewrite toward the simple side.
law zip_nil_left_symZipping the empty list with anything gives the empty list, reversed to rewrite toward the simple side.
law zip_nil_right_symZipping anything with the empty list gives the empty list, reversed to rewrite toward the simple side.
law head_cons_symThe head of a cons is its first element, reversed to rewrite toward the simple side.
law head_append_symThe head of an append is the head of the first part, or else of the second, reversed to rewrite toward the simple side.
law head_map_symThe head of a map is the mapped head, reversed to rewrite toward the simple side.
law tail_map_symThe tail of a map is the map of the tail, reversed to rewrite toward the simple side.
law get_cons_zero_symThe element at index zero of a cons is its head, reversed to rewrite toward the simple side.
law get_cons_succ_symThe element at index n + 1 of a cons is the element at index n of its tail, reversed to rewrite toward the simple side.
law get_map_symIndexing a map is mapping the indexed element, reversed to rewrite toward the simple side.
law length_set_symSetting an element does not change the length, reversed to rewrite toward the simple side.
law get_set_self_symReading the index just set gives the new value wherever the index is in range, reversed to rewrite toward the simple side.
law last_append_singleton_symThe last element of xs ++ [x] is x, reversed to rewrite toward the simple side.
law head_reverse_symThe head of the reverse is the last element, reversed to rewrite toward the simple side.
law last_reverse_symThe last element of the reverse is the head, reversed to rewrite toward the simple side.
law is_empty_iff_length_eq_zero_symA list is empty exactly when its length is zero, reversed to rewrite toward the simple side.
law is_empty_append_symAn append is empty exactly when both parts are, reversed to rewrite toward the simple side.
law is_empty_reverse_symThe reverse is empty exactly when the list is, reversed to rewrite toward the simple side.
law is_empty_map_symA map is empty exactly when the list is, reversed to rewrite toward the simple side.
law filter_reverse_symFiltering commutes with reversing: filter p (reverse xs) = reverse (filter p xs), reversed to rewrite toward the simple side.
law foldr_cons_nil_symFolding cons from the right, starting from the empty list, rebuilds the list, reversed to rewrite toward the simple side.
law foldl_reverse_symA left fold over the reverse is a right fold with the arguments flipped, reversed to rewrite toward the simple side.
law foldr_reverse_symA right fold over the reverse is a left fold with the arguments flipped, reversed to rewrite toward the simple side.
law range_succ_symRange(n + 1) is range(n) followed by n, reversed to rewrite toward the simple side.
law find_append_symFinding in an append finds in the first part, or else in the second, reversed to rewrite toward the simple side.
law all_eq_not_any_not_symAll elements satisfy f exactly when no element fails it, reversed to rewrite toward the simple side.
law any_eq_not_all_not_symSome element satisfies f exactly when not all elements fail it, reversed to rewrite toward the simple side.
law length_singleton_symA one-element list has length one, reversed to rewrite toward the simple side.