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 #
Equations
Instances For
Equations
Instances For
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]?
.
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]
.
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]!
.
mem #
isEmpty
#
Equations
Instances For
Equations
Instances For
any / all #
set #
This differs from getElem?_set_self
by monadically mapping Function.const _ a
over the Option
returned by l[i]?
.
BEq #
Equations
Instances For
Equations
Instances For
isEqv #
getLast #
getLast? #
getLast! #
Head and tail #
head #
Equations
Instances For
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
.
filter #
Instances For
filterMap #
Variant of filterMap_eq_map
with some ∘ f
expanded out to a lambda.
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
.
flatten #
flatMap #
replicate #
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 #
foldlM and foldrM #
foldl and foldr #
Variant of foldr_cons_eq_append
specalized to f = id
.
Equations
Instances For
Equations
Instances For
A reasoning principle for proving propositions about the result of List.foldl
by establishing an
invariant that is true for the initial data and preserved by the operation being folded.
Because the motive can return a type in any sort, this function may be used to construct data as well as to prove propositions.
Example:
example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
apply List.foldlRecOn
. show 0 < 1; trivial
. show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a
intros; omega
Equations
- List.foldlRecOn [] x✝³ x✝¹ x✝ = x✝¹
- List.foldlRecOn (hd :: tl) x✝³ x✝¹ x✝ = List.foldlRecOn tl x✝³ (x✝ x✝² x✝¹ hd ⋯) fun (y : β) (hy : motive y) (x : α) (hx : x ∈ tl) => x✝ y hy x ⋯
Instances For
A reasoning principle for proving propositions about the result of List.foldr
by establishing an
invariant that is true for the initial data and preserved by the operation being folded.
Because the motive can return a type in any sort, this function may be used to construct data as well as to prove propositions.
Example:
example {xs : List Nat} : xs.foldr (· + ·) 1 > 0 := by
apply List.foldrRecOn
. show 0 < 1; trivial
. show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b
intros; omega
Equations
- List.foldrRecOn [] x✝³ x✝¹ x✝ = x✝¹
- List.foldrRecOn (x_5 :: l) x✝³ x✝¹ x✝ = x✝ (List.foldr x✝³ x✝² l) (List.foldrRecOn l 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.
Further results about getLast
and getLast?
#
Additional operations #
leftpad #
List membership #
contains / elem #
Recall that the preferred simp normal form is contains
rather than elem
.
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
.
Logic #
any / all #
Manipulating elements #
replace #
insert #
removeAll
#
eraseDupsBy
and eraseDups
#
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]
.