Documentation

theorem List.length_nil {α : Type u} :

Eq nil.length 0

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

Eq (cons a nil).length 1

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

Eq (cons a as).length (HAdd.hAdd as.length 1)

set #

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

Eq (as.set i a).length as.length

foldl #

theorem List.foldl_nil {α✝ : Type u_1} {β✝ : Type u_2} {f : α✝ → β✝ → α✝} {b : α✝} :

Eq (foldl f b nil) b

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

Eq (foldl f b (cons a l)) (foldl f (f b a) l)

concat #

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

Eq (as.concat a).length (HAdd.hAdd as.length 1)

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

And (Eq as bs) (Eq a b)

Equality #

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

List α → List α → Bool

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

Equations

Eq (List.nil.beq List.nil) Bool.true
Eq ((List.cons a as).beq (List.cons b bs)) ((BEq.beq a b).and (as.beq bs))
Eq (x✝¹.beq x✝) Bool.false

Instances For

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

Eq (nil.beq nil) Bool.true

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

Eq ((cons a as).beq nil) Bool.false

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

Eq (nil.beq (cons a as)) Bool.false

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

Eq ((cons a as).beq (cons b bs)) ((BEq.beq a b).and (as.beq bs))

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

BEq (List α)

Equations

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

Instances For

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

LawfulBEq (List α)

@[specialize #[]]

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

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

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

Examples:

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

Equations

Eq (List.nil.isEqv List.nil x✝) Bool.true
Eq ((List.cons a as).isEqv (List.cons b bs) x✝) ((x✝ a b).and (as.isEqv bs x✝))
Eq (x✝².isEqv x✝¹ x✝) Bool.false

Instances For

theorem List.isEqv_nil_nil {α : Type u} {eqv : α → α → Bool} :

Eq (nil.isEqv nil eqv) Bool.true

theorem List.isEqv_nil_cons {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool} :

Eq (nil.isEqv (cons a as) eqv) Bool.false

theorem List.isEqv_cons_nil {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool} :

Eq ((cons a as).isEqv nil eqv) Bool.false

theorem List.isEqv_cons₂ {α✝ : Type u_1} {a : α✝} {as : List α✝} {b : α✝} {bs : List α✝} {eqv : α✝ → α✝ → Bool} :

Eq ((cons a as).isEqv (cons b bs) eqv) ((eqv a b).and (as.isEqv bs eqv))

Lexicographic ordering #

inductive List.Lex {α : Type u} (r : α → α → Prop) (as bs : List α) :

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

as is lexicographically smaller than bs if

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

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

Instances For

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

Decidable (Lex r l₁ l₂)

Instances For

@[reducible, inline]

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

List α → List α → Prop

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

as < bs if

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

Equations

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

Instances For

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

LT (List α)

Equations

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

Instances For

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

Decidable (LT.lt l₁ l₂)

Decidability of lexicographic ordering.

Equations

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

Instances For

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

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

Decidable (LT.lt l₁ l₂)

Decidability of lexicographic ordering.

Equations

Eq @List.hasDecidableLt @List.decidableLT

Instances For

@[reducible]

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

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

as ≤ bs if ¬ bs < as.

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

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

Equations

Eq (as.le bs) (Not (LT.lt bs as))

Instances For

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

LE (List α)

Equations

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

Instances For

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

Decidable (LE.le l₁ l₂)

Equations

Eq (l₁.decidableLE l₂) (inferInstanceAs (Decidable (Not (LT.lt l₂ l₁))))

Instances For

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

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

The lexicographic order with respect to lt is:

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

Equations

Eq (List.nil.lex (List.cons head tail) lt) Bool.true
Eq (l₁.lex List.nil lt) Bool.false
Eq ((List.cons a as).lex (List.cons b bs) lt) ((lt a b).or ((BEq.beq a b).and (as.lex bs lt)))

Instances For

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

Eq (nil.lex nil lt) Bool.false

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

Eq (nil.lex (cons b bs) lt) Bool.true

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

Eq ((cons a as).lex nil lt) Bool.false

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

Eq ((cons a as).lex (cons b bs) lt) ((lt a b).or ((BEq.beq a b).and (as.lex bs lt)))

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

Eq (as.lex nil lt) Bool.false

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

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

Eq (nil.lex nil lt) Bool.false

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

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

Eq (nil.lex (cons b bs) lt) Bool.true

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

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

Eq ((cons a as).lex nil lt) Bool.false

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

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

Eq ((cons a as).lex (cons b bs) lt) ((lt a b).or ((BEq.beq a b).and (as.lex bs lt)))

Alternative getters #

getLast #

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

Ne as nil → α

Returns the last element of a non-empty list.

Examples:

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

Equations

Eq (List.nil.getLast h) (absurd ⋯ h)
Eq ((List.cons a List.nil).getLast x_2) a
Eq ((List.cons head (List.cons b as)).getLast x_2) ((List.cons b as).getLast ⋯)

Instances For

getLast? #

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

List α → Option α

Returns the last element in the list, or none if the list is empty.

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

Examples:

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

Equations

Eq List.nil.getLast? Option.none
Eq (List.cons a as).getLast? (Option.some ((List.cons a as).getLast ⋯))

Instances For

theorem List.getLast?_nil {α : Type u} :

Eq nil.getLast? Option.none

getLastD #

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

Returns the last element in the list, or fallback if the list is empty.

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

Examples:

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

Equations

Eq (x✝¹.getLastD x✝) (List.getLastD.match_1 (fun (x : List α) (x : α) => α) x✝¹ x✝ (fun (a₀ : α) => a₀) fun (a : α) (as : List α) (x : α) => (List.cons a as).getLast ⋯)

Instances For

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

Eq (nil.getLastD a) a

theorem List.getLastD_cons {α : Type u} {a b : α} {l : List α} :

Eq ((cons b l).getLastD a) (l.getLastD b)

Head and tail #

head #

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

Ne as nil → α

Returns the first element of a non-empty list.

Equations

Eq (x✝¹.head x✝) (List.head.match_1 (fun (x : List α) (x : Ne x List.nil) => α) x✝¹ x✝ fun (a : α) (tail : List α) (x : Ne (List.cons a tail) List.nil) => a)

Instances For

theorem List.head_cons {α : Type u} {a : α} {l : List α} {h : Ne (cons a l) nil} :

Eq ((cons a l).head h) a

head? #

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

List α → Option α

Returns the first element in the list, if there is one. Returns none if the list is empty.

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

Examples:

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

Equations

Eq x✝.head? (List.getLast?.match_1 (fun (x : List α) => Option α) x✝ (fun (_ : Unit) => Option.none) fun (a : α) (tail : List α) => Option.some a)

Instances For

theorem List.head?_nil {α : Type u} :

Eq nil.head? Option.none

theorem List.head?_cons {α : Type u} {a : α} {l : List α} :

Eq (cons a l).head? (Option.some a)

headD #

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

Returns the first element in the list if there is one, or fallback if the list is empty.

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

Examples:

[].headD "empty" = "empty"
[].headD 2 = 2
["head", "shoulders", "knees"].headD "toes" = "head"

Equations

Eq (List.nil.headD x✝) x✝
Eq ((List.cons a as).headD x✝) a

Instances For

theorem List.headD_nil {α : Type u} {d : α} :

Eq (nil.headD d) d

theorem List.headD_cons {α : Type u} {a : α} {l : List α} {d : α} :

Eq ((cons a l).headD d) a

tail #

def List.tail {α : Type u} :

List α → List α

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

Examples:

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

Equations

Eq x✝.tail (List.getLast?.match_1 (fun (x : List α) => List α) x✝ (fun (_ : Unit) => List.nil) fun (head : α) (as : List α) => as)

Instances For

theorem List.tail_nil {α : Type u} :

Eq nil.tail nil

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

Eq (cons a as).tail as

tail? #

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

List α → Option (List α)

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

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

Examples:

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

Equations

Eq x✝.tail? (List.getLast?.match_1 (fun (x : List α) => Option (List α)) x✝ (fun (_ : Unit) => Option.none) fun (head : α) (as : List α) => Option.some as)

Instances For

theorem List.tail?_nil {α : Type u} :

Eq nil.tail? Option.none

theorem List.tail?_cons {α : Type u} {a : α} {l : List α} :

Eq (cons a l).tail? (Option.some l)

tailD #

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

List α

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

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

Examples:

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

Equations

Eq (l.tailD fallback) (List.getLast?.match_1 (fun (l : List α) => List α) l (fun (_ : Unit) => fallback) fun (head : α) (tl : List α) => tl)

Instances For

theorem List.tailD_nil {α : Type u} {l' : List α} :

Eq (nil.tailD l') l'

theorem List.tailD_cons {α : Type u} {a : α} {l l' : List α} :

Eq ((cons a l).tailD l') l

Basic `List` operations. #

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

map #

@[specialize #[]]

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

List β

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

O(|l|).

Examples:

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

Equations

Eq (List.map f List.nil) List.nil
Eq (List.map f (List.cons a as)) (List.cons (f a) (List.map f as))

Instances For

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

Eq (map f nil) nil

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

Eq (map f (cons a l)) (cons (f a) (map f l))

filter #

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

List α

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

O(|l|).

Examples:

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

Equations

Eq (List.filter p List.nil) List.nil
Eq (List.filter p (List.cons a as)) (List.filter.match_1 (fun (x : Bool) => List α) (p a) (fun (_ : Unit) => List.cons a (List.filter p as)) fun (_ : Unit) => List.filter p as)

Instances For

theorem List.filter_nil {α : Type u} {p : α → Bool} :

Eq (filter p nil) nil

filterMap #

@[specialize #[]]

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

List α → List β

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

O(|l|).

Example:

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

[10, 14, 14]

Equations

Eq (List.filterMap f List.nil) List.nil
Eq (List.filterMap f (List.cons a as)) (List.filterMap.match_1 (fun (x : Option β) => List β) (f a) (fun (_ : Unit) => List.filterMap f as) fun (b : β) => List.cons b (List.filterMap f as))

Instances For

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

Eq (filterMap f nil) nil

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

Eq (filterMap f (cons a l)) (filterMap.match_1 (fun (x : Option β) => List β) (f a) (fun (_ : Unit) => filterMap f l) fun (b : β) => cons b (filterMap f l))

foldr #

@[specialize #[]]

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

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

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

Examples:

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

Equations

Eq (List.foldr f init List.nil) init
Eq (List.foldr f init (List.cons a as)) (f a (List.foldr f init as))

Instances For

theorem List.foldr_nil {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹ → α✝¹} {b : α✝¹} :

Eq (foldr f b nil) b

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

Eq (foldr f b (cons a l)) (f a (foldr f b l))

reverse #

def List.reverseAux {α : Type u} :

List α → List α → List α

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

Equations

Eq (List.nil.reverseAux x✝) x✝
Eq ((List.cons a l).reverseAux x✝) (l.reverseAux (List.cons a x✝))

Instances For

theorem List.reverseAux_nil {α✝ : Type u_1} {r : List α✝} :

Eq (nil.reverseAux r) r

theorem List.reverseAux_cons {α✝ : Type u_1} {a : α✝} {l r : List α✝} :

Eq ((cons a l).reverseAux r) (l.reverseAux (cons a r))

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

List α

Reverses a list.

O(|as|).

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

Examples:

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

Equations

Eq as.reverse (as.reverseAux List.nil)

Instances For

theorem List.reverse_nil {α : Type u} :

Eq nil.reverse nil

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

Eq ((as.reverseAux bs).reverseAux cs) (bs.reverseAux ((as.reverseAux nil).reverseAux cs))

append #

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

List α

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

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

Examples:

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

Equations

Eq (List.nil.append x✝) x✝
Eq ((List.cons a l).append x✝) (List.cons a (l.append x✝))

Instances For

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

List α

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

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

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

Examples:

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

Equations

Eq (as.appendTR bs) (as.reverse.reverseAux bs)

Instances For

theorem List.append_eq_appendTR :

Eq @List.append @appendTR

def List.instAppend {α : Type u} :

Append (List α)

Equations

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

Instances For

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

Eq (as.append bs) (HAppend.hAppend as bs)

theorem List.nil_append {α : Type u} (as : List α) :

Eq (HAppend.hAppend nil as) as

theorem List.cons_append {α : Type u} {a : α} {as bs : List α} :

Eq (HAppend.hAppend (cons a as) bs) (cons a (HAppend.hAppend as bs))

theorem List.append_nil {α : Type u} (as : List α) :

Eq (HAppend.hAppend as nil) as

theorem List.instLawfulIdentityHAppendNil {α : Type u} :

Std.LawfulIdentity (fun (x1 x2 : List α) => HAppend.hAppend x1 x2) nil

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

Eq (HAppend.hAppend as bs).length (HAdd.hAdd as.length bs.length)

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

Eq (HAppend.hAppend (HAppend.hAppend as bs) cs) (HAppend.hAppend as (HAppend.hAppend bs cs))

theorem List.instAssociativeHAppend {α : Type u} :

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

theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) :

Eq (HAppend.hAppend as (cons b bs)) (HAppend.hAppend (HAppend.hAppend as (cons b nil)) bs)

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

Eq (as.concat a) (HAppend.hAppend as (cons a nil))

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

Eq (as.reverseAux bs) (HAppend.hAppend (as.reverseAux nil) bs)

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

Eq (cons a as).reverse (HAppend.hAppend as.reverse (cons a nil))

flatten #

def List.flatten {α : Type u} :

List (List α) → List α

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

O(|flatten L|).

Examples:

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

Equations

Eq List.nil.flatten List.nil
Eq (List.cons l L).flatten (HAppend.hAppend l L.flatten)

Instances For

theorem List.flatten_nil {α : Type u} :

Eq nil.flatten nil

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

Eq (cons l L).flatten (HAppend.hAppend l L.flatten)

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

abbrev List.join {α : Type u_1} :

List (List α) → List α

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

O(|flatten L|).

Examples:

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

Equations

Eq @List.join @List.flatten

Instances For

singleton #

@[inline]

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

List α

Constructs a single-element list.

Examples:

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

Equations

Eq (List.singleton a) (List.cons a List.nil)

Instances For

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

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

α → β

Equations

Eq @List.pure @Singleton.singleton

Instances For

flatMap #

@[inline]

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

List β

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

Examples:

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

Equations

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

Instances For

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

Eq (flatMap f nil) nil

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

Eq (flatMap f (cons x xs)) (HAppend.hAppend (f x) (flatMap f xs))

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

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

List β

Equations

Eq @List.bind @List.flatMap

Instances For

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

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

Eq (flatMap f nil) nil

Equations

Eq @List.nil_flatMap @List.flatMap_nil

Instances For

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

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

Eq (flatMap f (cons x xs)) (HAppend.hAppend (f x) (flatMap f xs))

Equations

Eq @List.cons_flatMap @List.flatMap_cons

Instances For

replicate #

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

List α

Creates a list that contains n copies of a.

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

Equations

Eq (List.replicate 0 x✝) List.nil
Eq (List.replicate n.succ x✝) (List.cons x✝ (List.replicate n x✝))

Instances For

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

Eq (replicate 0 a) nil

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

Eq (replicate (HAdd.hAdd n 1) a) (cons a (replicate n a))

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

Eq (replicate n a).length n

Additional functions #

leftpad and rightpad #

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

List α

Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l already has at least n elements, it is returned unmodified.

Examples:

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

Equations

Eq (List.leftpad n a l) (HAppend.hAppend (List.replicate (HSub.hSub n l.length) a) l)

Instances For

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

List α

Pads l : List α on the right with repeated occurrences of a : α until it is of length n. If l already has at least n elements, it is returned unmodified.

Examples:

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

Equations

Eq (List.rightpad n a l) (HAppend.hAppend l (List.replicate (HSub.hSub n l.length) a))

Instances For

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

Eq List.reduceOption (List.filterMap id)

Instances For

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 #

def List.instEmptyCollection {α : Type u} :

EmptyCollection (List α)

Equations

Eq List.instEmptyCollection { emptyCollection := List.nil }

Instances For

Eq EmptyCollection.emptyCollection nil

theorem List.empty_eq {α : Type u} :

isEmpty #

def List.isEmpty {α : Type u} :

List α → Bool

Checks whether a list is empty.

O(1).

Examples:

[].isEmpty = true
["grape"].isEmpty = false
["apple", "banana"].isEmpty = false

Equations

Eq List.nil.isEmpty Bool.true
Eq (List.cons a as).isEmpty Bool.false

Instances For

theorem List.isEmpty_nil {α : Type u} :

Eq nil.isEmpty Bool.true

theorem List.isEmpty_cons {α : Type u} {x : α} {xs : List α} :

Eq (cons x xs).isEmpty Bool.false

elem #

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

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

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

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

Example:

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

Equations

Eq (List.elem a List.nil) Bool.false
Eq (List.elem a (List.cons a_1 as)) (List.filter.match_1 (fun (x : Bool) => Bool) (BEq.beq a a_1) (fun (_ : Unit) => Bool.true) fun (_ : Unit) => List.elem a as)

Instances For

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

Eq (elem a nil) Bool.false

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

Eq (elem a (cons b bs)) (filter.match_1 (fun (x : Bool) => Bool) (BEq.beq a b) (fun (_ : Unit) => Bool.true) fun (_ : Unit) => elem a bs)

contains #

@[reducible, inline]

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

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

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

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

Examples:

[1, 4, 2, 3, 3, 7].contains 3 = true
List.contains [1, 4, 2, 3, 3, 7] 5 = false

Equations

Eq (as.contains a) (List.elem a as)

Instances For

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

Eq (nil.contains a) Bool.false

Mem #

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

List α → Prop

List membership, typically accessed via the ∈ operator.

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

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

Examples:

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

head {α : Type u} {a : α} (as : List α) : Mem a (cons a as)
The head of a list is a member: a ∈ a :: as.
tail {α : Type u} {a : α} (b : α) {as : List α} : Mem a as → Mem a (cons b as)
A member of the tail of a list is a member of the list: a ∈ l → a ∈ b :: l.

Instances For

def List.instMembership {α : Type u} :

Membership α (List α)

Equations

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

Instances For

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

Eq (elem a as) Bool.true → Membership.mem as a

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

Eq (elem a as) Bool.true

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

Decidable (Membership.mem as a)

Equations

Eq (List.instDecidableMemOfLawfulBEq a as) (decidable_of_decidable_of_iff ⋯)

Instances For

theorem List.mem_append_left {α : Type u} {a : α} {as : List α} (bs : List α) :

Membership.mem as a → Membership.mem (HAppend.hAppend as bs) a

theorem List.mem_append_right {α : Type u} {b : α} (as : List α) {bs : List α} :

Membership.mem bs b → Membership.mem (HAppend.hAppend as bs) b

def List.decidableBEx {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) :

Decidable (Exists fun (x : α) => And (Membership.mem l x) (p x))

Equations

One or more equations did not get rendered due to their size.

Instances For

def List.decidableBAll {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) :

Decidable (∀ (x : α), Membership.mem l x → p x)

Equations

One or more equations did not get rendered due to their size.

Instances For

Sublists #

take #

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

List α

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

O(min n |xs|).

Examples:

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

Equations

Eq (List.take 0 x✝) List.nil
Eq (List.take n.succ List.nil) List.nil
Eq (List.take n.succ (List.cons a as)) (List.cons a (List.take n as))

Instances For

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

Eq (take i nil) nil

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

Eq (take 0 l) nil

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

Eq (take (HAdd.hAdd i 1) (cons a as)) (cons a (take i as))

drop #

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

List α

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

O(min n |xs|).

Examples:

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

Equations

Eq (List.drop 0 x✝) x✝
Eq (List.drop n.succ List.nil) List.nil
Eq (List.drop n.succ (List.cons a as)) (List.drop n as)

Instances For

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

Eq (drop i nil) nil

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

Eq (drop 0 l) l

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

Eq (drop (HAdd.hAdd i 1) (cons a l)) (drop i l)

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

Eq (drop i as) nil

extract #

@[reducible, inline]

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

List α

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

Examples:

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

Equations

Eq (l.extract start stop) (List.take (HSub.hSub stop start) (List.drop start l))

Instances For

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

Eq (l.extract start stop) (take (HSub.hSub stop start) (drop start l))

takeWhile #

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

List α

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

O(|xs|).

Examples:

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

Equations

Eq (List.takeWhile p List.nil) List.nil
Eq (List.takeWhile p (List.cons a as)) (List.filter.match_1 (fun (x : Bool) => List α) (p a) (fun (_ : Unit) => List.cons a (List.takeWhile p as)) fun (_ : Unit) => List.nil)

Instances For

theorem List.takeWhile_nil {α : Type u} {p : α → Bool} :

Eq (takeWhile p nil) nil

dropWhile #

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

List α → List α

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

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

O(|l|).

Examples:

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

Equations

Eq (List.dropWhile p List.nil) List.nil
Eq (List.dropWhile p (List.cons a as)) (List.filter.match_1 (fun (x : Bool) => List α) (p a) (fun (_ : Unit) => List.dropWhile p as) fun (_ : Unit) => List.cons a as)

Instances For

theorem List.dropWhile_nil {α : Type u} {p : α → Bool} :

Eq (dropWhile p nil) nil

partition #

@[inline]

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

Prod (List α) (List α)

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

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

Examples:

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

Equations

Eq (List.partition p as) (List.partition.loop p as { fst := List.nil, snd := List.nil })

Instances For

@[specialize #[]]

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

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

Equations

One or more equations did not get rendered due to their size.
Eq (List.partition.loop p List.nil { fst := bs, snd := cs }) { fst := bs.reverse, snd := cs.reverse }

Instances For

dropLast #

def List.dropLast {α : Type u_1} :

List α → List α

Removes the last element of the list, if one exists.

Examples:

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

Equations

Eq List.nil.dropLast List.nil
Eq (List.cons head List.nil).dropLast List.nil
Eq (List.cons a as).dropLast (List.cons a as.dropLast)

Instances For

theorem List.dropLast_nil {α : Type u} :

Eq nil.dropLast nil

theorem List.dropLast_single {α✝ : Type u_1} {x : α✝} :

Eq (cons x nil).dropLast nil

theorem List.dropLast_cons₂ {α✝ : Type u_1} {x y : α✝} {zs : List α✝} :

Eq (cons x (cons y zs)).dropLast (cons x (cons y zs).dropLast)

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

Eq (cons a as).dropLast.length as.length

Subset #

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

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

Equations

Eq (l₁.Subset l₂) (∀ ⦃a : α⦄, Membership.mem l₁ a → Membership.mem l₂ a)

Instances For

def List.instHasSubset {α : Type u} :

HasSubset (List α)

Equations

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

Instances For

DecidableRel HasSubset.Subset

def List.instDecidableRelSubsetOfDecidableEq {α : Type u} [DecidableEq α] :

Equations

Eq (x✝¹.instDecidableRelSubsetOfDecidableEq x✝) (List.decidableBAll (Membership.mem x✝) x✝¹)

Instances For

Sublist and isSublist #

inductive List.Sublist {α : Type u_1} :

List α → List α → Prop

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

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

slnil {α : Type u_1} : nil.Sublist nil
The base case: [] is a sublist of []
cons {α : Type u_1} {l₁ l₂ : List α} (a : α) : l₁.Sublist l₂ → l₁.Sublist (List.cons 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₂ → (List.cons a l₁).Sublist (List.cons a l₂)
If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: l₂.

Instances For

def List.«term_<+_» :

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

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

Equations

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

Instances For

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

List α → List α → Bool

True if the first list is a potentially non-contiguous sub-sequence of the second list, comparing elements with the == operator.

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

Examples:

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

Equations

Eq (List.nil.isSublist x✝) Bool.true
Eq (x✝.isSublist List.nil) Bool.false
Eq ((List.cons hd₁ tl₁).isSublist (List.cons hd₂ tl₂)) (ite (Eq (BEq.beq hd₁ hd₂) Bool.true) (tl₁.isSublist tl₂) ((List.cons hd₁ tl₁).isSublist tl₂))

Instances For

IsPrefix / isPrefixOf / isPrefixOf? #

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

The first list is a prefix of the second.

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

The function List.isPrefixOf is a Boolean equivalent.

Conventions for notations in identifiers:

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

Equations

Eq (l₁.IsPrefix l₂) (Exists fun (t : List α) => Eq (HAppend.hAppend l₁ t) l₂)

Instances For

def List.«term_<+:_» :

The first list is a prefix of the second.

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

The function List.isPrefixOf is a Boolean equivalent.

Conventions for notations in identifiers:

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

Equations

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

Instances For

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

List α → List α → Bool

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

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

Examples:

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

Equations

Eq (List.nil.isPrefixOf x✝) Bool.true
Eq (x✝.isPrefixOf List.nil) Bool.false
Eq ((List.cons a as).isPrefixOf (List.cons b bs)) ((BEq.beq a b).and (as.isPrefixOf bs))

Instances For

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

Eq (nil.isPrefixOf l) Bool.true

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

Eq ((cons a as).isPrefixOf nil) Bool.false

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

Eq ((cons a as).isPrefixOf (cons b bs)) ((BEq.beq a b).and (as.isPrefixOf bs))

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

Option (List α)

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

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

Examples:

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

Instances For

IsSuffix / isSuffixOf / isSuffixOf? #

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

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

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

Examples:

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

Equations

Eq (l₁.isSuffixOf l₂) (l₁.reverse.isPrefixOf l₂.reverse)

Instances For

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

Eq (nil.isSuffixOf l) Bool.true

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

Option (List α)

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

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

Examples:

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

Equations

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

Instances For

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

The first list is a suffix of the second.

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

The function List.isSuffixOf is a Boolean equivalent.

Conventions for notations in identifiers:

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

Equations

Eq (l₁.IsSuffix l₂) (Exists fun (t : List α) => Eq (HAppend.hAppend t l₁) l₂)

Instances For

def List.«term_<:+_» :

The first list is a suffix of the second.

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

The function List.isSuffixOf is a Boolean equivalent.

Conventions for notations in identifiers:

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

Equations

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

Instances For

IsInfix #

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

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

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

Conventions for notations in identifiers:

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

Equations

Eq (l₁.IsInfix l₂) (Exists fun (s : List α) => Exists fun (t : List α) => Eq (HAppend.hAppend (HAppend.hAppend s l₁) t) l₂)

Instances For

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

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

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

Conventions for notations in identifiers:

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

Equations

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

Instances For

splitAt #

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

Prod (List α) (List α)

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

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

Examples:

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

Equations

Eq (List.splitAt n l) (List.splitAt.go l l n List.nil)

Instances For

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

List α → Nat → List α → Prod (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

Eq (List.splitAt.go l List.nil x✝¹ x✝) { fst := l, snd := List.nil }
Eq (List.splitAt.go l (List.cons x_3 xs) n.succ x✝) (List.splitAt.go l xs n (List.cons x_3 x✝))
Eq (List.splitAt.go l x✝² x✝¹ x✝) { fst := x✝.reverse, snd := x✝² }

Instances For

rotateLeft #

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

List α

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

O(|xs|).

Examples:

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

Equations

Eq (xs.rotateLeft i) (ite (LE.le xs.length 1) xs (let i := HMod.hMod i xs.length; let ys := List.take i xs; let zs := List.drop i xs; HAppend.hAppend zs ys))

Instances For

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

Eq (nil.rotateLeft n) nil

rotateRight #

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

List α

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

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

Examples:

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

Equations

Eq (xs.rotateRight i) (ite (LE.le xs.length 1) xs (let i := HSub.hSub xs.length (HMod.hMod i xs.length); let ys := List.take i xs; let zs := List.drop i xs; HAppend.hAppend zs ys))

Instances For

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

Eq (nil.rotateRight n) nil

Pairwise, Nodup #

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

List α → Prop

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

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

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

Examples:

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

nil {α : Type u} {R : α → α → Prop} : Pairwise R List.nil
All elements of the empty list are vacuously pairwise related.
cons {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : (∀ (a' : α), Membership.mem l a' → R a a') → Pairwise R l → Pairwise R (List.cons a l)
A nonempty list is pairwise related with R if the head is related to every element of the tail and the tail is itself pairwise related.
That is, a :: l is Pairwise R if:
- R relates a to every element of l
- l is Pairwise R.

Instances For

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

Iff (Pairwise R (cons a l)) (And (∀ (a' : α), Membership.mem l a' → R a a') (Pairwise R l))

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

Decidable (Pairwise R l)

Equations

One or more equations did not get rendered due to their size.

Instances For

def List.Nodup {α : Type u} :

List α → Prop

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

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

Equations

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

Instances For

def List.nodupDecidable {α : Type u} [DecidableEq α] (l : List α) :

Decidable l.Nodup

Equations

Eq List.nodupDecidable List.instDecidablePairwise

Instances For

Manipulating elements #

replace #

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

List α

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

O(|l|).

Examples:

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

Equations

Eq (List.nil.replace x✝¹ x✝) List.nil
Eq ((List.cons a as).replace x✝¹ x✝) (List.filter.match_1 (fun (x : Bool) => List α) (BEq.beq x✝¹ a) (fun (_ : Unit) => List.cons x✝ as) fun (_ : Unit) => List.cons a (as.replace x✝¹ x✝))

Instances For

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

Eq (nil.replace a b) nil

theorem List.replace_cons {α : Type u} {as : List α} {b c : α} [BEq α] {a : α} :

Eq ((cons a as).replace b c) (filter.match_1 (fun (x : Bool) => List α) (BEq.beq b a) (fun (_ : Unit) => cons c as) fun (_ : Unit) => cons a (as.replace b c))

modify #

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

List α

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

Examples:

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

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

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

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

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

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

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

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

Equations

Eq (l.modifyTailIdx i f) (List.modifyTailIdx.go f i l)

Instances For

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

Nat → List α → List α

Instances For

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

Eq (l.modifyTailIdx 0 f) (f l)

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

Eq (nil.modifyTailIdx (HAdd.hAdd i 1) f) nil

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

Eq ((cons a l).modifyTailIdx (HAdd.hAdd i 1) f) (cons a (l.modifyTailIdx i f))

@[inline]

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

List α → List α

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

Examples:

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

Equations

Eq (List.modifyHead f List.nil) List.nil
Eq (List.modifyHead f (List.cons a as)) (List.cons (f a) as)

Instances For

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

Eq (modifyHead f nil) nil

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

Eq (modifyHead f (cons a l)) (cons (f a) l)

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

List α

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

Examples:

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

Equations

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

Instances For

insert #

@[inline]

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

List α

Inserts an element into a list without duplication.

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

Examples:

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

Equations

Eq (List.insert a l) (ite (Eq (List.elem a l) Bool.true) l (List.cons a l))

Instances For

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

List α

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

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

Examples:

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

Equations

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

Instances For

erase #

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

List α → α → List α

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

O(|l|).

Examples:

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

Equations

Eq (List.nil.erase x✝) List.nil
Eq ((List.cons a as).erase x✝) (List.filter.match_1 (fun (x : Bool) => List α) (BEq.beq a x✝) (fun (_ : Unit) => as) fun (_ : Unit) => List.cons a (as.erase x✝))

Instances For

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

Eq (nil.erase a) nil

theorem List.erase_cons {α : Type u} [BEq α] {a b : α} {l : List α} :

Eq ((cons b l).erase a) (ite (Eq (BEq.beq b a) Bool.true) l (cons b (l.erase a)))

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

List α → List α

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

Examples:

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

Equations

Eq (List.eraseP p List.nil) List.nil
Eq (List.eraseP p (List.cons a as)) (bif p a then as else List.cons a (List.eraseP p as))

Instances For

eraseIdx #

def List.eraseIdx {α : Type u} (l : List α) (i : Nat) :

List α

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

O(i).

Examples:

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

Equations

Eq (List.nil.eraseIdx x✝) List.nil
Eq ((List.cons head as).eraseIdx 0) as
Eq ((List.cons a as).eraseIdx n.succ) (List.cons a (as.eraseIdx n))

Instances For

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

Eq (nil.eraseIdx i) nil

theorem List.eraseIdx_cons_zero {α✝ : Type u_1} {a : α✝} {as : List α✝} :

Eq ((cons a as).eraseIdx 0) as

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

Eq ((cons a as).eraseIdx (HAdd.hAdd i 1)) (cons a (as.eraseIdx i))

Finding elements

find? #

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

List α → Option α

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

O(|l|).

Examples:

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

Equations

Eq (List.find? p List.nil) Option.none
Eq (List.find? p (List.cons a as)) (List.filter.match_1 (fun (x : Bool) => Option α) (p a) (fun (_ : Unit) => Option.some a) fun (_ : Unit) => List.find? p as)

Instances For

theorem List.find?_nil {α : Type u} {p : α → Bool} :

Eq (find? p nil) Option.none

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

Eq (find? p (cons a as)) (filter.match_1 (fun (x : Bool) => Option α✝) (p a) (fun (_ : Unit) => Option.some a) fun (_ : Unit) => find? p as)

findSome? #

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

List α → Option β

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

O(|l|).

Examples:

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

Equations

Eq (List.findSome? f List.nil) Option.none
Eq (List.findSome? f (List.cons a as)) (List.findSome?.match_1 (fun (x : Option β) => Option β) (f a) (fun (b : β) => Option.some b) fun (_ : Unit) => List.findSome? f as)

Instances For

theorem List.findSome?_nil {α : Type u} {α✝ : Type u_1} {f : α → Option α✝} :

Eq (findSome? f nil) Option.none

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

Eq (findSome? f (cons a as)) (findSome?.match_1 (fun (x : Option β) => Option β) (f a) (fun (b : β) => Option.some b) fun (_ : Unit) => findSome? f as)

findIdx #

@[inline]

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

Nat

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

Examples:

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

Equations

Eq (List.findIdx p l) (List.findIdx.go p l 0)

Instances For

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

Eq (List.findIdx.go p List.nil x✝) x✝
Eq (List.findIdx.go p (List.cons a l) x✝) (bif p a then x✝ else List.findIdx.go p l (HAdd.hAdd x✝ 1))

Instances For

theorem List.findIdx_nil {α : Type u} {p : α → Bool} :

Eq (findIdx p nil) 0

idxOf #

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

List α → Nat

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

Examples:

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

Equations

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

Instances For

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

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

List α → Nat

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

Equations

Eq @List.indexOf @List.idxOf

Instances For

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

Eq (idxOf x nil) 0

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

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

Eq (idxOf x nil) 0

findIdx? #

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

Option Nat

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

Examples:

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

Equations

Eq (List.findIdx? p l) (List.findIdx?.go p l 0)

Instances For

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

List α → Nat → Option Nat

Equations

Eq (List.findIdx?.go p List.nil x✝) Option.none
Eq (List.findIdx?.go p (List.cons a l) x✝) (ite (Eq (p a) Bool.true) (Option.some x✝) (List.findIdx?.go p l (HAdd.hAdd x✝ 1)))

Instances For

idxOf? #

@[inline]

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

List α → Option Nat

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

Examples:

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

Equations

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

Instances For

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

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

List α → Option Nat

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

Equations

Eq @List.indexOf? @List.idxOf?

Instances For

findFinIdx? #

@[inline]

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

Option (Fin l.length)

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

Examples:

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

Equations

Eq (List.findFinIdx? p l) (List.findFinIdx?.go p l l 0 ⋯)

Instances For

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

Option (Fin l.length)

Equations

Eq (List.findFinIdx?.go p l List.nil x x_1) Option.none
Eq (List.findFinIdx?.go p l (List.cons a l_1) x x_1) (ite (Eq (p a) Bool.true) (Option.some ⟨x, ⋯⟩) (List.findFinIdx?.go p l l_1 (HAdd.hAdd x 1) ⋯))

Instances For

finIdxOf? #

@[inline]

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

Option (Fin l.length)

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

Examples:

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

Equations

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

Instances For

countP #

@[inline]

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

Nat

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

Examples:

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

Equations

Eq (List.countP p l) (List.countP.go p l 0)

Instances For

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

Eq (List.countP.go p List.nil x✝) x✝
Eq (List.countP.go p (List.cons a l) x✝) (bif p a then List.countP.go p l (HAdd.hAdd x✝ 1) else List.countP.go p l x✝)

Instances For

count #

@[inline]

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

List α → Nat

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

Examples:

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

Equations

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

Instances For

lookup #

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

α → List (Prod α β) → Option β

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

O(|l|).

Examples:

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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

Eq (lookup a nil) Option.none

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

Eq (lookup a (cons { fst := k, snd := b } as)) (filter.match_1 (fun (x : Bool) => Option β✝) (BEq.beq a k) (fun (_ : Unit) => Option.some b) fun (_ : Unit) => lookup a as)

Permutations #

Perm #

inductive List.Perm {α : Type u} :

List α → List α → Prop

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

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

List.isPerm is a Boolean equivalent of this relation.

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

Instances For

def List.«term_~_» :

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

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

List.isPerm is a Boolean equivalent of this relation.

Equations

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

Instances For

isPerm #

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

List α → List α → Bool

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

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

Equations

Eq (List.nil.isPerm x✝) x✝.isEmpty
Eq ((List.cons a l).isPerm x✝) ((x✝.contains a).and (l.isPerm (x✝.erase a)))

Instances For

Logical operations #

any #

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

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

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

Examples:

[2, 4, 6].any (· % 2 = 0) = true
[2, 4, 6].any (· % 2 = 1) = false
[2, 4, 5, 6].any (· % 2 = 0) = true
[2, 4, 5, 6].any (· % 2 = 1) = true

Equations

Eq (x✝¹.any x✝) (List.any.match_1 (fun (x : List α) (x : α → Bool) => Bool) x✝¹ x✝ (fun (x : α → Bool) => Bool.false) fun (h : α) (t : List α) (p : α → Bool) => (p h).or (t.any p))

Instances For

theorem List.any_nil {α✝ : Type u_1} {f : α✝ → Bool} :

Eq (nil.any f) Bool.false

theorem List.any_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {f : α✝ → Bool} :

Eq ((cons a l).any f) ((f a).or (l.any f))

all #

def List.all {α : Type u} :

List α → (α → Bool) → Bool

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

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

Examples:

[a, b, c].all p = (p a && (p b && p c))
[2, 4, 6].all (· % 2 = 0) = true
[2, 4, 5, 6].all (· % 2 = 0) = false

Equations

Eq (x✝¹.all x✝) (List.any.match_1 (fun (x : List α) (x : α → Bool) => Bool) x✝¹ x✝ (fun (x : α → Bool) => Bool.true) fun (h : α) (t : List α) (p : α → Bool) => (p h).and (t.all p))

Instances For

theorem List.all_nil {α✝ : Type u_1} {f : α✝ → Bool} :

Eq (nil.all f) Bool.true

theorem List.all_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {f : α✝ → Bool} :

Eq ((cons a l).all f) ((f a).and (l.all f))

or #

def List.or (bs : List Bool) :

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

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

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

Equations

Eq bs.or (bs.any id)

Instances For

theorem List.or_nil :

Eq nil.or Bool.false

theorem List.or_cons {a : Bool} {l : List Bool} :

Eq (cons a l).or (a.or l.or)

and #

def List.and (bs : List Bool) :

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

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

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

Equations

Eq bs.and (bs.all id)

Instances For

theorem List.and_nil :

Eq nil.and Bool.true

theorem List.and_cons {a : Bool} {l : List Bool} :

Eq (cons a l).and (a.and l.and)

Zippers #

zipWith #

@[specialize #[]]

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

List γ

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

O(min |xs| |ys|).

Examples:

[1, 2].zipWith (· + ·) [5, 6] = [6, 8]
[1, 2, 3].zipWith (· + ·) [5, 6, 10] = [6, 8, 13]
[].zipWith (· + ·) [5, 6] = []
[x₁, x₂, x₃].zipWith f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

Equations

Eq (List.zipWith f (List.cons x_2 xs) (List.cons y ys)) (List.cons (f x_2 y) (List.zipWith f xs ys))
Eq (List.zipWith f x✝¹ x✝) List.nil

Instances For

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

Eq (zipWith f nil l) nil

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

Eq (zipWith f l nil) nil

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

Eq (zipWith f (cons a as) (cons b bs)) (cons (f a b) (zipWith f as bs))

zip #

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

List α → List β → List (Prod α β)

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

O(min |xs| |ys|).

Examples:

["Mon", "Tue", "Wed"].zip [1, 2, 3] = [("Mon", 1), ("Tue", 2), ("Wed", 3)]
["Mon", "Tue", "Wed"].zip [1, 2] = [("Mon", 1), ("Tue", 2)]
[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]

Equations

Eq List.zip (List.zipWith Prod.mk)

Instances For

theorem List.zip_nil_left {α : Type u} {β : Type v} {l : List β} :

Eq (nil.zip l) nil

theorem List.zip_nil_right {α : Type u} {β : Type v} {l : List α} :

Eq (l.zip nil) nil

theorem List.zip_cons_cons {α✝ : Type u_1} {a : α✝} {as : List α✝} {α✝¹ : Type u_2} {b : α✝¹} {bs : List α✝¹} :

Eq ((cons a as).zip (cons b bs)) (cons { fst := a, snd := b } (as.zip bs))

zipWithAll #

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

List α → List β → List γ

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

Examples:

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

Instances For

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

Eq (zipWithAll f as nil) (map (fun (a : α✝) => f (Option.some a) Option.none) as)

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

Eq (zipWithAll f nil bs) (map (fun (b : α✝¹) => f Option.none (Option.some b)) bs)

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

Eq (zipWithAll f (cons a as) (cons b bs)) (cons (f (Option.some a) (Option.some b)) (zipWithAll f as bs))

unzip #

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

Prod (List α) (List β)

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

O(|l|).

Examples:

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem List.unzip_nil {α : Type u} {β : Type v} :

Eq nil.unzip { fst := nil, snd := nil }

theorem List.unzip_cons {α : Type u} {β : Type v} {t : List (Prod α β)} {h : Prod α β} :

Eq (cons h t).unzip (unzip.match_1 (fun (x : Prod (List α) (List β)) => Prod (List α) (List β)) t.unzip fun (as : List α) (bs : List β) => { fst := cons h.fst as, snd := cons h.snd bs })

Ranges and enumeration #

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

List α → α

Computes the sum of the elements of a list.

Examples:

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

Equations

Eq List.sum (List.foldr (fun (x1 x2 : α) => HAdd.hAdd x1 x2) 0)

Instances For

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

Eq nil.sum 0

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

Eq (cons a l).sum (HAdd.hAdd a l.sum)

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

def Nat.sum (l : List Nat) :

Nat

Sum of a list of natural numbers.

Equations

Eq (Nat.sum l) (List.foldr (fun (x1 x2 : Nat) => HAdd.hAdd x1 x2) 0 l)

Instances For

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

theorem Nat.sum_nil :

Eq (Nat.sum List.nil) 0

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

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

Eq (Nat.sum (List.cons a l)) (HAdd.hAdd a (Nat.sum l))

range #

def List.range (n : Nat) :

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

O(n).

Examples:

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

Equations

Eq (List.range n) (List.range.loop n List.nil)

Instances For

def List.range.loop :

Nat → List Nat → List Nat

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem List.range_zero :

Eq (range 0) nil

range' #

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

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

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

Examples:

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

Equations

Eq (List.range' x✝¹ 0 x✝) List.nil
Eq (List.range' x✝¹ n.succ x✝) (List.cons x✝¹ (List.range' (HAdd.hAdd x✝¹ x✝) n x✝))

Instances For

iota #

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

def List.iota :

Nat → List Nat

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

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

Equations

Eq (List.iota 0) List.nil
Eq (List.iota n.succ) (List.cons n.succ (List.iota n))

Instances For

theorem List.iota_zero :

Eq (iota 0) nil

theorem List.iota_succ {i : Nat} :

Eq (iota (HAdd.hAdd i 1)) (cons (HAdd.hAdd i 1) (iota i))

zipIdx #

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

List (Prod α Nat)

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

O(|l|).

Examples:

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

Equations

Eq (List.nil.zipIdx x✝) List.nil
Eq ((List.cons x_2 xs).zipIdx x✝) (List.cons { fst := x_2, snd := x✝ } (xs.zipIdx (HAdd.hAdd x✝ 1)))

Instances For

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

Eq (nil.zipIdx i) nil

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

Eq ((cons a as).zipIdx i) (cons { fst := a, snd := i } (as.zipIdx (HAdd.hAdd i 1)))

enumFrom #

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

def List.enumFrom {α : Type u} :

Nat → List α → List (Prod 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

Eq (List.enumFrom x✝ List.nil) List.nil
Eq (List.enumFrom x✝ (List.cons x_2 xs)) (List.cons { fst := x✝, snd := x_2 } (List.enumFrom (HAdd.hAdd x✝ 1) xs))

Instances For

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

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

Eq (enumFrom i nil) nil

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

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

Eq (enumFrom i (cons a as)) (cons { fst := i, snd := a } (enumFrom (HAdd.hAdd i 1) as))

enum #

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

def List.enum {α : Type u} :

List α → List (Prod 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

Eq List.enum (List.enumFrom 0)

Instances For

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

theorem List.enum_nil {α : Type u} :

Eq nil.enum nil

Minima and maxima #

min? #

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

List α → Option α

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

Examples:

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

Equations

Eq List.nil.min? Option.none
Eq (List.cons a as).min? (Option.some (List.foldl Min.min a as))

Instances For

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

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

List α → Option α

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

Examples:

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

Equations

Eq @List.minimum? @List.min?

Instances For

max? #

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

List α → Option α

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

Examples:

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

Equations

Eq List.nil.max? Option.none
Eq (List.cons a as).max? (Option.some (List.foldl Max.max a as))

Instances For

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

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

List α → Option α

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

Examples:

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

Equations

Eq @List.maximum? @List.max?

Instances For

Other list operations #

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

intersperse #

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

List α

Alternates the elements of l with sep.

O(|l|).

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

Examples:

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

Equations

Eq (List.intersperse sep List.nil) List.nil
Eq (List.intersperse sep (List.cons head List.nil)) (List.cons head List.nil)
Eq (List.intersperse sep (List.cons a as)) (List.cons a (List.cons sep (List.intersperse sep as)))

Instances For

theorem List.intersperse_nil {α : Type u} {sep : α} :

Eq (intersperse sep nil) nil

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

Eq (intersperse sep (cons x nil)) (cons x nil)

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

Eq (intersperse sep (cons x (cons y zs))) (cons x (cons sep (intersperse sep (cons y zs))))

intercalate #

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

List α

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

O(|xs|).

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

Examples:

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

Equations

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

Instances For

eraseDups #

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

List α

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

O(|l|^2).

Examples:

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

Equations

Eq as.eraseDups (List.eraseDups.loop as List.nil)

Instances For

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

List α → List α → List α

Equations

One or more equations did not get rendered due to their size.

Instances For

eraseReps #

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

List α → List α

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

O(|l|).

Example:

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

Equations

Eq x✝.eraseReps (List.getLast?.match_1 (fun (x : List α) => List α) x✝ (fun (_ : Unit) => List.nil) fun (a : α) (as : List α) => List.eraseReps.loop a as List.nil)

Instances For

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

α → List α → List α → List α

Equations

One or more equations did not get rendered due to their size.

Instances For

span #

@[inline]

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

Prod (List α) (List α)

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

O(|l|).

Examples:

[6, 8, 9, 5, 2, 9].span (· > 5) = ([6, 8, 9], [5, 2, 9])
[6, 8, 9, 5, 2, 9].span (· > 10) = ([], [6, 8, 9, 5, 2, 9])
[6, 8, 9, 5, 2, 9].span (· > 0) = ([6, 8, 9, 5, 2, 9], [])

Equations

Eq (List.span p as) (List.span.loop p as List.nil)

Instances For

@[specialize #[]]

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

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

Equations

One or more equations did not get rendered due to their size.

Instances For

splitBy #

@[specialize #[]]

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

List α → List (List α)

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

O(|l|).

Examples:

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

Equations

Eq (List.splitBy R x✝) (List.getLast?.match_1 (fun (x : List α) => List (List α)) x✝ (fun (_ : Unit) => List.nil) fun (a : α) (as : List α) => List.splitBy.loop R as a List.nil List.nil)

Instances For

@[specialize #[]]

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

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

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

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

Equations

One or more equations did not get rendered due to their size.

Instances For

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

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

List α → List (List α)

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

O(|l|).

Examples:

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

Equations

Eq @List.groupBy @List.splitBy

Instances For

removeAll #

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

List α

Removes all elements of xs that are present in ys.

O(|xs| * |ys|).

Examples:

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

Equations

Eq (xs.removeAll ys) (List.filter (fun (x : α) => (List.elem x ys).not) xs)

Instances For

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

Eq (HAdd.hAdd as.length n) (as.lengthTRAux n)

theorem List.length_eq_lengthTR :

Eq @length @lengthTR

map #

@[inline]

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

List β

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

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

Examples:

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

Equations

Eq (List.mapTR f as) (List.mapTR.loop f as List.nil)

Instances For

@[specialize #[]]

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

List α → List β → List β

Equations

Eq (List.mapTR.loop f List.nil x✝) x✝.reverse
Eq (List.mapTR.loop f (List.cons a as) x✝) (List.mapTR.loop f as (List.cons (f a) x✝))

Instances For

theorem List.mapTR_loop_eq {α : Type u} {β : Type v} {f : α → β} {as : List α} {bs : List β} :

Eq (mapTR.loop f as bs) (HAppend.hAppend bs.reverse (map f as))

theorem List.map_eq_mapTR :

Eq @map @mapTR

filter #

@[inline]

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

List α

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

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

Examples:

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

Equations

Eq (List.filterTR p as) (List.filterTR.loop p as List.nil)

Instances For

@[specialize #[]]

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

List α → List α → List α

Equations

One or more equations did not get rendered due to their size.
Eq (List.filterTR.loop p List.nil x✝) x✝.reverse

Instances For

theorem List.filterTR_loop_eq {α : Type u} {p : α → Bool} {as bs : List α} :

Eq (filterTR.loop p as bs) (HAppend.hAppend bs.reverse (filter p as))

theorem List.filter_eq_filterTR :

Eq @filter @filterTR

replicate #

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

List α

Creates a list that contains n copies of a.

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

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

Equations

Eq (List.replicateTR n a) (List.replicateTR.loop a n List.nil)

Instances For

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

Nat → List α → List α

Equations

Eq (List.replicateTR.loop a 0 x✝) x✝
Eq (List.replicateTR.loop a n.succ x✝) (List.replicateTR.loop a n (List.cons a x✝))

Instances For

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

Eq (replicateTR.loop a n (replicate m a)) (replicate (HAdd.hAdd n m) a)

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

Eq (replicateTR.loop a n acc) (HAppend.hAppend (replicate n a) acc)

theorem List.replicate_eq_replicateTR :

Eq @replicate @replicateTR

Additional functions #

leftpad #

@[inline]

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

List α

Pads l : List α on the left with repeated occurrences of a : α until it is of length n. If l already has at least n elements, it is returned unmodified.

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

Examples:

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

Equations

Eq (List.leftpadTR n a l) (List.replicateTR.loop a (HSub.hSub n l.length) l)

Instances For

theorem List.leftpad_eq_leftpadTR :

Eq @leftpad @leftpadTR

Zippers #

unzip #

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

Prod (List α) (List β)

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

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

Examples:

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

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem List.unzip_eq_unzipTR :

Eq @unzip @unzipTR

Ranges and enumeration #

range' #

@[inline]

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

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

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

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

Examples:

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

Equations

Eq (List.range'TR s n step) (List.range'TR.go step n (HAdd.hAdd s (HMul.hMul step n)) List.nil)

Instances For

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

Nat → Nat → List Nat → List Nat

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

Equations

Eq (List.range'TR.go step 0 x✝¹ x✝) x✝
Eq (List.range'TR.go step n.succ x✝¹ x✝) (List.range'TR.go step n (HSub.hSub x✝¹ step) (List.cons (HSub.hSub x✝¹ step) x✝))

Instances For

theorem List.range'_eq_range'TR :

Eq @range' @range'TR

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

Eq (range'TR.go step n (HAdd.hAdd s (HMul.hMul step n)) (range' (HAdd.hAdd s (HMul.hMul step n)) m step)) (range' s (HAdd.hAdd n m) step)

iota #

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

def List.iotaTR (n : Nat) :

Tail-recursive version of List.iota.

Equations

Eq (List.iotaTR n) (List.iotaTR.go n List.nil)

Instances For

def List.iotaTR.go :

Nat → List Nat → List Nat

Equations

Eq (List.iotaTR.go 0 x✝) x✝.reverse
Eq (List.iotaTR.go n.succ x✝) (List.iotaTR.go n (List.cons n.succ x✝))

Instances For

theorem List.iota_eq_iotaTR :

Eq iota iotaTR

Other list operations #

intersperse #

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

List α

Alternates the elements of l with sep.

O(|l|).

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

Examples:

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

Equations

Eq (List.intersperseTR sep List.nil) List.nil
Eq (List.intersperseTR sep (List.cons x_1 List.nil)) (List.cons x_1 List.nil)
Eq (List.intersperseTR sep (List.cons x_1 (List.cons y xs))) (List.cons x_1 (List.cons sep (List.cons y (List.foldr (fun (a : α) (r : List α) => List.cons sep (List.cons a r)) List.nil xs))))

Instances For