Basic operations on List.

We define

• basic operations on List,
• simp lemmas for applying the operations on .nil and .cons arguments (in the cases where the right hand side is simple to state; otherwise these are deferred to Init.Data.List.Lemmas),
• the minimal lemmas which are required for setting up Init.Data.Array.Basic.

In Init.Data.List.Impl we give tail-recursive versions of these operations along with @[csimp] lemmas,

In Init.Data.List.Lemmas we develop the full API for these functions.

Recall that length, get, set, fold, and concat have already been defined in Init.Prelude.

The operations are organized as follow:

• Equality: beq, isEqv.
• Lexicographic ordering: lt, le, and instances.
• Basic operations: map, filter, filterMap, foldr, append, join, pure, bind, replicate, and reverse.
• List membership: isEmpty, elem, contains, mem (and the ∈ notation), and decidability for predicates quantifying over membership in a List.
• Sublists: take, drop, takeWhile, dropWhile, partition, dropLast, isPrefixOf, isPrefixOf?, isSuffixOf, isSuffixOf?, rotateLeft and rotateRight.
• Manipulating elements: replace, insert, erase, eraseIdx, find?, findSome?, and lookup.
• Logic: any, all, or, and and.
• Zippers: zipWith, zip, zipWithAll, and unzip.
• Ranges and enumeration: range, iota, enumFrom, and enum.
• Minima and maxima: minimum? and maximum?.
• Other functions: intersperse, intercalate, eraseDups, eraseReps, span, groupBy, removeAll (currently these functions are mostly only used in meta code, and do not have API suitable for verification).

Further operations are defined in Init.Data.List.BasicAux (because they use Array in their implementations), namely:

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

Preliminaries from Init.Prelude

length

@[simp]

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

@[simp]

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

@[simp]

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

set

@[simp]

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

foldl

@[simp]

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

@[simp]

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

concat

@[simp]

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

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

Equality

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

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

@[specialize #[]]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Lexicographic ordering

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

The lexicographic order on lists. [] < a::as, and a::as < b::bs if a < b or if a and b are equivalent and as < bs.

• nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), [].lt (b :: bs)

  [] is the smallest element in the order.

• head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → (a :: as).lt (b :: bs)

  If a < b then a::as < b::bs.

• tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b → ¬b < a → as.lt bs → (a :: as).lt (b :: bs)

  If a and b are equivalent and as < bs, then a::as < b::bs.

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

Equations

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

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

Equations

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

@[reducible]

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

The lexicographic order on lists.

Equations

• a.le b = ¬b < a

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

Equations

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

instance List.instDecidableLeOfDecidableRelLt {α : Type u} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (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

• x.getLast? = match x with | [] => none | a :: as => 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

• x✝.getLastD x = match x✝, x with | [], a₀ => a₀ | a :: as, x => (a :: as).getLast ⋯

@[simp]

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

@[simp]

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

• x✝.head x = match x✝, x with | a :: tail, x => 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

• x.head? = match x with | [] => none | a :: tail => 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

• x✝.headD x = match x✝, x with | [], fallback => fallback | a :: tail, 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 α → Option (List α)

Drops the first element of the list.

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

Equations

• x.tail? = match x with | [] => none | head :: as => 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

• list.tailD fallback = match list with | [] => fallback | head :: tl => tl

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

Instances For

• List.canLift

@[simp]

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

@[simp]

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

filter

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

O(|l|). filter f l returns the list of elements in l for which f returns true.

filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]

Equations

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

@[simp]

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

filterMap

@[specialize #[]]

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

O(|l|). filterMap f l takes a function f : α → Option β and applies it to each element of l; the resulting non-none values are collected to form the output list.

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

Equations

• List.filterMap f [] = []
• List.filterMap f (a :: as) = match f a with | none => List.filterMap f as | some b => b :: List.filterMap f as

@[simp]

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

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

foldr

@[specialize #[]]

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

O(|l|). Applies function f to all of the elements of the list, from right to left.

• foldr f init [a, b, c] = f a <| f b <| f c <| init

Equations

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

@[simp]

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

@[simp]

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

reverse

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

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

Equations

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

@[simp]

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

@[simp]

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

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

O(|as|). Reverse of a list:

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

Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.

Equations

• as.reverse = as.reverseAux []

@[simp]

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

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

append

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

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

Equations

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

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

Tail-recursive version of List.append.

Most of the tail-recursive implementations are in Init.Data.List.Impl, but appendTR must be set up immediately, because otherwise Append (List α) instance below will not use it.

Equations

• as.appendTR bs = as.reverse.reverseAux bs

@[csimp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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 (x x_1 : List α) => x ++ x_1

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

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

• x.isEmpty = match x with | [] => true | head :: tail => false

@[simp]

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

@[simp]

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

elem

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

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

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

Equations

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

@[simp]

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

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

@[deprecated]

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

notElem a l is !(elem a l).

Equations

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

contains

@[reducible, inline]

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

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

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

Equations

• as.contains a = List.elem a as

@[simp]

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

Mem

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

a ∈ l is a predicate which asserts that a is in the list l. Unlike elem, this uses = instead of == and is suited for mathematical reasoning.

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

• head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)

  The head of a list is a member: a ∈ a :: as.

• tail: ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a as → List.Mem a (b :: as)

  A member of the tail of a list is a member of the list: a ∈ l → a ∈ b :: l.

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

Equations

• List.instMembership = { mem := List.Mem }

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_cons_succ : ∀ {α : 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

isPrefixOf

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)

isPrefixOf?

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

isSuffixOf

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

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

Equations

• l₁.isSuffixOf l₂ = l₁.reverse.isPrefixOf l₂.reverse

@[simp]

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

isSuffixOf?

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)

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 = let len := xs.length; if len ≤ 1 then xs else let n := n % len; 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 = let len := xs.length; if len ≤ 1 then xs else let n := len - n % len; 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 = []

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

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

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

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

Logical operations

any

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

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

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

Short-circuits upon encountering the first true.

Equations

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

@[simp]

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

@[simp]

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

all

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

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

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

Short-circuits upon encountering the first false.

Equations

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

@[simp]

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

@[simp]

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

or

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

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

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

Equations

• bs.or = bs.any id

@[simp]

theorem List.or_nil : [].or = false

@[simp]

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

and

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

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

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

Equations

• bs.and = bs.all id

@[simp]

theorem List.and_nil : [].and = true

@[simp]

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

Zippers

zipWith

@[specialize #[]]

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

O(min |xs| |ys|). Applies f to the two lists in parallel, stopping at the shorter list.

• zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

Equations

• List.zipWith f (x_2 :: xs) (y :: ys) = f x_2 y :: List.zipWith f xs ys
• List.zipWith f x✝ x = []

Instances For

• List.instIsSymmOpZipWith

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

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

iota

def List.iota : Nat → List Nat

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

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

Equations

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

@[simp]

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

@[simp]

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

enumFrom

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

O(|l|). enumFrom n l is like enum but it allows you to specify the initial index.

• enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]

Equations

• List.enumFrom x [] = []
• List.enumFrom x (x_2 :: xs) = (x, x_2) :: List.enumFrom (x + 1) xs

@[simp]

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

@[simp]

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

enum

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

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

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

Equations

• List.enum = List.enumFrom 0

@[simp]

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

Minima and maxima

minimum?

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

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

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

Equations

• x.minimum? = match x with | [] => none | a :: as => some (List.foldl min a as)

maximum?

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

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

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

Equations

• x.maximum? = match x with | [] => none | a :: as => some (List.foldl max a as)

Other list operations

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

intersperse

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

O(|l|). intersperse sep l alternates sep and the elements of l:

• intersperse sep [] = []
• intersperse sep [a] = [a]
• intersperse sep [a, b] = [a, sep, b]
• intersperse sep [a, b, c] = [a, sep, b, sep, c]

Equations

• List.intersperse sep [] = []
• List.intersperse sep [head] = [head]
• List.intersperse sep (a :: as) = a :: sep :: List.intersperse sep as

@[simp]

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

@[simp]

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

@[simp]

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

intercalate

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

O(|xs|). intercalate sep xs alternates sep and the elements of xs:

• intercalate sep [] = []
• intercalate sep [a] = a
• intercalate sep [a, b] = a ++ sep ++ b
• intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c

Equations

• sep.intercalate xs = (List.intersperse sep xs).join

eraseDups

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

O(|l|^2). Erase duplicated elements in the list. Keeps the first occurrence of duplicated elements.

• eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]

Equations

• as.eraseDups = List.eraseDups.loop as []

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

Equations

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

eraseReps

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

O(|l|). Erase repeated adjacent elements. Keeps the first occurrence of each run.

• eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]

Equations

• x.eraseReps = match x with | [] => [] | a :: as => 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 x = match x with | [] => [] | a :: as => List.groupBy.loop R as a [] []

@[specialize #[]]

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

Equations

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

removeAll

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

O(|xs|). Computes the "set difference" of lists, by filtering out all elements of xs which are also in ys.

• removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]

Equations

• xs.removeAll ys = List.filter (fun (x : α) => !List.elem x ys) xs