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, operation 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.
Preliminaries #
cons #
Equations
Instances For
length #
Instances For
L[i] and L[i]? #
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]
.
If one has l.get i
in an expression (with i : Fin l.length
) and h : l = l'
,
rw [h]
will give a "motive it 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]
.
mem #
any / all #
set #
Lexicographic ordering #
foldlM and foldrM #
foldl and foldr #
getD #
getLast #
getLast? #
Head and tail #
head #
tail #
Basic operations #
map #
filter #
Equations
Instances For
Equations
Instances For
filterMap #
append #
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
.
join #
bind #
replicate #
reverse #
List membership #
elem / contains #
Sublists #
take and drop #
Further results on List.take
and List.drop
, which rely on stronger automation in Nat
,
are given in Init.Data.List.TakeDrop
.
takeWhile and dropWhile #
partition #
dropLast #
dropLast
is the specification for Array.pop
, so theorems about List.dropLast
are often used for theorems about Array.pop
.
isPrefixOf #
isSuffixOf #
rotateLeft #
rotateRight #
Manipulating elements #
replace #
insert #
erase #
find? #
findSome? #
lookup #
Logic #
any / all #
Zippers #
zip #
See also List.zip_replicate
in Init.Data.List.TakeDrop
for a generalization with different lengths.
zipWith #
Equations
Instances For
See also List.zipWith_replicate
in Init.Data.List.TakeDrop
for a generalization with different lengths.
zipWithAll #
Equations
Instances For
unzip #
Ranges and enumeration #
enumFrom #
enum #
Minima and maxima #
minimum? #
maximum? #
Monadic operations #
mapM #
Alternate (non-tail-recursive) form of mapM for proofs.
Equations
- List.mapM' f [] = pure []
- List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)