Basic properties of lists #
mem #
length #
Alias of the reverse direction of List.length_pos
.
Alias of the forward direction of List.length_pos
.
Alias of List.Sublist.length_le
.
set-theoretic notation of lists #
Equations
- List.instInsertList = { insert := List.insert }
bounded quantifiers over lists #
list subset #
Alias of the forward direction of List.subset_nil
.
append #
replicate #
Alias of the reverse direction of List.eq_replicate_length
.
pure #
bind #
concat #
reverse #
empty #
dropLast #
getLast #
getLast? #
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.
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 H0 H1 Hn [] = H0
- List.bidirectionalRec H0 H1 Hn [a] = H1 a
Like bidirectionalRec
, but with the list parameter placed first.
Equations
- List.bidirectionalRecOn l H0 H1 Hn = List.bidirectionalRec H0 H1 Hn l
sublists #
Equations
- One or more equations did not get rendered due to their size.
- List.decidableSublist [] x = isTrue (_ : List.Sublist [] x)
- List.decidableSublist (head :: tail) [] = isFalse (_ : List.Sublist (head :: tail) [] → List.noConfusionType False (head :: tail) [])
indexOf #
nth element #
A version of get_map
that can be used for rewriting.
A version of nthLe_map
that can be used for rewriting.
If one has nthLe L i hi
in a formula and h : L = L'
, one can not rw h
in the formula as
hi
gives i < L.length
and not i < L'.length
. The lemma nth_le_of_eq
can be used to make
such a rewrite, with rw (nth_le_of_eq h)
.
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 #
Taking the first n
elements in l₁ ++ l₂
is the same as appending the first n
elements
of l₁
to the first n - l₁.length
elements of l₂
.
The i
-th element of a list coincides with the i
-th element of any of its prefixes of
length > i
. Version designed to rewrite from the big list to the small list.
The i
-th element of a list coincides with the i
-th element of any of its prefixes of
length > i
. Version designed to rewrite from the big list to the small list.
The i
-th element of a list coincides with the i
-th element of any of its prefixes of
length > i
. Version designed to rewrite from the small list to the big list.
The i
-th element of a list coincides with the i
-th element of any of its prefixes of
length > i
. Version designed to rewrite from the small list to the big list.
Dropping the elements up to n
in l₁ ++ l₂
is the same as dropping the elements up to n
in l₁
, dropping the elements up to n - l₁.length
in l₂
, and appending them.
The i + j
-th element of a list coincides with the j
-th element of the list obtained by
dropping the first i
elements. Version designed to rewrite from the big list to the small list.
The i + j
-th element of a list coincides with the j
-th element of the list obtained by
dropping the first i
elements. Version designed to rewrite from the big list to the small list.
The i + j
-th element of a list coincides with the j
-th element of the list obtained by
dropping the first i
elements. Version designed to rewrite from the small list to the big list.
The i + j
-th element of a list coincides with the j
-th element of the list obtained by
dropping the first i
elements. Version designed to rewrite from the small list to the big list.
foldl, foldr #
Induction principle for values produced by a foldr
: if a property holds
for the seed element b : β
and for all incremental op : α → β → β→ β → β→ β
performed on the elements (a : α) ∈ l∈ l
. 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.
Induction principle for values produced by a foldl
: if a property holds
for the seed element b : β
and for all incremental op : β → α → β→ α → β→ β
performed on the elements (a : α) ∈ l∈ l
. 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.
foldlM, foldrM, mapM #
intersperse #
splitAt and splitOn #
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 #
Partial map. If f : Π a, p a → β→ β
is a partial function defined on
a : α
satisfying p
, then pmap f l h
is essentially the same as map f l
but is defined only when all members of l
satisfy p
, using the proof
to apply f
.