Basic operations on List
. #
We define
- basic operations on
List
, - simp lemmas for applying the operations on
.nil
and.cons
arguments (in the cases where the right hand side is simple to state; otherwise these are deferred toInit.Data.List.Lemmas
), - the minimal lemmas which are required for setting up
Init.Data.Array.Basic
.
In Init.Data.List.Impl
we give tail-recursive versions of these operations
along with @[csimp]
lemmas,
In Init.Data.List.Lemmas
we develop the full API for these functions.
Recall that length
, get
, set
, fold
, and concat
have already been defined in Init.Prelude
.
The operations are organized as follow:
- Equality:
beq
,isEqv
. - Lexicographic ordering:
lt
,le
, and instances. - Basic operations:
map
,filter
,filterMap
,foldr
,append
,join
,pure
,bind
,replicate
, andreverse
. - List membership:
isEmpty
,elem
,contains
,mem
(and the∈
notation), and decidability for predicates quantifying over membership in aList
. - Sublists:
take
,drop
,takeWhile
,dropWhile
,partition
,dropLast
,isPrefixOf
,isPrefixOf?
,isSuffixOf
,isSuffixOf?
,rotateLeft
androtateRight
. - Manipulating elements:
replace
,insert
,erase
,eraseIdx
,find?
,findSome?
, andlookup
. - Logic:
any
,all
,or
, andand
. - Zippers:
zipWith
,zip
,zipWithAll
, andunzip
. - Ranges and enumeration:
range
,iota
,enumFrom
, andenum
. - Minima and maxima:
minimum?
andmaximum?
. - Other functions:
intersperse
,intercalate
,eraseDups
,eraseReps
,span
,groupBy
,removeAll
(currently these functions are mostly only used in meta code, and do not have API suitable for verification).
Further operations are defined in Init.Data.List.BasicAux
(because they use Array
in their implementations), namely:
Preliminaries from Init.Prelude
#
length #
set #
foldl #
concat #
Equality #
O(min |as| |bs|)
. Returns true if as
and bs
have the same length,
and they are pairwise related by eqv
.
Equations
Instances For
Lexicographic ordering #
The lexicographic order on lists.
[] < a::as
, and a::as < b::bs
if a < b
or if a
and b
are equivalent and as < bs
.
- nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), [].lt (b :: bs)
[]
is the smallest element in the order. - head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → (a :: as).lt (b :: bs)
If
a < b
thena::as < b::bs
. - tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α},
¬a < b → ¬b < a → as.lt bs → (a :: as).lt (b :: bs)
If
a
andb
are equivalent andas < bs
, thena::as < b::bs
.
Instances For
Equations
- x✝.instDecidableLeOfDecidableRelLt x = inferInstanceAs (Decidable ¬x < x✝)
Alternative getters #
get? #
Returns the i
-th element in the list (zero-based).
If the index is out of bounds (i ≥ as.length
), this function returns none
.
Also see get
, getD
and get!
.
Instances For
getD #
getLast #
getLast? #
getLastD #
Head and tail #
head #
head? #
headD #
tail? #
tailD #
Basic List
operations. #
We define the basic functional programming operations on List
:
map
, filter
, filterMap
, foldr
, append
, join
, pure
, bind
, replicate
, and reverse
.
map #
filter #
O(|l|)
. filter f l
returns the list of elements in l
for which f
returns true.
filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]
Equations
- List.filter p [] = []
- List.filter p (a :: as) = match p a with | true => a :: List.filter p as | false => List.filter p as
Instances For
filterMap #
O(|l|)
. filterMap f l
takes a function f : α → Option β
and applies it to each element of l
;
the resulting non-none
values are collected to form the output list.
filterMap
(fun x => if x > 2 then some (2 * x) else none)
[1, 2, 5, 2, 7, 7]
= [10, 14, 14]
Equations
- List.filterMap f [] = []
- List.filterMap f (a :: as) = match f a with | none => List.filterMap f as | some b => b :: List.filterMap f as
Instances For
foldr #
O(|l|)
. Applies function f
to all of the elements of the list, from right to left.
foldr f init [a, b, c] = f a <| f b <| f c <| init
Equations
- List.foldr f init [] = init
- List.foldr f init (a :: as) = f a (List.foldr f init as)
Instances For
reverse #
Auxiliary for List.reverse
. List.reverseAux l r = l.reverse ++ r
, but it is defined directly.
Instances For
O(|as|)
. Reverse of a list:
[1, 2, 3, 4].reverse = [4, 3, 2, 1]
Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.
Equations
- as.reverse = as.reverseAux []
Instances For
append #
Tail-recursive version of List.append
.
Most of the tail-recursive implementations are in Init.Data.List.Impl
,
but appendTR
must be set up immediately,
because otherwise Append (List α)
instance below will not use it.
Equations
- as.appendTR bs = as.reverse.reverseAux bs
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
join #
pure #
bind #
bind xs f
is the bind operation of the list monad. It applies f
to each element of xs
to get a list of lists, and then concatenates them all together.
Instances For
Equations
Instances For
Equations
Instances For
replicate #
replicate n a
is n
copies of a
:
replicate 5 a = [a, a, a, a, a]
Equations
- List.replicate 0 x = []
- List.replicate n.succ x = x :: List.replicate n x
Instances For
List membership #
EmptyCollection #
Equations
- List.instEmptyCollection = { emptyCollection := [] }
isEmpty #
elem #
contains #
Mem #
a ∈ l
is a predicate which asserts that a
is in the list l
.
Unlike elem
, this uses =
instead of ==
and is suited for mathematical reasoning.
a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z
- head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)
The head of a list is a member:
a ∈ a :: as
. - tail: ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a as → List.Mem a (b :: as)
A member of the tail of a list is a member of the list:
a ∈ l → a ∈ b :: l
.
Instances For
Equations
- List.instMembership = { mem := List.Mem }
Equations
Equations
- List.decidableBEx p [] = isFalse ⋯
- List.decidableBEx p (a :: as) = if h₁ : p a then isTrue ⋯ else match List.decidableBEx p as with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯
Equations
- List.decidableBAll p [] = isTrue ⋯
- List.decidableBAll p (a :: as) = if h₁ : p a then match List.decidableBAll p as with | isTrue h₂ => isTrue ⋯ | isFalse h₂ => isFalse ⋯ else isFalse ⋯
Sublists #
take #
drop #
takeWhile #
O(|xs|)
. Returns the longest initial segment of xs
for which p
returns true.
Equations
- List.takeWhile p [] = []
- List.takeWhile p (a :: as) = match p a with | true => a :: List.takeWhile p as | false => []
Instances For
dropWhile #
O(|l|)
. dropWhile p l
removes elements from the list until it finds the first element
for which p
returns false; this element and everything after it is returned.
dropWhile (· < 4) [1, 3, 2, 4, 2, 7, 4] = [4, 2, 7, 4]
Equations
- List.dropWhile p [] = []
- List.dropWhile p (a :: as) = match p a with | true => List.dropWhile p as | false => a :: as
Instances For
partition #
O(|l|)
. partition p l
calls p
on each element of l
, partitioning the list into two lists
(l_true, l_false)
where l_true
has the elements where p
was true
and l_false
has the elements where p
is false.
partition p l = (filter p l, filter (not ∘ p) l)
, but it is slightly more efficient
since it only has to do one pass over the list.
partition (· > 2) [1, 2, 5, 2, 7, 7] = ([5, 7, 7], [1, 2, 2])
Equations
- List.partition p as = List.partition.loop p as ([], [])
Instances For
Equations
- List.partition.loop p [] (bs, cs) = (bs.reverse, cs.reverse)
- List.partition.loop p (a :: as) (bs, cs) = match p a with | true => List.partition.loop p as (a :: bs, cs) | false => List.partition.loop p as (bs, a :: cs)
Instances For
dropLast #
isPrefixOf #
isPrefixOf l₁ l₂
returns true
Iff l₁
is a prefix of l₂
.
That is, there exists a t
such that l₂ == l₁ ++ t
.
Equations
Instances For
isPrefixOf? #
isSuffixOf #
isSuffixOf l₁ l₂
returns true
Iff l₁
is a suffix of l₂
.
That is, there exists a t
such that l₂ == t ++ l₁
.
Equations
- l₁.isSuffixOf l₂ = l₁.reverse.isPrefixOf l₂.reverse
Instances For
isSuffixOf? #
isSuffixOf? l₁ l₂
returns some t
when l₂ == t ++ l₁
.
Equations
- l₁.isSuffixOf? l₂ = Option.map List.reverse (l₁.reverse.isPrefixOf? l₂.reverse)
Instances For
rotateLeft #
O(n)
. Rotates the elements of xs
to the left such that the element at
xs[i]
rotates to xs[(i - n) % l.length]
.
rotateLeft [1, 2, 3, 4, 5] 3 = [4, 5, 1, 2, 3]
rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]
rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]
Equations
Instances For
rotateRight #
O(n)
. Rotates the elements of xs
to the right such that the element at
xs[i]
rotates to xs[(i + n) % l.length]
.
rotateRight [1, 2, 3, 4, 5] 3 = [3, 4, 5, 1, 2]
rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]
rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]
Equations
Instances For
Manipulating elements #
replace #
insert #
erase #
eraseIdx #
find? #
O(|l|)
. find? p l
returns the first element for which p
returns true,
or none
if no such element is found.
Equations
- List.find? p [] = none
- List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as
Instances For
findSome? #
O(|l|)
. findSome? f l
applies f
to each element of l
, and returns the first non-none
result.
findSome? (fun x => if x < 5 then some (10 * x) else none) [7, 6, 5, 8, 1, 2, 6] = some 10
Equations
- List.findSome? f [] = none
- List.findSome? f (a :: as) = match f a with | some b => some b | none => List.findSome? f as
Instances For
lookup #
O(|l|)
. lookup a l
treats l : List (α × β)
like an association list,
and returns the first β
value corresponding to an α
value in the list equal to a
.
Equations
- List.lookup x [] = none
- List.lookup x ((k, b) :: es) = match x == k with | true => some b | false => List.lookup x es
Instances For
Logical operations #
any #
all #
or #
and #
Zippers #
zipWith #
O(min |xs| |ys|)
. Applies f
to the two lists in parallel, stopping at the shorter list.
zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
Equations
- List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
- List.zipWith f x✝ x = []
Instances For
zip #
O(min |xs| |ys|)
. Combines the two lists into a list of pairs, with one element from each list.
The longer list is truncated to match the shorter list.
zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]
Equations
- List.zip = List.zipWith Prod.mk
Instances For
zipWithAll #
O(max |xs| |ys|)
.
Version of List.zipWith
that continues to the end of both lists,
passing none
to one argument once the shorter list has run out.
Equations
- List.zipWithAll f [] x = List.map (fun (b : β) => f none (some b)) x
- List.zipWithAll f (a :: as) [] = List.map (fun (a : α) => f (some a) none) (a :: as)
- List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs
Instances For
unzip #
O(|l|)
. Separates a list of pairs into two lists containing the first components and second components.
unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])
Equations
Instances For
Ranges and enumeration #
range #
O(n)
. range n
is the numbers from 0
to n
exclusive, in increasing order.
range 5 = [0, 1, 2, 3, 4]
Equations
- List.range n = List.range.loop n []
Instances For
Equations
- List.range.loop 0 x = x
- List.range.loop n.succ x = List.range.loop n (n :: x)
Instances For
iota #
enumFrom #
O(|l|)
. enumFrom n l
is like enum
but it allows you to specify the initial index.
enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]
Equations
- List.enumFrom x [] = []
- List.enumFrom x (x_2 :: xs) = (x, x_2) :: List.enumFrom (x + 1) xs
Instances For
enum #
Minima and maxima #
minimum? #
Returns the smallest element of the list, if it is not empty.
Equations
- x.minimum? = match x with | [] => none | a :: as => some (List.foldl min a as)
Instances For
maximum? #
Returns the largest element of the list, if it is not empty.
Equations
- x.maximum? = match x with | [] => none | a :: as => some (List.foldl max a as)
Instances For
Other list operations #
The functions are currently mostly used in meta code, and do not have sufficient API developed for verification work.
intersperse #
O(|l|)
. intersperse sep l
alternates sep
and the elements of l
:
intersperse sep [] = []
intersperse sep [a] = [a]
intersperse sep [a, b] = [a, sep, b]
intersperse sep [a, b, c] = [a, sep, b, sep, c]
Equations
- List.intersperse sep [] = []
- List.intersperse sep [head] = [head]
- List.intersperse sep (a :: as) = a :: sep :: List.intersperse sep as
Instances For
intercalate #
O(|xs|)
. intercalate sep xs
alternates sep
and the elements of xs
:
intercalate sep [] = []
intercalate sep [a] = a
intercalate sep [a, b] = a ++ sep ++ b
intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c
Equations
- sep.intercalate xs = (List.intersperse sep xs).join
Instances For
eraseDups #
O(|l|^2)
. Erase duplicated elements in the list.
Keeps the first occurrence of duplicated elements.
eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]
Equations
- as.eraseDups = List.eraseDups.loop as []
Instances For
Equations
- List.eraseDups.loop [] x = x.reverse
- List.eraseDups.loop (a :: l) x = match List.elem a x with | true => List.eraseDups.loop l x | false => List.eraseDups.loop l (a :: x)
Instances For
eraseReps #
O(|l|)
. Erase repeated adjacent elements. Keeps the first occurrence of each run.
eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]
Equations
- x.eraseReps = match x with | [] => [] | a :: as => List.eraseReps.loop a as []
Instances For
Equations
- List.eraseReps.loop x✝ [] x = (x✝ :: x).reverse
- List.eraseReps.loop x✝ (a' :: as) x = match x✝ == a' with | true => List.eraseReps.loop x✝ as x | false => List.eraseReps.loop a' as (x✝ :: x)
Instances For
span #
O(|l|)
. span p l
splits the list l
into two parts, where the first part
contains the longest initial segment for which p
returns true
and the second part is everything else.
span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])
span (· > 10) [6, 8, 9, 5, 2, 9] = ([], [6, 8, 9, 5, 2, 9])
Equations
- List.span p as = List.span.loop p as []
Instances For
Equations
- List.span.loop p [] x = (x.reverse, [])
- List.span.loop p (a :: l) x = match p a with | true => List.span.loop p l (a :: x) | false => (x.reverse, a :: l)
Instances For
groupBy #
O(|l|)
. groupBy R l
splits l
into chains of elements
such that adjacent elements are related by R
.
groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]
groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]
Equations
- List.groupBy R x = match x with | [] => [] | a :: as => List.groupBy.loop R as a [] []
Instances For
Equations
- List.groupBy.loop R (a :: as) x✝¹ x✝ x = match R x✝¹ a with | true => List.groupBy.loop R as a (x✝¹ :: x✝) x | false => List.groupBy.loop R as a [] ((x✝¹ :: x✝).reverse :: x)
- List.groupBy.loop R [] x✝¹ x✝ x = ((x✝¹ :: x✝).reverse :: x).reverse
Instances For
removeAll #
O(|xs|)
. Computes the "set difference" of lists,
by filtering out all elements of xs
which are also in ys
.
removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]
Equations
- xs.removeAll ys = List.filter (fun (x : α) => !List.elem x ys) xs