Theorems about List
operations. #
For each List
operation, we would like theorems describing the following, when relevant:
- if it is a "convenience" function, a
@[simp]
lemma reducing it to more basic operations (e.g.List.partition_eq_filter_filter
), and otherwise: - any special cases of equational lemmas that require additional hypotheses
- lemmas for special cases of the arguments (e.g.
List.map_id
) - the length of the result
(f L).length
- the
i
-th element, described via(f L)[i]
and/or(f L)[i]?
(these should typically be@[simp]
) - consequences for
f L
of the factx ∈ L
orx ∉ L
- conditions characterising
x ∈ f L
(often but not always@[simp]
) - injectivity statements, or congruence statements of the form
p L M → f L = f M
. - conditions characterising the result, i.e. of the form
f L = M ↔ p M
for some predicatep
, along with special cases ofM
(e.g.List.append_eq_nil : L ++ M = [] ↔ L = [] ∧ M = []
) - negative characterisations are also useful, e.g.
List.cons_ne_nil
- interactions with all previously described
List
operations where possible (some of these should be@[simp]
, particularly if the result can be described by a single operation) - characterising
(∀ (i) (_ : i ∈ f L), P i)
, for some predicateP
Of course for any individual operation, not all of these will be relevant or helpful, so some judgement is required.
General principles for simp
normal forms for List
operations:
- Conversion operations (e.g.
toArray
, orlength
) should be moved inwards aggressively, to make the conversion effective. - Similarly, operations which work on elements should be moved inwards in preference to
"structural" operations on the list, e.g. we prefer to simplify
List.map f (L ++ M) ~> (List.map f L) ++ (List.map f M)
,List.map f L.reverse ~> (List.map f L).reverse
, andList.map f (L.take n) ~> (List.map f L).take n
. - Arithmetic operations are "light", so e.g. we prefer to simplify
drop i (drop j L)
todrop (i + j) L
, rather than the other way round. - Function compositions are "light", so we prefer to simplify
(L.map f).map g
toL.map (g ∘ f)
. - We try to avoid non-linear left hand sides (i.e. with subexpressions appearing multiple times), but this is only a weak preference.
- Generally, we prefer that the right hand side does not introduce duplication, however generally duplication of higher order arguments (functions, predicates, etc) is allowed, as we expect to be able to compute these once they reach ground terms.
See also
Init.Data.List.Attach
for definitions and lemmas aboutList.attach
andList.pmap
.Init.Data.List.Count
for lemmas aboutList.countP
andList.count
.Init.Data.List.Erase
for lemmas aboutList.eraseP
andList.erase
.Init.Data.List.Find
for lemmas aboutList.find?
,List.findSome?
,List.findIdx
,List.findIdx?
, andList.indexOf
Init.Data.List.MinMax
for lemmas aboutList.min?
andList.max?
.Init.Data.List.Pairwise
for lemmas aboutList.Pairwise
andList.Nodup
.Init.Data.List.Sublist
for lemmas aboutList.Subset
,List.Sublist
,List.IsPrefix
,List.IsSuffix
, andList.IsInfix
.Init.Data.List.TakeDrop
for additional lemmas aboutList.take
andList.drop
.Init.Data.List.Zip
for lemmas aboutList.zip
,List.zipWith
,List.zipWithAll
, andList.unzip
.
Further results, which first require developing further automation around Nat
, appear in
Init.Data.List.Nat.Basic
: miscellaneous lemmasInit.Data.List.Nat.Range
:List.range
andList.enum
Init.Data.List.Nat.TakeDrop
:List.take
andList.drop
Also
Init.Data.List.Monadic
for addiation lemmas aboutList.mapM
andList.forM
.
Preliminaries #
nil #
length #
cons #
L[i] and L[i]? #
get
and get?
. #
We simplify l.get i
to l[i.1]'i.2
and l.get? i
to l[i]?
.
getD #
We simplify away getD
, replacing getD l n a
with (l[n]?).getD a
.
Because of this, there is only minimal API for getD
.
get! #
We simplify l.get! n
to l[n]!
.
getElem! #
We simplify l[n]!
to (l[n]?).getD default
.
getElem? and getElem #
If one has l[i]
in an expression and h : l = l'
,
rw [h]
will give a "motive it not type correct" error, as it cannot rewrite the
implicit i < l.length
to i < l'.length
directly. The theorem getElem_of_eq
can be used to make
such a rewrite, with rw [getElem_of_eq h]
.
mem #
isEmpty
#
any / all #
set #
This differs from getElem?_set_self
by monadically mapping Function.const _ a
over the Option
returned by l[i]?
.
This differs from getElem?_set
by monadically mapping Function.const _ a
over the Option
returned by l[j]
?
BEq #
Lexicographic ordering #
foldlM and foldrM #
foldl and foldr #
Instances For
Equations
Instances For
Prove a proposition about the result of List.foldl
,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in Sort _
, so this may be used to construct data,
as well as to prove propositions.
Equations
- List.foldlRecOn [] x✝³ x✝² x✝¹ x✝ = x✝¹
- List.foldlRecOn (hd :: tl) x✝³ x✝² x✝¹ x✝ = List.foldlRecOn tl x✝³ (x✝³ x✝² hd) (x✝ x✝² x✝¹ hd ⋯) fun (y : β) (hy : motive y) (x : α) (hx : x ∈ tl) => x✝ y hy x ⋯
Instances For
Prove a proposition about the result of List.foldr
,
by proving it for the initial data,
and the implication that the operation applied to any element of the list preserves the property.
The motive can take values in Sort _
, so this may be used to construct data,
as well as to prove propositions.
Equations
- List.foldrRecOn [] x✝³ x✝² x✝¹ x✝ = x✝¹
- List.foldrRecOn (x_5 :: l) x✝³ x✝² x✝¹ x✝ = x✝ (List.foldr x✝³ x✝² l) (List.foldrRecOn l x✝³ x✝² x✝¹ fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => x✝ b c a ⋯) x_5 ⋯
Instances For
We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.
We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.
getLast #
getLast? #
getLast! #
Head and tail #
head #
headD #
simp
unfolds headD
in terms of head?
and Option.getD
.
tailD #
simp
unfolds tailD
in terms of tail?
and Option.getD
.
tail #
Basic operations #
map #
map_id_fun'
differs from map_id_fun
by representing the identity function as a lambda, rather than id
.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
filter #
Equations
Instances For
Instances For
Equations
Instances For
Instances For
Equations
Instances For
filterMap #
Instances For
append #
Variant of append_inj_right
instead requiring equality of the lengths of the second lists.
Variant of append_inj_left
instead requiring equality of the lengths of the second lists.
Instances For
Equations
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
Instances For
Equations
Instances For
concat #
Note that concat_eq_append
is a @[simp]
lemma, so concat
should usually not appear in goals.
As such there's no need for a thorough set of lemmas describing concat
.
Equations
Instances For
flatten #
flatMap #
Equations
Instances For
Equations
Instances For
replicate #
Instances For
Equations
Instances For
Variant of map_const
using a lambda rather than Function.const
.
Instances For
Every list is either empty, a non-empty replicate
, or begins with a non-empty replicate
followed by a different element.
An induction principle for lists based on contiguous runs of identical elements.
reverse #
Variant of getElem?_reverse
with a hypothesis giving the linear relation between the indices.
Instances For
Instances For
Further results about getLast
and getLast?
#
Additional operations #
leftpad #
List membership #
elem / contains #
Sublists #
partition #
Because we immediately simplify partition
into two filter
s for verification purposes,
we do not separately develop much theory about it.
dropLast #
dropLast
is the specification for Array.pop
, so theorems about List.dropLast
are often used for theorems about Array.pop
.
splitAt #
We don't provide any API for splitAt
, beyond the @[simp]
lemma
splitAt n l = (l.take n, l.drop n)
,
which is proved in Init.Data.List.TakeDrop
.
Manipulating elements #
replace #
insert #
Logic #
any / all #
Equations
Instances For
Equations
Instances For
Legacy lemmas about get
, get?
, and get!
. #
Hopefully these should not be needed, in favour of lemmas about xs[i]
, xs[i]?
, and xs[i]!
,
to which these simplify.
We may consider deprecating or downstreaming these lemmas.
If one has l.get i
in an expression (with i : Fin l.length
) and h : l = l'
,
rw [h]
will give a "motive is not type correct" error, as it cannot rewrite the
i : Fin l.length
to Fin l'.length
directly. The theorem get_of_eq
can be used to make
such a rewrite, with rw [get_of_eq h]
.