Basic properties of lists #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
mem #
Alias of List.append_of_mem
.
See also eq_append_cons_of_mem
, which proves a stronger version
in which the initial list must not contain the element.
length #
Alias of the reverse direction of List.length_pos
.
set-theoretic notation of lists #
Equations
- List.instInsertOfDecidableEq_mathlib = { insert := List.insert }
Equations
- ⋯ = ⋯
bounded quantifiers over lists #
list subset #
append #
replicate #
pure #
bind #
concat #
reverse #
empty #
Alias of List.isEmpty_iff
.
getLast #
If the last element of l
does not satisfy p
, then it is also the last element of
l.filter p
.
getLast? #
Alias of List.getLast?_eq_none_iff
.
Alias of List.getLast?_eq_none_iff
.
Alias of List.getLast?_eq_none_iff
.
head(!?) and tail #
Induction from the right #
Induction principle from the right for lists: if a property holds for the empty list, and
for l ++ [a]
if it holds for l
, then it holds for all lists. The principle is given for
a Sort
-valued predicate, i.e., it can also be used to construct data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bidirectional induction principle for lists: if a property holds for the empty list, the
singleton list, and a :: (l ++ [b])
from l
, then it holds for all lists. This can be used to
prove statements about palindromes. The principle is given for a Sort
-valued predicate, i.e., it
can also be used to construct data.
Equations
- One or more equations did not get rendered due to their size.
- List.bidirectionalRec nil singleton cons_append [] = nil
- List.bidirectionalRec nil singleton cons_append [a] = singleton a
Instances For
Like bidirectionalRec
, but with the list parameter placed first.
Equations
- l.bidirectionalRecOn H0 H1 Hn = List.bidirectionalRec H0 H1 Hn l
Instances For
sublists #
Alias of List.cons_sublist_cons
.
Alias of List.sublist_nil
.
indexOf #
nth element #
Alias of List.eraseIdx_eq_modifyNthTail
.
map #
A single List.map
of a composition of functions is equal to
composing a List.map
with another List.map
, fully applied.
This is the reverse direction of List.map_map
.
zipWith #
take, drop #
foldl, foldr #
Consider two lists l₁
and l₂
with designated elements a₁
and a₂
somewhere in them:
l₁ = x₁ ++ [a₁] ++ z₁
and l₂ = x₂ ++ [a₂] ++ z₂
.
Assume the designated element a₂
is present in neither x₁
nor z₁
.
We conclude that the lists are equal (l₁ = l₂
) if and only if their respective parts are equal
(x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
).
foldlM, foldrM, mapM #
intersperse #
splitAt and splitOn #
Alias of List.splitAt_eq
.
The original list L
can be recovered by joining the lists produced by splitOnP p L
,
interspersed with the elements L.filter p
.
When a list of the form [...xs, sep, ...as]
is split on p
, the first element is xs
,
assuming no element in xs
satisfies p
but sep
does satisfy p
intercalate [x]
is the left inverse of splitOn x
splitOn x
is the left inverse of intercalate [x]
, on the domain
consisting of each nonempty list of lists ls
whose elements do not contain x
modifyLast #
map for partial functions #
Alias of List.attach_map_coe
.
Alias of List.attach_map_val
.
find #
lookmap #
filter #
filterMap #
filter #
Alias of List.dropWhile_get_zero_not
.
erasep #
erase #
diff #
map₂Left' #
map₂Right' #
zipLeft' #
zipRight' #
map₂Left #
map₂Right #
zipLeft #
zipRight #
Forall #
Equations
- List.instDecidablePredForall p x = decidable_of_iff' (∀ (x_1 : α), x_1 ∈ x → p x_1) ⋯
Miscellaneous lemmas #
The images of disjoint lists under a partially defined map are disjoint
The images of disjoint lists under an injective map are disjoint
Alias of List.disjoint_map
.
The images of disjoint lists under an injective map are disjoint