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

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

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

@List.append = @List.appendTR

@[csimp]

theorem List.append_eq_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 α) :

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

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

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

Instances For

def List.«term_<+_» :

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

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₂

Instances For

List.instDecidableIsPrefixOfDecidableEq

def List.«term_<+:_» :

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

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

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₂

Instances For

List.instDecidableIsSuffixOfDecidableEq

def List.«term_<:+_» :

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

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_<:+:_» :

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.

Instances For

List.instDecidablePairwise

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

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

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.

Instances For

List.decidablePerm

def List.«term_~_» :

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

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

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 #

min? #

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

List α → Option α

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

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

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

List α → Option α

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

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

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

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

List α → Option α

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

[].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 : α) :

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

The arguments of groupBy.loop l ag g gs represent the following:

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

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

@List.length = @List.lengthTR

@[csimp]

theorem List.length_eq_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

@List.filter = @List.filterTR

@[csimp]

theorem List.filter_eq_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

@List.replicate = @List.replicateTR

@[csimp]

theorem List.replicate_eq_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

@List.leftpad = @List.leftpadTR

@[csimp]

theorem List.leftpad_eq_leftpadTR :

Zippers #

unzip #