Basic properties of lists
mem
length
set-theoretic notation of lists
bounded quantifiers over lists
list subset
append
repeat
pure
bind
concat
reverse
is_nil
init
last
last'
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.
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
- list.bidirectional_rec H0 H1 Hn (a :: b :: l) = let l' : list α := (b :: l).init, b' : α := (b :: l).last _ in _.mpr (Hn a l' b' (list.bidirectional_rec H0 H1 Hn l'))
- list.bidirectional_rec H0 H1 Hn [a] = H1 a
- list.bidirectional_rec H0 H1 Hn list.nil = H0
Like bidirectional_rec
, but with the list parameter placed first.
Equations
- l.bidirectional_rec_on H0 H1 Hn = list.bidirectional_rec H0 H1 Hn l
sublists
Equations
- (a :: l₁).decidable_sublist (b :: l₂) = dite (a = b) (λ (h : a = b), decidable_of_decidable_of_iff (l₁.decidable_sublist l₂) _) (λ (h : ¬a = b), decidable_of_decidable_of_iff ((a :: l₁).decidable_sublist l₂) _)
- (a :: l₁).decidable_sublist list.nil = is_false _
- list.nil.decidable_sublist (hd :: tl) = is_true _
- list.nil.decidable_sublist list.nil = is_true list.decidable_sublist._main._proof_1
index_of
nth element
If one has nth_le 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
.
map₂
take, drop
foldl, foldr
mfoldl, mfoldr, mmap
prod and sum
A list with sum not zero must have positive length.
A list with positive sum must have positive length.
join
In a join, taking the first elements up to an index which is the sum of the lengths of the
first i
sublists, is the same as taking the join of the first i
sublists.
In a join, dropping all the elements up to an index which is the sum of the lengths of the
first i
sublists, is the same as taking the join after dropping the first i
sublists.
Taking only the first i+1
elements in a list, and then dropping the first i
ones, one is
left with a list of length 1
made of the i
-th element of the original list.