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 to Init.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, foldl, and concat have already been defined in Init.Prelude.

The operations are organized as follow:

• Equality: beq, isEqv.
• Lexicographic ordering: lt, le, and instances.
• Head and tail operators: head, head?, headD?, tail, tail?, tailD.
• Basic operations: map, filter, filterMap, foldr, append, join, pure, bind, replicate, and reverse.
• Additional functions defined in terms of these: leftpad, rightPad, and reduceOption.
• List membership: isEmpty, elem, contains, mem (and the ∈ notation), and decidability for predicates quantifying over membership in a List.
• Sublists: take, drop, takeWhile, dropWhile, partition, dropLast, isPrefixOf, isPrefixOf?, isSuffixOf, isSuffixOf?, Subset, Sublist, rotateLeft and rotateRight.
• Manipulating elements: replace, insert, erase, eraseP, eraseIdx.
• Finding elements: find?, findSome?, findIdx, indexOf, findIdx?, indexOf?, countP, count, and lookup.
• Logic: any, all, or, and and.
• Zippers: zipWith, zip, zipWithAll, and unzip.
• Ranges and enumeration: range, iota, enumFrom, and enum.
• Minima and maxima: minimum? and maximum?.
• 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:

• Variant getters: get!, get?, getD, getLast, getLast!, getLast?, and getLastD.
• Head and tail: head!, tail!.
• Other operations on sublists: partitionMap, rotateLeft, and rotateRight.

Preliminaries from Init.Prelude

length

@[simp]

theorem List.length_nil {α : Type u} : [].length = 0

@[simp]

theorem List.length_singleton {α : Type u} (a : α) : [a].length = 1

@[simp]

theorem List.length_cons {α : Type u_1} (a : α) (as : List α) : (a :: as).length = as.length + 1

set

@[simp]

theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) : (as.set i a).length = as.length

foldl

@[simp]

theorem List.foldl_nil : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → α} {b : α}, List.foldl f b [] = b

@[simp]

theorem List.foldl_cons {α : Type u} {β : Type v} {a : α} {f : β → α → β} (l : List α) (b : β) : List.foldl f b (a :: l) = List.foldl f (f b a) l

concat

theorem List.length_concat {α : Type u} (as : List α) (a : α) : (as.concat a).length = as.length + 1

theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : as.concat a = bs.concat b) : as = bs ∧ a = b

Equality

def List.beq {α : Type u} [BEq α] : List α → List α → Bool

The equality relation on lists asserts that they have the same length and they are pairwise BEq.

Equations

• [].beq [] = true
• (a :: as).beq (b :: bs) = (a == b && as.beq bs)
• x✝.beq x = false

instance List.instBEq {α : Type u} [BEq α] : BEq (List α)

Equations

• List.instBEq = { beq := List.beq }

instance List.instLawfulBEq {α : Type u} [BEq α] [LawfulBEq α] : LawfulBEq (List α)

Equations

• ⋯ = ⋯

@[specialize #[]]

def List.isEqv {α : Type u} (as : List α) (bs : List α) (eqv : α → α → Bool) : Bool

O(min |as| |bs|). Returns true if as and bs have the same length, and they are pairwise related by eqv.

Equations

• [].isEqv [] x = true
• (a :: as).isEqv (b :: bs) x = (x a b && as.isEqv bs x)
• x✝¹.isEqv x✝ x = false

@[simp]

theorem List.isEqv_nil_nil {α : Type u} {eqv : α → α → Bool} : [].isEqv [] eqv = true

@[simp]

theorem List.isEqv_nil_cons {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool} : [].isEqv (a :: as) eqv = false

@[simp]

theorem List.isEqv_cons_nil {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool} : (a :: as).isEqv [] eqv = false

theorem List.isEqv_cons₂ : ∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : α → α → Bool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)

Lexicographic ordering

inductive List.lt {α : Type u} [LT α] : List α → List α → Prop

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 then a::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 and b are equivalent and as < bs, then a::as < b::bs.

instance List.instLT {α : Type u} [LT α] : LT (List α)

Equations

• List.instLT = { lt := List.lt }

instance List.hasDecidableLt {α : Type u} [LT α] [h : DecidableRel fun (x1 x2 : α) => x1 < x2] (l₁ : List α) (l₂ : List α) : Decidable (l₁ < l₂)

Equations

• One or more equations did not get rendered due to their size.
• [].hasDecidableLt [] = isFalse ⋯
• [].hasDecidableLt (head :: tail) = isTrue ⋯
• (head :: tail).hasDecidableLt [] = isFalse ⋯

@[reducible]

def List.le {α : Type u} [LT α] (a : List α) (b : List α) : Prop

The lexicographic order on lists.

Equations

• a.le b = ¬b < a

instance List.instLEOfLT {α : Type u} [LT α] : LE (List α)

Equations

• List.instLEOfLT = { le := List.le }

instance List.instDecidableLeOfDecidableRelLt {α : Type u} [LT α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (l₁ : List α) (l₂ : List α) : Decidable (l₁ ≤ l₂)

Equations

• x✝.instDecidableLeOfDecidableRelLt x = inferInstanceAs (Decidable ¬x < x✝)

Alternative getters

get?

def List.get? {α : Type u} (as : List α) (i : Nat) : Option α

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!.

Equations

• (a :: tail).get? 0 = some a
• (head :: as).get? n.succ = as.get? n
• x✝.get? x = none

@[simp]

theorem List.get?_nil {α : Type u} {n : Nat} : [].get? n = none

@[simp]

theorem List.get?_cons_zero {α : Type u} {a : α} {l : List α} : (a :: l).get? 0 = some a

@[simp]

theorem List.get?_cons_succ {α : Type u} {a : α} {l : List α} {n : Nat} : (a :: l).get? (n + 1) = l.get? n

theorem List.ext_get? {α : Type u} {l₁ : List α} {l₂ : List α} : (∀ (n : Nat), l₁.get? n = l₂.get? n) → l₁ = l₂

@[reducible, inline, deprecated]

abbrev List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} : (∀ (n : Nat), l₁.get? n = l₂.get? n) → l₁ = l₂

Deprecated alias for ext_get?. The preferred extensionality theorem is now ext_getElem?.

Equations

• @List.ext = @List.ext_get?

getD

def List.getD {α : Type u} (as : List α) (i : Nat) (fallback : α) : α

Returns the i-th element in the list (zero-based).

If the index is out of bounds (i ≥ as.length), this function returns fallback. See also get? and get!.

Equations

• as.getD i fallback = (as.get? i).getD fallback

@[simp]

theorem List.getD_nil {n : Nat} : ∀ {α : Type u_1} {d : α}, [].getD n d = d

@[simp]

theorem List.getD_cons_zero : ∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x

@[simp]

theorem List.getD_cons_succ : ∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d

getLast

def List.getLast {α : Type u} (as : List α) : as ≠ [] → α

Returns the last element of a non-empty list.

Equations

• [].getLast h = absurd ⋯ h
• [a].getLast x_2 = a
• (head :: b :: as).getLast x_2 = (b :: as).getLast ⋯

getLast?

def List.getLast? {α : Type u} : List α → Option α

Returns the last element in the list.

If the list is empty, this function returns none. Also see getLastD and getLast!.

Equations

• [].getLast? = none
• (a :: as).getLast? = some ((a :: as).getLast ⋯)

@[simp]

theorem List.getLast?_nil {α : Type u} : [].getLast? = none

getLastD

def List.getLastD {α : Type u} (as : List α) (fallback : α) : α

Returns the last element in the list.

If the list is empty, this function returns fallback. Also see getLast? and getLast!.

Equations

• [].getLastD x = x
• (a :: as).getLastD x = (a :: as).getLast ⋯

theorem List.getLastD_nil {α : Type u} (a : α) : [].getLastD a = a

theorem List.getLastD_cons {α : Type u} (a : α) (b : α) (l : List α) : (b :: l).getLastD a = l.getLastD b

Head and tail

head

def List.head {α : Type u} (as : List α) : as ≠ [] → α

Returns the first element of a non-empty list.

Equations

• (a :: tail).head x_2 = a

@[simp]

theorem List.head_cons {α : Type u} {a : α} {l : List α} {h : a :: l ≠ []} : (a :: l).head h = a

head?

def List.head? {α : Type u} : List α → Option α

Returns the first element in the list.

If the list is empty, this function returns none. Also see headD and head!.

Equations

• [].head? = none
• (a :: as).head? = some a

@[simp]

theorem List.head?_nil {α : Type u} : [].head? = none

@[simp]

theorem List.head?_cons {α : Type u} {a : α} {l : List α} : (a :: l).head? = some a

headD

def List.headD {α : Type u} (as : List α) (fallback : α) : α

Returns the first element in the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations

• [].headD x = x
• (a :: as).headD x = a

@[simp]

theorem List.headD_nil {α : Type u} {d : α} : [].headD d = d

@[simp]

theorem List.headD_cons {α : Type u} {a : α} {l : List α} {d : α} : (a :: l).headD d = a

tail

def List.tail {α : Type u} : List α → List α

Get the tail of a nonempty list, or return [] for [].

Equations

• [].tail = []
• (a :: as).tail = as

@[simp]

theorem List.tail_nil {α : Type u} : [].tail = []

@[simp]

theorem List.tail_cons {α : Type u} {a : α} {as : List α} : (a :: as).tail = as

tail?

def List.tail? {α : Type u} : List α → Option (List α)

Drops the first element of the list.

If the list is empty, this function returns none. Also see tailD and tail!.

Equations

• [].tail? = none
• (a :: as).tail? = some as

@[simp]

theorem List.tail?_nil {α : Type u} : [].tail? = none

@[simp]

theorem List.tail?_cons {α : Type u} {a : α} {l : List α} : (a :: l).tail? = some l

tailD

def List.tailD {α : Type u} (list : List α) (fallback : List α) : List α

Drops the first element of the list.

If the list is empty, this function returns fallback. Also see head? and head!.

Equations

• [].tailD fallback = fallback
• (a :: as).tailD fallback = as

@[simp]

theorem List.tailD_nil {α : Type u} {l' : List α} : [].tailD l' = l'

@[simp]

theorem List.tailD_cons {α : Type u} {a : α} {l : List α} {l' : List α} : (a :: l).tailD l' = l

Basic List operations.

We define the basic functional programming operations on List: map, filter, filterMap, foldr, append, join, pure, bind, replicate, and reverse.

map

@[specialize #[]]

def List.map {α : Type u} {β : Type v} (f : α → β) : List α → List β

O(|l|). map f l applies f to each element of the list.

• map f [a, b, c] = [f a, f b, f c]

Equations

• List.map f [] = []
• List.map f (a :: as) = f a :: List.map f as

@[simp]

theorem List.map_nil {α : Type u} {β : Type v} {f : α → β} : List.map f [] = []

@[simp]

theorem List.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (l : List α) : List.map f (a :: l) = f a :: List.map f l

filter

def List.filter {α : Type u} (p : α → Bool) : List α → List α

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

@[simp]

theorem List.filter_nil {α : Type u} (p : α → Bool) : List.filter p [] = []

filterMap

@[specialize #[]]

def List.filterMap {α : Type u} {β : Type v} (f : α → Option β) : List α → List β

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

@[simp]

theorem List.filterMap_nil {α : Type u} {β : Type v} (f : α → Option β) : List.filterMap f [] = []

theorem List.filterMap_cons {α : Type u} {β : Type v} (f : α → Option β) (a : α) (l : List α) : List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l

foldr

@[specialize #[]]

def List.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) : List α → β

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)

@[simp]

theorem List.foldr_nil : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α_1 → α_1} {b : α_1}, List.foldr f b [] = b

@[simp]

theorem List.foldr_cons {α : Type u} {a : α} : ∀ {α_1 : Type u_1} {f : α → α_1 → α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)

reverse

def List.reverseAux {α : Type u} : List α → List α → List α

Auxiliary for List.reverse. List.reverseAux l r = l.reverse ++ r, but it is defined directly.

Equations

• [].reverseAux x = x
• (a :: l).reverseAux x = l.reverseAux (a :: x)

@[simp]

theorem List.reverseAux_nil : ∀ {α : Type u_1} {r : List α}, [].reverseAux r = r

@[simp]

theorem List.reverseAux_cons : ∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)

def List.reverse {α : Type u} (as : List α) : List α

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 []

@[simp]

theorem List.reverse_nil {α : Type u} : [].reverse = []

theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) : (as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux []).reverseAux cs)

append

def List.append {α : Type u} (xs : List α) (ys : List α) : List α

O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first list.

Equations

• [].append x = x
• (a :: l).append x = a :: l.append x

def List.appendTR {α : Type u} (as : List α) (bs : List α) : List α

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

@[csimp]

theorem List.append_eq_appendTR : @List.append = @List.appendTR

instance List.instAppend {α : Type u} : Append (List α)

Equations

• List.instAppend = { append := List.append }

@[simp]

theorem List.append_eq {α : Type u} (as : List α) (bs : List α) : as.append bs = as ++ bs

@[simp]

theorem List.nil_append {α : Type u} (as : List α) : [] ++ as = as

@[simp]

theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) : a :: as ++ bs = a :: (as ++ bs)

@[simp]

theorem List.append_nil {α : Type u} (as : List α) : as ++ [] = as

instance List.instLawfulIdentityHAppendNil {α : Type u} : Std.LawfulIdentity (fun (x1 x2 : List α) => x1 ++ x2) []

Equations

• ⋯ = ⋯

@[simp]

theorem List.length_append {α : Type u} (as : List α) (bs : List α) : (as ++ bs).length = as.length + bs.length

@[simp]

theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) : as ++ bs ++ cs = as ++ (bs ++ cs)

instance List.instAssociativeHAppend {α : Type u} : Std.Associative fun (x1 x2 : List α) => x1 ++ x2

Equations

• ⋯ = ⋯

theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs

@[simp]

theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) : as.concat a = as ++ [a]

theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) : as.reverseAux bs = as.reverseAux [] ++ bs

@[simp]

theorem List.reverse_cons {α : Type u} (a : α) (as : List α) : (a :: as).reverse = as.reverse ++ [a]

join

def List.join {α : Type u} : List (List α) → List α

O(|join L|). join L concatenates all the lists in L into one list.

• join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]

Equations

• [].join = []
• (a :: as).join = a ++ as.join

@[simp]

theorem List.join_nil {α : Type u} : [].join = []

@[simp]

theorem List.join_cons : ∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join

pure

@[inline]

def List.pure {α : Type u} (a : α) : List α

pure x = [x] is the pure operation of the list monad.

Equations

• List.pure a = [a]

bind

@[inline]

def List.bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β

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.

• [2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]

Equations

• a.bind b = (List.map b a).join

@[simp]

theorem List.bind_nil {α : Type u} {β : Type v} (f : α → List β) : [].bind f = []

@[simp]

theorem List.bind_cons {α : Type u} {β : Type v} (x : α) (xs : List α) (f : α → List β) : (x :: xs).bind f = f x ++ xs.bind f

@[reducible, inline, deprecated List.bind_nil]

abbrev List.nil_bind {α : Type u_1} {β : Type u_2} (f : α → List β) : [].bind f = []

Equations

• @List.nil_bind = @List.bind_nil

@[reducible, inline, deprecated List.bind_cons]

abbrev List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : α → List β) : (x :: xs).bind f = f x ++ xs.bind f

Equations

• @List.cons_bind = @List.bind_cons

replicate

def List.replicate {α : Type u} (n : Nat) (a : α) : List α

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

@[simp]

theorem List.replicate_zero : ∀ {α : Type u_1} {a : α}, List.replicate 0 a = []

theorem List.replicate_succ {α : Type u} (a : α) (n : Nat) : List.replicate (n + 1) a = a :: List.replicate n a

@[simp]

theorem List.length_replicate {α : Type u} (n : Nat) (a : α) : (List.replicate n a).length = n

Additional functions

leftpad and rightpad

def List.leftpad {α : Type u} (n : Nat) (a : α) (l : List α) : List α

Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

Equations

• List.leftpad n a l = List.replicate (n - l.length) a ++ l

def List.rightpad {α : Type u} (n : Nat) (a : α) (l : List α) : List α

Pads l : List α on the right with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

Equations

• List.rightpad n a l = l ++ List.replicate (n - l.length) a

reduceOption

@[inline]

def List.reduceOption {α : Type u_1} : List (Option α) → List α

Drop nones from a list, and replace each remaining some a with a.

Equations

• List.reduceOption = List.filterMap id

List membership

• L.contains a : Bool determines, using a [BEq α] instance, whether L contains an element · == a.
• a ∈ L : Prop is the proposition (only decidable if α has decidable equality) that L contains an element · = a.

EmptyCollection

instance List.instEmptyCollection {α : Type u} : EmptyCollection (List α)

Equations

• List.instEmptyCollection = { emptyCollection := [] }

@[simp]

theorem List.empty_eq {α : Type u} : ∅ = []

isEmpty

def List.isEmpty {α : Type u} : List α → Bool

O(1). isEmpty l is true if the list is empty.

• isEmpty [] = true
• isEmpty [a] = false
• isEmpty [a, b] = false

Equations

• [].isEmpty = true
• (a :: as).isEmpty = false

@[simp]

theorem List.isEmpty_nil {α : Type u} : [].isEmpty = true

@[simp]

theorem List.isEmpty_cons {α : Type u} {x : α} {xs : List α} : (x :: xs).isEmpty = false

elem

def List.elem {α : Type u} [BEq α] (a : α) : List α → Bool

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false

Equations

• List.elem a [] = false
• List.elem a (a_1 :: as) = match a == a_1 with | true => true | false => List.elem a as

@[simp]

theorem List.elem_nil {α : Type u} {a : α} [BEq α] : List.elem a [] = false

theorem List.elem_cons {α : Type u} {b : α} {bs : List α} [BEq α] {a : α} : List.elem a (b :: bs) = match a == b with | true => true | false => List.elem a bs

@[deprecated]

def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) : Bool

notElem a l is !(elem a l).

Equations

• List.notElem a as = !List.elem a as

contains

@[reducible, inline]

abbrev List.contains {α : Type u} [BEq α] (as : List α) (a : α) : Bool

O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

• elem 3 [1, 4, 2, 3, 3, 7] = true
• elem 5 [1, 4, 2, 3, 3, 7] = false

Equations

• as.contains a = List.elem a as

@[simp]

theorem List.contains_nil {α : Type u} {a : α} [BEq α] : [].contains a = false

Mem

inductive List.Mem {α : Type u} (a : α) : List α → Prop

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.

instance List.instMembership {α : Type u} : Membership α (List α)

Equations

• List.instMembership = { mem := fun (l : List α) (a : α) => List.Mem a l }

theorem List.mem_of_elem_eq_true {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} : List.elem a as = true → a ∈ as

theorem List.elem_eq_true_of_mem {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} (h : a ∈ as) : List.elem a as = true

instance List.instDecidableMemOfLawfulBEq {α : Type u} [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a ∈ as)

Equations

• List.instDecidableMemOfLawfulBEq a as = decidable_of_decidable_of_iff ⋯

theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs

theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs

instance List.decidableBEx {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) : Decidable (∃ (x : α), x ∈ l ∧ p x)

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 ⋯

instance List.decidableBAll {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) : Decidable (∀ (x : α), x ∈ l → p x)

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

def List.take {α : Type u} : Nat → List α → List α

O(min n |xs|). Returns the first n elements of xs, or the whole list if n is too large.

• take 0 [a, b, c, d, e] = []
• take 3 [a, b, c, d, e] = [a, b, c]
• take 6 [a, b, c, d, e] = [a, b, c, d, e]

Equations

• List.take 0 x = []
• List.take n.succ [] = []
• List.take n.succ (a :: as) = a :: List.take n as

@[simp]

theorem List.take_nil {α : Type u} {i : Nat} : List.take i [] = []

@[simp]

theorem List.take_zero {α : Type u} (l : List α) : List.take 0 l = []

@[simp]

theorem List.take_succ_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

drop

def List.drop {α : Type u} : Nat → List α → List α

O(min n |xs|). Removes the first n elements of xs.

• drop 0 [a, b, c, d, e] = [a, b, c, d, e]
• drop 3 [a, b, c, d, e] = [d, e]
• drop 6 [a, b, c, d, e] = []

Equations

• List.drop 0 x = x
• List.drop n.succ [] = []
• List.drop n.succ (a :: as) = List.drop n as

@[simp]

theorem List.drop_nil {α : Type u} {i : Nat} : List.drop i [] = []

@[simp]

theorem List.drop_zero {α : Type u} (l : List α) : List.drop 0 l = l

@[simp]

theorem List.drop_succ_cons : ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) = List.drop n l

theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : as.length ≤ i) : List.drop i as = []

takeWhile

def List.takeWhile {α : Type u} (p : α → Bool) (xs : List α) : List α

O(|xs|). Returns the longest initial segment of xs for which p returns true.

• takeWhile (· > 5) [7, 6, 4, 8] = [7, 6]
• takeWhile (· > 5) [7, 6, 6, 8] = [7, 6, 6, 8]

Equations

• List.takeWhile p [] = []
• List.takeWhile p (a :: as) = match p a with | true => a :: List.takeWhile p as | false => []

@[simp]

theorem List.takeWhile_nil {α : Type u} {p : α → Bool} : List.takeWhile p [] = []

dropWhile

def List.dropWhile {α : Type u} (p : α → Bool) : List α → List α

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

@[simp]

theorem List.dropWhile_nil {α : Type u} {p : α → Bool} : List.dropWhile p [] = []

partition

@[inline]

def List.partition {α : Type u} (p : α → Bool) (as : List α) : List α × List α

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 ([], [])

@[specialize #[]]

def List.partition.loop {α : Type u} (p : α → Bool) : List α → List α × List α → List α × List α

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)

dropLast

def List.dropLast {α : Type u_1} : List α → List α

Removes the last element of the list.

• dropLast [] = []
• dropLast [a] = []
• dropLast [a, b, c] = [a, b]

Equations

• [].dropLast = []
• [head].dropLast = []
• (a :: as).dropLast = a :: as.dropLast

@[simp]

theorem List.dropLast_nil {α : Type u} : [].dropLast = []

@[simp]

theorem List.dropLast_single : ∀ {α : Type u_1} {x : α}, [x].dropLast = []

@[simp]

theorem List.dropLast_cons₂ : ∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast

@[simp]

theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) : (a :: as).dropLast.length = as.length

Subset

def List.Subset {α : Type u} (l₁ : List α) (l₂ : List α) : Prop

l₁ ⊆ l₂ means that every element of l₁ is also an element of l₂, ignoring multiplicity.

Equations

• l₁.Subset l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂

instance List.instHasSubset {α : Type u} : HasSubset (List α)

Equations

• List.instHasSubset = { Subset := List.Subset }

instance List.instDecidableRelSubsetOfDecidableEq {α : Type u} [DecidableEq α] : DecidableRel Subset

Equations

• x✝.instDecidableRelSubsetOfDecidableEq x = List.decidableBAll (Membership.mem x) x✝

Sublist and isSublist

inductive List.Sublist {α : Type u_1} : List α → List α → Prop

l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

• slnil: ∀ {α : Type u_1}, [].Sublist []

  the base case: [] is a sublist of []

• cons: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → l₁.Sublist (a :: l₂)

  If l₁ is a subsequence of l₂, then it is also a subsequence of a :: l₂.

• cons₂: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)

  If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: l₂.

def List.«term_<+_» : Lean.TrailingParserDescr

l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

Equations

• List.«term_<+_» = Lean.ParserDescr.trailingNode `List.term_<+_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+ ") (Lean.ParserDescr.cat `term 51))

def List.isSublist {α : Type u} [BEq α] : List α → List α → Bool

True if the first list is a potentially non-contiguous sub-sequence of the second list.

Equations

• [].isSublist x = true
• x.isSublist [] = false
• (hd₁ :: tl₁).isSublist (hd₂ :: tl₂) = if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else (hd₁ :: tl₁).isSublist tl₂

IsPrefix / isPrefixOf / isPrefixOf?

def List.IsPrefix {α : Type u} (l₁ : List α) (l₂ : List α) : Prop

IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations

• (l₁ <+: l₂) = ∃ (t : List α), l₁ ++ t = l₂

def List.«term_<+:_» : Lean.TrailingParserDescr

IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations

• List.«term_<+:_» = Lean.ParserDescr.trailingNode `List.term_<+:_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <+: ") (Lean.ParserDescr.cat `term 51))

def List.isPrefixOf {α : Type u} [BEq α] : List α → List α → Bool

isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

Equations

• [].isPrefixOf x = true
• x.isPrefixOf [] = false
• (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

@[simp]

theorem List.isPrefixOf_nil_left {α : Type u} {l : List α} [BEq α] : [].isPrefixOf l = true

@[simp]

theorem List.isPrefixOf_cons_nil {α : Type u} {a : α} {as : List α} [BEq α] : (a :: as).isPrefixOf [] = false

theorem List.isPrefixOf_cons₂ {α : Type u} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} : (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

def List.isPrefixOf? {α : Type u} [BEq α] : List α → List α → Option (List α)

isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

Equations

• [].isPrefixOf? x = some x
• x.isPrefixOf? [] = none
• (a :: as).isPrefixOf? (b :: bs) = if (a == b) = true then as.isPrefixOf? bs else none

IsSuffix / isSuffixOf / isSuffixOf?

def List.isSuffixOf {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) : Bool

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

@[simp]

theorem List.isSuffixOf_nil_left {α : Type u} {l : List α} [BEq α] : [].isSuffixOf l = true

def List.isSuffixOf? {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) : Option (List α)

isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

Equations

• l₁.isSuffixOf? l₂ = Option.map List.reverse (l₁.reverse.isPrefixOf? l₂.reverse)

def List.IsSuffix {α : Type u} (l₁ : List α) (l₂ : List α) : Prop

IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations

• (l₁ <:+ l₂) = ∃ (t : List α), t ++ l₁ = l₂

def List.«term_<:+_» : Lean.TrailingParserDescr

IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations

• List.«term_<:+_» = Lean.ParserDescr.trailingNode `List.term_<:+_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+ ") (Lean.ParserDescr.cat `term 51))

IsInfix

def List.IsInfix {α : Type u} (l₁ : List α) (l₂ : List α) : Prop

IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations

• (l₁ <:+: l₂) = ∃ (s : List α), ∃ (t : List α), s ++ l₁ ++ t = l₂

def List.«term_<:+:_» : Lean.TrailingParserDescr

IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations

• List.«term_<:+:_» = Lean.ParserDescr.trailingNode `List.term_<:+:_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+: ") (Lean.ParserDescr.cat `term 51))

splitAt

def List.splitAt {α : Type u} (n : Nat) (l : List α) : List α × List α

Split a list at an index.

splitAt 2 [a, b, c] = ([a, b], [c])

Equations

• List.splitAt n l = List.splitAt.go l l n []

def List.splitAt.go {α : Type u} (l : List α) : List α → Nat → List α → List α × List α

Auxiliary for splitAt: splitAt.go l xs n acc = (acc.reverse ++ take n xs, drop n xs) if n < xs.length, and (l, []) otherwise.

Equations

• List.splitAt.go l [] x✝ x = (l, [])
• List.splitAt.go l (x_3 :: xs) n.succ x = List.splitAt.go l xs n (x_3 :: x)
• List.splitAt.go l x✝¹ x✝ x = (x.reverse, x✝¹)

rotateLeft

def List.rotateLeft {α : Type u} (xs : List α) (n : optParam Nat 1) : List α

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

• xs.rotateLeft n = if xs.length ≤ 1 then xs else let n := n % xs.length; let b := List.take n xs; let e := List.drop n xs; e ++ b

@[simp]

theorem List.rotateLeft_nil {α : Type u} {n : Nat} : [].rotateLeft n = []

rotateRight

def List.rotateRight {α : Type u} (xs : List α) (n : optParam Nat 1) : List α

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

• xs.rotateRight n = if xs.length ≤ 1 then xs else let n := xs.length - n % xs.length; let b := List.take n xs; let e := List.drop n xs; e ++ b

@[simp]

theorem List.rotateRight_nil {α : Type u} {n : Nat} : [].rotateRight n = []

Pairwise, Nodup

inductive List.Pairwise {α : Type u} (R : α → α → Prop) : List α → Prop

Pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (·≠·) then it asserts l has no duplicates, and if R = (·<·) then it asserts that l is (strictly) sorted.

• nil: ∀ {α : Type u} {R : α → α → Prop}, List.Pairwise R []

  All elements of the empty list are vacuously pairwise related.

• cons: ∀ {α : Type u} {R : α → α → Prop} {a : α} {l : List α}, (∀ (a' : α), a' ∈ l → R a a') → List.Pairwise R l → List.Pairwise R (a :: l)

  a :: l is Pairwise R if a R-relates to every element of l, and l is Pairwise R.

@[simp]

theorem List.pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : List.Pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ List.Pairwise R l

instance List.instDecidablePairwise {α : Type u} {R : α → α → Prop} [DecidableRel R] (l : List α) : Decidable (List.Pairwise R l)

Equations

• One or more equations did not get rendered due to their size.
• [].instDecidablePairwise = isTrue ⋯

def List.Nodup {α : Type u} : List α → Prop

Nodup l means that l has no duplicates, that is, any element appears at most once in the List. It is defined as Pairwise (≠).

Equations

• List.Nodup = List.Pairwise fun (x1 x2 : α) => x1 ≠ x2

instance List.nodupDecidable {α : Type u} [DecidableEq α] (l : List α) : Decidable l.Nodup

Equations

• List.nodupDecidable = List.instDecidablePairwise

Manipulating elements

replace

def List.replace {α : Type u} [BEq α] : List α → α → α → List α

O(|l|). replace l a b replaces the first element in the list equal to a with b.

• replace [1, 4, 2, 3, 3, 7] 3 6 = [1, 4, 2, 6, 3, 7]
• replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]

Equations

• [].replace x✝ x = []
• (a :: as).replace x✝ x = match x✝ == a with | true => x :: as | false => a :: as.replace x✝ x

@[simp]

theorem List.replace_nil {α : Type u} {a : α} {b : α} [BEq α] : [].replace a b = []

theorem List.replace_cons {α : Type u} {as : List α} {b : α} {c : α} [BEq α] {a : α} : (a :: as).replace b c = match b == a with | true => c :: as | false => a :: as.replace b c

insert

@[inline]

def List.insert {α : Type u} [BEq α] (a : α) (l : List α) : List α

Inserts an element into a list without duplication.

Equations

• List.insert a l = if List.elem a l = true then l else a :: l

erase

def List.erase {α : Type u_1} [BEq α] : List α → α → List α

O(|l|). erase l a removes the first occurrence of a from l.

• erase [1, 5, 3, 2, 5] 5 = [1, 3, 2, 5]
• erase [1, 5, 3, 2, 5] 6 = [1, 5, 3, 2, 5]

Equations

• [].erase x = []
• (a :: as).erase x = match a == x with | true => as | false => a :: as.erase x

@[simp]

theorem List.erase_nil {α : Type u} [BEq α] (a : α) : [].erase a = []

theorem List.erase_cons {α : Type u} [BEq α] (a : α) (b : α) (l : List α) : (b :: l).erase a = if (b == a) = true then l else b :: l.erase a

def List.eraseP {α : Type u} (p : α → Bool) : List α → List α

eraseP p l removes the first element of l satisfying the predicate p.

Equations

• List.eraseP p [] = []
• List.eraseP p (a :: as) = bif p a then as else a :: List.eraseP p as

eraseIdx

def List.eraseIdx {α : Type u} : List α → Nat → List α

O(i). eraseIdx l i removes the i'th element of the list l.

• erase [a, b, c, d, e] 0 = [b, c, d, e]
• erase [a, b, c, d, e] 1 = [a, c, d, e]
• erase [a, b, c, d, e] 5 = [a, b, c, d, e]

Equations

• [].eraseIdx x = []
• (head :: as).eraseIdx 0 = as
• (a :: as).eraseIdx n.succ = a :: as.eraseIdx n

@[simp]

theorem List.eraseIdx_nil {α : Type u} {i : Nat} : [].eraseIdx i = []

@[simp]

theorem List.eraseIdx_cons_zero : ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as

@[simp]

theorem List.eraseIdx_cons_succ : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i

Finding elements

find?

def List.find? {α : Type u} (p : α → Bool) : List α → Option α

O(|l|). find? p l returns the first element for which p returns true, or none if no such element is found.

• find? (· < 5) [7, 6, 5, 8, 1, 2, 6] = some 1
• find? (· < 1) [7, 6, 5, 8, 1, 2, 6] = none

Equations

• List.find? p [] = none
• List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

@[simp]

theorem List.find?_nil {α : Type u} {p : α → Bool} : List.find? p [] = none

theorem List.find?_cons : ∀ {α : Type u_1} {a : α} {as : List α} {p : α → Bool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

findSome?

def List.findSome? {α : Type u} {β : Type v} (f : α → Option β) : List α → Option β

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

@[simp]

theorem List.findSome?_nil {α : Type u} : ∀ {α_1 : Type u_1} {f : α → Option α_1}, List.findSome? f [] = none

theorem List.findSome?_cons {α : Type u} {β : Type v} {a : α} {as : List α} {f : α → Option β} : List.findSome? f (a :: as) = match f a with | some b => some b | none => List.findSome? f as

findIdx

@[inline]

def List.findIdx {α : Type u} (p : α → Bool) (l : List α) : Nat

Returns the index of the first element satisfying p, or the length of the list otherwise.

Equations

• List.findIdx p l = List.findIdx.go p l 0

@[specialize #[]]

def List.findIdx.go {α : Type u} (p : α → Bool) : List α → Nat → Nat

Auxiliary for findIdx: findIdx.go p l n = findIdx p l + n

Equations

• List.findIdx.go p [] x = x
• List.findIdx.go p (a :: l) x = bif p a then x else List.findIdx.go p l (x + 1)

@[simp]

theorem List.findIdx_nil {α : Type u_1} (p : α → Bool) : List.findIdx p [] = 0

indexOf

def List.indexOf {α : Type u} [BEq α] (a : α) : List α → Nat

Returns the index of the first element equal to a, or the length of the list otherwise.

Equations

• List.indexOf a = List.findIdx fun (x : α) => x == a

@[simp]

theorem List.indexOf_nil {α : Type u} {x : α} [BEq α] : List.indexOf x [] = 0

findIdx?

def List.findIdx? {α : Type u} (p : α → Bool) : List α → optParam Nat 0 → Option Nat

Return the index of the first occurrence of an element satisfying p.

Equations

• List.findIdx? p [] x = none
• List.findIdx? p (a :: l) x = if p a = true then some x else List.findIdx? p l (x + 1)

indexOf?

@[inline]

def List.indexOf? {α : Type u} [BEq α] (a : α) : List α → Option Nat

Return the index of the first occurrence of a in the list.

Equations

• List.indexOf? a✝ a = List.findIdx? (fun (x : α) => x == a✝) a

countP

@[inline]

def List.countP {α : Type u} (p : α → Bool) (l : List α) : Nat

countP p l is the number of elements of l that satisfy p.

Equations

• List.countP p l = List.countP.go p l 0

@[specialize #[]]

def List.countP.go {α : Type u} (p : α → Bool) : List α → Nat → Nat

Auxiliary for countP: countP.go p l acc = countP p l + acc.

Equations

• List.countP.go p [] x = x
• List.countP.go p (a :: l) x = bif p a then List.countP.go p l (x + 1) else List.countP.go p l x

count

@[inline]

def List.count {α : Type u} [BEq α] (a : α) : List α → Nat

count a l is the number of occurrences of a in l.

Equations

• List.count a = List.countP fun (x : α) => x == a

lookup

def List.lookup {α : Type u} {β : Type v} [BEq α] : α → List (α × β) → Option β

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.

• lookup 3 [(1, 2), (3, 4), (3, 5)] = some 4
• lookup 2 [(1, 2), (3, 4), (3, 5)] = none

Equations

• List.lookup x [] = none
• List.lookup x ((k, b) :: es) = match x == k with | true => some b | false => List.lookup x es

@[simp]

theorem List.lookup_nil {α : Type u} {β : Type v} {a : α} [BEq α] : List.lookup a [] = none

theorem List.lookup_cons {α : Type u} : ∀ {β : Type u_1} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ((k, b) :: es) = match a == k with | true => some b | false => List.lookup a es

Permutations

Perm

inductive List.Perm {α : Type u} : List α → List α → Prop

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

• nil: ∀ {α : Type u}, [].Perm []

  [] ~ []

• cons: ∀ {α : Type u} (x : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)

  l₁ ~ l₂ → x::l₁ ~ x::l₂

• swap: ∀ {α : Type u} (x y : α) (l : List α), (y :: x :: l).Perm (x :: y :: l)

  x::y::l ~ y::x::l

• trans: ∀ {α : Type u} {l₁ l₂ l₃ : List α}, l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃

  Perm is transitive.

def List.«term_~_» : Lean.TrailingParserDescr

Perm l₁ l₂ or l₁ ~ l₂ asserts that l₁ and l₂ are permutations of each other. This is defined by induction using pairwise swaps.

Equations

• List.«term_~_» = Lean.ParserDescr.trailingNode `List.term_~_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ ") (Lean.ParserDescr.cat `term 51))

isPerm

def List.isPerm {α : Type u} [BEq α] : List α → List α → Bool

O(|l₁| * |l₂|). Computes whether l₁ is a permutation of l₂. See isPerm_iff for a characterization in terms of List.Perm.

Equations

• [].isPerm x = x.isEmpty
• (a :: l).isPerm x = (x.contains a && l.isPerm (x.erase a))

Logical operations

any

def List.any {α : Type u} : List α → (α → Bool) → Bool

O(|l|). Returns true if p is true for any element of l.

• any p [a, b, c] = p a || p b || p c

Short-circuits upon encountering the first true.

Equations

• [].any x = false
• (h :: t).any x = (x h || t.any x)

@[simp]

theorem List.any_nil : ∀ {α : Type u_1} {f : α → Bool}, [].any f = false

@[simp]

theorem List.any_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).any f = (f a || l.any f)

all

def List.all {α : Type u} : List α → (α → Bool) → Bool

O(|l|). Returns true if p is true for every element of l.

• all p [a, b, c] = p a && p b && p c

Short-circuits upon encountering the first false.

Equations

• [].all x = true
• (h :: t).all x = (x h && t.all x)

@[simp]

theorem List.all_nil : ∀ {α : Type u_1} {f : α → Bool}, [].all f = true

@[simp]

theorem List.all_cons : ∀ {α : Type u_1} {a : α} {l : List α} {f : α → Bool}, (a :: l).all f = (f a && l.all f)

or

def List.or (bs : List Bool) : Bool

O(|l|). Returns true if true is an element of the list of booleans l.

• or [a, b, c] = a || b || c

Equations

• bs.or = bs.any id

@[simp]

theorem List.or_nil : [].or = false

@[simp]

theorem List.or_cons {a : Bool} {l : List Bool} : (a :: l).or = (a || l.or)

and

def List.and (bs : List Bool) : Bool

O(|l|). Returns true if every element of l is the value true.

• and [a, b, c] = a && b && c

Equations

• bs.and = bs.all id

@[simp]

theorem List.and_nil : [].and = true

@[simp]

theorem List.and_cons {a : Bool} {l : List Bool} : (a :: l).and = (a && l.and)

Zippers

zipWith

@[specialize #[]]

def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (xs : List α) (ys : List β) : List γ

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 = []

@[simp]

theorem List.zipWith_nil_left {α : Type u} {β : Type v} {γ : Type w} {l : List β} {f : α → β → γ} : List.zipWith f [] l = []

@[simp]

theorem List.zipWith_nil_right {α : Type u} {β : Type v} {γ : Type w} {l : List α} {f : α → β → γ} : List.zipWith f l [] = []

@[simp]

theorem List.zipWith_cons_cons {α : Type u} {β : Type v} {γ : Type w} {a : α} {as : List α} {b : β} {bs : List β} {f : α → β → γ} : List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs

zip

def List.zip {α : Type u} {β : Type v} : List α → List β → List (α × β)

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

@[simp]

theorem List.zip_nil_left {α : Type u} {β : Type v} {l : List β} : [].zip l = []

@[simp]

theorem List.zip_nil_right {α : Type u} {β : Type v} {l : List α} : l.zip [] = []

@[simp]

theorem List.zip_cons_cons : ∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = (a, b) :: as.zip bs

zipWithAll

def List.zipWithAll {α : Type u} {β : Type v} {γ : Type w} (f : Option α → Option β → γ) : List α → List β → List γ

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

@[simp]

theorem List.zipWithAll_nil_right : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as

@[simp]

theorem List.zipWithAll_nil_left : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs

@[simp]

theorem List.zipWithAll_cons_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

unzip

def List.unzip {α : Type u} {β : Type v} : List (α × β) → List α × List β

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

• [].unzip = ([], [])
• ((a, b) :: t).unzip = match t.unzip with | (al, bl) => (a :: al, b :: bl)

@[simp]

theorem List.unzip_nil {α : Type u} {β : Type v} : [].unzip = ([], [])

@[simp]

theorem List.unzip_cons {α : Type u} {β : Type v} {t : List (α × β)} {h : α × β} : (h :: t).unzip = match t.unzip with | (al, bl) => (h.fst :: al, h.snd :: bl)

Ranges and enumeration

def Nat.sum (l : List Nat) : Nat

Sum of a list of natural numbers.

Equations

• Nat.sum l = List.foldr (fun (x1 x2 : Nat) => x1 + x2) 0 l

@[simp]

theorem Nat.sum_nil : Nat.sum [] = 0

@[simp]

theorem Nat.sum_cons (a : Nat) (l : List Nat) : Nat.sum (a :: l) = a + Nat.sum l

range

def List.range (n : Nat) : List Nat

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 []

def List.range.loop : Nat → List Nat → List Nat

Equations

• List.range.loop 0 x = x
• List.range.loop n.succ x = List.range.loop n (n :: x)

@[simp]

theorem List.range_zero : List.range 0 = []

range'

def List.range' (start : Nat) (len : Nat) (step : optParam Nat 1) : List Nat

range' start len step is the list of numbers [start, start+step, ..., start+(len-1)*step]. It is intended mainly for proving properties of range and iota.

Equations

• List.range' x✝ 0 x = []
• List.range' x✝ n.succ x = x✝ :: List.range' (x✝ + x) n x

iota

def List.iota : Nat → List Nat

O(n). iota n is the numbers from 1 to n inclusive, in decreasing order.

• iota 5 = [5, 4, 3, 2, 1]

Equations

• List.iota 0 = []
• List.iota n.succ = n.succ :: List.iota n

@[simp]

theorem List.iota_zero : List.iota 0 = []

@[simp]

theorem List.iota_succ {i : Nat} : List.iota (i + 1) = (i + 1) :: List.iota i

enumFrom

def List.enumFrom {α : Type u} : Nat → List α → List (Nat × α)

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

@[simp]

theorem List.enumFrom_nil {α : Type u} {i : Nat} : List.enumFrom i [] = []

@[simp]

theorem List.enumFrom_cons : ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = (i, a) :: List.enumFrom (i + 1) as

enum

def List.enum {α : Type u} : List α → List (Nat × α)

O(|l|). enum l pairs up each element with its index in the list.

• enum [a, b, c] = [(0, a), (1, b), (2, c)]

Equations

• List.enum = List.enumFrom 0

@[simp]

theorem List.enum_nil {α : Type u} : [].enum = []

Minima and maxima

minimum?

def List.minimum? {α : Type u} [Min α] : List α → Option α

Returns the smallest element of the list, if it is not empty.

• [].minimum? = none
• [4].minimum? = some 4
• [1, 4, 2, 10, 6].minimum? = some 1

Equations

• [].minimum? = none
• (a :: as).minimum? = some (List.foldl min a as)

maximum?

def List.maximum? {α : Type u} [Max α] : List α → Option α

Returns the largest element of the list, if it is not empty.

• [].maximum? = none
• [4].maximum? = some 4
• [1, 4, 2, 10, 6].maximum? = some 10

Equations

• [].maximum? = none
• (a :: as).maximum? = some (List.foldl max a as)

Other list operations

The functions are currently mostly used in meta code, and do not have sufficient API developed for verification work.

intersperse

def List.intersperse {α : Type u} (sep : α) : List α → List α

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

@[simp]

theorem List.intersperse_nil {α : Type u} (sep : α) : List.intersperse sep [] = []

@[simp]

theorem List.intersperse_single {α : Type u} {x : α} (sep : α) : List.intersperse sep [x] = [x]

@[simp]

theorem List.intersperse_cons₂ {α : Type u} {x : α} {y : α} {zs : List α} (sep : α) : List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)

intercalate

def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) : List α

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

eraseDups

def List.eraseDups {α : Type u_1} [BEq α] (as : List α) : List α

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 []

def List.eraseDups.loop {α : Type u_1} [BEq α] : List α → List α → List α

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)

eraseReps

def List.eraseReps {α : Type u_1} [BEq α] : List α → List α

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

• [].eraseReps = []
• (a :: as).eraseReps = List.eraseReps.loop a as []

def List.eraseReps.loop {α : Type u_1} [BEq α] : α → List α → List α → List α

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)

span

@[inline]

def List.span {α : Type u} (p : α → Bool) (as : List α) : List α × List α

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 []

@[specialize #[]]

def List.span.loop {α : Type u} (p : α → Bool) : List α → List α → List α × List α

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)

groupBy

@[specialize #[]]

def List.groupBy {α : Type u} (R : α → α → Bool) : List α → List (List α)

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 [] = []
• List.groupBy R (a :: as) = List.groupBy.loop R as a [] []

@[specialize #[]]

def List.groupBy.loop {α : Type u} (R : α → α → Bool) : List α → α → List α → List (List α) → List (List α)

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

removeAll

def List.removeAll {α : Type u} [BEq α] (xs : List α) (ys : List α) : List α

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

Runtime re-implementations using @[csimp]

More of these re-implementations are provided in Init/Data/List/Impl.lean. They can not be here, because the remaining ones required Array for their implementation.

This leaves a dangerous situation: if you import this file, but not Init/Data/List/Impl.lean, then at runtime you will get non tail-recursive versions.

length

theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n

@[csimp]

theorem List.length_eq_lengthTR : @List.length = @List.lengthTR

map

@[inline]

def List.mapTR {α : Type u} {β : Type v} (f : α → β) (as : List α) : List β

Tail-recursive version of List.map.

Equations

• List.mapTR f as = List.mapTR.loop f as []

@[specialize #[]]

def List.mapTR.loop {α : Type u} {β : Type v} (f : α → β) : List α → List β → List β

Equations

• List.mapTR.loop f [] x = x.reverse
• List.mapTR.loop f (a :: as) x = List.mapTR.loop f as (f a :: x)

theorem List.mapTR_loop_eq {α : Type u} {β : Type v} (f : α → β) (as : List α) (bs : List β) : List.mapTR.loop f as bs = bs.reverse ++ List.map f as

@[csimp]

theorem List.map_eq_mapTR : @List.map = @List.mapTR

filter

@[inline]

def List.filterTR {α : Type u} (p : α → Bool) (as : List α) : List α

Tail-recursive version of List.filter.

Equations

• List.filterTR p as = List.filterTR.loop p as []

@[specialize #[]]

def List.filterTR.loop {α : Type u} (p : α → Bool) : List α → List α → List α

Equations

• List.filterTR.loop p [] x = x.reverse
• List.filterTR.loop p (a :: l) x = match p a with | true => List.filterTR.loop p l (a :: x) | false => List.filterTR.loop p l x

theorem List.filterTR_loop_eq {α : Type u} (p : α → Bool) (as : List α) (bs : List α) : List.filterTR.loop p as bs = bs.reverse ++ List.filter p as

@[csimp]

theorem List.filter_eq_filterTR : @List.filter = @List.filterTR

replicate

def List.replicateTR {α : Type u} (n : Nat) (a : α) : List α

Tail-recursive version of List.replicate.

Equations

• List.replicateTR n a = List.replicateTR.loop a n []

def List.replicateTR.loop {α : Type u} (a : α) : Nat → List α → List α

Equations

• List.replicateTR.loop a 0 x = x
• List.replicateTR.loop a n.succ x = List.replicateTR.loop a n (a :: x)

theorem List.replicateTR_loop_replicate_eq {α : Type u} (a : α) (m : Nat) (n : Nat) : List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a

theorem List.replicateTR_loop_eq : ∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc

@[csimp]

theorem List.replicate_eq_replicateTR : @List.replicate = @List.replicateTR

Additional functions

leftpad

@[inline]

def List.leftpadTR {α : Type u} (n : Nat) (a : α) (l : List α) : List α

Optimized version of leftpad.

Equations

• List.leftpadTR n a l = List.replicateTR.loop a (n - l.length) l

@[csimp]

theorem List.leftpad_eq_leftpadTR : @List.leftpad = @List.leftpadTR

Zippers

unzip

def List.unzipTR {α : Type u} {β : Type v} (l : List (α × β)) : List α × List β

Tail recursive version of List.unzip.

Equations

• l.unzipTR = List.foldr (fun (x : α × β) (x_1 : List α × List β) => match x with | (a, b) => match x_1 with | (al, bl) => (a :: al, b :: bl)) ([], []) l

@[csimp]

theorem List.unzip_eq_unzipTR : @List.unzip = @List.unzipTR

Ranges and enumeration

range'

@[inline]

def List.range'TR (s : Nat) (n : Nat) (step : optParam Nat 1) : List Nat

Optimized version of range'.

Equations

• List.range'TR s n step = List.range'TR.go step n (s + step * n) []

def List.range'TR.go (step : optParam Nat 1) : Nat → Nat → List Nat → List Nat

Auxiliary for range'TR: range'TR.go n e = [e-n, ..., e-1] ++ acc.

Equations

• List.range'TR.go step 0 x✝ x = x
• List.range'TR.go step n.succ x✝ x = List.range'TR.go step n (x✝ - step) ((x✝ - step) :: x)

@[csimp]

theorem List.range'_eq_range'TR : @List.range' = @List.range'TR

theorem List.range'_eq_range'TR.go (step : optParam Nat 1) (s : Nat) (n : Nat) (m : Nat) : List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step

iota

def List.iotaTR (n : Nat) : List Nat

Tail-recursive version of List.iota.

Equations

• List.iotaTR n = List.iotaTR.go n []

def List.iotaTR.go : Nat → List Nat → List Nat

Equations

• List.iotaTR.go 0 x = x.reverse
• List.iotaTR.go n.succ x = List.iotaTR.go n (n.succ :: x)

@[csimp]

theorem List.iota_eq_iotaTR : List.iota = List.iotaTR

Other list operations

intersperse

def List.intersperseTR {α : Type u} (sep : α) : List α → List α

Tail recursive version of List.intersperse.

Equations

• List.intersperseTR sep [] = []
• List.intersperseTR sep [x_1] = [x_1]
• List.intersperseTR sep (x_1 :: y :: xs) = x_1 :: sep :: y :: List.foldr (fun (a : α) (r : List α) => sep :: a :: r) [] xs

@[csimp]

theorem List.intersperse_eq_intersperseTR : @List.intersperse = @List.intersperseTR