doc-next-gen

Mathlib.Data.List.Defs

Module docstring

{"## 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 ","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. "}

List.instSDiffOfDecidableEq_mathlib instance
[DecidableEq α] : SDiff (List α)
Full source 
instance [DecidableEq α] : SDiff (List α) :=
  ⟨List.diff⟩
Set Difference Operation on Lists with Decidable Equality
Informal description
For any type $\alpha$ with decidable equality, the type of lists over $\alpha$ has a set difference operation.
List.getI definition
[Inhabited α] (l : List α) (n : Nat) : α
Full source 
/-- "Inhabited" `get` function: returns `default` instead of `none` in the case
  that the index is out of bounds. -/
def getI [Inhabited α] (l : List α) (n : Nat) : α :=
  getD l n default
Default value list accessor
Informal description
Given a list `l` of elements of type `α` (where `α` has a default value) and a natural number index `n`, the function returns the element at position `n` in `l` if `n` is within bounds; otherwise, it returns the default value of `α`.
List.headI definition
[Inhabited α] : List α → α
Full source 
/-- The head of a list, or the default element of the type is the list is `nil`. -/
def headI [Inhabited α] : List α → α
  | []       => default
  | (a :: _) => a
Head of a list with default value
Informal description
Given a type `α` with a default element and a list `l : List α`, the function returns the first element of `l` if `l` is non-empty, and returns the default element of `α` if `l` is empty.
List.headI_nil theorem
[Inhabited α] : ([] : List α).headI = default
Full source 
@[simp] theorem headI_nil [Inhabited α] : ([] : List α).headI = default := rfl
Head of Empty List is Default Element
Informal description
For any inhabited type $\alpha$, the head of the empty list (with default value) is equal to the default element of $\alpha$, i.e., $\text{headI}([]) = \text{default}$.
List.headI_cons theorem
[Inhabited α] {h : α} {t : List α} : (h :: t).headI = h
Full source 
@[simp] theorem headI_cons [Inhabited α] {h : α} {t : List α} : (h :: t).headI = h := rfl
Head of a Cons List is the First Element
Informal description
For any type $\alpha$ with a default element, and for any element $h \in \alpha$ and list $t$ of elements in $\alpha$, the head of the list $h :: t$ is equal to $h$.
List.getLastI definition
[Inhabited α] : List α → α
Full source 
/-- The last element of a list, with the default if list empty -/
def getLastI [Inhabited α] : List α → α
  | [] => default
  | [a] => a
  | [_, b] => b
  | _ :: _ :: l => getLastI l
Default-extended last element of a list
Informal description
The function `List.getLastI` takes a list of elements of type `α` (where `α` has a default inhabitant) and returns its last element. If the list is empty, it returns the default value of `α`. For a singleton list `[a]`, it returns `a`. For a list with two elements `[_, b]`, it returns `b`. For longer lists, it recursively processes the list to find the last element.
List.takeI definition
[Inhabited α] (n : Nat) (l : List α) : List α
Full source 
/-- "Inhabited" `take` function: Take `n` elements from a list `l`. If `l` has less than `n`
  elements, append `n - length l` elements `default`. -/
def takeI [Inhabited α] (n : Nat) (l : List α) : List α :=
  takeD n l default
Default-extended list truncation
Informal description
Given a type `α` with a default inhabitant, a natural number `n`, and a list `l` of elements of type `α`, the function `List.takeI` returns a list consisting of the first `n` elements of `l`. If `l` has fewer than `n` elements, the remaining positions are filled with the default value of `α`.
List.findM definition
{α} {m : Type u → Type v} [Alternative m] (tac : α → m PUnit) : List α → m α
Full source 
/-- `findM tac l` returns the first element of `l` on which `tac` succeeds, and
fails otherwise. -/
def findM {α} {m : Type u → Type v} [Alternative m] (tac : α → m PUnit) : List α → m α :=
  List.firstM fun a => (tac a) $> a
First element satisfying a monadic predicate
Informal description
Given a monad `m` with an `Alternative` instance, a predicate `tac : α → m PUnit`, and a list `l : List α`, the function `List.findM` returns the first element of `l` for which `tac` succeeds (i.e., does not fail). If no such element exists, the function fails.
List.findM?' definition
{m : Type u → Type v} [Monad m] {α : Type u} (p : α → m (ULift Bool)) : List α → m (Option α)
Full source 
/-- `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`. -/
def findM?'
    {m : Type u → Type v}
    [Monad m] {α : Type u}
    (p : α → m (ULift Bool)) : List α → m (Option α)
  | [] => pure none
  | x :: xs => do
    let ⟨px⟩ ← p x
    if px then pure (some x) else findM?' p xs
Monadic find-first in a list with short-circuiting
Informal description
Given a monad `m`, a predicate `p : α → m (ULift Bool)`, and a list `l : List α`, the function `List.findM?'` returns the first element `x` of `l` for which `p x` evaluates to `true` (wrapped in `ULift`). The search short-circuits, meaning `p` is not evaluated for subsequent elements once a matching element is found. The result is returned as an `Option α` wrapped in the monad `m`.
List.orM definition
: List (m Bool) → m Bool
Full source 
/-- `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. -/
def orM : List (m Bool) → m Bool :=
  anyM id
Short-circuiting monadic disjunction of a list of booleans
Informal description
Given a list of monadic boolean values `xs`, `orM` evaluates each boolean in sequence, returning `true` as soon as any element evaluates to `true` (short-circuiting behavior). If all elements evaluate to `false`, it returns `false`.
List.andM definition
: List (m Bool) → m Bool
Full source 
/-- `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. -/
def andM : List (m Bool) → m Bool :=
  allM id
Monadic conjunction of a list of boolean actions
Informal description
Given a monad `m` and a list of monadic boolean values `xs : List (m Bool)`, the function `List.andM` evaluates each boolean in sequence, returning `true` if all actions evaluate to `true`. The evaluation short-circuits: if any action returns `false`, subsequent actions are not executed.
List.foldlIdxM definition
{α β} (f : ℕ → β → α → m β) (b : β) (as : List α) : m β
Full source 
/-- Monadic variant of `foldlIdx`. -/
def foldlIdxM {α β} (f : ℕ → β → α → m β) (b : β) (as : List α) : m β :=
  as.foldlIdx
    (fun i ma b => do
      let a ← ma
      f i a b)
    (pure b)
Monadic indexed left fold over a list
Informal description
Given a monadic function `f : ℕ → β → α → m β`, an initial value `b : β`, and a list `as : List α`, the function `foldlIdxM` performs a left fold over the list while tracking the current index. At each step, it applies `f` to the current index, the accumulated value, and the current list element, returning the result in the monadic context `m`.
List.foldrIdxM definition
{α β} (f : ℕ → α → β → m β) (b : β) (as : List α) : m β
Full source 
/-- Monadic variant of `foldrIdx`. -/
def foldrIdxM {α β} (f : ℕ → α → β → m β) (b : β) (as : List α) : m β :=
  as.foldrIdx
    (fun i a mb => do
      let b ← mb
      f i a b)
    (pure b)
Monadic right-fold with index over a list
Informal description
Given a monadic function `f : ℕ → α → β → m β`, an initial value `b : β`, and a list `as : List α`, the function `List.foldrIdxM` performs a right-fold over the list while tracking the index of each element. The fold starts with the initial value `b` and applies `f` at each step, passing the current index, element, and accumulated value. The result is wrapped in the monad `m`.
List.mapIdxMAux' definition
{α} (f : ℕ → α → m PUnit) : ℕ → List α → m PUnit
Full source 
/-- Auxiliary definition for `mapIdxM'`. -/
def mapIdxMAux' {α} (f : ℕ → α → m PUnit) : ℕ → List α → m PUnit
  | _, [] => pure ⟨⟩
  | i, a :: as => f i a *> mapIdxMAux' f (i + 1) as
Monadic indexed map auxiliary function (unit result)
Informal description
The auxiliary function `mapIdxMAux'` takes a function `f : ℕ → α → m PUnit`, a starting index `i : ℕ`, and a list `as : List α`. It applies `f` to each element of the list along with its corresponding index (starting from `i`), sequencing the results in the monad `m`. The function returns the monadic unit `⟨⟩` after processing all elements. For an empty list, it returns the pure unit. For a non-empty list `a :: as`, it first applies `f i a`, then recursively processes the remaining list `as` with the index incremented by 1.
List.mapIdxM' definition
{α} (f : ℕ → α → m PUnit) (as : List α) : m PUnit
Full source 
/-- A variant of `mapIdxM` specialised to applicative actions which
return `Unit`. -/
def mapIdxM' {α} (f : ℕ → α → m PUnit) (as : List α) : m PUnit :=
  mapIdxMAux' f 0 as
Monadic indexed map with unit result
Informal description
The function `List.mapIdxM'` takes a monadic function `f : ℕ → α → m PUnit` and a list `as : List α`. It applies `f` to each element of the list along with its corresponding index (starting from 0), sequencing the results in the monad `m`. The function returns the monadic unit `⟨⟩` after processing all elements. This is a specialized version of `mapIdxM` for applicative actions that return `Unit`.
List.Forall definition
(p : α → Prop) : List α → Prop
Full source 
/-- `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`. -/
@[simp]
def Forall (p : α → Prop) : List α → Prop
  | [] => True
  | x :: [] => p x
  | x :: l => p x ∧ Forall p l
Universal quantification over a list
Informal description
The predicate `List.Forall p l` checks that every element `x` in the list `l` satisfies the property `p x`. It is defined recursively as follows: - For the empty list `[]`, it is trivially true. - For a singleton list `[x]`, it is `p x`. - For a list `x :: l`, it is `p x` and `List.Forall p l`. This is equivalent to `∀ a ∈ l, p a` but unfolds directly to a conjunction, e.g., `List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2`.
List.permutationsAux2 definition
(t : α) (ts : List α) (r : List β) : List α → (List α → β) → List α × List β
Full source 
/-- 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]]) -/
def permutationsAux2 (t : α) (ts : List α) (r : List β) : List α → (List α → β) → ListList α × List β
  | [], _ => (ts, r)
  | y :: ys, f =>
    let (us, zs) := permutationsAux2 t ts r ys (fun x : List α => f (y :: x))
    (y :: us, f (t :: y :: us) :: zs)
Auxiliary function for generating permutations with insertions
Informal description
The auxiliary function `permutationsAux2` takes an element `t`, a list `ts`, an accumulator `r`, a list `ys`, and a function `f`. It returns a pair consisting of the concatenation of `ys` and `ts`, and a list formed by applying `f` to all lists obtained by inserting `t` at every possible position in `ys` followed by `ts`, appended with `r`. For example, `permutationsAux2 10 [4, 5, 6] [] [1, 2, 3] id` returns: - The list `[1, 2, 3, 4, 5, 6]` - The list of lists `[[10, 1, 2, 3, 4, 5, 6], [1, 10, 2, 3, 4, 5, 6], [1, 2, 10, 3, 4, 5, 6]]`
List.permutationsAux.rec definition
{C : List α → List α → Sort v} (H0 : ∀ is, C [] is) (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
Full source 
/-- 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₂`. -/
@[elab_as_elim]
def permutationsAux.rec {C : List α → List α → Sort v} (H0 : ∀ is, C [] is)
    (H1 : ∀ t ts is, C ts (t :: is) → C is [] → C (t :: ts) is) : ∀ l₁ l₂, C l₁ l₂
  | [], is => H0 is
  | t :: ts, is =>
      H1 t ts is (permutationsAux.rec H0 H1 ts (t :: is)) (permutationsAux.rec H0 H1 is [])
  termination_by ts is => (length ts + length is, length ts)
  decreasing_by all_goals (simp_wf; omega)
Recursor for pairs of lists
Informal description
A recursor for pairs of lists. To define a property $C(l_1, l_2)$ for all lists $l_1$ and $l_2$, it suffices to: 1. Define $C([], l_2)$ for any list $l_2$, and 2. Show how to extend the definition when prepending an element to $l_1$, given that $C$ holds for the tail of $l_1$ with the element added to $l_2$, and for $l_2$ with the empty list. More precisely, given: - A base case $H_0$ proving $C([], l_2)$ for any $l_2$, and - An inductive step $H_1$ which, given an element $t$, lists $ts$ and $is$, and proofs of $C(ts, t :: is)$ and $C(is, [])$, produces a proof of $C(t :: ts, is)$, then $C(l_1, l_2)$ holds for all lists $l_1$ and $l_2$.
List.permutationsAux definition
: List α → List α → List (List α)
Full source 
/-- An auxiliary function for defining `permutations`. `permutationsAux ts is` is the set of all
permutations of `is ++ ts` that do not fix `ts`. -/
def permutationsAux : List α → List α → List (List α) :=
  permutationsAux.rec (fun _ => []) fun t ts is IH1 IH2 =>
    foldr (fun y r => (permutationsAux2 t ts r y id).2) IH1 (is :: IH2)
Auxiliary function for generating non-fixing permutations
Informal description
The auxiliary function `permutationsAux` takes two lists `ts` and `is` and returns a list of all permutations of `is ++ ts` that do not fix `ts`. More precisely, it generates all permutations where the elements of `ts` appear in some order that is not their original order in `ts`. This is used as a helper function for generating all permutations of a list.
List.permutations definition
(l : List α) : List (List α)
Full source 
/-- 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]] -/
def permutations (l : List α) : List (List α) :=
  l :: permutationsAux l []
List of all permutations
Informal description
Given a list $l$ of elements of type $\alpha$, the function `permutations` returns a list of all possible permutations of $l$. For example, `permutations [1, 2, 3]` returns the list `[[1, 2, 3], [2, 1, 3], [3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]`.
List.permutations'Aux definition
(t : α) : List α → List (List α)
Full source 
/-- `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]] -/
@[simp]
def permutations'Aux (t : α) : List α → List (List α)
  | [] => [[t]]
  | y :: ys => (t :: y :: ys) :: (permutations'Aux t ys).map (cons y)
Insert element into all positions of a list (auxiliary function for permutations)
Informal description
Given an element $t$ of type $\alpha$ and a list $ys$ of elements of type $\alpha$, the function `permutations'Aux` inserts $t$ into every possible position in $ys$, including the last position. Specifically: - If $ys$ is empty, the result is the singleton list containing $[t]$. - If $ys$ is of the form $y :: ys'$, the result is the list obtained by prepending $t$ to $y :: ys'$, concatenated with the list obtained by inserting $t$ into every position of $ys'$ and then prepending $y$ to each resulting list. This function is designed for use in specifications and is simpler than the more general `permutationsAux2` function, which serves a similar purpose but skips the last position when inserting $t$.
List.permutations' definition
: List α → List (List α)
Full source 
/-- 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]] -/
@[simp]
def permutations' : List α → List (List α)
  | [] => [[]]
  | t :: ts => (permutations' ts).flatMap <| permutations'Aux t
List of all permutations (simpler definition)
Informal description
Given a list $l$ of elements of type $\alpha$, the function `permutations'` returns a list of all possible permutations of $l$. The permutations are generated by inserting the first element of $l$ into all possible positions of each permutation of the remaining elements. For example, `permutations' [1, 2, 3]` returns the list `[[1, 2, 3], [2, 1, 3], [2, 3, 1], [1, 3, 2], [3, 1, 2], [3, 2, 1]]`.
List.extractp definition
(p : α → Prop) [DecidablePred p] : List α → Option α × List α
Full source 
/-- `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)`. -/
def extractp (p : α → Prop) [DecidablePred p] : List α → OptionOption α × List α
  | [] => (none, [])
  | a :: l =>
    if p a then (some a, l)
    else
      let (a', l') := extractp p l
      (a', a :: l')
Extract and remove first satisfying element from list
Informal description
The function `extractp` takes a decidable predicate `p` and a list `l`, and returns a pair consisting of: 1. An optional element of `l` that satisfies `p` (wrapped in `some` if found, `none` otherwise) 2. The remaining list with this element removed (if found) For the empty list, it returns `(none, [])`. For a non-empty list `a :: l`, it first checks if `a` satisfies `p`. If yes, it returns `(some a, l)`. If not, it recursively processes the tail `l` and prepends `a` to the resulting list.
List.instSProd instance
: SProd (List α) (List β) (List (α × β))
Full source 
/-- Notation for calculating the product of a `List`
-/

instance instSProd : SProd (List α) (List β) (List (α × β)) where
  sprod := List.product
List Cartesian Product Operation
Informal description
For any types $\alpha$ and $\beta$, the Cartesian product operation $(\times)$ can be extended to lists, where the product of a list $l_1$ of elements in $\alpha$ and a list $l_2$ of elements in $\beta$ is a list of pairs $(a, b)$ for $a \in l_1$ and $b \in l_2$.
List.decidableChain instance
{R : α → α → Prop} [DecidableRel R] (a : α) (l : List α) : Decidable (Chain R a l)
Full source 
instance decidableChain {R : α → α → Prop} [DecidableRel R] (a : α) (l : List α) :
    Decidable (Chain R a l) := by
  induction l generalizing a with
  | nil => exact decidable_of_decidable_of_iff (p := True) (by simp)
  | cons b as ih =>
    haveI := ih; exact decidable_of_decidable_of_iff (p := (R a b ∧ Chain R b as)) (by simp)
Decidability of Chain Property for Lists
Informal description
For any relation $R$ on a type $\alpha$ with a decidable predicate, and any element $a \in \alpha$ and list $l$ of elements in $\alpha$, the property $\text{Chain}(R, a, l)$ is decidable. Here, $\text{Chain}(R, a, l)$ means that the list $l$ forms a chain starting with $a$ under the relation $R$, i.e., $R(a, l_1)$ holds, $R(l_1, l_2)$ holds, and so on for consecutive elements in $l$.
List.decidableChain' instance
{R : α → α → Prop} [DecidableRel R] (l : List α) : Decidable (Chain' R l)
Full source 
instance decidableChain' {R : α → α → Prop} [DecidableRel R] (l : List α) :
    Decidable (Chain' R l) := by
  cases l
  · exact inferInstanceAs (Decidable True)
  · exact inferInstanceAs (Decidable (Chain _ _ _))
Decidability of Chain' Property for Lists
Informal description
For any relation $R$ on a type $\alpha$ with a decidable predicate and any list $l$ of elements in $\alpha$, the property $\text{Chain'}(R, l)$ is decidable. Here, $\text{Chain'}(R, l)$ means that the list $l$ forms a chain under the relation $R$, i.e., $R(l_1, l_2)$ holds, $R(l_2, l_3)$ holds, and so on for consecutive elements in $l$.
List.dedup definition
[DecidableEq α] : List α → List α
Full source 
/-- `dedup l` removes duplicates from `l` (taking only the last occurrence).
  Defined as `pwFilter (≠)`.

     dedup [1, 0, 2, 2, 1] = [0, 2, 1] -/
def dedup [DecidableEq α] : List α → List α :=
  pwFilter (· ≠ ·)
List deduplication (keeping last occurrences)
Informal description
Given a list `l` with elements of type `α` (where equality is decidable), the function `dedup` removes duplicate elements from `l`, keeping only the last occurrence of each element. For example, `dedup [1, 0, 2, 2, 1]` results in `[0, 2, 1]`.
List.destutter' definition
(R : α → α → Prop) [DecidableRel R] : α → List α → List α
Full source 
/-- 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]`. -/
def destutter' (R : α → α → Prop) [DecidableRel R] : α → List α → List α
  | a, [] => [a]
  | a, h :: l => if R a h then a :: destutter' R h l else destutter' R a l
Greedy destuttering of a list with respect to a relation
Informal description
Given a binary relation $R$ on a type $\alpha$ with decidable relation, an element $a \in \alpha$, and a list $l$ of elements of $\alpha$, the function `destutter'` greedily constructs a sublist of $a :: l$ such that for every pair of adjacent elements $x$ and $y$ in the resulting list, $R(x, y)$ holds. 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]`
List.destutter definition
(R : α → α → Prop) [DecidableRel R] : List α → List α
Full source 
/-- 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]`. -/
def destutter (R : α → α → Prop) [DecidableRel R] : List α → List α
  | h :: l => destutter' R h l
  | [] => []
Greedy destuttering of a list with respect to a relation
Informal description
Given a binary relation $R$ on a type $\alpha$ with decidable relation and a list $l$ of elements of $\alpha$, the function `destutter` greedily constructs a sublist of $l$ such that for every pair of adjacent elements $x$ and $y$ in the resulting list, $R(x, y)$ holds. 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]`
List.chooseX definition
: ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }
Full source 
/-- 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`. -/
def chooseX : ∀ l : List α, ∀ _ : ∃ a, a ∈ l ∧ p a, { a // a ∈ l ∧ p a }
  | [], hp => False.elim (Exists.elim hp fun _ h => not_mem_nil h.left)
  | l :: ls, hp =>
    if pl : p l then ⟨l, ⟨mem_cons.mpr <| Or.inl rfl, pl⟩⟩
    else
      -- pattern matching on `hx` too makes this not reducible!
      let ⟨a, ha⟩ :=
        chooseX ls
          (hp.imp fun _ ⟨o, h₂⟩ => ⟨(mem_cons.mp o).resolve_left fun e => pl <| e ▸ h₂, h₂⟩)
      ⟨a, mem_cons.mpr <| Or.inr ha.1, ha.2⟩
First element satisfying a predicate in a list with proofs
Informal description
Given a list \( l \) of elements of type \( \alpha \) and a decidable predicate \( p \) on \( \alpha \), if there exists an element \( a \in l \) such that \( p(a) \) holds, then `List.chooseX` returns the first such element \( a \) along with proofs that \( a \in l \) and \( p(a) \).
List.choose definition
(hp : ∃ a, a ∈ l ∧ p a) : α
Full source 
/-- 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`. -/
def choose (hp : ∃ a, a ∈ l ∧ p a) : α :=
  chooseX p l hp
First element satisfying a predicate in a list
Informal description
Given a list \( l \) of elements of type \( \alpha \) and a decidable predicate \( p \) on \( \alpha \), if there exists an element \( a \in l \) such that \( p(a) \) holds, then `List.choose` returns the first such element \( a \).
List.mapDiagM' definition
{m} [Monad m] {α} (f : α → α → m Unit) : List α → m Unit
Full source 
/-- `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`.
-/
def mapDiagM' {m} [Monad m] {α} (f : α → α → m Unit) : List α → m Unit
  | [] => return ()
  | h :: t => do
    _ ← f h h
    _ ← t.mapM' (f h)
    t.mapDiagM' f
Upper triangular monadic mapping on a list
Informal description
Given a monadic function $f : \alpha \to \alpha \to m \text{ Unit}$ and a list $l$ of elements of type $\alpha$, `mapDiagM' f l` applies $f$ to all pairs of elements in the upper triangular part of $l \times l$. Specifically, for each element $e \in l$, it first applies $f$ to $(e, e)$, then applies $f$ to $(e, e')$ for each subsequent element $e'$ appearing after $e$ in $l$. For example, if $l = [1, 2, 3]$, then `mapDiagM' f l` will evaluate in order: $f(1, 1)$, $f(1, 2)$, $f(1, 3)$, $f(2, 2)$, $f(2, 3)$, $f(3, 3)$.
List.map₂Left' definition
(f : α → Option β → γ) : List α → List β → List γ × List β
Full source 
/-- 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'])
```
-/
@[simp]
def map₂Left' (f : α → Option β → γ) : List α → List β → ListList γ × List β
  | [], bs => ([], bs)
  | a :: as, [] => ((a :: as).map fun a => f a none, [])
  | a :: as, b :: bs =>
    let rec' := map₂Left' f as bs
    (f a (some b) :: rec'.fst, rec'.snd)
Left-biased pairwise mapping with remaining elements
Informal description
Given a function $f : \alpha \to \text{Option } \beta \to \gamma$ and two lists $as : \text{List } \alpha$ and $bs : \text{List } \beta$, the function $\text{map₂Left'}$ applies $f$ pairwise to elements of $as$ and $bs$. If $bs$ is shorter than $as$, $f$ is applied to the remaining elements of $as$ with $\text{none}$ as the second argument. The function returns a pair consisting of the list of results from applying $f$ and the remaining elements of $bs$ (if any).
List.map₂Right' definition
(f : Option α → β → γ) (as : List α) (bs : List β) : List γ × List α
Full source 
/-- 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])
```
-/
def map₂Right' (f : Option α → β → γ) (as : List α) (bs : List β) : ListList γ × List α :=
  map₂Left' (flip f) bs as
Right-biased pairwise mapping with remaining elements
Informal description
Given a function $f : \text{Option } \alpha \to \beta \to \gamma$ and two lists $as : \text{List } \alpha$ and $bs : \text{List } \beta$, the function $\text{map₂Right'}$ applies $f$ pairwise to elements of $as$ and $bs$. If $as$ is shorter than $bs$, $f$ is applied to $\text{none}$ for the remaining elements of $bs$. The function returns a pair consisting of the list of results from applying $f$ and the remaining elements of $as$ (if any). For example: - $\text{map₂Right' prod.mk } [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])$ - $\text{map₂Right' prod.mk } [1, 2] ['a'] = ([(some 1, 'a')], [2])$
List.map₂Left definition
(f : α → Option β → γ) : List α → List β → List γ
Full source 
/-- 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
```
-/
@[simp]
def map₂Left (f : α → Option β → γ) : List α → List β → List γ
  | [], _ => []
  | a :: as, [] => (a :: as).map fun a => f a none
  | a :: as, b :: bs => f a (some b) :: map₂Left f as bs
Left-biased pairwise mapping with optional elements
Informal description
Given a function \( f : \alpha \to \text{Option } \beta \to \gamma \) and two lists \( as : \text{List } \alpha \) and \( bs : \text{List } \beta \), the function `List.map₂Left` applies \( f \) to each pair of elements \( (a_i, \text{some } b_i) \) where \( a_i \in as \) and \( b_i \in bs \). If \( bs \) is shorter than \( as \), the remaining elements \( a_i \) are paired with `none`. The result is a list of \( \gamma \) elements obtained from these applications. For example: - `map₂Left Prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]` - `map₂Left Prod.mk [1] ['a', 'b'] = [(1, some 'a')]`
List.map₂Right definition
(f : Option α → β → γ) (as : List α) (bs : List β) : List γ
Full source 
/-- 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
```
-/
def map₂Right (f : Option α → β → γ) (as : List α) (bs : List β) : List γ :=
  map₂Left (flip f) bs as
Right-biased pairwise mapping with optional elements
Informal description
Given a function \( f : \text{Option } \alpha \to \beta \to \gamma \) and two lists \( as : \text{List } \alpha \) and \( bs : \text{List } \beta \), the function `List.map₂Right` applies \( f \) to each pair of elements \( (\text{some } a_i, b_i) \) where \( a_i \in as \) and \( b_i \in bs \). If \( as \) is shorter than \( bs \), the remaining elements \( b_i \) are paired with `none`. The result is a list of \( \gamma \) elements obtained from these applications. For example: - `map₂Right Prod.mk [1, 2] ['a'] = [(some 1, 'a')]` - `map₂Right Prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]`
List.zipWith3 definition
(f : α → β → γ → δ) : List α → List β → List γ → List δ
Full source 
/-- Ternary version of `List.zipWith`. -/
def zipWith3 (f : α → β → γ → δ) : List α → List β → List γ → List δ
  | x :: xs, y :: ys, z :: zs => f x y z :: zipWith3 f xs ys zs
  | _, _, _ => []
Element-wise application of a ternary function to three lists
Informal description
Given a function \( f : \alpha \to \beta \to \gamma \to \delta \) and three lists \( [x_1, \ldots, x_n] \), \( [y_1, \ldots, y_n] \), and \( [z_1, \ldots, z_n] \), the function `List.zipWith3` applies \( f \) element-wise to the lists, producing a new list \( [f(x_1, y_1, z_1), \ldots, f(x_n, y_n, z_n)] \). If the lists have different lengths, the resulting list has length equal to the shortest input list.
List.zipWith4 definition
(f : α → β → γ → δ → ε) : List α → List β → List γ → List δ → List ε
Full source 
/-- Quaternary version of `list.zipWith`. -/
def zipWith4 (f : α → β → γ → δ → ε) : List α → List β → List γ → List δ → List ε
  | x :: xs, y :: ys, z :: zs, u :: us => f x y z u :: zipWith4 f xs ys zs us
  | _, _, _, _ => []
Element-wise application of a quaternary function to four lists
Informal description
The function `List.zipWith4` takes a function $f : \alpha \times \beta \times \gamma \times \delta \to \varepsilon$ and four lists of elements of types $\alpha$, $\beta$, $\gamma$, and $\delta$ respectively, and returns a list of elements of type $\varepsilon$. The resulting list is obtained by applying $f$ element-wise to the corresponding elements of the four input lists. If the input lists have different lengths, the resulting list has length equal to the minimum of the lengths of the input lists.
List.zipWith5 definition
(f : α → β → γ → δ → ε → ζ) : List α → List β → List γ → List δ → List ε → List ζ
Full source 
/-- Quinary version of `list.zipWith`. -/
def zipWith5 (f : α → β → γ → δ → ε → ζ) : List α → List β → List γ → List δ → List ε → List ζ
  | x :: xs, y :: ys, z :: zs, u :: us, v :: vs => f x y z u v :: zipWith5 f xs ys zs us vs
  | _, _, _, _, _ => []
Zipping five lists with a five-argument function
Informal description
The function `List.zipWith5` takes a function $f$ of five arguments and five lists, and returns a list where each element is the result of applying $f$ to the corresponding elements of the input lists. If the input lists have different lengths, the result list has the length of the shortest input list. More precisely, given a function $f : \alpha \times \beta \times \gamma \times \delta \times \epsilon \to \zeta$ and lists $xs : \text{List } \alpha$, $ys : \text{List } \beta$, $zs : \text{List } \gamma$, $us : \text{List } \delta$, and $vs : \text{List } \epsilon$, the function returns a list $[\ f\ x_1\ y_1\ z_1\ u_1\ v_1,\ \ldots,\ f\ x_n\ y_n\ z_n\ u_n\ v_n\ ]$ where $n$ is the minimum length of the input lists. If any input list is empty, the result is the empty list.
List.replaceIf definition
: List α → List Bool → List α → List α
Full source 
/-- 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`. -/
def replaceIf : List α → List Bool → List α → List α
  | l, _, [] => l
  | [], _, _ => []
  | l, [], _ => l
  | n :: ns, tf :: bs, e@(c :: cs) => if tf then c :: ns.replaceIf bs cs else n :: ns.replaceIf bs e
Conditional list replacement
Informal description
Given an initial list `old`, a list of booleans, and a replacement list `new`, the function `replaceIf` processes the elements of `old` sequentially. For each element in `old`, if the corresponding boolean in the boolean list is `true`, it replaces the element with the next element from `new`; otherwise, it keeps the original element. The function continues this process until one of the lists is exhausted. More formally, for lists `old = [x₁, x₂, ..., xₙ]`, `bools = [b₁, b₂, ..., bₘ]`, and `new = [y₁, y₂, ..., yₖ]`, the result is a list where each element `xᵢ` is replaced by `yⱼ` (where `j` is the current position in `new`) if `bᵢ` is `true`, and remains `xᵢ` otherwise, proceeding until any of the lists `old`, `bools`, or `new` is fully processed.
List.iterate definition
(f : α → α) (a : α) : (n : ℕ) → List α
Full source 
/-- `iterate f a n` is `[a, f a, ..., f^[n - 1] a]`. -/
@[simp]
def iterate (f : α → α) (a : α) : (n : ℕ) → List α
  | 0     => []
  | n + 1 => a :: iterate f (f a) n
Iterated application of a function
Informal description
Given a function \( f : \alpha \to \alpha \), an initial value \( a \in \alpha \), and a natural number \( n \), the list `iterate f a n` is defined as \([a, f(a), f^2(a), \dots, f^{n-1}(a)]\), where \( f^k \) denotes the \( k \)-fold composition of \( f \).
List.iterateTR definition
(f : α → α) (a : α) (n : ℕ) : List α
Full source 
/-- Tail-recursive version of `List.iterate`. -/
@[inline]
def iterateTR (f : α → α) (a : α) (n : ℕ) : List α :=
  loop a n []
where
  /-- `iterateTR.loop f a n l := iterate f a n ++ reverse l`. -/
  @[simp, specialize]
  loop (a : α) (n : ℕ) (l : List α) : List α :=
    match n with
    | 0     => reverse l
    | n + 1 => loop (f a) n (a :: l)
Tail-recursive iterated function application on lists
Informal description
The tail-recursive version of the `List.iterate` function. Given a function \( f : \alpha \to \alpha \), an initial value \( a \in \alpha \), and a natural number \( n \), it returns the list \([a, f(a), f^2(a), \dots, f^{n-1}(a)]\) computed in a tail-recursive manner. The auxiliary function `loop` maintains an accumulator list \( l \) and computes the result as the reverse of \( l \) concatenated with the iterated values, ensuring tail-recursion optimization.
List.iterateTR_loop_eq theorem
(f : α → α) (a : α) (n : ℕ) (l : List α) : iterateTR.loop f a n l = reverse l ++ iterate f a n
Full source 
theorem iterateTR_loop_eq (f : α → α) (a : α) (n : ℕ) (l : List α) :
    iterateTR.loop f a n l = reverse l ++ iterate f a n := by
  induction n generalizing a l <;> simp [*]
Equality between tail-recursive loop and reversed list concatenation with iteration
Informal description
For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, natural number $n$, and list $l$ of elements of type $\alpha$, the tail-recursive loop `iterateTR.loop f a n l` produces the same result as concatenating the reverse of $l$ with the list obtained by iterating $f$ $n$ times starting from $a$, i.e., $\text{reverse}(l) +\!\!+ \text{iterate}(f, a, n)$.
List.iterate_eq_iterateTR theorem
: @iterate = @iterateTR
Full source 
@[csimp]
theorem iterate_eq_iterateTR : @iterate = @iterateTR := by
  funext α f a n
  exact Eq.symm <| iterateTR_loop_eq f a n []
Equality of Iterated Function Application and Its Tail-Recursive Version
Informal description
The function `List.iterate` is equal to its tail-recursive counterpart `List.iterateTR`. That is, for any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural number $n$, the list $[a, f(a), f^2(a), \dots, f^{n-1}(a)]$ produced by `iterate` is identical to the list produced by `iterateTR`.
List.mapAccumr definition
(f : α → γ → γ × β) : List α → γ → γ × List β
Full source 
/-- Runs a function over a list returning the intermediate results and a final result. -/
def mapAccumr (f : α → γ → γ × β) : List α → γ → γ × List β
  | [], c => (c, [])
  | y :: yr, c =>
    let r := mapAccumr f yr c
    let z := f y r.1
    (z.1, z.2 :: r.2)
Right-folded map with accumulator
Informal description
Given a function \( f : \alpha \to \gamma \to \gamma \times \beta \) and a list \( L \) of elements of type \( \alpha \), the function `mapAccumr` processes the list from right to left. For each element \( y \) in \( L \), it applies \( f \) to \( y \) and the current accumulator value (initially \( c \)), updating the accumulator and collecting the results into a new list. The final result is a pair consisting of the last accumulator value and the list of results. More precisely, for an empty list, the result is \( (c, []) \). For a non-empty list \( y :: yr \), it recursively processes \( yr \) with the initial accumulator \( c \), then applies \( f \) to \( y \) and the resulting accumulator from the recursive call, producing a new accumulator and a result. The final result is the new accumulator paired with the result of \( f \) prepended to the list of results from the recursive call.
List.length_mapAccumr theorem
: ∀ (f : α → γ → γ × β) (x : List α) (s : γ), length (mapAccumr f x s).2 = length x
Full source 
/-- Length of the list obtained by `mapAccumr`. -/
@[simp]
theorem length_mapAccumr :
    ∀ (f : α → γ → γ × β) (x : List α) (s : γ), length (mapAccumr f x s).2 = length x
  | f, _ :: x, s => congr_arg succ (length_mapAccumr f x s)
  | _, [], _ => rfl
Length Preservation in Right-Folded Map with Accumulator
Informal description
For any function $f : \alpha \to \gamma \to \gamma \times \beta$, any list $x$ of elements of type $\alpha$, and any initial accumulator value $s : \gamma$, the length of the resulting list from `mapAccumr f x s` is equal to the length of the input list $x$. In other words, $\text{length}\big((\text{mapAccumr}\, f\, x\, s).2\big) = \text{length}\, x$.
List.mapAccumr₂ definition
(f : α → β → γ → γ × δ) : List α → List β → γ → γ × List δ
Full source 
/-- Runs a function over two lists returning the intermediate results and a final result. -/
def mapAccumr₂ (f : α → β → γ → γ × δ) : List α → List β → γ → γ × List δ
  | [], _, c => (c, [])
  | _, [], c => (c, [])
  | x :: xr, y :: yr, c =>
    let r := mapAccumr₂ f xr yr c
    let q := f x y r.1
    (q.1, q.2 :: r.2)
Right-accumulating map over two lists
Informal description
Given a function \( f : \alpha \to \beta \to \gamma \to \gamma \times \delta \), two lists \( x : \text{List } \alpha \) and \( y : \text{List } \beta \), and an initial accumulator value \( c : \gamma \), the function `List.mapAccumr₂` processes the lists from right to left, applying \( f \) to each pair of elements and the current accumulator value. It returns a pair consisting of the final accumulator value and a list of the results of \( f \). If either list is empty, it returns the accumulator and an empty list.
List.length_mapAccumr₂ theorem
: ∀ (f : α → β → γ → γ × δ) (x y c), length (mapAccumr₂ f x y c).2 = min (length x) (length y)
Full source 
/-- Length of a list obtained using `mapAccumr₂`. -/
@[simp]
theorem length_mapAccumr₂ :
    ∀ (f : α → β → γ → γ × δ) (x y c), length (mapAccumr₂ f x y c).2 = min (length x) (length y)
  | f, _ :: x, _ :: y, c =>
    calc
      succ (length (mapAccumr₂ f x y c).2) = succ (min (length x) (length y)) :=
        congr_arg succ (length_mapAccumr₂ f x y c)
      _ = min (succ (length x)) (succ (length y)) := Eq.symm (succ_min_succ (length x) (length y))
  | _, _ :: _, [], _ => rfl
  | _, [], _ :: _, _ => rfl
  | _, [], [], _ => rfl
Length of Result List in Right-Accumulating Map over Two Lists Equals Minimum Length
Informal description
For any function $f : \alpha \to \beta \to \gamma \to \gamma \times \delta$, lists $x : \text{List } \alpha$ and $y : \text{List } \beta$, and initial accumulator value $c : \gamma$, the length of the resulting list from $\text{mapAccumr₂}\ f\ x\ y\ c$ is equal to the minimum of the lengths of $x$ and $y$. That is, \[ \text{length}\ (\text{mapAccumr₂}\ f\ x\ y\ c).2 = \min(\text{length}\ x, \text{length}\ y). \]