Documentation

@[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} {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 : α✝} :

foldl f b [] = b

@[simp]

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

foldl f b (a :: l) = 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 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

Checks whether two lists have the same length and their elements are pairwise BEq. Normally used via the == operator.

Equations

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

@[simp]

theorem List.beq_nil_nil {α : Type u} [BEq α] :

[].beq [] = true

@[simp]

theorem List.beq_cons_nil {α : Type u} [BEq α] {a : α} {as : List α} :

(a :: as).beq [] = false

@[simp]

theorem List.beq_nil_cons {α : Type u} [BEq α] {a : α} {as : List α} :

[].beq (a :: as) = false

theorem List.beq_cons₂ {α : Type u} [BEq α] {a b : α} {as bs : List α} :

(a :: as).beq (b :: bs) = (a == b && as.beq bs)

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

BEq (List α)

Equations

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

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

LawfulBEq (List α)

@[specialize #[]]

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

Returns true if as and bs have the same length and they are pairwise related by eqv.

O(min |as| |bs|). Short-circuits at the first non-related pair of elements.

Examples:

[1, 2, 3].isEqv [2, 3, 4] (· < ·) = true
[1, 2, 3].isEqv [2, 2, 4] (· < ·) = false
[1, 2, 3].isEqv [2, 3] (· < ·) = false

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.Lex {α : Type u} (r : α → α → Prop) (as bs : List α) :

Lexicographic ordering for lists with respect to an ordering of elements.

as is lexicographically smaller than bs if

as is empty and bs is non-empty, or
both as and bs are non-empty, and the head of as is less than the head of bs according to r, or
both as and bs are non-empty, their heads are equal, and the tail of as is less than the tail of bs.

nil {α : Type u} {r : α → α → Prop} {a : α} {l : List α} : Lex r [] (a :: l)
[] is the smallest element in the lexicographic order.
rel {α : Type u} {r : α → α → Prop} {a₁ : α} {l₁ : List α} {a₂ : α} {l₂ : List α} (h : r a₁ a₂) : Lex r (a₁ :: l₁) (a₂ :: l₂)
If the head of the first list is smaller than the head of the second, then the first list is lexicographically smaller than the second list.
cons {α : Type u} {r : α → α → Prop} {a : α} {l₁ l₂ : List α} (h : Lex r l₁ l₂) : Lex r (a :: l₁) (a :: l₂)
If two lists have the same head, then their tails determine their lexicographic order. If the tail of the first list is lexicographically smaller than the tail of the second list, then the entire first list is lexicographically smaller than the entire second list.

Instances For

List.decidableLex

instance List.decidableLex {α : Type u} [DecidableEq α] (r : α → α → Prop) [h : DecidableRel r] (l₁ l₂ : List α) :

Decidable (Lex r l₁ l₂)

Equations

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

@[reducible, inline]

abbrev List.lt {α : Type u} [LT α] :

List α → List α → Prop

Lexicographic ordering of lists with respect to an ordering on their elements.

as < bs if

as is empty and bs is non-empty, or
both as and bs are non-empty, and the head of as is less than the head of bs, or
both as and bs are non-empty, their heads are equal, and the tail of as is less than the tail of bs.

Equations

List.lt = List.Lex fun (x1 x2 : α) => x1 < x2

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

LT (List α)

Equations

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

instance List.decidableLT {α : Type u} [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :

Decidable (l₁ < l₂)

Decidability of lexicographic ordering.

Equations

l₁.decidableLT l₂ = List.decidableLex (fun (x1 x2 : α) => x1 < x2) l₁ l₂

@[reducible, inline, deprecated List.decidableLT (since := "2024-12-13")]

abbrev List.hasDecidableLt {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :

Decidable (l₁ < l₂)

Decidability of lexicographic ordering.

Equations

@List.hasDecidableLt = @List.decidableLT

@[reducible]

def List.le {α : Type u} [LT α] (as bs : List α) :

Non-strict ordering of lists with respect to a strict ordering of their elements.

as ≤ bs if ¬ bs < as.

This relation can be treated as a lexicographic order if the underlying LT α instance is well-behaved. In particular, it should be irreflexive, asymmetric, and antisymmetric. These requirements are precisely formulated in List.cons_le_cons_iff. If these hold, then as ≤ bs if and only if:

as is empty, or
both as and bs are non-empty, and the head of as is less than the head of bs, or
both as and bs are non-empty, their heads are equal, and the tail of as is less than or equal to the tail of bs.

Equations

as.le bs = ¬bs < as

instance List.instLE {α : Type u} [LT α] :

LE (List α)

Equations

List.instLE = { le := List.le }

instance List.decidableLE {α : Type u} [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :

Decidable (l₁ ≤ l₂)

Equations

l₁.decidableLE l₂ = inferInstanceAs (Decidable ¬l₂ < l₁)

def List.lex {α : Type u} [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) :

Compares lists lexicographically with respect to a comparison on their elements.

The lexicographic order with respect to lt is:

[].lex (b :: bs) is true
as.lex [] = false is false
(a :: as).lex (b :: bs) is true if lt a b or a == b and lex lt as bs is true.

Equations

[].lex (head :: tail) lt = true
l₁.lex [] lt = false
(a :: as).lex (b :: bs) lt = (lt a b || a == b && as.lex bs lt)

theorem List.nil_lex_nil {α : Type u} {lt : α → α → Bool} [BEq α] :

[].lex [] lt = false

@[simp]

theorem List.nil_lex_cons {α : Type u} {lt : α → α → Bool} [BEq α] {b : α} {bs : List α} :

[].lex (b :: bs) lt = true

theorem List.cons_lex_nil {α : Type u} {lt : α → α → Bool} [BEq α] {a : α} {as : List α} :

(a :: as).lex [] lt = false

@[simp]

theorem List.cons_lex_cons {α : Type u} {lt : α → α → Bool} [BEq α] {a b : α} {as bs : List α} :

(a :: as).lex (b :: bs) lt = (lt a b || a == b && as.lex bs lt)

@[simp]

theorem List.lex_nil {α : Type u} {lt : α → α → Bool} [BEq α] {as : List α} :

as.lex [] lt = false

@[deprecated List.nil_lex_nil (since := "2025-02-10")]

theorem List.lex_nil_nil {α : Type u} {lt : α → α → Bool} [BEq α] :

[].lex [] lt = false

@[deprecated List.nil_lex_cons (since := "2025-02-10")]

theorem List.lex_nil_cons {α : Type u} {lt : α → α → Bool} [BEq α] {b : α} {bs : List α} :

[].lex (b :: bs) lt = true

@[deprecated List.cons_lex_nil (since := "2025-02-10")]

theorem List.lex_cons_nil {α : Type u} {lt : α → α → Bool} [BEq α] {a : α} {as : List α} :

(a :: as).lex [] lt = false

@[deprecated List.cons_lex_cons (since := "2025-02-10")]

theorem List.lex_cons_cons {α : Type u} {lt : α → α → Bool} [BEq α] {a b : α} {as bs : List α} :

(a :: as).lex (b :: bs) lt = (lt a b || a == b && as.lex bs lt)

Alternative getters #

getLast #

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

as ≠ [] → α

Returns the last element of a non-empty list.

Examples:

["circle", "rectangle"].getLast (by decide) = "rectangle"
["circle"].getLast (by decide) = "circle"

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, or none if the list is empty.

Alternatives include List.getLastD, which takes a fallback value for empty lists, and List.getLast!, which panics on empty lists.

Examples:

["circle", "rectangle"].getLast? = some "rectangle"
["circle"].getLast? = some "circle"
([] : List String).getLast? = none

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, or fallback if the list is empty.

Alternatives include List.getLast?, which returns an Option, and List.getLast!, which panics on empty lists.

Examples:

["circle", "rectangle"].getLastD "oval" = "rectangle"
["circle"].getLastD "oval" = "circle"
([] : List String).getLastD "oval" = "oval"

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 there is one. Returns none if the list is empty.

Use List.headD to provide a fallback value for empty lists, or List.head! to panic on empty lists.

Examples:

([] : List Nat).head? = none
[3, 2, 1].head? = some 3

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 there is one, or fallback if the list is empty.

Use List.head? to return an Option, and List.head! to panic on empty lists.

Examples:

[].headD "empty" = "empty"
[].headD 2 = 2
["head", "shoulders", "knees"].headD "toes" = "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 α

Drops the first element of a nonempty list, returning the tail. Returns [] when the argument is empty.

Examples:

["apple", "banana", "grape"].tail = ["banana", "grape"]
["apple"].tail = []
([] : List String).tail = []

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 a nonempty list, returning the tail. Returns none when the argument is empty.

Alternatives include List.tail, which returns the empty list on failure, List.tailD, which returns an explicit fallback value, and List.tail!, which panics on the empty list.

Examples:

["apple", "banana", "grape"].tail? = some ["banana", "grape"]
["apple"].tail? = some []
([] : List String).tail = none

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} (l fallback : List α) :

List α

Drops the first element of a nonempty list, returning the tail. Returns none when the argument is empty.

Alternatives include List.tail, which returns the empty list on failure, List.tail?, which returns an Option, and List.tail!, which panics on the empty list.

Examples:

["apple", "banana", "grape"].tailD ["orange"] = ["banana", "grape"]
["apple"].tailD ["orange"] = []
[].tailD ["orange"] = ["orange"]

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 l' : List α} :

(a :: l).tailD l' = l

Basic `List` operations. #

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

map #

@[specialize #[]]

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

List β

Applies a function to each element of the list, returning the resulting list of values.

O(|l|).

Examples:

[a, b, c].map f = [f a, f b, f c]
[].map Nat.succ = []
["one", "two", "three"].map (·.length) = [3, 3, 5]
["one", "two", "three"].map (·.reverse) = ["eno", "owt", "eerht"]

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 : α → β} :

map f [] = []

@[simp]

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

map f (a :: l) = f a :: map f l

filter #

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

List α

Returns the list of elements in l for which p returns true.

O(|l|).

Examples:

[1, 2, 5, 2, 7, 7].filter (· > 2) = [5, 7, 7]
[1, 2, 5, 2, 7, 7].filter (fun _ => false) = []
[1, 2, 5, 2, 7, 7].filter (fun _ => true) = [1, 2, 5, 2, 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} :

filter p [] = []

filterMap #

@[specialize #[]]

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

List α → List β

Applies a function that returns an Option to each element of a list, collecting the non-none values.

O(|l|).

Example:

#eval [1, 2, 5, 2, 7, 7].filterMap fun x =>
  if x > 2 then some (2 * x) else none

[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 β} :

filterMap f [] = []

theorem List.filterMap_cons {α : Type u} {β : Type v} {f : α → Option β} {a : α} {l : List α} :

filterMap f (a :: l) = match f a with | none => filterMap f l | some b => b :: filterMap f l

foldr #

@[specialize #[]]

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

Folds a function over a list from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the list in reverse order, using f.

O(|l|). Replaced at runtime with List.foldrTR.

Examples:

[a, b, c].foldr f init = f a (f b (f c init))
[1, 2, 3].foldr (toString · ++ ·) "" = "123"
[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"

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} {α✝¹ : Type u_2} {f : α✝ → α✝¹ → α✝¹} {b : α✝¹} :

foldr f b [] = b

@[simp]

theorem List.foldr_cons {α : Type u} {β : Type v} {a : α} {l : List α} {f : α → β → β} {b : β} :

foldr f b (a :: l) = f a (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 α

Reverses a list.

O(|as|).

Because of the “functional but in place” optimization implemented by Lean's compiler, this function does not allocate a new list when its reference to the input list is unshared: it simply walks the linked list and reverses all the node pointers.

Examples:

[1, 2, 3, 4].reverse = [4, 3, 2, 1]
[].reverse = []

Equations

as.reverse = as.reverseAux []

@[simp]

theorem List.reverse_nil {α : Type u} :

[].reverse = []

theorem List.reverseAux_reverseAux {α : Type u} {as bs cs : List α} :

(as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux []).reverseAux cs)

append #

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

List α

Appends two lists. Normally used via the ++ operator.

Appending lists takes time proportional to the length of the first list: O(|xs|).

Examples:

[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5].
[] ++ [4, 5] = [4, 5].
[1, 2, 3] ++ [] = [1, 2, 3].

Equations

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

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

List α

Appends two lists. Normally used via the ++ operator.

Appending lists takes time proportional to the length of the first list: O(|xs|).

This is a tail-recursive version of List.append.

Examples:

[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5].
[] ++ [4, 5] = [4, 5].
[1, 2, 3] ++ [] = [1, 2, 3].

Equations

as.appendTR bs = as.reverse.reverseAux bs

@[csimp]

theorem List.append_eq_appendTR :

@List.append = @appendTR

instance List.instAppend {α : Type u} :

Append (List α)

Equations

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

@[simp]

theorem List.append_eq {α : Type u} {as 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 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) []

@[simp]

theorem List.length_append {α : Type u} {as bs : List α} :

(as ++ bs).length = as.length + bs.length

@[simp]

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

as ++ bs ++ cs = as ++ (bs ++ cs)

instance List.instAssociativeHAppend {α : Type u} :

Std.Associative fun (x1 x2 : List α) => x1 ++ x2

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 bs : List α} :

as.reverseAux bs = as.reverseAux [] ++ bs

@[simp]

theorem List.reverse_cons {α : Type u} {a : α} {as : List α} :

(a :: as).reverse = as.reverse ++ [a]

flatten #

def List.flatten {α : Type u} :

List (List α) → List α

Concatenates a list of lists into a single list, preserving the order of the elements.

O(|flatten L|).

Examples:

[["a"], ["b", "c"]].flatten = ["a", "b", "c"]
[["a"], [], ["b", "c"], ["d", "e", "f"]].flatten = ["a", "b", "c", "d", "e", "f"]

Equations

[].flatten = []
(l :: L).flatten = l ++ L.flatten

@[simp]

theorem List.flatten_nil {α : Type u} :

[].flatten = []

@[simp]

theorem List.flatten_cons {α✝ : Type u_1} {l : List α✝} {L : List (List α✝)} :

(l :: L).flatten = l ++ L.flatten

@[reducible, inline, deprecated List.flatten (since := "2024-10-14")]

abbrev List.join {α : Type u_1} :

List (List α) → List α

Concatenates a list of lists into a single list, preserving the order of the elements.

O(|flatten L|).

Examples:

[["a"], ["b", "c"]].flatten = ["a", "b", "c"]
[["a"], [], ["b", "c"], ["d", "e", "f"]].flatten = ["a", "b", "c", "d", "e", "f"]

Equations

@List.join = @List.flatten

singleton #

@[inline]

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

List α

Constructs a single-element list.

Examples:

List.singleton 5 = [5].
List.singleton "green" = ["green"].
List.singleton [1, 2, 3] = [[1, 2, 3]]

Equations

List.singleton a = [a]

@[reducible, inline, deprecated Singleton.singleton (since := "2024-10-16")]

abbrev List.pure {α : outParam (Type u_1)} {β : Type u_2} [self : Singleton α β] :

α → β

Equations

@List.pure = @singleton

flatMap #

@[inline]

def List.flatMap {α : Type u} {β : Type v} (b : α → List β) (as : List α) :

List β

Applies a function that returns a list to each element of a list, and concatenates the resulting lists.

Examples:

[2, 3, 2].flatMap List.range = [0, 1, 0, 1, 2, 0, 1]
["red", "blue"].flatMap String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']

Equations

List.flatMap b as = (List.map b as).flatten

@[simp]

theorem List.flatMap_nil {α : Type u} {β : Type v} {f : α → List β} :

flatMap f [] = []

@[simp]

theorem List.flatMap_cons {α : Type u} {β : Type v} {x : α} {xs : List α} {f : α → List β} :

flatMap f (x :: xs) = f x ++ flatMap f xs

@[reducible, inline, deprecated List.flatMap (since := "2024-10-16")]

abbrev List.bind {α : Type u_1} {β : Type u_2} (b : α → List β) (as : List α) :

List β

Equations

@List.bind = @List.flatMap

@[reducible, inline, deprecated List.flatMap_nil (since := "2024-10-16")]

abbrev List.nil_flatMap {α : Type u_1} {β : Type u_2} {f : α → List β} :

flatMap f [] = []

Equations

@List.nil_flatMap = @List.flatMap_nil

@[reducible, inline, deprecated List.flatMap_cons (since := "2024-10-16")]

abbrev List.cons_flatMap {α : Type u_1} {β : Type u_2} {x : α} {xs : List α} {f : α → List β} :

flatMap f (x :: xs) = f x ++ flatMap f xs

Equations

@List.cons_flatMap = @List.flatMap_cons

replicate #

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

List α

Creates a list that contains n copies of a.

List.replicate 5 "five" = ["five", "five", "five", "five", "five"]
List.replicate 0 "zero" = []
List.replicate 2 ' ' = [' ', ' ']

Equations

List.replicate 0 x✝ = []
List.replicate n.succ x✝ = x✝ :: List.replicate n x✝

@[simp]

theorem List.replicate_zero {α : Type u} {a : α} :

replicate 0 a = []

theorem List.replicate_succ {α : Type u} {a : α} {n : Nat} :

replicate (n + 1) a = a :: replicate n a

@[simp]

theorem List.length_replicate {α : Type u} {n : Nat} {a : α} :

(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 already has at least n elements, it is returned unmodified.

Examples:

[1, 2, 3].leftpad 5 0 = [0, 0, 1, 2, 3]
["red", "green", "blue"].leftpad 4 "blank" = ["blank", "red", "green", "blue"]
["red", "green", "blue"].leftpad 3 "blank" = ["red", "green", "blue"]
["red", "green", "blue"].leftpad 1 "blank" = ["red", "green", "blue"]

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 already has at least n elements, it is returned unmodified.

Examples:

[1, 2, 3].rightpad 5 0 = [1, 2, 3, 0, 0]
["red", "green", "blue"].rightpad 4 "blank" = ["red", "green", "blue", "blank"]
["red", "green", "blue"].rightpad 3 "blank" = ["red", "green", "blue"]
["red", "green", "blue"].rightpad 1 "blank" = ["red", "green", "blue"]

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

Checks whether a list is empty.

O(1).

Examples:

[].isEmpty = true
["grape"].isEmpty = false
["apple", "banana"].isEmpty = 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 : α) (l : List α) :

Checks whether a is an element of l, using == to compare elements.

O(|l|). List.contains is a synonym that takes the list before the element.

The preferred simp normal form is l.contains a. When LawfulBEq α is available, l.contains a = true ↔ a ∈ l and l.contains a = false ↔ a ∉ l.

Example:

List.elem 3 [1, 4, 2, 3, 3, 7] = true
List.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 α] :

elem a [] = false

theorem List.elem_cons {α : Type u} {b : α} {bs : List α} [BEq α] {a : α} :

elem a (b :: bs) = match a == b with | true => true | false => elem a bs

contains #

@[reducible, inline]

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

Checks whether a is an element of as, using == to compare elements.

O(|as|). List.elem is a synonym that takes the element before the list.

The preferred simp normal form is l.contains a, and when LawfulBEq α is available, l.contains a = true ↔ a ∈ l and l.contains a = false ↔ a ∉ l.

Examples:

[1, 4, 2, 3, 3, 7].contains 3 = true
List.contains [1, 4, 2, 3, 3, 7] 5 = 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

List membership, typically accessed via the ∈ operator.

a ∈ l means that a is an element of the list l. Elements are compared according to Lean's logical equality.

The related function List.elem is a Boolean membership test that uses a BEq α instance.

Examples:

a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z

head {α : Type u} {a : α} (as : List α) : Mem a (a :: as)
The head of a list is a member: a ∈ a :: as.
tail {α : Type u} {a : α} (b : α) {as : List α} : Mem a as → 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 α} :

elem a as = true → a ∈ as

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

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_left {α : Type u} {a : α} {as : List α} (bs : List α) :

a ∈ as → a ∈ as ++ bs

theorem List.mem_append_right {α : Type u} {b : α} (as : List α) {bs : 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} (n : Nat) (xs : List α) :

List α

Extracts the first n elements of xs, or the whole list if n is greater than xs.length.

O(min n |xs|).

Examples:

[a, b, c, d, e].take 0 = []
[a, b, c, d, e].take 3 = [a, b, c]
[a, b, c, d, e].take 6 = [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} :

take i [] = []

@[simp]

theorem List.take_zero {α : Type u} {l : List α} :

take 0 l = []

@[simp]

theorem List.take_succ_cons {α : Type u} {a : α} {as : List α} {i : Nat} :

take (i + 1) (a :: as) = a :: take i as

drop #

def List.drop {α : Type u} (n : Nat) (xs : List α) :

List α

Removes the first n elements of the list xs. Returns the empty list if n is greater than the length of the list.

O(min n |xs|).

Examples:

[0, 1, 2, 3, 4].drop 0 = [0, 1, 2, 3, 4]
[0, 1, 2, 3, 4].drop 3 = [3, 4]
[0, 1, 2, 3, 4].drop 6 = []

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} :

drop i [] = []

@[simp]

theorem List.drop_zero {α : Type u} {l : List α} :

drop 0 l = l

@[simp]

theorem List.drop_succ_cons {α : Type u} {a : α} {l : List α} {i : Nat} :

drop (i + 1) (a :: l) = drop i l

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

drop i as = []

extract #

@[reducible, inline]

abbrev List.extract {α : Type u} (l : List α) (start : Nat := 0) (stop : Nat := l.length) :

List α

Returns the slice of l from indices start (inclusive) to stop (exclusive).

Examples:

[0, 1, 2, 3, 4, 5].extract 1 2 = [1]
[0, 1, 2, 3, 4, 5].extract 2 2 = []
[0, 1, 2, 3, 4, 5].extract 2 4 = [2, 3]
[0, 1, 2, 3, 4, 5].extract 2 = [2, 3, 4, 5]
[0, 1, 2, 3, 4, 5].extract (stop := 2) = [0, 1]

Equations

l.extract start stop = List.take (stop - start) (List.drop start l)

@[simp]

theorem List.extract_eq_drop_take {α : Type u} {l : List α} {start stop : Nat} :

l.extract start stop = take (stop - start) (drop start l)

takeWhile #

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

List α

Returns the longest initial segment of xs for which p returns true.

O(|xs|).

Examples:

[7, 6, 4, 8].takeWhile (· > 5) = [7, 6]
[7, 6, 6, 5].takeWhile (· > 5) = [7, 6, 6]
[7, 6, 6, 8].takeWhile (· > 5) = [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} :

takeWhile p [] = []

dropWhile #

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

List α → List α

Removes the longest prefix of a list for which p returns true.

Elements are removed from the list until one is encountered for which p returns false. This element and the remainder of the list are returned.

O(|l|).

Examples:

[1, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [4, 2, 7, 4]
[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]
[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []

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} :

dropWhile p [] = []

partition #

@[inline]

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

List α × List α

Returns a pair of lists that together contain all the elements of as. The first list contains those elements for which p returns true, and the second contains those for which p returns false.

O(|l|). as.partition p is equivalent to (as.filter p, as.filter (not ∘ p)), but it is slightly more efficient since it only has to do one pass over the list.

Examples:

[1, 2, 5, 2, 7, 7].partition (· > 2) = ([5, 7, 7], [1, 2, 2])
[1, 2, 5, 2, 7, 7].partition (fun _ => false) = ([], [1, 2, 5, 2, 7, 7])
[1, 2, 5, 2, 7, 7].partition (fun _ => true) = ([1, 2, 5, 2, 7, 7], [])

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, if one exists.

Examples:

[].dropLast = []
["tea"].dropLast = []
["tea", "coffee", "juice"].dropLast = ["tea", "coffee"]

Equations

@[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₁ l₂ : List α) :

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

The first list is a non-contiguous sub-list of the second list. Typically written with the <+ operator.

In other words, l₁ <+ l₂ means that l₁ can be transformed into l₂ by repeatedly inserting new elements.

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

Instances For

def List.«term_<+_» :

The first list is a non-contiguous sub-list of the second list. Typically written with the <+ operator.

In other words, l₁ <+ l₂ means that l₁ can be transformed into l₂ by repeatedly inserting new elements.

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, comparing elements with the == operator.

The relation List.Sublist is a logical characterization of this property.

Examples:

[1, 3].isSublist [0, 1, 2, 3, 4] = true
[1, 3].isSublist [0, 1, 2, 4] = false

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₁ l₂ : List α) :

The first list is a prefix of the second.

IsPrefix l₁ l₂, written l₁ <+: l₂, means that there exists some t : List α such that l₂ has the form l₁ ++ t.

The function List.isPrefixOf is a Boolean equivalent.

Conventions for notations in identifiers:

The recommended spelling of <+: in identifiers is prefix (not isPrefix).

Equations

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

Instances For

List.instDecidableIsPrefixOfDecidableEq

def List.«term_<+:_» :

The first list is a prefix of the second.

IsPrefix l₁ l₂, written l₁ <+: l₂, means that there exists some t : List α such that l₂ has the form l₁ ++ t.

The function List.isPrefixOf is a Boolean equivalent.

Conventions for notations in identifiers:

The recommended spelling of <+: in identifiers is prefix (not isPrefix).

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

Checks whether the first list is a prefix of the second.

The relation List.IsPrefixOf expresses this property with respect to logical equality.

Examples:

[1, 2].isPrefixOf [1, 2, 3] = true
[1, 2].isPrefixOf [1, 2] = true
[1, 2].isPrefixOf [1] = false
[1, 2].isPrefixOf [1, 1, 2, 3] = false

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 α] (l₁ l₂ : List α) :

Option (List α)

If the first list is a prefix of the second, returns the result of dropping the prefix.

In other words, isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

Examples:

[1, 2].isPrefixOf? [1, 2, 3] = some [3]
[1, 2].isPrefixOf? [1, 2] = some []
[1, 2].isPrefixOf? [1] = none
[1, 2].isPrefixOf? [1, 1, 2, 3] = none

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₁ l₂ : List α) :

Checks whether the first list is a suffix of the second.

The relation List.IsSuffixOf expresses this property with respect to logical equality.

Examples:

[2, 3].isSuffixOf [1, 2, 3] = true
[2, 3].isSuffixOf [1, 2, 3, 4] = false
[2, 3].isSuffixOf [1, 2] = false
[2, 3].isSuffixOf [1, 1, 2, 3] = true

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₁ l₂ : List α) :

Option (List α)

If the first list is a suffix of the second, returns the result of dropping the suffix from the second.

In other words, isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

Examples:

[2, 3].isSuffixOf? [1, 2, 3] = some [1]
[2, 3].isSuffixOf? [1, 2, 3, 4] = none
[2, 3].isSuffixOf? [1, 2] = none
[2, 3].isSuffixOf? [1, 1, 2, 3] = some [1, 1]

Equations

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

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

The first list is a suffix of the second.

IsSuffix l₁ l₂, written l₁ <:+ l₂, means that there exists some t : List α such that l₂ has the form t ++ l₁.

The function List.isSuffixOf is a Boolean equivalent.

Conventions for notations in identifiers:

The recommended spelling of <:+ in identifiers is suffix (not isSuffix).

Equations

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

Instances For

List.instDecidableIsSuffixOfDecidableEq

def List.«term_<:+_» :

The first list is a suffix of the second.

IsSuffix l₁ l₂, written l₁ <:+ l₂, means that there exists some t : List α such that l₂ has the form t ++ l₁.

The function List.isSuffixOf is a Boolean equivalent.

Conventions for notations in identifiers:

The recommended spelling of <:+ in identifiers is suffix (not isSuffix).

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₁ l₂ : List α) :

The first list is a contiguous sub-list of the second list. Typically written with the <:+: operator.

In other words, l₁ <:+: l₂ means that there exist lists s : List α and t : List α such that l₂ has the form s ++ l₁ ++ t.

Conventions for notations in identifiers:

The recommended spelling of <:+: in identifiers is infix (not isInfix).

Equations

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

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

The first list is a contiguous sub-list of the second list. Typically written with the <:+: operator.

In other words, l₁ <:+: l₂ means that there exist lists s : List α and t : List α such that l₂ has the form s ++ l₁ ++ t.

Conventions for notations in identifiers:

The recommended spelling of <:+: in identifiers is infix (not isInfix).

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 α

Splits a list at an index, resulting in the first n elements of l paired with the remaining elements.

If n is greater than the length of l, then the resulting pair consists of l and the empty list. List.splitAt is equivalent to a combination of List.take and List.drop, but it is more efficient.

Examples:

["red", "green", "blue"].splitAt 2 = (["red", "green"], ["blue"])
["red", "green", "blue"].splitAt 3 = (["red", "green", "blue], [])
["red", "green", "blue"].splitAt 4 = (["red", "green", "blue], [])

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 α) (i : Nat := 1) :

List α

Rotates the elements of xs to the left, moving i % xs.length elements from the start of the list to the end.

O(|xs|).

Examples:

[1, 2, 3, 4, 5].rotateLeft 3 = [4, 5, 1, 2, 3]
[1, 2, 3, 4, 5].rotateLeft 5 = [1, 2, 3, 4, 5]
[1, 2, 3, 4, 5].rotateLeft 1 = [2, 3, 4, 5, 1]

Equations

xs.rotateLeft i = if xs.length ≤ 1 then xs else let i := i % xs.length; let ys := List.take i xs; let zs := List.drop i xs; zs ++ ys

@[simp]

theorem List.rotateLeft_nil {α : Type u} {n : Nat} :

[].rotateLeft n = []

rotateRight #

def List.rotateRight {α : Type u} (xs : List α) (i : Nat := 1) :

List α

Rotates the elements of xs to the right, moving i % xs.length elements from the end of the list to the start.

After rotation, the element at xs[n] is at index (i + n) % l.length. O(|xs|).

Examples:

[1, 2, 3, 4, 5].rotateRight 3 = [3, 4, 5, 1, 2]
[1, 2, 3, 4, 5].rotateRight 5 = [1, 2, 3, 4, 5]
[1, 2, 3, 4, 5].rotateRight 1 = [5, 1, 2, 3, 4]

Equations

xs.rotateRight i = if xs.length ≤ 1 then xs else let i := xs.length - i % xs.length; let ys := List.take i xs; let zs := List.drop i xs; zs ++ ys

@[simp]

theorem List.rotateRight_nil {α : Type u} {n : Nat} :

[].rotateRight n = []

Pairwise, Nodup #

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

List α → Prop

Each element of a list is related to all later elements of the list by R.

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

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

Examples:

Pairwise (· < ·) [1, 2, 3] ↔ (1 < 2 ∧ 1 < 3) ∧ 2 < 3
Pairwise (· = ·) [1, 2, 3] = False
Pairwise (· ≠ ·) [1, 2, 3] = True

nil {α : Type u} {R : α → α → Prop} : 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') → Pairwise R l → Pairwise R (a :: l)
A nonempty list is pairwise related with R if the head is related to every element of the tail and the tail is itself pairwise related.
That is, a :: l is Pairwise R if:
- R relates a to every element of l
- l is Pairwise R.

Instances For

List.instDecidablePairwise

@[simp]

theorem List.pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : List α} :

Pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ Pairwise R l

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

Decidable (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

The list has no duplicates: it contains every element at most once.

It is defined as Pairwise (· ≠ ·): each element is unequal to all other elements.

Equations

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

Instances For

List.nodupDecidable

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 α] (l : List α) (a b : α) :

List α

Replaces the first element of the list l that is equal to a with b. If no element is equal to a, then the list is returned unchanged.

O(|l|).

Examples:

[1, 4, 2, 3, 3, 7].replace 3 6 = [1, 4, 2, 6, 3, 7]
[1, 4, 2, 3, 3, 7].replace 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

modify #

def List.modifyTailIdx {α : Type u} (l : List α) (i : Nat) (f : List α → List α) :

List α

Replaces the nth tail of l with the result of applying f to it. Returns the input without using f if the index is larger than the length of the List.

Examples:

["circle", "square", "triangle"].modifyTailIdx 1 List.reverse

["circle", "triangle", "square"]

["circle", "square", "triangle"].modifyTailIdx 1 (fun xs => xs ++ xs)

["circle", "square", "triangle", "square", "triangle"]

["circle", "square", "triangle"].modifyTailIdx 2 (fun xs => xs ++ xs)

["circle", "square", "triangle", "triangle"]

["circle", "square", "triangle"].modifyTailIdx 5 (fun xs => xs ++ xs)

["circle", "square", "triangle"]

Equations

l.modifyTailIdx i f = List.modifyTailIdx.go f i l

def List.modifyTailIdx.go {α : Type u} (f : List α → List α) :

Nat → List α → List α

Equations

List.modifyTailIdx.go f 0 x✝ = f x✝
List.modifyTailIdx.go f n.succ [] = []
List.modifyTailIdx.go f n.succ (a :: as) = a :: List.modifyTailIdx.go f n as

@[simp]

theorem List.modifyTailIdx_zero {α : Type u} {f : List α → List α} {l : List α} :

l.modifyTailIdx 0 f = f l

@[simp]

theorem List.modifyTailIdx_succ_nil {α : Type u} {f : List α → List α} {i : Nat} :

[].modifyTailIdx (i + 1) f = []

@[simp]

theorem List.modifyTailIdx_succ_cons {α : Type u} {f : List α → List α} {i : Nat} {a : α} {l : List α} :

(a :: l).modifyTailIdx (i + 1) f = a :: l.modifyTailIdx i f

@[inline]

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

List α → List α

Replace the head of the list with the result of applying f to it. Returns the empty list if the list is empty.

Examples:

[1, 2, 3].modifyHead (· * 10) = [10, 2, 3]
[].modifyHead (· * 10) = []

Equations

List.modifyHead f [] = []
List.modifyHead f (a :: as) = f a :: as

@[simp]

theorem List.modifyHead_nil {α : Type u} {f : α → α} :

modifyHead f [] = []

@[simp]

theorem List.modifyHead_cons {α : Type u} {a : α} {l : List α} {f : α → α} :

modifyHead f (a :: l) = f a :: l

def List.modify {α : Type u} (l : List α) (i : Nat) (f : α → α) :

List α

Replaces the element at the given index, if it exists, with the result of applying f to it. If the index is invalid, the list is returned unmodified.

Examples:

[1, 2, 3].modify 0 (· * 10) = [10, 2, 3]
[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]
[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]

Equations

l.modify i f = l.modifyTailIdx i (List.modifyHead f)

insert #

@[inline]

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

List α

Inserts an element into a list without duplication.

If the element is present in the list, the list is returned unmodified. Otherwise, the new element is inserted at the head of the list.

Examples:

[1, 2, 3].insert 0 = [0, 1, 2, 3]
[1, 2, 3].insert 4 = [4, 1, 2, 3]
[1, 2, 3].insert 2 = [1, 2, 3]

Equations

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

def List.insertIdx {α : Type u} (xs : List α) (i : Nat) (a : α) :

List α

Inserts an element into a list at the specified index. If the index is greater than the length of the list, then the list is returned unmodified.

In other words, the new element is inserted into the list l after the first i elements of l.

Examples:

["tues", "thur", "sat"].insertIdx 1 "wed" = ["tues", "wed", "thur", "sat"]
["tues", "thur", "sat"].insertIdx 2 "wed" = ["tues", "thur", "wed", "sat"]
["tues", "thur", "sat"].insertIdx 3 "wed" = ["tues", "thur", "sat", "wed"]
["tues", "thur", "sat"].insertIdx 4 "wed" = ["tues", "thur", "sat"]

Equations

xs.insertIdx i a = xs.modifyTailIdx i (List.cons a)

erase #

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

List α → α → List α

Removes the first occurrence of a from l. If a does not occur in l, the list is returned unmodified.

O(|l|).

Examples:

[1, 5, 3, 2, 5].erase 5 = [1, 3, 2, 5]
[1, 5, 3, 2, 5].erase 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 α

Removes the first element of a list for which p returns true. If no element satisfies p, then the list is returned unchanged.

Examples:

[2, 1, 2, 1, 3, 4].eraseP (· < 2) = [2, 2, 1, 3, 4]
[2, 1, 2, 1, 3, 4].eraseP (· > 2) = [2, 1, 2, 1, 4]
[2, 1, 2, 1, 3, 4].eraseP (· > 8) = [2, 1, 2, 1, 3, 4]

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} (l : List α) (i : Nat) :

List α

Removes the element at the specified index. If the index is out of bounds, the list is returned unmodified.

O(i).

Examples:

[0, 1, 2, 3, 4].eraseIdx 0 = [1, 2, 3, 4]
[0, 1, 2, 3, 4].eraseIdx 1 = [0, 2, 3, 4]
[0, 1, 2, 3, 4].eraseIdx 5 = [0, 1, 2, 3, 4]

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 α

Returns the first element of the list for which the predicate p returns true, or none if no such element is found.

O(|l|).

Examples:

[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1
[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = 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} :

find? p [] = none

theorem List.find?_cons {α✝ : Type u_1} {a : α✝} {as : List α✝} {p : α✝ → Bool} :

find? p (a :: as) = match p a with | true => some a | false => find? p as

findSome? #

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

List α → Option β

Returns the first non-none result of applying f to each element of the list in order. Returns none if f returns none for all elements of the list.

O(|l|).

Examples:

[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none

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} {α✝ : Type u_1} {f : α → Option α✝} :

findSome? f [] = none

theorem List.findSome?_cons {α : Type u} {β : Type v} {a : α} {as : List α} {f : α → Option β} :

findSome? f (a :: as) = match f a with | some b => some b | none => findSome? f as

findIdx #

@[inline]

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

Nat

Returns the index of the first element for which p returns true, or the length of the list if there is no such element.

Examples:

[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = 4
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = 7

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} {p : α → Bool} :

findIdx p [] = 0

idxOf #

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

List α → Nat

Returns the index of the first element equal to a, or the length of the list if no element is equal to a.

Examples:

["carrot", "potato", "broccoli"].idxOf "carrot" = 0
["carrot", "potato", "broccoli"].idxOf "broccoli" = 2
["carrot", "potato", "broccoli"].idxOf "tomato" = 3
["carrot", "potato", "broccoli"].idxOf "anything else" = 3

Equations

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

@[reducible, inline, deprecated List.idxOf (since := "2025-01-29")]

abbrev List.indexOf {α : Type u_1} [BEq α] (a : α) :

List α → Nat

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

Equations

@List.indexOf = @List.idxOf

@[simp]

theorem List.idxOf_nil {α : Type u} {x : α} [BEq α] :

idxOf x [] = 0

@[deprecated List.idxOf_nil (since := "2025-01-29")]

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

idxOf x [] = 0

findIdx? #

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

Option Nat

Returns the index of the first element for which p returns true, or none if there is no such element.

Examples:

[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4
[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none

Equations

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

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

List α → Nat → Option Nat

Equations

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

idxOf? #

@[inline]

def List.idxOf? {α : Type u} [BEq α] (a : α) :

List α → Option Nat

Returns the index of the first element equal to a, or none if no element is equal to a.

Examples:

["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0
["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2
["carrot", "potato", "broccoli"].idxOf? "tomato" = none
["carrot", "potato", "broccoli"].idxOf? "anything else" = none

Equations

List.idxOf? a = List.findIdx? fun (x : α) => x == a

@[reducible, inline, deprecated List.idxOf? (since := "2025-01-29")]

abbrev List.indexOf? {α : Type u_1} [BEq α] (a : α) :

List α → Option Nat

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

Equations

@List.indexOf? = @List.idxOf?

findFinIdx? #

@[inline]

def List.findFinIdx? {α : Type u} (p : α → Bool) (l : List α) :

Option (Fin l.length)

Returns the index of the first element for which p returns true, or none if there is no such element. The index is returned as a Fin, which guarantees that it is in bounds.

Examples:

[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)
[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none

Equations

List.findFinIdx? p l = List.findFinIdx?.go p l l 0 ⋯

def List.findFinIdx?.go {α : Type u} (p : α → Bool) (l l' : List α) (i : Nat) (h : l'.length + i = l.length) :

Option (Fin l.length)

Equations

List.findFinIdx?.go p l [] x x_1 = none
List.findFinIdx?.go p l (a :: l_1) x x_1 = if p a = true then some ⟨x, ⋯⟩ else List.findFinIdx?.go p l l_1 (x + 1) ⋯

finIdxOf? #

@[inline]

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

Option (Fin l.length)

Returns the index of the first element equal to a, or the length of the list if no element is equal to a. The index is returned as a Fin, which guarantees that it is in bounds.

Examples:

["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0
["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2
["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none
["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none

Equations

List.finIdxOf? a = List.findFinIdx? fun (x : α) => x == a

countP #

@[inline]

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

Nat

Counts the number of elements in the list l that satisfy the Boolean predicate p.

Examples:

[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2
[1, 2, 3, 4, 5].countP (· < 5) = 4
[1, 2, 3, 4, 5].countP (· > 5) = 0

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

Counts the number of times an element occurs in a list.

Examples:

[1, 1, 2, 3, 5].count 1 = 2
[1, 1, 2, 3, 5].count 5 = 1
[1, 1, 2, 3, 5].count 4 = 0

Equations

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

lookup #

def List.lookup {α : Type u} {β : Type v} [BEq α] :

α → List (α × β) → Option β

Treats the list as an association list that maps keys to values, returning the first value whose key is equal to the specified key.

O(|l|).

Examples:

[(1, "one"), (3, "three"), (3, "other")].lookup 3 = some "three"
[(1, "one"), (3, "three"), (3, "other")].lookup 2 = none

Equations

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

@[simp]

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

lookup a [] = none

theorem List.lookup_cons {α : Type u} {β✝ : Type u_1} {b : β✝} {as : List (α × β✝)} {a : α} [BEq α] {k : α} :

lookup a ((k, b) :: as) = match a == k with | true => some b | false => lookup a as

Permutations #

Perm #

inductive List.Perm {α : Type u} :

List α → List α → Prop

Two lists are permutations of each other if they contain the same elements, each occurring the same number of times but not necessarily in the same order.

One list can be proven to be a permutation of another by showing how to transform one into the other by repeatedly swapping adjacent elements.

List.isPerm is a Boolean equivalent of this relation.

nil {α : Type u} : [].Perm []
The empty list is a permutation of the empty list: [] ~ [].
cons {α : Type u} (x : α) {l₁ l₂ : List α} : l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)
If one list is a permutation of the other, adding the same element as the head of each yields lists that are permutations of each other: l₁ ~ l₂ → x::l₁ ~ x::l₂.
swap {α : Type u} (x y : α) (l : List α) : (y :: x :: l).Perm (x :: y :: l)
If two lists are identical except for having their first two elements swapped, then they are permutations of each other: x::y::l ~ y::x::l.
trans {α : Type u} {l₁ l₂ l₃ : List α} : l₁.Perm l₂ → l₂.Perm l₃ → l₁.Perm l₃
Permutation is transitive: l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃.

Instances For

def List.«term_~_» :

Two lists are permutations of each other if they contain the same elements, each occurring the same number of times but not necessarily in the same order.

One list can be proven to be a permutation of another by showing how to transform one into the other by repeatedly swapping adjacent elements.

List.isPerm is a Boolean equivalent of this relation.

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

Returns true if l₁ and l₂ are permutations of each other. O(|l₁| * |l₂|).

The relation List.Perm is a logical characterization of permutations. When the BEq α instance corresponds to DecidableEq α, isPerm l₁ l₂ ↔ l₁ ~ l₂ (use the theorem isPerm_iff).

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} (l : List α) (p : α → Bool) :

Returns true if p returns true for any element of l.

O(|l|). Short-circuits upon encountering the first true.

Examples:

[2, 4, 6].any (· % 2 = 0) = true
[2, 4, 6].any (· % 2 = 1) = false
[2, 4, 5, 6].any (· % 2 = 0) = true
[2, 4, 5, 6].any (· % 2 = 1) = 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

Returns true if p returns true for every element of l.

O(|l|). Short-circuits upon encountering the first false.

Examples:

[a, b, c].all p = (p a && (p b && p c))
[2, 4, 6].all (· % 2 = 0) = true
[2, 4, 5, 6].all (· % 2 = 0) = 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) :

Returns true if true is an element of the list bs.

O(|bs|). Short-circuits at the first true value.

[true, true, true].or = true
[true, false, true].or = true
[false, false, false].or = false
[false, false, true].or = true
[].or = false

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) :

Returns true if every element of bs is the value true.

O(|bs|). Short-circuits at the first false value.

[true, true, true].and = true
[true, false, true].and = false
[true, false, false].and = false
[].and = true

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 γ

Applies a function to the corresponding elements of two lists, stopping at the end of the shorter list.

O(min |xs| |ys|).

Examples:

[1, 2].zipWith (· + ·) [5, 6] = [6, 8]
[1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13]
[].zipWith (· + ·) [5, 6] = []
[x₁, x₂, x₃].zipWith f [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 : α → β → γ} :

zipWith f [] l = []

@[simp]

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

zipWith f l [] = []

@[simp]

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

zipWith f (a :: as) (b :: bs) = f a b :: zipWith f as bs

zip #

def List.zip {α : Type u} {β : Type v} :

List α → List β → List (α × β)

Combines two lists into a list of pairs in which the first and second components are the corresponding elements of each list. The resulting list is the length of the shorter of the input lists.

O(min |xs| |ys|).

Examples:

["Mon", "Tue", "Wed"].zip [1, 2, 3] = [("Mon", 1), ("Tue", 2), ("Wed", 3)]
["Mon", "Tue", "Wed"].zip [1, 2] = [("Mon", 1), ("Tue", 2)]
[x₁, x₂, x₃].zip [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 α✝} {α✝¹ : Type u_2} {b : α✝¹} {bs : List α✝¹} :

(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 γ

Applies a function to the corresponding elements of both lists, stopping when there are no more elements in either list. If one list is shorter than the other, the function is passed none for the missing elements.

Examples:

[1, 6].zipWithAll min [5, 2] = [some 1, some 2]
[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]
[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]

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 {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : Option α✝ → Option α✝¹ → α✝²} {as : List α✝} :

zipWithAll f as [] = map (fun (a : α✝) => f (some a) none) as

@[simp]

theorem List.nil_zipWithAll {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : Option α✝ → Option α✝¹ → α✝²} {bs : List α✝¹} :

zipWithAll f [] bs = map (fun (b : α✝¹) => f none (some b)) bs

@[simp]

theorem List.zipWithAll_cons_cons {α✝ : Type u_1} {α✝¹ : Type u_2} {α✝² : Type u_3} {f : Option α✝ → Option α✝¹ → α✝²} {a : α✝} {as : List α✝} {b : α✝¹} {bs : List α✝¹} :

zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: zipWithAll f as bs

unzip #

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

List α × List β

Separates a list of pairs into two lists that contain the respective first and second components.

O(|l|).

Examples:

[("Monday", 1), ("Tuesday", 2)].unzip = (["Monday", "Tuesday"], [1, 2])
[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = ([x₁, x₂, x₃], [y₁, y₂, y₃])
([] : List (Nat × String)).unzip = (([], []) : List Nat × List String)

Equations

[].unzip = ([], [])
((a, b) :: t).unzip = match t.unzip with | (as, bs) => (a :: as, b :: bs)

@[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 | (as, bs) => (h.fst :: as, h.snd :: bs)

Ranges and enumeration #

def List.sum {α : Type u_1} [Add α] [Zero α] :

List α → α

Computes the sum of the elements of a list.

Examples:

[a, b, c].sum = a + (b + (c + 0))
[1, 2, 5].sum = 8

Equations

List.sum = List.foldr (fun (x1 x2 : α) => x1 + x2) 0

@[simp]

theorem List.sum_nil {α : Type u} [Add α] [Zero α] :

[].sum = 0

@[simp]

theorem List.sum_cons {α : Type u} [Add α] [Zero α] {a : α} {l : List α} :

(a :: l).sum = a + l.sum

@[deprecated List.sum (since := "2024-10-17")]

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, deprecated List.sum_nil (since := "2024-10-17")]

theorem Nat.sum_nil :

Nat.sum [] = 0

@[simp, deprecated List.sum_cons (since := "2024-10-17")]

theorem Nat.sum_cons (a : Nat) (l : List Nat) :

Nat.sum (a :: l) = a + Nat.sum l

range #

def List.range (n : Nat) :

Returns a list of the numbers from 0 to n exclusive, in increasing order.

O(n).

Examples:

range 5 = [0, 1, 2, 3, 4]
range 0 = []
range 2 = [0, 1]

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 :

range 0 = []

range' #

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

Returns a list of the numbers with the given length len, starting at start and increasing by step at each element.

In other words, List.range' start len step is [start, start+step, ..., start+(len-1)*step].

Examples:

List.range' 0 3 (step := 1) = [0, 1, 2]
List.range' 0 3 (step := 2) = [0, 2, 4]
List.range' 0 4 (step := 2) = [0, 2, 4, 6]
List.range' 3 4 (step := 2) = [3, 5, 7, 9]

Equations

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

iota #

@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]

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 :

iota 0 = []

@[simp]

theorem List.iota_succ {i : Nat} :

iota (i + 1) = (i + 1) :: iota i

zipIdx #

def List.zipIdx {α : Type u} (l : List α) (n : Nat := 0) :

List (α × Nat)

Pairs each element of a list with its index, optionally starting from an index other than 0.

O(|l|).

Examples:

[a, b, c].zipIdx = [(a, 0), (b, 1), (c, 2)]
[a, b, c].zipIdx 5 = [(a, 5), (b, 6), (c, 7)]

Equations

[].zipIdx x✝ = []
(x_2 :: xs).zipIdx x✝ = (x_2, x✝) :: xs.zipIdx (x✝ + 1)

@[simp]

theorem List.zipIdx_nil {α : Type u} {i : Nat} :

[].zipIdx i = []

@[simp]

theorem List.zipIdx_cons {α✝ : Type u_1} {a : α✝} {as : List α✝} {i : Nat} :

(a :: as).zipIdx i = (a, i) :: as.zipIdx (i + 1)

enumFrom #

@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]

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, deprecated List.zipIdx_nil (since := "2025-01-21")]

theorem List.enumFrom_nil {α : Type u} {i : Nat} :

enumFrom i [] = []

@[simp, deprecated List.zipIdx_cons (since := "2025-01-21")]

theorem List.enumFrom_cons {α✝ : Type u_1} {a : α✝} {as : List α✝} {i : Nat} :

enumFrom i (a :: as) = (i, a) :: enumFrom (i + 1) as

enum #

@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]

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, deprecated List.zipIdx_nil (since := "2025-01-21")]

theorem List.enum_nil {α : Type u} :

[].enum = []

Minima and maxima #

min? #

def List.min? {α : Type u} [Min α] :

List α → Option α

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

Examples:

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

Equations

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

@[reducible, inline, deprecated List.min? (since := "2024-09-29")]

abbrev List.minimum? {α : Type u_1} [Min α] :

List α → Option α

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

Examples:

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

Equations

@List.minimum? = @List.min?

max? #

def List.max? {α : Type u} [Max α] :

List α → Option α

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

Examples:

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

Equations

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

@[reducible, inline, deprecated List.max? (since := "2024-09-29")]

abbrev List.maximum? {α : Type u_1} [Max α] :

List α → Option α

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

Examples:

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

Equations

@List.maximum? = @List.max?

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 : α) (l : List α) :

List α

Alternates the elements of l with sep.

O(|l|).

List.intercalate is a similar function that alternates a separator list with elements of a list of lists.

Examples:

List.intersperse "then" [] = []
List.intersperse "then" ["walk"] = ["walk"]
List.intersperse "then" ["walk", "run"] = ["walk", "then", "run"]
List.intersperse "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]

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 : α} :

intersperse sep [] = []

@[simp]

theorem List.intersperse_single {α : Type u} {x sep : α} :

intersperse sep [x] = [x]

@[simp]

theorem List.intersperse_cons₂ {α : Type u} {x y : α} {zs : List α} {sep : α} :

intersperse sep (x :: y :: zs) = x :: sep :: intersperse sep (y :: zs)

intercalate #

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

List α

Alternates the lists in xs with the separator sep, appending them. The resulting list is flattened.

O(|xs|).

List.intersperse is a similar function that alternates a separator element with the elements of a list.

Examples:

List.intercalate sep [] = []
List.intercalate sep [a] = a
List.intercalate sep [a, b] = a ++ sep ++ b
List.intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c

Equations

sep.intercalate xs = (List.intersperse sep xs).flatten

eraseDups #

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

List α

Erases duplicated elements in the list, keeping the first occurrence of duplicated elements.

O(|l|^2).

Examples:

[1, 3, 2, 2, 3, 5].eraseDups = [1, 3, 2, 5]
["red", "green", "green", "blue"].eraseDups = ["red", "green", "blue"]

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 α

Erases repeated elements, keeping the first element of each run.

O(|l|).

Example:

[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = [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 α

Splits a list into the the longest initial segment for which p returns true, paired with the remainder of the list.

O(|l|).

Examples:

[6, 8, 9, 5, 2, 9].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].span (· > 0) = ([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)

splitBy #

@[specialize #[]]

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

List α → List (List α)

Splits a list into the longest segments in which each pair of adjacent elements are related by R.

O(|l|).

Examples:

[1, 1, 2, 2, 2, 3, 2].splitBy (· == ·) = [[1, 1], [2, 2, 2], [3], [2]]
[1, 2, 5, 4, 5, 1, 4].splitBy (· < ·) = [[1, 2, 5], [4, 5], [1, 4]]
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => true) = [[1, 2, 5, 4, 5, 1, 4]]
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => false) = [[1], [2], [5], [4], [5], [1], [4]]

Equations

List.splitBy R [] = []
List.splitBy R (a :: as) = List.splitBy.loop R as a [] []

@[specialize #[]]

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

List α → α → List α → List (List α) → List (List α)

The arguments of splitBy.loop l b g gs represent the following:

l : List α are the elements which we still need to split.
b : α is the previous element for which a comparison was performed.
r : List α is the group currently being assembled, in reverse order.
acc : List (List α) is all of the groups that have been completed, in reverse order.

Equations

List.splitBy.loop R (a :: as) x✝² x✝¹ x✝ = match R x✝² a with | true => List.splitBy.loop R as a (x✝² :: x✝¹) x✝ | false => List.splitBy.loop R as a [] ((x✝² :: x✝¹).reverse :: x✝)
List.splitBy.loop R [] x✝² x✝¹ x✝ = ((x✝² :: x✝¹).reverse :: x✝).reverse

@[reducible, inline, deprecated List.splitBy (since := "2024-10-30")]

abbrev List.groupBy {α : Type u_1} (R : α → α → Bool) :

List α → List (List α)

Splits a list into the longest segments in which each pair of adjacent elements are related by R.

O(|l|).

Examples:

[1, 1, 2, 2, 2, 3, 2].splitBy (· == ·) = [[1, 1], [2, 2, 2], [3], [2]]
[1, 2, 5, 4, 5, 1, 4].splitBy (· < ·) = [[1, 2, 5], [4, 5], [1, 4]]
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => true) = [[1, 2, 5, 4, 5, 1, 4]]
[1, 2, 5, 4, 5, 1, 4].splitBy (fun _ _ => false) = [[1], [2], [5], [4], [5], [1], [4]]

Equations

@List.groupBy = @List.splitBy

removeAll #

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

List α

Removes all elements of xs that are present in ys.

O(|xs| * |ys|).

Examples:

[1, 1, 5, 1, 2, 4, 5].removeAll [1, 2, 2] = [5, 4, 5]
[1, 2, 3, 2].removeAll [] = [1, 2, 3, 2]
[1, 2, 3, 2].removeAll [3] = [1, 2, 2]

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 :

@length = @lengthTR

map #

@[inline]

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

List β

Applies a function to each element of the list, returning the resulting list of values.

O(|l|). This is the tail-recursive variant of List.map, used in runtime code.

Examples:

[a, b, c].mapTR f = [f a, f b, f c]
[].mapTR Nat.succ = []
["one", "two", "three"].mapTR (·.length) = [3, 3, 5]
["one", "two", "three"].mapTR (·.reverse) = ["eno", "owt", "eerht"]

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 β} :

mapTR.loop f as bs = bs.reverse ++ map f as

@[csimp]

theorem List.map_eq_mapTR :

@map = @mapTR

filter #

@[inline]

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

List α

Returns the list of elements in l for which p returns true.

O(|l|). This is a tail-recursive version of List.filter, used at runtime.

Examples:

[1, 2, 5, 2, 7, 7].filterTR (· > 2) = [5, 7, 7]
[1, 2, 5, 2, 7, 7].filterTR (fun _ => false) = []
[1, 2, 5, 2, 7, 7].filterTR (fun _ => true) = * [1, 2, 5, 2, 7, 7]

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 bs : List α} :

filterTR.loop p as bs = bs.reverse ++ filter p as

@[csimp]

theorem List.filter_eq_filterTR :

@filter = @filterTR

replicate #

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

List α

Creates a list that contains n copies of a.

This is a tail-recursive version of List.replicate.

List.replicateTR 5 "five" = ["five", "five", "five", "five", "five"]
List.replicateTR 0 "zero" = []
List.replicateTR 2 ' ' = [' ', ' ']

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 n : Nat} :

replicateTR.loop a n (replicate m a) = replicate (n + m) a

theorem List.replicateTR_loop_eq {α✝ : Type u_1} {a : α✝} {acc : List α✝} (n : Nat) :

replicateTR.loop a n acc = replicate n a ++ acc

@[csimp]

theorem List.replicate_eq_replicateTR :

@replicate = @replicateTR

Additional functions #

leftpad #

@[inline]

def List.leftpadTR {α : 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 already has at least n elements, it is returned unmodified.

This is a tail-recursive version of List.leftpad, used at runtime.

Examples:

[1, 2, 3].leftPadTR 5 0 = [0, 0, 1, 2, 3]
["red", "green", "blue"].leftPadTR 4 "blank" = ["blank", "red", "green", "blue"]
["red", "green", "blue"].leftPadTR 3 "blank" = ["red", "green", "blue"]
["red", "green", "blue"].leftPadTR 1 "blank" = ["red", "green", "blue"]

Equations

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

@[csimp]

theorem List.leftpad_eq_leftpadTR :

@leftpad = @leftpadTR

Zippers #

unzip #

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

List α × List β

Separates a list of pairs into two lists that contain the respective first and second components.

O(|l|). This is a tail-recursive version of List.unzip that's used at runtime.

Examples:

[("Monday", 1), ("Tuesday", 2)].unzipTR = (["Monday", "Tuesday"], [1, 2])
[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzipTR = ([x₁, x₂, x₃], [y₁, y₂, y₃])
([] : List (Nat × String)).unzipTR = (([], []) : List Nat × List String)

Equations

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

@[csimp]

theorem List.unzip_eq_unzipTR :

@unzip = @unzipTR

Ranges and enumeration #

range' #

@[inline]

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

Returns a list of the numbers with the given length len, starting at start and increasing by step at each element.

In other words, List.range'TR start len step is [start, start+step, ..., start+(len-1)*step].

This is a tail-recursive version of List.range'.

Examples:

List.range'TR 0 3 (step := 1) = [0, 1, 2]
List.range'TR 0 3 (step := 2) = [0, 2, 4]
List.range'TR 0 4 (step := 2) = [0, 2, 4, 6]
List.range'TR 3 4 (step := 2) = [3, 5, 7, 9]

Equations

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

def List.range'TR.go (step : 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 :

@range' = @range'TR

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

range'TR.go step n (s + step * n) (range' (s + step * n) m step) = range' s (n + m) step

iota #

@[deprecated "Use `List.range' 1 n` instead of `iota n`." (since := "2025-01-20")]

def List.iotaTR (n : 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 :

iota = iotaTR

Other list operations #

intersperse #

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

List α

Alternates the elements of l with sep.

O(|l|).

This is a tail-recursive version of List.intersperse, used at runtime.

Examples:

List.intersperseTR "then" [] = []
List.intersperseTR "then" ["walk"] = ["walk"]
List.intersperseTR "then" ["walk", "run"] = ["walk", "then", "run"]
List.intersperseTR "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]

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