bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law true_and_symTrue is a left identity for and: true and a is a, reversed to rewrite toward the simple side.
- law and_false_symFalse absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.
- law false_and_symFalse absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.
- law or_false_symFalse is a right identity for or: a or false is a, reversed to rewrite toward the simple side.
- law false_or_symFalse is a left identity for or: false or a is a, reversed to rewrite toward the simple side.
- law or_true_symTrue absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.
- law true_or_symTrue absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.
- law de_morgan_and_symDe Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.
- law de_morgan_or_symDe Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.
- law and_self_symAnd with itself: a and a is a, reversed to rewrite toward the simple side.
- law or_self_symOr with itself: a or a is a, reversed to rewrite toward the simple side.
- law and_not_self_symA boolean and its negation are never both true: a and (not a) is false, reversed to rewrite toward the simple side.
- law or_not_self_symA boolean or its negation is always true: a or (not a) is true, reversed to rewrite toward the simple side.
- law and_or_distrib_left_symAnd distributes over or: a and (b or c) is (a and b) or (a and c), reversed to rewrite toward the simple side.
- law or_and_distrib_left_symOr distributes over and: a or (b and c) is (a or b) and (a or c), reversed to rewrite toward the simple side.
- law and_or_absorb_symAbsorption: a and (a or b) is a, reversed to rewrite toward the simple side.
- law or_and_absorb_symAbsorption: a or (a and b) is a, reversed to rewrite toward the simple side.
- law xor_comm_symExclusive or is commutative, reversed to rewrite toward the simple side.
- law xor_assoc_symExclusive or is associative, reversed to rewrite toward the simple side.
- law xor_self_symA boolean xor itself is false, reversed to rewrite toward the simple side.
- law xor_false_symFalse is an identity for xor: a xor false is a, reversed to rewrite toward the simple side.
- law xor_true_symXor with true negates: a xor true is not a, reversed to rewrite toward the simple side.
- law cmp_refl_symComparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.
- law cong2Applying a two-argument function to equal arguments gives equal results.
- law substIf a equals b, any property of a is also a property of b.
- law trans3Equality chains through three steps: a = b, b = c and c = d give a = d.
- law cong_succEqual naturals have equal successors.
- law append_nilThe empty list is a right identity for append: xs ++ [] = xs.
- law nil_appendThe empty list is a left identity for append: [] ++ xs = xs.
- law append_assocAppend is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
- law length_appendThe length of an append is the sum of the lengths.
- def internal_reverse_go_append
- law reverse_go_specThe reverse accumulator loop appends the reversed list to the accumulator.
- def internal_reverse_append_go
- law reverse_appendReversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.
- def internal_reverse_go_go
- law reverse_reverseReversing twice gives the list back.
- def internal_length_reverse_go
- law length_reverseReversing preserves the length.
- law foldr_appendA right fold over an append folds the first part onto the fold of the second.
- law take_append_dropTaking n elements and appending the rest after dropping n gives the list back.
- law length_mapMapping preserves the length.
- law map_appendMapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.
- law map_mapMapping twice is mapping the composition: map g (map f xs) = map (g .
- law take_zeroTaking zero elements gives the empty list.
- law drop_zeroDropping zero elements gives the list back.
- law take_nilTaking from the empty list gives the empty list.
- law drop_nilDropping from the empty list gives the empty list.
- law length_takeTaking n elements leaves min(n, length) of them.
- law length_dropDropping n elements leaves length - n of them.
- law take_lengthTaking as many elements as the list has gives the list back.
- law drop_lengthDropping as many elements as the list has gives the empty list.
- law take_takeTaking m from the first n is taking min(n, m).
- law drop_dropDropping m after dropping n is dropping n + m.
- law reverse_nilReversing the empty list gives the empty list.
- law reverse_singletonReversing a one-element list gives it back.
- law length_replicateReplicating x n times gives a list of length n.
- def internal_length_range_go
- law length_rangeRange(n) has length n.
- law length_zipA zip is as long as the shorter of the two lists.
- law append_consAppending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).
- law length_nilThe empty list has length zero.
- law length_consA cons is one longer than its tail.
- law concat_appendConcatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.
- law foldl_appendA left fold over an append folds the second part from the fold of the first.
- def internal_map_reverse_go
- law map_reverseMapping commutes with reversing: map f (reverse xs) = reverse (map f xs).
- def internal_all_ifBase 2.0.38 short-circuits each through a thunk (List.all.if, List.any.if, List.find.if), so the cons step is proved by cases on the head's test.
- def internal_any_if
- def internal_find_putWhat List.find does with its head: Some{h} on a hit, else the rest (Base until 2.0.37 had it as List.find.put).
- def internal_find_if
- def internal_all_consThe cons case of all, any, find and contains as lemmas, so a change to their Base definitions stays in one place (PLAN F39).
- def internal_all_cons_testThe cons case of all with the head's test given as a value, for a head that cannot be used twice (a pair under a predicate that reads both parts).
- def internal_any_cons
- def internal_find_cons
- def internal_any_cons_test
- def internal_contains_cons
- def internal_all_if_andThe cons step of all_append, any_append and contains_append, given the step for the tail; proved by cases on the head's test.
- def internal_any_if_or
- def internal_all_cons_and
- def internal_any_cons_or
- def internal_contains_cons_or
- law all_appendAll over an append is all over each part, joined by and.
- law any_appendAny over an append is any over each part, joined by or.
- def internal_filter_put_append
- law filter_appendFiltering an append filters each part.
- law contains_appendAn append contains x iff either part does.
- def internal_length_filter_put_le
- law length_filter_leFiltering never makes a list longer.
- def memMembership in a list, as a reusable proposition.
- def sorted_byA list is sorted by a comparator when every adjacent pair is in order.
- def internal_or_of_right
- def internal_or_of_or
- def internal_and_left
- def internal_and_right
- def internal_mem_append_left
- def internal_mem_append_right
- law mem_cons_selfThe head of a Nat list is a member of it (membership by Nat.is_eq).
- law mem_cons_of_memA member of a Nat list stays a member when a head is prepended.
- law not_mem_nilNo Nat is a member of the empty list.