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! i
to l[i]!
.
getElem! #
We simplify l[i]!
to (l[i]?).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]?
.
BEq #
isEqv #
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
.
Equations
Instances For
Equations
Instances For
Equations
Instances For
filter #
Equations
Instances For
Equations
Instances For
filterMap #
Equations
Instances For
append #
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
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
.