doc-next-gen

Init.Data.List.Control

Module docstring

{"Remark: we can define mapM, mapM₂ and forM using Applicative instead of Monad. Example: def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β) | [] => pure [] | a::as => List.cons <$> (f a) <*> mapM as

However, we consider f <$> a <*> b an anti-idiom because the generated code may produce unnecessary closure allocations. Suppose m is a Monad, and it uses the default implementation for Applicative.seq. Then, the compiler expands f <$> a <*> b <*> c into something equivalent to (Functor.map f a >>= fun g_1 => Functor.map g_1 b) >>= fun g_2 => Functor.map g_2 c In an ideal world, the compiler may eliminate the temporary closures g_1 and g_2 after it inlines Functor.map and Monad.bind. However, this can easily fail. For example, suppose Functor.map f a >>= fun g_1 => Functor.map g_1 b expanded into a match-expression. This is not unreasonable and can happen in many different ways, e.g., we are using a monad that may throw exceptions. Then, the compiler has to decide whether it will create a join-point for the continuation of the match or float it. If the compiler decides to float, then it will be able to eliminate the closures, but it may not be feasible since floating match expressions may produce exponential blowup in the code size.

Finally, we rarely use mapM with something that is not a Monad.

Users that want to use mapM with Applicative should use mapA instead. "}

List.mapM definition
{m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)
Full source 
/--
Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of
results.

This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be
more convenient to reason about. `List.forM` is the variant that discards the results and
`List.mapA` is the variant that works with `Applicative`.
-/
@[inline]
def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β) :=
  let rec @[specialize] loop
    | [],      bs => pure bs.reverse
    | a :: as, bs => do loop as ((← f a)::bs)
  loop as []
Monadic map over a list (tail-recursive)
Informal description
Given a monad `m`, a function `f : α → m β`, and a list `as : List α`, the function `List.mapM` applies `f` to each element of `as` from left to right, collecting the results in a list wrapped in the monadic context `m`. The implementation is tail-recursive, ensuring stack safety for long lists. More formally, for an empty list `[]`, it returns `pure []`. For a non-empty list `a::as`, it applies `f` to the head `a`, then recursively applies `mapM` to the tail `as`, accumulating the results in reverse order and finally reversing them to maintain the original order.
List.mapA definition
{m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
Full source 
/--
Applies the applicative action `f` on every element in the list, left-to-right, and returns the list
of results.

If `m` is also a `Monad`, then using `mapM` can be more efficient.

See `List.forA` for the variant that discards the results. See `List.mapM` for the variant that
works with `Monad`.

This function is not tail-recursive, so it may fail with a stack overflow on long lists.
-/
@[specialize]
def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
  | []    => pure []
  | a::as => List.cons <$> f a <*> mapA f as
Applicative map over a list
Informal description
Given an applicative functor `m`, a function `f : α → m β`, and a list `as : List α`, the function `List.mapA` applies `f` to each element of `as` from left to right, collecting the results in a list wrapped in the applicative context `m`. More formally, for an empty list `[]`, it returns `pure []`. For a non-empty list `a::as`, it applies `f` to the head `a`, then recursively applies `mapA` to the tail `as`, and combines the results using the applicative operations `<$>` (map) and `<*>` (sequential application). Note that this function is not tail-recursive, so it may fail with a stack overflow on long lists.
List.forM definition
{m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit
Full source 
/--
Applies the monadic action `f` to every element in the list, in order.

`List.mapM` is a variant that collects results. `List.forA` is a variant that works on any
`Applicative`.
-/
@[specialize]
protected def forM {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit :=
  match as with
  | []      => pure ⟨⟩
  | a :: as => do f a; List.forM as f
Monadic iteration over a list with side effects
Informal description
Given a monad `m`, a list `as` of elements of type `α`, and a monadic action `f` that takes an element of `α` and returns a monadic computation in `m` producing a unit value, `List.forM` sequentially applies `f` to each element of `as` in order, discarding the results and returning a monadic computation that produces a unit value when all actions are complete.
List.forA definition
{m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit
Full source 
/--
Applies the applicative action `f` to every element in the list, in order.

If `m` is also a `Monad`, then using `List.forM` can be more efficient.

`List.mapA` is a variant that collects results.
-/
@[specialize]
def forA {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit :=
  match as with
  | []      => pure ⟨⟩
  | a :: as => f a *> forA as f
Applicative sequential iteration over a list
Informal description
Given an applicative functor `m`, a list `as` of elements of type `α`, and a function `f : α → m PUnit`, the function `List.forA` applies `f` to each element of `as` in sequence, discarding the results and returning a computation in `m` that produces the unit value. This is the applicative version of `List.forM`, which is more efficient when `m` is also a monad.
List.filterAuxM definition
{m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → List α → m (List α)
Full source 
@[specialize]
def filterAuxM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → List α → m (List α)
  | [],     acc => pure acc
  | h :: t, acc => do
    let b ← f h
    filterAuxM f t (cond b (h :: acc) acc)
Monadic auxiliary list filter
Informal description
Given a monadic predicate `f : α → m Bool` and two lists `t` and `acc` of type `List α`, the function `filterAuxM` recursively processes the list `t`, applying `f` to each element. If the result of `f h` is `true`, the element `h` is prepended to the accumulator list `acc`; otherwise, `acc` remains unchanged. The function returns the filtered list in the monadic context `m`.
List.filterM definition
{m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)
Full source 
/--
Applies the monadic predicate `p` to every element in the list, in order from left to right, and
returns the list of elements for which `p` returns `true`.

`O(|l|)`.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7
```
```output
[1, 2, 2]
```
-/
@[inline]
def filterM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α) := do
  let as ← filterAuxM p as []
  pure as.reverse
Monadic list filter
Informal description
Given a monadic predicate `p : α → m Bool` and a list `as : List α`, the function `List.filterM` applies `p` to each element of `as` in order, collecting the elements for which `p` returns `true` into a new list. The resulting list is returned within the monadic context `m`. The operation has time complexity `O(|as|)`.
List.filterRevM definition
{m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)
Full source 
/--
Applies the monadic predicate `p` on every element in the list in reverse order, from right to left,
and returns those elements for which `p` returns `true`. The elements of the returned list are in
the same order as in the input list.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterRevM fun x => do
  IO.println s!"Checking {x}"
  return x < 3
```
```output
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1
```
```output
[1, 2, 2]
```
-/
@[inline]
def filterRevM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α) :=
  filterAuxM p as.reverse []
Reverse-order monadic list filter
Informal description
Given a monadic predicate `p : α → m Bool` and a list `as : List α`, the function `filterRevM` applies `p` to each element of `as` in reverse order (from right to left) and returns a list of elements for which `p` returns `true`. The order of elements in the resulting list matches their original order in `as`.
List.filterMapM definition
{m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β)
Full source 
/--
Applies a monadic function that returns an `Option` to each element of a list, collecting the
non-`none` values.

`O(|l|)`.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterMapM fun x => do
  IO.println s!"Examining {x}"
  if x > 2 then return some (2 * x)
  else return none
```
```output
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7
```
```output
[10, 14, 14]
```
-/
@[inline]
def filterMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β) :=
  let rec @[specialize] loop
    | [],     bs => pure bs.reverse
    | a :: as, bs => do
      match (← f a) with
      | none   => loop as bs
      | some b => loop as (b::bs)
  loop as []
Monadic filter and map over a list with optional results
Informal description
Given a monad `m`, a function `f : α → m (Option β)`, and a list `as : List α`, the function `List.filterMapM` applies `f` to each element of `as` in sequence, collecting all results of the form `some b` into a list. The resulting list is returned in the same order as the original elements, and the computation is performed within the monadic context `m`. The time complexity is linear in the length of the input list.
List.flatMapM definition
{m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)
Full source 
/--
Applies a monadic function that returns a list to each element of a list, from left to right, and
concatenates the resulting lists.
-/
@[inline]
def flatMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β) :=
  let rec @[specialize] loop
    | [],     bs => pure bs.reverse.flatten
    | a :: as, bs => do
      let bs' ← f a
      loop as (bs' :: bs)
  loop as []
Monadic flat map over a list
Informal description
Given a monad `m`, a function `f : α → m (List β)`, and a list `as : List α`, the function `List.flatMapM` applies `f` to each element of `as` from left to right, resulting in a list of lists in the monadic context, and then concatenates these lists into a single list. The concatenation is performed efficiently by reversing the intermediate results before flattening. More formally, for each element `a` in `as`, `f a` produces a monadic computation that yields a list `bs' : List β`. These lists are collected in reverse order and then concatenated (flattened) to produce the final result in the monad `m`.
List.foldlM definition
{m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s → α → m s) → (init : s) → List α → m s
Full source 
/--
Folds a monadic function over a list from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in order, using `f`.

Example:
```lean example
example [Monad m] (f : α → β → m α) :
    List.foldlM (m := m) f x₀ [a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure x₃)
  := by rfl
```
-/
@[specialize]
def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s → α → m s) → (init : s) → List α → m s
  | _, s, []      => pure s
  | f, s, a :: as => do
    let s' ← f s a
    List.foldlM f s' as
Monadic left-fold over a list
Informal description
Given a monad `m`, a function `f : s → α → m s`, an initial value `init : s`, and a list `as : List α`, the function `List.foldlM` performs a left-fold over the list using the monadic function `f`. It starts with the initial value `init` and sequentially applies `f` to each element of the list, threading the state through the monadic context. The result is a monadic computation producing the final state after processing all elements of the list. For example, folding over the list `[a, b, c]` with initial state `x₀` is equivalent to the monadic computation: ```lean do let x₁ ← f x₀ a let x₂ ← f x₁ b let x₃ ← f x₂ c pure x₃ ```
List.foldlM_nil theorem
[Monad m] {f : β → α → m β} {b : β} : [].foldlM f b = pure b
Full source 
@[simp] theorem foldlM_nil [Monad m] {f : β → α → m β} {b : β} : [].foldlM f b = pure b := rfl
Monadic left-fold over empty list yields initial state
Informal description
For any monad `m` and any function `f : β → α → m β`, the monadic left-fold over an empty list `[]` with initial state `b : β` is equal to `pure b`.
List.foldlM_cons theorem
[Monad m] {f : β → α → m β} {b : β} {a : α} {l : List α} : (a :: l).foldlM f b = f b a >>= l.foldlM f
Full source 
@[simp] theorem foldlM_cons [Monad m] {f : β → α → m β} {b : β} {a : α} {l : List α} :
    (a :: l).foldlM f b = f b a >>= l.foldlM f := by
  simp [List.foldlM]
Monadic left-fold recursion for non-empty lists
Informal description
For any monad `m`, function `f : β → α → m β`, initial state `b : β`, element `a : α`, and list `l : List α`, the monadic left-fold of the list `a :: l` with initial state `b` is equal to first applying `f` to `b` and `a`, then binding the result to continue folding over the remaining list `l` with `f`. In symbols: $$\text{foldlM}_m\, f\, b\, (a :: l) = f\, b\, a \gg= \text{foldlM}_m\, f\, \cdot\, l$$
List.foldrM definition
{m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s
Full source 
/--
Folds a monadic 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`.

Example:
```lean example
example [Monad m] (f : α → β → m β) :
  List.foldrM (m := m) f x₀ [a, b, c] = (do
    let x₁ ← f c x₀
    let x₂ ← f b x₁
    let x₃ ← f a x₂
    pure x₃)
  := by rfl
```
-/
@[inline]
def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s :=
  l.reverse.foldlM (fun s a => f a s) init
Monadic right-fold over a list
Informal description
Given a monad `m`, a function `f : α → s → m s`, an initial value `init : s`, and a list `l : List α`, the function `List.foldrM` performs a right-fold over the list using the monadic function `f`. It processes the list in reverse order, starting with the initial value `init` and sequentially applying `f` to each element of the list, threading the state through the monadic context. The result is a monadic computation producing the final state after processing all elements of the list. For example, folding over the list `[a, b, c]` with initial state `x₀` is equivalent to the monadic computation: ```lean do let x₁ ← f a x₀ let x₂ ← f b x₁ let x₃ ← f c x₂ pure x₃ ```
List.foldrM_nil theorem
[Monad m] {f : α → β → m β} {b : β} : [].foldrM f b = pure b
Full source 
@[simp] theorem foldrM_nil [Monad m] {f : α → β → m β} {b : β} : [].foldrM f b = pure b := rfl
Monadic right-fold of empty list yields pure initial state
Informal description
For any monad `m`, function `f : α → β → m β`, and initial state `b : β`, the monadic right-fold of the empty list `[]` with `f` and `b` is equal to the pure monadic value `pure b`.
List.firstM definition
{m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
Full source 
/--
Maps `f` over the list and collects the results with `<|>`. The result for the end of the list is
`failure`.

Examples:
 * `[[], [1, 2], [], [2]].firstM List.head? = some 1`
 * `[[], [], []].firstM List.head? = none`
 * `[].firstM List.head? = none`
-/
@[specialize]
def firstM {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β
  | []    => failure
  | a::as => f a <|> firstM f as
First successful monadic result in a list
Informal description
Given a monad `m` with an `Alternative` instance, a function `f : α → m β`, and a list `l : List α`, the function `List.firstM` applies `f` to each element of `l` in order and returns the first successful result (i.e., the first non-failure) using the `<|>` (alternative choice) operator. If all applications of `f` result in failure or the list is empty, it returns `failure`.
List.anyM definition
{m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) : (l : List α) → m Bool
Full source 
/--
Returns true if the monadic predicate `p` returns `true` for any element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `true`. The elements in `l` are examined in
order from left to right.
-/
@[specialize]
def anyM {m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) : (l : List α) → m Bool
  | []    => pure false
  | a::as => do
    match (← p a) with
    | true  => pure true
    | false => anyM p as
Monadic existential quantification over a list
Informal description
Given a monadic predicate `p : α → m Bool` and a list `l : List α`, the function `List.anyM` returns `true` in the monad `m` if `p` evaluates to `true` for any element in `l`. The evaluation is performed in order from left to right and short-circuits upon encountering the first `true`.
List.allM definition
{m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) : (l : List α) → m Bool
Full source 
/--
Returns true if the monadic predicate `p` returns `true` for every element of `l`.

`O(|l|)`. Short-circuits upon encountering the first `false`. The elements in `l` are examined in
order from left to right.
-/
@[specialize]
def allM {m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) : (l : List α) → m Bool
  | []    => pure true
  | a::as => do
    match (← p a) with
    | true  => allM p as
    | false => pure false
Monadic universal quantification over a list
Informal description
Given a monadic predicate `p` and a list `l`, the function `allM` returns `true` if `p` evaluates to `true` for every element in `l`. The evaluation is performed in order from left to right and short-circuits upon encountering the first `false`. The time complexity is linear in the length of the list.
List.findM? definition
{m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : List α → m (Option α)
Full source 
/--
Returns the first element of the list for which the monadic predicate `p` returns `true`, or `none`
if no such element is found. Elements of the list are checked in order.

`O(|l|)`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
-/
@[specialize]
def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : List α → m (Option α)
  | []    => pure none
  | a::as => do
    match (← p a) with
    | true  => pure (some a)
    | false => findM? p as
Monadic find first in list
Informal description
Given a monadic predicate `p : α → m Bool` and a list `as : List α`, the function `List.findM?` returns the first element `a` in `as` for which `p a` evaluates to `true` in the monad `m`, wrapped in `some`. If no such element exists, it returns `none`. The elements are checked in order, and the operation has time complexity $O(|as|)$.
List.findM?_pure theorem
{m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) : findM? (m := m) (pure <| p ·) as = pure (as.find? p)
Full source 
@[simp]
theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
    findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
  induction as with
  | nil => rfl
  | cons a as ih =>
    simp only [findM?, find?]
    cases p a with
    | true  => simp
    | false => simp [ih]
Monadic Find with Pure Predicate Equals Pure of Non-Monadic Find
Informal description
For any monad $m$ that is a lawful monad, any predicate $p : \alpha \to \text{Bool}$, and any list $as : \text{List } \alpha$, the monadic find operation `findM?` with the predicate `pure ∘ p` applied to $as$ is equal to the pure monad applied to the result of the non-monadic find operation `as.find? p`. That is, $\text{findM?} (\text{pure} \circ p) as = \text{pure} (as.\text{find?} p)$.
List.findM?_id theorem
(p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p
Full source 
@[simp]
theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
  findM?_pure _ _
Monadic Find with Identity Monad Equals Non-Monadic Find
Informal description
For any predicate $p : \alpha \to \text{Bool}$ and any list $as : \text{List } \alpha$, the monadic find operation `findM?` with the identity monad `Id` applied to $p$ and $as$ is equal to the non-monadic find operation `as.find? p$. That is, $\text{findM?}_{Id} p as = as.\text{find?} p$.
List.findSomeM? definition
{m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
Full source 
/--
Returns the first non-`none` result of applying the monadic function `f` to each element of the
list, in order. Returns `none` if `f` returns `none` for all elements.

`O(|l|)`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
-/
@[specialize]
def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
  | []    => pure none
  | a::as => do
    match (← f a) with
    | some b => pure (some b)
    | none   => findSomeM? f as
First non-`none` result of a monadic function over a list
Informal description
Given a monadic function \( f : \alpha \to m (\text{Option } \beta) \) and a list \( \text{as} : \text{List } \alpha \), the function `findSomeM?` applies \( f \) to each element of `as` in order until it finds the first element for which \( f \) returns `some b`. It then returns `some b` in the monadic context \( m \). If no such element is found, it returns `none` in \( m \). The operation has time complexity \( O(|\text{as}|) \).
List.findSomeM?_pure theorem
[Monad m] [LawfulMonad m] {f : α → Option β} {as : List α} : findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f)
Full source 
@[simp]
theorem findSomeM?_pure [Monad m] [LawfulMonad m] {f : α → Option β} {as : List α} :
    findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f) := by
  induction as with
  | nil => rfl
  | cons a as ih =>
    simp only [findSomeM?, findSome?]
    cases f a with
    | some b => simp
    | none   => simp [ih]
Equivalence of `findSomeM?` with Pure Function and `findSome?` under Pure Monad
Informal description
For any monad `m` that is a lawful monad, any function `f : α → Option β`, and any list `as : List α`, the monadic operation `findSomeM?` applied to the pure function `f` and the list `as` is equal to the pure monadic value of the non-monadic operation `findSome?` applied to `f` and `as`. That is, \[ \text{findSomeM? } (\text{pure} \circ f) \text{ as} = \text{pure } (\text{as.findSome? } f). \]
List.findSomeM?_id theorem
{f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f
Full source 
@[simp]
theorem findSomeM?_id {f : α → Option β} {as : List α} : findSomeM? (m := Id) f as = as.findSome? f :=
  findSomeM?_pure
Equivalence of `findSomeM?` and `findSome?` in the Identity Monad
Informal description
For any function $f : \alpha \to \text{Option } \beta$ and any list $\text{as} : \text{List } \alpha$, the monadic operation $\text{findSomeM?}$ in the identity monad $\text{Id}$ applied to $f$ and $\text{as}$ is equal to the non-monadic operation $\text{as.findSome? } f$. That is, \[ \text{findSomeM? } f \text{ as} = \text{as.findSome? } f. \]
List.findM?_eq_findSomeM? theorem
[Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} : as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none
Full source 
theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :
    as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by
  induction as with
  | nil => rfl
  | cons a as ih =>
    simp only [findM?, findSomeM?]
    simp [ih]
    congr
    apply funext
    intro b
    cases b <;> simp
Equivalence of Monadic Find Operations: `findM?` and `findSomeM?`
Informal description
For any monad `m` that is a lawful monad, any monadic predicate `p : α → m Bool`, and any list `as : List α`, the monadic operation `findM?` is equivalent to applying `findSomeM?` to a function that returns `some a` if `p a` evaluates to `true` and `none` otherwise. That is, \[ \text{as.findM? } p = \text{as.findSomeM? } \left( \lambda a \Rightarrow \text{if } (p a) \text{ then } \text{some } a \text{ else } \text{none} \right). \]
List.forIn' definition
{α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β
Full source 
@[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
    | [], b, _    => pure b
    | a::as', b, h => do
      have : a ∈ as := by
        clear f
        have ⟨bs, h⟩ := h
        subst h
        exact mem_append_right _ (Mem.head ..)
      match (← f a this b) with
      | ForInStep.done b  => pure b
      | ForInStep.yield b =>
        have : Exists (fun bs => bs ++ as' = as) := have ⟨bs, h⟩ := h; ⟨bs ++ [a], by rw [← h, append_cons (bs := as')]⟩
        loop as' b this
  loop as init ⟨[], rfl⟩
Monadic iteration over a list with membership proof
Informal description
The function `List.forIn'` is a monadic iteration over a list `as` of type `List α`, starting with an initial state `init` of type `β`. For each element `a` in the list `as`, it applies a function `f` that takes the element `a`, a proof that `a` is in `as`, and the current state `β`, and returns a monadic action producing a `ForInStep β`. The iteration continues until all elements are processed or until `f` returns a `ForInStep.done` value, which terminates the iteration early. The function `f` must preserve the invariant that the element being processed is indeed in the original list `as`. The implementation uses a helper function `loop` that recursively processes the list, maintaining the invariant that the remaining list `as'` is a suffix of the original list `as`. For each element `a`, it first proves that `a` is in the original list `as`, then applies `f` to `a` and the current state. If `f` returns `ForInStep.done`, the loop terminates with the current state. If `f` returns `ForInStep.yield`, the loop continues with the updated state and the remaining elements of the list.
List.instForIn'InferInstanceMembership instance
: ForIn' m (List α) α inferInstance
Full source 
instance : ForIn' m (List α) α inferInstance where
  forIn' := List.forIn'
Monadic Iteration with Membership Proofs for Lists
Informal description
For any monad `m` and type `α`, the type `List α` has a `ForIn'` instance that enables monadic iteration over lists with membership proofs. This allows the use of `for h : x in xs` notation in `do`-blocks, where `h` provides a proof that `x` is an element of `xs`.
List.forIn'_eq_forIn' theorem
[Monad m] : @List.forIn' α β m _ = forIn'
Full source 
@[simp] theorem forIn'_eq_forIn' [Monad m] : @List.forIn' α β m _ = forIn' := rfl
Equality of List-Specialized and Generic Monadic Iteration Functions
Informal description
For any monad `m`, the function `List.forIn'` is equal to the function `forIn'` when specialized to lists.
List.forIn'_nil theorem
[Monad m] {f : (a : α) → a ∈ [] → β → m (ForInStep β)} {b : β} : forIn' [] b f = pure b
Full source 
@[simp] theorem forIn'_nil [Monad m] {f : (a : α) → a ∈ [] → β → m (ForInStep β)} {b : β} : forIn' [] b f = pure b :=
  rfl
Monadic Iteration over Empty List Yields Initial State
Informal description
For any monad `m`, any type `α`, and any function `f` that takes an element `a` of type `α` with a proof that `a` is in the empty list `[]`, a state `b` of type `β`, and returns a monadic action producing a `ForInStep β`, the monadic iteration over the empty list with initial state `b` and function `f` is equivalent to returning `b` in the monadic context. That is, `forIn' [] b f = pure b`.
List.forIn_nil theorem
[Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b
Full source 
@[simp] theorem forIn_nil [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b :=
  rfl
Monadic Iteration over Empty List Yields Initial State
Informal description
For any monad `m`, any function `f : α → β → m (ForInStep β)`, and any initial state `b : β`, the monadic iteration over an empty list `[]` with initial state `b` and step function `f` is equal to `pure b`.
List.instForM instance
: ForM m (List α) α
Full source 
instance : ForM m (List α) α where
  forM := List.forM
Monadic Iteration over Lists
Informal description
For any monad `m`, the type `List α` is equipped with a `ForM` instance, allowing monadic iteration over lists of elements of type `α`.
List.forM_eq_forM theorem
[Monad m] : @List.forM m _ α = forM
Full source 
@[simp] theorem forM_eq_forM [Monad m] : @List.forM m _ α = forM := rfl
Equality of List.forM and Generic forM
Informal description
For any monad `m`, the function `List.forM` is equal to the generic monadic iteration function `forM` when specialized to lists of type `List α`.
List.forM_nil theorem
[Monad m] {f : α → m PUnit} : forM [] f = pure ⟨⟩
Full source 
@[simp] theorem forM_nil [Monad m] {f : α → m PUnit} : forM [] f = pure ⟨⟩ :=
  rfl
Monadic Iteration over Empty List Yields Trivial Result
Informal description
For any monad `m` and any function `f : α → m PUnit`, applying the monadic iteration `forM` to the empty list `[]` with `f` is equal to the pure computation `pure ⟨⟩`, where `⟨⟩` is the unique element of `PUnit`.
List.forM_cons theorem
[Monad m] {f : α → m PUnit} {a : α} {as : List α} : forM (a :: as) f = f a >>= fun _ => forM as f
Full source 
@[simp] theorem forM_cons [Monad m] {f : α → m PUnit} {a : α} {as : List α} : forM (a::as) f = f a >>= fun _ => forM as f :=
  rfl
Monadic Iteration over Non-empty List
Informal description
For any monad `m`, a function `f : α → m PUnit`, an element `a : α`, and a list `as : List α`, the monadic iteration over the list `a :: as` with `f` is equal to first applying `f` to `a` and then iterating over `as` with `f`, i.e., \[ \text{forM} (a :: as) f = f a \gg \lambda \_. \text{forM} as f. \]
List.instFunctor instance
: Functor List
Full source 
instance : Functor List where
  map := List.map
List as a Functor
Informal description
The type constructor `List` is a functor, meaning it can be mapped over using the `<$>` operation that applies a function to each element of the list while preserving the list structure.