Definitions on lists

This file contains various definitions on lists. It does not contain proofs about these definitions, those are contained in other files in Data.List

instance List.instSDiffOfDecidableEq_mathlib {α : Type u_1} [DecidableEq α] : SDiff (List α)

Equations

• List.instSDiffOfDecidableEq_mathlib = { sdiff := List.diff }

def List.getI {α : Type u_1} [Inhabited α] (l : List α) (n : ℕ) : α

"Inhabited" get function: returns default instead of none in the case that the index is out of bounds.

Equations

• l.getI n = l.getD n default

def List.headI {α : Type u_1} [Inhabited α] : List α → α

The head of a list, or the default element of the type is the list is nil.

Equations

• [].headI = default
• (a :: tail).headI = a

@[simp]

theorem List.headI_nil {α : Type u_1} [Inhabited α] : [].headI = default

@[simp]

theorem List.headI_cons {α : Type u_1} [Inhabited α] {h : α} {t : List α} : (h :: t).headI = h

def List.getLastI {α : Type u_1} [Inhabited α] : List α → α

The last element of a list, with the default if list empty

Equations

• [].getLastI = default
• [a].getLastI = a
• [head, b].getLastI = b
• (head :: head_1 :: l).getLastI = l.getLastI

@[inline, deprecated List.pure]

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

List with a single given element.

Equations

• List.ret a = [a]

def List.takeI {α : Type u_1} [Inhabited α] (n : ℕ) (l : List α) : List α

"Inhabited" take function: Take n elements from a list l. If l has less than n elements, append n - length l elements default.

Equations

• List.takeI n l = List.takeD n l default

def List.findM {α : Type u} {m : Type u → Type v} [Alternative m] (tac : α → m PUnit) : List α → m α

findM tac l returns the first element of l on which tac succeeds, and fails otherwise.

Equations

• List.findM tac = List.firstM fun (a : α) => tac a $> a

def List.findM?' {m : Type u → Type v} [Monad m] {α : Type u} (p : α → m (ULift Bool)) : List α → m (Option α)

findM? p l returns the first element a of l for which p a returns true. findM? short-circuits, so p is not necessarily run on every a in l. This is a monadic version of List.find.

Equations

• List.findM?' p [] = pure none
• List.findM?' p (a :: tail) = do let __discr ← p a match __discr with | { down := px } => if px = true then pure (some a) else List.findM?' p tail

def List.orM {m : Type → Type v} [Monad m] : List (m Bool) → m Bool

orM xs runs the actions in xs, returning true if any of them returns true. orM short-circuits, so if an action returns true, later actions are not run.

Equations

• List.orM = List.anyM id

def List.andM {m : Type → Type v} [Monad m] : List (m Bool) → m Bool

andM xs runs the actions in xs, returning true if all of them return true. andM short-circuits, so if an action returns false, later actions are not run.

Equations

• List.andM = List.allM id

def List.foldlIdxM {m : Type v → Type w} [Monad m] {α : Type u_7} {β : Type v} (f : ℕ → β → α → m β) (b : β) (as : List α) : m β

Monadic variant of foldlIdx.

Equations

• List.foldlIdxM f b as = List.foldlIdx (fun (i : ℕ) (ma : m β) (b : α) => do let a ← ma f i a b) (pure b) as

def List.foldrIdxM {m : Type v → Type w} [Monad m] {α : Type u_7} {β : Type v} (f : ℕ → α → β → m β) (b : β) (as : List α) : m β

Monadic variant of foldrIdx.

Equations

• List.foldrIdxM f b as = List.foldrIdx (fun (i : ℕ) (a : α) (mb : m β) => do let b ← mb f i a b) (pure b) as

def List.mapIdxMAux' {m : Type v → Type w} [Monad m] {α : Type u_7} (f : ℕ → α → m PUnit) : ℕ → List α → m PUnit

Auxiliary definition for mapIdxM'.

Equations

• List.mapIdxMAux' f x [] = pure PUnit.unit
• List.mapIdxMAux' f x (a :: as) = f x a *> List.mapIdxMAux' f (x + 1) as

def List.mapIdxM' {m : Type v → Type w} [Monad m] {α : Type u_7} (f : ℕ → α → m PUnit) (as : List α) : m PUnit

A variant of mapIdxM specialised to applicative actions which return Unit.

Equations

• List.mapIdxM' f as = List.mapIdxMAux' f 0 as

def List.Forall {α : Type u_1} (p : α → Prop) : List α → Prop

l.Forall p is equivalent to ∀ a ∈ l, p a, but unfolds directly to a conjunction, i.e. List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations

• List.Forall p [] = True
• List.Forall p [x_1] = p x_1
• List.Forall p (x_1 :: l) = (p x_1 ∧ List.Forall p l)

def List.permutationsAux2 {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) : List α → (List α → β) → List α × List β

An auxiliary function for defining permutations. permutationsAux2 t ts r ys f is equal to (ys ++ ts, (insert_left ys t ts).map f ++ r), where insert_left ys t ts (not explicitly defined) is the list of lists of the form insert_nth n t (ys ++ ts) for 0 ≤ n < length ys.

permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
  ([1, 2, 3, 4, 5, 6],
   [[10, 1, 2, 3, 4, 5, 6],
    [1, 10, 2, 3, 4, 5, 6],
    [1, 2, 10, 3, 4, 5, 6]]) 

Equations

• List.permutationsAux2 t ts r [] x = (ts, r)
• List.permutationsAux2 t ts r (y :: ys) x = match List.permutationsAux2 t ts r ys fun (x_1 : List α) => x (y :: x_1) with | (us, zs) => (y :: us, x (t :: y :: us) :: zs)

@[irreducible]

def List.permutationsAux.rec {α : Type u_1} {C : List α → List α → Sort v} (H0 : (is : List α) → C [] is) (H1 : (t : α) → (ts is : List α) → C ts (t :: is) → C is [] → C (t :: ts) is) (l₁ : List α) (l₂ : List α) : C l₁ l₂

A recursor for pairs of lists. To have C l₁ l₂ for all l₁, l₂, it suffices to have it for l₂ = [] and to be able to pour the elements of l₁ into l₂.

Equations

• List.permutationsAux.rec H0 H1 [] x = H0 x
• List.permutationsAux.rec H0 H1 (t :: ts) x = H1 t ts x (List.permutationsAux.rec H0 H1 ts (t :: x)) (List.permutationsAux.rec H0 H1 x [])

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

An auxiliary function for defining permutations. permutationsAux ts is is the set of all permutations of is ++ ts that do not fix ts.

Equations

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

def List.permutations {α : Type u_1} (l : List α) : List (List α)

List of all permutations of l.

permutations [1, 2, 3] = [[1, 2, 3], [2, 1, 3], [3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]

Equations

• l.permutations = l :: l.permutationsAux []

def List.permutations'Aux {α : Type u_1} (t : α) : List α → List (List α)

permutations'Aux t ts inserts t into every position in ts, including the last. This function is intended for use in specifications, so it is simpler than permutationsAux2, which plays roughly the same role in permutations.

Note that (permutationsAux2 t [] [] ts id).2 is similar to this function, but skips the last position:

permutations'Aux 10 [1, 2, 3] =
  [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
(permutationsAux2 10 [] [] [1, 2, 3] id).2 =
  [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]] 

Equations

• List.permutations'Aux t [] = [[t]]
• List.permutations'Aux t (a :: tail) = (t :: a :: tail) :: List.map (List.cons a) (List.permutations'Aux t tail)

def List.permutations' {α : Type u_1} : List α → List (List α)

List of all permutations of l. This version of permutations is less efficient but has simpler definitional equations. The permutations are in a different order, but are equal up to permutation, as shown by List.permutations_perm_permutations'.

 permutations [1, 2, 3] =
   [[1, 2, 3], [2, 1, 3], [2, 3, 1],
    [1, 3, 2], [3, 1, 2], [3, 2, 1]] 

Equations

• [].permutations' = [[]]
• (a :: tail).permutations' = tail.permutations'.flatMap (List.permutations'Aux a)

def List.extractp {α : Type u_1} (p : α → Prop) [DecidablePred p] : List α → Option α × List α

extractp p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

Equations

• List.extractp p [] = (none, [])
• List.extractp p (a :: tail) = if p a then (some a, tail) else match List.extractp p tail with | (a', l') => (a', a :: l')

instance List.instSProd {α : Type u_1} {β : Type u_2} : SProd (List α) (List β) (List (α × β))

Notation for calculating the product of a List

Equations

• List.instSProd = { sprod := List.product }

instance List.decidableChain {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (a : α) (l : List α) : Decidable (List.Chain R a l)

Equations

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

instance List.decidableChain' {α : Type u_1} {R : α → α → Prop} [DecidableRel R] (l : List α) : Decidable (List.Chain' R l)

Equations

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

def List.dedup {α : Type u_1} [DecidableEq α] : List α → List α

dedup l removes duplicates from l (taking only the last occurrence). Defined as pwFilter (≠).

dedup [1, 0, 2, 2, 1] = [0, 2, 1]

Equations

• List.dedup = List.pwFilter fun (x1 x2 : α) => x1 ≠ x2

def List.destutter' {α : Type u_1} (R : α → α → Prop) [DecidableRel R] : α → List α → List α

Greedily create a sublist of a :: l such that, for every two adjacent elements a, b, R a b holds. Mostly used with ≠; for example, destutter' (≠) 1 [2, 2, 1, 1] = [1, 2, 1], destutter' (≠) 1, [2, 3, 3] = [1, 2, 3], destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

Equations

• List.destutter' R x [] = [x]
• List.destutter' R x (h :: l) = if R x h then x :: List.destutter' R h l else List.destutter' R x l

def List.destutter {α : Type u_1} (R : α → α → Prop) [DecidableRel R] : List α → List α

Greedily create a sublist of l such that, for every two adjacent elements a, b ∈ l, R a b holds. Mostly used with ≠; for example, destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1], destutter (≠) [1, 2, 3, 3] = [1, 2, 3], destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

Equations

• List.destutter R (h :: l) = List.destutter' R h l
• List.destutter R [] = []

def List.chooseX {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : (∃ (a : α), a ∈ l ∧ p a) → { a : α // a ∈ l ∧ p a }

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns both a and proofs of a ∈ l and p a.

Equations

• List.chooseX p [] hp = ⋯.elim
• List.chooseX p (l :: ls) hp = if pl : p l then ⟨l, ⋯⟩ else match List.chooseX p ls ⋯ with | ⟨a, ha⟩ => ⟨a, ⋯⟩

def List.choose {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : α

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns a : α, and properties are given by choose_mem and choose_property.

Equations

• List.choose p l hp = (List.chooseX p l hp).val

def List.mapDiagM' {m : Type → Type u_7} [Monad m] {α : Type u_8} (f : α → α → m Unit) : List α → m Unit

mapDiagM' f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

Example: suppose l = [1, 2, 3]. mapDiagM' f l will evaluate, in this order, f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3.

Equations

• List.mapDiagM' f [] = pure ()
• List.mapDiagM' f (a :: tail) = do let __discr ← f a a let x : Unit := __discr let __discr ← List.mapM' (f a) tail let x : List Unit := __discr List.mapDiagM' f tail

def List.map₂Left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → List γ × List β

Left-biased version of List.map₂. map₂Left' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ. Returns the results of the f applications and the remaining bs.

map₂Left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])

map₂Left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])

Equations

• List.map₂Left' f [] x = ([], x)
• List.map₂Left' f (a :: as) [] = (List.map (fun (a : α) => f a none) (a :: as), [])
• List.map₂Left' f (a :: as) (b :: bs) = (f a (some b) :: (List.map₂Left' f as bs).fst, (List.map₂Left' f as bs).snd)

def List.map₂Right' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) : List γ × List α

Right-biased version of List.map₂. map₂Right' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ. Returns the results of the f applications and the remaining as.

map₂Right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])

map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])

Equations

• List.map₂Right' f as bs = List.map₂Left' (flip f) bs as

def List.map₂Left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) : List α → List β → List γ

Left-biased version of List.map₂. map₂Left f as bs applies f to each pair aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ.

map₂Left Prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]

map₂Left Prod.mk [1] ['a', 'b'] = [(1, some 'a')]

map₂Left f as bs = (map₂Left' f as bs).fst

Equations

• List.map₂Left f [] x = []
• List.map₂Left f (a :: as) [] = List.map (fun (a : α) => f a none) (a :: as)
• List.map₂Left f (a :: as) (b :: bs) = f a (some b) :: List.map₂Left f as bs

def List.map₂Right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → β → γ) (as : List α) (bs : List β) : List γ

Right-biased version of List.map₂. map₂Right f as bs applies f to each pair aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ.

map₂Right Prod.mk [1, 2] ['a'] = [(some 1, 'a')]

map₂Right Prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]

map₂Right f as bs = (map₂Right' f as bs).fst

Equations

• List.map₂Right f as bs = List.map₂Left (flip f) bs as

def List.mapAsyncChunked {α : Type u_7} {β : Type u_8} (f : α → β) (xs : List α) (chunk_size : optParam ℕ 1024) : List β

Asynchronous version of List.map.

Equations

• List.mapAsyncChunked f xs chunk_size = (List.map (fun (xs : List α) => Task.spawn fun (x : Unit) => List.map f xs) (List.toChunks chunk_size xs)).flatMap Task.get

We add some n-ary versions of List.zipWith for functions with more than two arguments. These can also be written in terms of List.zip or List.zipWith. For example, zipWith3 f xs ys zs could also be written as zipWith id (zipWith f xs ys) zs or as (zip xs <| zip ys zs).map <| fun ⟨x, y, z⟩ ↦ f x y z.

def List.zipWith3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → δ) : List α → List β → List γ → List δ

Ternary version of List.zipWith.

Equations

• List.zipWith3 f (x_3 :: xs) (y :: ys) (z :: zs) = f x_3 y z :: List.zipWith3 f xs ys zs
• List.zipWith3 f x✝¹ x✝ x = []

def List.zipWith4 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : α → β → γ → δ → ε) : List α → List β → List γ → List δ → List ε

Quaternary version of list.zipWith.

Equations

• List.zipWith4 f (x_4 :: xs) (y :: ys) (z :: zs) (u :: us) = f x_4 y z u :: List.zipWith4 f xs ys zs us
• List.zipWith4 f x✝² x✝¹ x✝ x = []

def List.zipWith5 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β → γ → δ → ε → ζ) : List α → List β → List γ → List δ → List ε → List ζ

Quinary version of list.zipWith.

Equations

• List.zipWith5 f (x_5 :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) = f x_5 y z u v :: List.zipWith5 f xs ys zs us vs
• List.zipWith5 f x✝³ x✝² x✝¹ x✝ x = []

def List.replaceIf {α : Type u_1} : List α → List Bool → List α → List α

Given a starting list old, a list of booleans and a replacement list new, read the items in old in succession and either replace them with the next element of new or not, according as to whether the corresponding boolean is true or false.

Equations

• x✝.replaceIf x [] = x✝
• [].replaceIf x✝ x = []
• x✝.replaceIf [] x = x✝
• (n :: ns).replaceIf (tf :: bs) (c :: cs) = if tf = true then c :: ns.replaceIf bs cs else n :: ns.replaceIf bs (c :: cs)

def List.iterate {α : Type u_1} (f : α → α) (a : α) (n : ℕ) : List α

iterate f a n is [a, f a, ..., f^[n - 1] a].

Equations

• List.iterate f a 0 = []
• List.iterate f a n.succ = a :: List.iterate f (f a) n

@[inline]

def List.iterateTR {α : Type u_1} (f : α → α) (a : α) (n : ℕ) : List α

Tail-recursive version of List.iterate.

Equations

• List.iterateTR f a n = List.iterateTR.loop f a n []

@[specialize #[]]

def List.iterateTR.loop {α : Type u_1} (f : α → α) (a : α) (n : ℕ) (l : List α) : List α

iterateTR.loop f a n l := iterate f a n ++ reverse l.

Equations

• List.iterateTR.loop f a 0 l = l.reverse
• List.iterateTR.loop f a n_1.succ l = List.iterateTR.loop f (f a) n_1 (a :: l)

theorem List.iterateTR_loop_eq {α : Type u_1} (f : α → α) (a : α) (n : ℕ) (l : List α) : List.iterateTR.loop f a n l = l.reverse ++ List.iterate f a n

@[csimp]

theorem List.iterate_eq_iterateTR : @List.iterate = @List.iterateTR

def List.mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) : List α → γ → γ × List β

Runs a function over a list returning the intermediate results and a final result.

Equations

• List.mapAccumr f [] x = (x, [])
• List.mapAccumr f (y :: yr) x = ((f y (List.mapAccumr f yr x).fst).fst, (f y (List.mapAccumr f yr x).fst).snd :: (List.mapAccumr f yr x).snd)

@[simp]

theorem List.length_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → γ → γ × β) (x : List α) (s : γ) : (List.mapAccumr f x s).snd.length = x.length

Length of the list obtained by mapAccumr.

def List.mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) : List α → List β → γ → γ × List δ

Runs a function over two lists returning the intermediate results and a final result.

Equations

• List.mapAccumr₂ f [] x✝ x = (x, [])
• List.mapAccumr₂ f x✝ [] x = (x, [])
• List.mapAccumr₂ f (x_3 :: xr) (y :: yr) x = ((f x_3 y (List.mapAccumr₂ f xr yr x).fst).fst, (f x_3 y (List.mapAccumr₂ f xr yr x).fst).snd :: (List.mapAccumr₂ f xr yr x).snd)

@[simp]

theorem List.length_mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : List α) (y : List β) (c : γ) : (List.mapAccumr₂ f x y c).snd.length = min x.length y.length

Length of a list obtained using mapAccumr₂.

def List.finRange (n : ℕ) : List (Fin n)

All elements of Fin n, from 0 to n-1. The corresponding finset is Finset.univ.

Equations

• List.finRange n = List.pmap Fin.mk (List.range n) ⋯

@[deprecated List.mem_cons]

theorem List.mem_cons_eq {α : Type u_1} (a : α) (y : α) (l : List α) : (a ∈ y :: l) = (a = y ∨ a ∈ l)

theorem List.eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {b : α} {l : List α} {a : α}, a ∈ b :: l → a = b ∨ a ∈ l

Alias of the forward direction of List.mem_cons.

@[deprecated List.not_mem_nil]

theorem List.not_exists_mem_nil {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), x ∈ [] ∧ p x

@[deprecated List.not_exists_mem_nil]

theorem List.not_bex_nil {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), x ∈ [] ∧ p x

Alias of List.not_exists_mem_nil.

@[deprecated List.exists_mem_cons]

theorem List.bex_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), ∃ (x_1 : x ∈ a :: l), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ l), p x

Alias of List.exists_mem_cons.

@[deprecated List.Sublist.length_le]

theorem List.length_le_of_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length

Alias of List.Sublist.length_le.