bend-mathlib
Search uses release 0.8.1.0 · 1,126 definitions
Definitions (1,126)
- law mem_append_leftA member of xs is a member of xs ++ ys (Nat lists).
- law mem_append_rightA member of ys is a member of xs ++ ys (Nat lists).
- law sorted_nilThe empty Nat list is sorted by Nat.is_le.
- law sorted_singleA one-element Nat list is sorted by Nat.is_le.
- def internal_sorted_cons_trueThe step of sorted_by, with a literal pair head so the kernel reduces the predicate (PLAN F39).
- def internal_sorted_cons_false
- def internal_sorted_cons_testThe cons step of sorted_by's pairs with the head written as (x, y): internal_all_cons_test at a variable pair head is outside what --verdict can check.
- law sorted_cons_cons_introA Nat list sorted by Nat.is_le stays sorted under a head that is <= the next element.
- def internal_sorted_tail_step
- law sorted_cons_cons_elim_leThe first two elements of a Nat list sorted by Nat.is_le are in order.
- law sorted_cons_cons_elim_tailThe tail of a Nat list of two or more elements sorted by Nat.is_le is sorted.
- law sorted_tailThe tail of a nonempty Nat list sorted by Nat.is_le is sorted.
- def internal_sorted_take_cons
- law sorted_takeA prefix of a Nat list sorted by Nat.is_le is sorted.
- law sorted_dropA suffix of a Nat list sorted by Nat.is_le is sorted.
- def internal_sorted_skip
- def internal_sorted_filter_cons_put
- def internal_sorted_filter_cons
- def internal_sorted_filter_put
- law sorted_filterFiltering a Nat list sorted by Nat.is_le keeps it sorted.
- def internal_head_le_mem_step
- def internal_head_le_mem
- law sorted_head_le_memThe head of a Nat list sorted by Nat.is_le is <= every member of its tail.
- def internal_le_of_mem_step
- law sorted_le_of_memThe head of a Nat list sorted by Nat.is_le is <= every member of the list.
- def internal_sorted_append_cons
- law sorted_appendAppending two Nat lists sorted by Nat.is_le, with every element of the first <= every element of the second, gives a sorted list.
- law take_leftTaking the length of the first part of an append gives the first part back.
- law drop_leftDropping the length of the first part of an append gives the second part.
- law take_appendTaking past the first part of an append keeps it and takes the rest from the second part.
- law drop_appendDropping past the first part of an append drops the rest from the second part.
- law take_append_of_le_lengthTaking at most the length of the first part of an append only sees the first part.
- law drop_append_of_le_lengthDropping at most the length of the first part of an append drops only from the first part.
- law map_takeMapping commutes with taking: map f (take n xs) = take n (map f xs).
- law map_dropMapping commutes with dropping: map f (drop n xs) = drop n (map f xs).
- law take_replicateTaking m from n copies of x gives min(m, n) copies of x.
- law drop_replicateDropping m from n copies of x gives n - m copies of x.
- law length_take_leTaking n elements gives at most n of them.
- law length_tailThe tail is one shorter than the list, or empty: length (tail xs) = length xs - 1.
- law map_idMapping the identity gives the list back.
- law foldr_mapA right fold over a map folds with the mapped function: foldr g z (map f xs) = foldr (g .
- law foldl_mapA 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.
- law replicate_addReplicating m + n times appends m copies to n copies.
- def internal_replicate_append_nil
- def internal_replicate_append_cons
- def internal_reverse_go_replicate
- law reverse_replicateReversing n copies of x gives them back.
- law filter_trueFiltering with an always-true predicate gives the list back.
- law filter_falseFiltering with an always-false predicate gives the empty list.
- def internal_filter_put_filter
- law filter_filterFiltering twice is filtering by both predicates: filter p (filter q xs) = filter (p and q) xs.
- def internal_all_filter_put
- law all_filterAll over a filter checks q only where p holds: all q (filter p xs) = all (not p or q) xs.
- def internal_any_filter_put
- law any_filterAny over a filter looks for q only where p holds: any q (filter p xs) = any (p and q) xs.
- def internal_all_mapUnfolds List.all directly, so its proof depends on Base's definition (PLAN F39).
- def internal_any_map
- law all_mapAll over a map checks the composed predicate: all p (map f xs) = all (p .
- law any_mapAny over a map checks the composed predicate: any p (map f xs) = any (p .
- def internal_all_reverse_go
- law all_reverseReversing does not change whether all elements satisfy a predicate.
- def internal_any_reverse_go
- law any_reverseReversing does not change whether some element satisfies a predicate.
- def internal_contains_reverse_go
- law contains_reverseReversing does not change whether a list contains x.
- law zip_nil_leftZipping the empty list with anything gives the empty list.
- law zip_nil_rightZipping anything with the empty list gives the empty list.
- law head_consThe head of a cons is its first element.
- law head_appendThe head of an append is the head of the first part, or else of the second.
- law head_mapThe head of a map is the mapped head.
- law tail_mapThe tail of a map is the map of the tail.
- law get_cons_zeroThe element at index zero of a cons is its head.
- law get_cons_succThe element at index n + 1 of a cons is the element at index n of its tail.
- law get_mapIndexing a map is mapping the indexed element.
- law length_setSetting an element does not change the length.
- law get_set_selfReading the index just set gives the new value wherever the index is in range.
- def internal_last_go_append_singleton
- law last_append_singletonThe last element of xs ++ [x] is x.
- def internal_head_reverse_go
- law head_reverseThe head of the reverse is the last element.
- def internal_last_reverse_go
- law last_reverseThe last element of the reverse is the head.
- law is_empty_iff_length_eq_zeroA list is empty exactly when its length is zero.
- law is_empty_appendAn append is empty exactly when both parts are.
- def internal_is_empty_reverse_go
- law is_empty_reverseThe reverse is empty exactly when the list is.
- law is_empty_mapA map is empty exactly when the list is.
- def internal_reverse_filter_put
- law filter_reverseFiltering commutes with reversing: filter p (reverse xs) = reverse (filter p xs).
- law foldr_cons_nilFolding cons from the right, starting from the empty list, rebuilds the list.
- def internal_foldl_reverse_go
- law foldl_reverseA left fold over the reverse is a right fold with the arguments flipped.
- def internal_foldr_reverse_go
- law foldr_reverseA right fold over the reverse is a left fold with the arguments flipped.
- def internal_range_go_append
- law range_succRange(n + 1) is range(n) followed by n.
- def internal_find_put_or
- law find_appendFinding in an append finds in the first part, or else in the second.
- def internal_and_not_eq_not_or_not
- def internal_all_eq_not_any_not