Init.Data.List.Monadic

List.mapM' definition

[Monad m] (f : α → m β) : List α → m (List β)

Full source

/--
Applies the monadic action `f` on every element in the list, left-to-right, and returns the list of
results.

This is a non-tail-recursive variant of `List.mapM` that's easier to reason about. It cannot be used
as the main definition and replaced by the tail-recursive version because they can only be proved
equal when `m` is a `LawfulMonad`.
-/
def mapM' [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | a :: l => return (← f a) :: (← l.mapM' f)

Left-to-right monadic map over a list (non-tail-recursive)

Informal description

Given a monad `m`, a function `f : α → m β`, and a list `l : List α`, the function `List.mapM'` applies `f` to each element of `l` from left to right, collecting the results in a monadic context, and returns the list of results. More precisely: - For the empty list `[]`, it returns `pure []`. - For a list `a :: l`, it applies `f` to `a`, then recursively applies `mapM'` to `l`, and combines the results as `(f a) :: (mapM' f l)` in the monadic context. This is a non-tail-recursive variant of `List.mapM` that is easier to reason about but cannot be used as the main definition due to its non-tail-recursive nature.

List.mapM'_nil theorem

[Monad m] {f : α → m β} : mapM' f [] = pure []

Full source

@[simp] theorem mapM'_nil [Monad m] {f : α → m β} : mapM' f [] = pure [] := rfl

Monadic Map of Empty List Yields Pure Empty List

Informal description

For any monad `m` and function `f : α → m β`, applying the monadic map operation `mapM'` to the empty list `[]` yields the monadic value `pure []`.

List.mapM'_cons theorem

[Monad m] {f : α → m β} : mapM' f (a :: l) = return ((← f a) :: (← l.mapM' f))

Full source

@[simp] theorem mapM'_cons [Monad m] {f : α → m β} :
    mapM' f (a :: l) = return ((← f a) :: (← l.mapM' f)) :=
  rfl

Monadic Map of Cons List Yields Cons of Monadic Results

Informal description

For any monad $m$ and function $f : \alpha \to m \beta$, the monadic map operation `mapM'` applied to a non-empty list $a :: l$ satisfies: \[ \text{mapM}'\, f\, (a :: l) = \text{return}\, ((\leftarrow f\, a) :: (\leftarrow l.\text{mapM}'\, f)) \] where $\leftarrow$ denotes monadic binding.

List.mapM'_eq_mapM theorem

[Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : mapM' f l = mapM f l

Full source

theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
    mapM' f l = mapM f l := by simp [go, mapM] where
  go : ∀ l acc, mapM.loop f l acc = return acc.reverse ++ (← mapM' f l)
    | [], acc => by simp [mapM.loop, mapM']
    | a::l, acc => by simp [go l, mapM.loop, mapM']

Equivalence of Non-Tail-Recursive and Standard Monadic Map Operations on Lists

Informal description

For any monad `m` that satisfies the monad laws, any function `f : α → m β`, and any list `l : List α`, the non-tail-recursive monadic map operation `mapM'` is equal to the standard monadic map operation `mapM`, i.e., `mapM' f l = mapM f l`.

List.mapM_nil theorem

[Monad m] {f : α → m β} : [].mapM f = pure []

Full source

@[simp] theorem mapM_nil [Monad m] {f : α → m β} : [].mapM f = pure [] := rfl

Monadic Map of Empty List Yields Pure Empty List

Informal description

For any monad `m` and any function `f : α → m β`, applying the monadic map operation `mapM` to the empty list `[]` with function `f` yields the pure empty list `pure []`.

List.mapM_cons theorem

[Monad m] [LawfulMonad m] {f : α → m β} : (a :: l).mapM f = (return (← f a) :: (← l.mapM f))

Full source

@[simp] theorem mapM_cons [Monad m] [LawfulMonad m] {f : α → m β} :
    (a :: l).mapM f = (return (← f a) :: (← l.mapM f)) := by simp [← mapM'_eq_mapM, mapM']

Monadic Map Decomposition for Non-Empty Lists

Informal description

For any monad `m` that satisfies the monad laws, and any function `f : α → m β`, the monadic map operation on a non-empty list `a :: l` is equal to the monadic operation that first applies `f` to `a`, then recursively applies `mapM f` to `l`, and combines the results as `(f a) :: (mapM f l)` in the monadic context.

List.mapM_pure theorem

[Monad m] [LawfulMonad m] {l : List α} {f : α → β} : l.mapM (m := m) (pure <| f ·) = pure (l.map f)

Full source

@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] {l : List α} {f : α → β} :
    l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
  induction l <;> simp_all

Monadic Map of Pure Function Equals Pure of Map: `mapM (pure ∘ f) = pure (map f)`

Informal description

For any monad `m` that satisfies the monad laws, any list `l : List α`, and any function `f : α → β`, the monadic map operation `mapM` applied to `l` with the pure function `pure ∘ f` is equal to the pure list obtained by applying `f` to each element of `l`, i.e., `l.mapM (pure ∘ f) = pure (l.map f)`.

List.mapM_id theorem

{l : List α} {f : α → Id β} : l.mapM f = l.map f

Full source

@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
  mapM_pure

Monadic Map Equals Standard Map in Identity Monad: $\text{mapM}_f(l) = \text{map}_f(l)$ in `Id`

Informal description

For any list $l$ of elements of type $\alpha$ and any function $f : \alpha \to \beta$, the monadic map operation `mapM` applied to $l$ with $f$ in the identity monad `Id` is equal to the standard map operation `map` applied to $l$ with $f$, i.e., $l.\text{mapM}\ f = l.\text{map}\ f$.

List.mapM_append theorem

 [Monad m] [LawfulMonad m] {f : α → m β} {l₁ l₂ : List α} : (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f))

Full source

@[simp] theorem mapM_append [Monad m] [LawfulMonad m] {f : α → m β} {l₁ l₂ : List α} :
    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]

Monadic Map Distributes Over List Concatenation: $\text{mapM}_f(l_1 ++ l_2) = \text{mapM}_f(l_1) ++ \text{mapM}_f(l_2)$ in monad $m$

Informal description

Let $m$ be a monad that satisfies the monad laws, $f : \alpha \to m \beta$ a function, and $l_1, l_2$ lists of elements of type $\alpha$. Then the monadic map operation applied to the concatenated list $l_1 ++ l_2$ is equal to the monadic operation that first applies `mapM f` to $l_1$ and $l_2$ separately, then concatenates the results in the monadic context.

List.foldlM_cons_eq_append theorem

 [Monad m] [LawfulMonad m] {f : α → m β} {as : List α} {b : β} {bs : List β} :
  (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
    (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc)

Full source

/-- Auxiliary lemma for `mapM_eq_reverse_foldlM_cons`. -/
theorem foldlM_cons_eq_append [Monad m] [LawfulMonad m] {f : α → m β} {as : List α} {b : β} {bs : List β} :
    (as.foldlM (init := b :: bs) fun acc a => return ((← f a) :: acc)) =
      (· ++ b :: bs) <$> as.foldlM (init := []) fun acc a => return ((← f a) :: acc) := by
  induction as generalizing b bs with
  | nil => simp
  | cons a as ih =>
    simp only [bind_pure_comp] at ih
    simp [ih, _root_.map_bind, Functor.map_map, Function.comp_def]

Monadic Fold with Cons Initial Value Equals Append Transformation

Informal description

Let $m$ be a monad with lawful monadic operations, $f : \alpha \to m \beta$ a function, $as$ a list of elements of type $\alpha$, and $b, bs$ elements and a list of type $\beta$ respectively. Then the monadic fold of $as$ with initial value $b :: bs$ and accumulator function $\lambda acc\ a, \text{return} (f(a) :: acc)$ is equal to the monadic fold of $as$ with initial value $[]$ and the same accumulator function, followed by appending $b :: bs$ to the result.

List.mapM_eq_reverse_foldlM_cons theorem

 [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
  mapM f l = reverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) [])

Full source

theorem mapM_eq_reverse_foldlM_cons [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
    mapM f l = reversereverse <$> (l.foldlM (fun acc a => return ((← f a) :: acc)) []) := by
  rw [← mapM'_eq_mapM]
  induction l with
  | nil => simp
  | cons a as ih =>
    simp only [mapM'_cons, ih, bind_map_left, foldlM_cons, LawfulMonad.bind_assoc, pure_bind,
      foldlM_cons_eq_append, _root_.map_bind, Functor.map_map, Function.comp_def, reverse_append,
      reverse_cons, reverse_nil, nil_append, singleton_append]
    simp [bind_pure_comp]

Monadic Map as Reverse of Monadic Fold: $\text{mapM}\ f\ l = \text{reverse} \mathbin{\text{\textdollar}} \text{foldlM}\ (\lambda\ \text{acc}\ a,\ \text{return}\ (f(a) :: \text{acc}))\ []\ l$

Informal description

Let $m$ be a monad that satisfies the monad laws, $f : \alpha \to m \beta$ a function, and $l$ a list of elements of type $\alpha$. Then the monadic map operation $\text{mapM}\ f\ l$ is equal to reversing the result of the monadic fold operation that accumulates the results of applying $f$ to each element of $l$ in a list, i.e., \[ \text{mapM}\ f\ l = \text{reverse} \mathbin{\text{\textdollar}} \left(\text{foldlM}\ (\lambda\ \text{acc}\ a,\ \text{return}\ (f(a) :: \text{acc}))\ []\ l\right) \] where $\mathbin{\text{\textdollar}}$ denotes the monadic map operation.

List.filterMapM_nil theorem

[Monad m] {f : α → m (Option β)} : [].filterMapM f = pure []

Full source

@[simp] theorem filterMapM_nil [Monad m] {f : α → m (Option β)} : [].filterMapM f = pure [] := rfl

Empty List Property for `filterMapM`

Informal description

For any monad `m` and function `f : α → m (Option β)`, applying `filterMapM` to the empty list `[]` yields the pure empty list `pure []` in the monad `m`.

List.filterMapM_loop_eq theorem

 [Monad m] [LawfulMonad m] {f : α → m (Option β)} {l : List α} {acc : List β} :
  filterMapM.loop f l acc = (acc.reverse ++ ·) <$> filterMapM.loop f l []

Full source

theorem filterMapM_loop_eq [Monad m] [LawfulMonad m] {f : α → m (Option β)} {l : List α} {acc : List β} :
    filterMapM.loop f l acc = (acc.reverse ++ ·) <$> filterMapM.loop f l [] := by
  induction l generalizing acc with
  | nil => simp [filterMapM.loop]
  | cons a l ih =>
    simp only [filterMapM.loop, _root_.map_bind]
    congr
    funext b?
    split <;> rename_i b
    · apply ih
    · rw [ih, ih (acc := [b])]
      simp

Monadic Filter-Map Loop Equivalence via Reverse Concatenation

Informal description

Let $m$ be a monad satisfying the monad laws, $f : \alpha \to m (\text{Option} \beta)$ a function, $l$ a list of elements of type $\alpha$, and $\text{acc}$ a list of elements of type $\beta$. Then the monadic filter-map loop satisfies: \[ \text{filterMapM.loop}\ f\ l\ \text{acc} = (\text{acc.reverse} \mathbin{+\kern-1.5ex+} \cdot) \mathbin{\text{\textdollar}} \text{filterMapM.loop}\ f\ l\ [] \] where $\mathbin{+\kern-1.5ex+}$ denotes list concatenation and $\mathbin{\text{\textdollar}}$ is the monadic map operation.

List.filterMapM_cons theorem

 [Monad m] [LawfulMonad m] {f : α → m (Option β)} :
  (a :: l).filterMapM f = do
    match (← f a) with
    | none =>
      filterMapM f l
    | some b =>
      return (b :: (← filterMapM f l))

Full source

@[simp] theorem filterMapM_cons [Monad m] [LawfulMonad m] {f : α → m (Option β)} :
    (a :: l).filterMapM f = do
      match (← f a) with
      | none => filterMapM f l
      | some b => return (b :: (← filterMapM f l)) := by
  conv => lhs; unfold filterMapM; unfold filterMapM.loop
  congr
  funext b?
  split <;> rename_i b
  · simp [filterMapM]
  · simp only [bind_pure_comp]
    rw [filterMapM_loop_eq, filterMapM]
    simp

Recursive Definition of Monadic Filter-Map for Non-Empty Lists

Informal description

Let $m$ be a lawful monad and $f : \alpha \to m (\text{Option} \beta)$ a function. For any non-empty list $a :: l$ of elements of type $\alpha$, the monadic filter-map operation satisfies: \[ \text{filterMapM}_f (a :: l) = \begin{cases} \text{filterMapM}_f l & \text{if } f(a) \text{ returns } \text{none}, \\ b :: \text{filterMapM}_f l & \text{if } f(a) \text{ returns } \text{some } b. \end{cases} \]

List.flatMapM_nil theorem

[Monad m] {f : α → m (List β)} : [].flatMapM f = pure []

Full source

@[simp] theorem flatMapM_nil [Monad m] {f : α → m (List β)} : [].flatMapM f = pure [] := rfl

Monadic FlatMap of Empty List Yields Pure Empty List

Informal description

For any monad $m$ and any function $f : \alpha \to m (\text{List} \beta)$, the monadic flatMap operation applied to the empty list `[]` with $f$ is equal to the pure monadic value of the empty list, i.e., $\text{flatMapM}_f [] = \text{pure} []$.

List.flatMapM_loop_eq theorem

 [Monad m] [LawfulMonad m] {f : α → m (List β)} {l : List α} {acc : List (List β)} :
  flatMapM.loop f l acc = (acc.reverse.flatten ++ ·) <$> flatMapM.loop f l []

Full source

theorem flatMapM_loop_eq [Monad m] [LawfulMonad m] {f : α → m (List β)} {l : List α} {acc : List (List β)} :
    flatMapM.loop f l acc = (acc.reverse.flatten ++ ·) <$> flatMapM.loop f l [] := by
  induction l generalizing acc with
  | nil => simp [flatMapM.loop]
  | cons a l ih =>
    simp only [flatMapM.loop, append_nil, _root_.map_bind]
    congr
    funext bs
    rw [ih, ih (acc := [bs])]
    simp

Equality for Monadic FlatMap Loop with Accumulator

Informal description

Let $m$ be a lawful monad, $f : \alpha \to m (\text{List} \beta)$ a function, $l$ a list of elements of type $\alpha$, and $acc$ a list of lists of elements of type $\beta$. Then the monadic flatMap loop operation satisfies: $$\text{flatMapM.loop}_f\ l\ acc = \text{map}\ (\lambda x \mapsto \text{flatten}(\text{reverse}(acc)) \mathbin{+\kern-0.5em+} x)\ (\text{flatMapM.loop}_f\ l\ [])$$ where $\mathbin{+\kern-0.5em+}$ denotes list concatenation and $\text{flatten}$ concatenates a list of lists.

List.flatMapM_cons theorem

 [Monad m] [LawfulMonad m] {f : α → m (List β)} :
  (a :: l).flatMapM f = do
    let bs ← f a
    return (bs ++ (← l.flatMapM f))

Full source

@[simp] theorem flatMapM_cons [Monad m] [LawfulMonad m] {f : α → m (List β)} :
    (a :: l).flatMapM f = do
      let bs ← f a
      return (bs ++ (← l.flatMapM f)) := by
  conv => lhs; unfold flatMapM; unfold flatMapM.loop
  congr
  funext bs
  rw [flatMapM_loop_eq, flatMapM]
  simp

Monadic FlatMap of Cons List Equals Concatenation of Results

Informal description

Let $m$ be a lawful monad and $f : \alpha \to m (\text{List} \beta)$ a function. For any list $a :: l$ (consisting of head $a$ and tail $l$), the monadic flatMap operation satisfies: $$\text{flatMapM}_f (a :: l) = \text{do } bs \leftarrow f a; \text{ return } (bs \mathbin{+\kern-0.5em+} \text{flatMapM}_f l)$$ where $\mathbin{+\kern-0.5em+}$ denotes list concatenation.

List.foldlM_map theorem

 [Monad m] {f : β₁ → β₂} {g : α → β₂ → m α} {l : List β₁} {init : α} :
  (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init

Full source

theorem foldlM_map [Monad m] {f : β₁ → β₂} {g : α → β₂ → m α} {l : List β₁} {init : α} :
    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
  induction l generalizing g init <;> simp [*]

Monadic Left Fold of Mapped List Equals Fold with Composed Operation

Informal description

Let $m$ be a monad, $f : \beta_1 \to \beta_2$ a function, $g : \alpha \to \beta_2 \to m \alpha$ a binary operation, $l$ a list of elements of type $\beta_1$, and $\text{init} \in \alpha$. Then the monadic left fold of the mapped list $l.\text{map}(f)$ with operation $g$ and initial value $\text{init}$ is equal to the monadic left fold of $l$ with operation $\lambda x y \mapsto g x (f y)$ and initial value $\text{init}$. In symbols: $$\text{foldlM}_g\ \text{init}\ (l.\text{map}(f)) = \text{foldlM}_{(\lambda x y \mapsto g x (f y))}\ \text{init}\ l$$

List.foldrM_map theorem

 [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ → α → m α} {l : List β₁} {init : α} :
  (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init

Full source

theorem foldrM_map [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ → α → m α} {l : List β₁} {init : α} :
    (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
  induction l generalizing g init <;> simp [*]

Monadic Right Fold of Mapped List Equals Fold with Composed Operation

Informal description

Let $m$ be a monad that satisfies the monad laws, $f : \beta_1 \to \beta_2$ a function, $g : \beta_2 \to \alpha \to m \alpha$ a binary operation, $l$ a list of elements of type $\beta_1$, and $\text{init} \in \alpha$. Then the monadic right fold of the mapped list $l.\text{map}(f)$ with operation $g$ and initial value $\text{init}$ is equal to the monadic right fold of $l$ with operation $\lambda x\ y \mapsto g (f x) y$ and initial value $\text{init}$. In symbols: $$\text{foldrM}_g\ \text{init}\ (l.\text{map}(f)) = \text{foldrM}_{(\lambda x\ y \mapsto g (f x) y)}\ \text{init}\ l$$

List.foldlM_filterMap theorem

 [Monad m] [LawfulMonad m] {f : α → Option β} {g : γ → β → m γ} {l : List α} {init : γ} :
  (l.filterMap f).foldlM g init =
    l.foldlM
      (fun x y =>
        match f y with
        | some b => g x b
        | none => pure x)
      init

Full source

theorem foldlM_filterMap [Monad m] [LawfulMonad m] {f : α → Option β} {g : γ → β → m γ} {l : List α} {init : γ} :
    (l.filterMap f).foldlM g init =
      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
  induction l generalizing init with
  | nil => rfl
  | cons a l ih =>
    simp only [filterMap_cons, foldlM_cons]
    cases f a <;> simp [ih]

Monadic Left Fold over Filtered and Mapped List Equals Conditional Fold over Original List

Informal description

Let $m$ be a monad with lawful monad operations, and let $f : \alpha \to \text{Option } \beta$ be a function that maps elements of type $\alpha$ to optional values of type $\beta$. Let $g : \gamma \to \beta \to m \gamma$ be a monadic function, $l$ a list of elements of type $\alpha$, and $\text{init}$ an initial value of type $\gamma$. Then the monadic left fold of $g$ over the list obtained by filtering and mapping $l$ with $f$ is equal to the monadic left fold over the original list $l$ where for each element $y \in l$, we apply $g$ to the current accumulator and $f(y)$ if $f(y)$ is $\text{some } b$, otherwise we keep the accumulator unchanged. In symbols: $$\text{foldlM}\ g\ \text{init}\ (\text{filterMap}\ f\ l) = \text{foldlM}\ (\lambda x\ y, \text{match}\ f(y)\ \text{with}\ |\ \text{some}\ b \Rightarrow g\ x\ b\ |\ \text{none} \Rightarrow \text{pure}\ x)\ \text{init}\ l$$

List.foldrM_filterMap theorem

 [Monad m] [LawfulMonad m] {f : α → Option β} {g : β → γ → m γ} {l : List α} {init : γ} :
  (l.filterMap f).foldrM g init =
    l.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init

Full source

theorem foldrM_filterMap [Monad m] [LawfulMonad m] {f : α → Option β} {g : β → γ → m γ} {l : List α} {init : γ} :
    (l.filterMap f).foldrM g init =
      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
  induction l generalizing init with
  | nil => rfl
  | cons a l ih =>
    simp only [filterMap_cons, foldrM_cons]
    cases f a <;> simp [ih]

Monadic Right Fold over Filtered and Mapped List Equals Conditional Fold over Original List

Informal description

Let $m$ be a monad that satisfies the monad laws, $f : \alpha \to \text{Option } \beta$ a function mapping elements to optional values, $g : \beta \to \gamma \to m \gamma$ a monadic function, $l$ a list of elements of type $\alpha$, and $\text{init}$ an initial value of type $\gamma$. Then the monadic right fold of $g$ over the list obtained by filtering and mapping $l$ with $f$ is equal to the monadic right fold over the original list $l$, where for each element $x \in l$, if $f(x) = \text{some } b$, we apply $g$ to $b$ and the accumulator, otherwise we keep the accumulator unchanged. In symbols: $$\text{foldrM}\ g\ \text{init}\ (\text{filterMap}\ f\ l) = \text{foldrM}\ (\lambda x\ y, \text{match}\ f(x)\ \text{with}\ |\ \text{some}\ b \Rightarrow g\ b\ y\ |\ \text{none} \Rightarrow \text{pure}\ y)\ \text{init}\ l$$

List.foldlM_filter theorem

 [Monad m] [LawfulMonad m] {p : α → Bool} {g : β → α → m β} {l : List α} {init : β} :
  (l.filter p).foldlM g init = l.foldlM (fun x y => if p y then g x y else pure x) init

Full source

theorem foldlM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : β → α → m β} {l : List α} {init : β} :
    (l.filter p).foldlM g init =
      l.foldlM (fun x y => if p y then g x y else pure x) init := by
  induction l generalizing init with
  | nil => rfl
  | cons a l ih =>
    simp only [filter_cons, foldlM_cons]
    split <;> simp [ih]

Monadic Left Fold over Filtered List Equals Conditional Fold over Original List

Informal description

Let $m$ be a monad satisfying the monad laws, $p : \alpha \to \text{Bool}$ a predicate, $g : \beta \to \alpha \to m \beta$ a monadic function, $l$ a list of elements of type $\alpha$, and $\text{init}$ an initial value of type $\beta$. Then the monadic left fold of $g$ over the filtered list $l.\text{filter}(p)$ with initial value $\text{init}$ is equal to the monadic left fold over the original list $l$ where for each element $y \in l$, we apply $g$ to the current accumulator and $y$ if $p(y)$ holds, otherwise we keep the accumulator unchanged. In symbols: $$\text{foldlM}\ g\ \text{init}\ (l.\text{filter}(p)) = \text{foldlM}\ (\lambda x\ y \Rightarrow \text{if}\ p(y)\ \text{then}\ g\ x\ y\ \text{else}\ \text{pure}\ x)\ \text{init}\ l$$

List.foldrM_filter theorem

 [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β → m β} {l : List α} {init : β} :
  (l.filter p).foldrM g init = l.foldrM (fun x y => if p x then g x y else pure y) init

Full source

theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β → m β} {l : List α} {init : β} :
    (l.filter p).foldrM g init =
      l.foldrM (fun x y => if p x then g x y else pure y) init := by
  induction l generalizing init with
  | nil => rfl
  | cons a l ih =>
    simp only [filter_cons, foldrM_cons]
    split <;> simp [ih]

Monadic Right Fold over Filtered List Equals Conditional Fold over Original List

Informal description

Let $m$ be a monad satisfying the monad laws, $p : \alpha \to \text{Bool}$ a predicate, $g : \alpha \to \beta \to m \beta$ a monadic function, $l$ a list of elements of type $\alpha$, and $\text{init}$ an initial value of type $\beta$. Then the monadic right fold of $g$ over the filtered list $\text{filter}\ p\ l$ with initial value $\text{init}$ is equal to the monadic right fold over the original list $l$, where for each element $x \in l$, we apply $g$ to $x$ and the accumulator if $p(x)$ holds, otherwise we keep the accumulator unchanged. In symbols: $$\text{foldrM}\ g\ \text{init}\ (\text{filter}\ p\ l) = \text{foldrM}\ (\lambda x\ y, \text{if}\ p(x)\ \text{then}\ g\ x\ y\ \text{else}\ \text{pure}\ y)\ \text{init}\ l$$

List.foldlM_attachWith theorem

 [Monad m] {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x } → m β} {b} :
  (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

Full source

@[simp] theorem foldlM_attachWith [Monad m]
    {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
    (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
  induction l generalizing b with
  | nil => simp
  | cons a l ih => simp [ih, foldlM_map]

Monadic Left Fold of Attached List with Predicate Equals Fold of Attached List with Witnessed Predicate

Informal description

Let $m$ be a monad, $l$ a list of elements of type $\alpha$, and $q : \alpha \to \text{Prop}$ a predicate such that for every $a \in l$, $q(a)$ holds (witnessed by $H$). Let $f : \beta \to \{x \mid q(x)\} \to m \beta$ be a function and $b \in \beta$. Then the monadic left fold of the list $l.\text{attachWith}(q, H)$ with operation $f$ and initial value $b$ is equal to the monadic left fold of the attached list $l.\text{attach}$ with operation $\lambda b \langle a, h \rangle \mapsto f b \langle a, H a h \rangle$ and initial value $b$. In symbols: $$\text{foldlM}_f\ b\ (l.\text{attachWith}(q, H)) = \text{foldlM}_{(\lambda b \langle a, h \rangle \mapsto f b \langle a, H a h \rangle)}\ b\ (l.\text{attach})$$

List.foldrM_attachWith theorem

 [Monad m] [LawfulMonad m] {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x } → β → m β} {b} :
  (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Full source

@[simp] theorem foldrM_attachWith [Monad m] [LawfulMonad m]
    {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → m β} {b} :
    (l.attachWith q H).foldrM f b = l.attach.foldrM (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
  induction l generalizing b with
  | nil => simp
  | cons a l ih => simp [ih, foldrM_map]

Monadic Right Fold of Attached List with Predicate Equals Fold of Attached List with Witnessed Predicate

Informal description

Let $m$ be a monad that satisfies the monad laws, $l$ a list of elements of type $\alpha$, and $q : \alpha \to \text{Prop}$ a predicate such that for every $a \in l$, $q(a)$ holds (witnessed by $H$). Let $f : \{x \mid q(x)\} \to \beta \to m \beta$ be a function and $b \in \beta$. Then the monadic right fold of the list $l.\text{attachWith}(q, H)$ with operation $f$ and initial value $b$ is equal to the monadic right fold of the attached list $l.\text{attach}$ with operation $\lambda a\ \text{acc} \mapsto f \langle a.1, H a.1 a.2 \rangle\ \text{acc}$ and initial value $b$. In symbols: $$\text{foldrM}_f\ b\ (l.\text{attachWith}(q, H)) = \text{foldrM}_{(\lambda a\ \text{acc} \mapsto f \langle a.1, H a.1 a.2 \rangle\ \text{acc})}\ b\ (l.\text{attach})$$

List.forM_nil' theorem

[Monad m] : ([] : List α).forM f = (pure .unit : m PUnit)

Full source

@[deprecated forM_nil (since := "2025-01-31")]
theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl

Monadic For-Loop on Empty List Yields Unit

Informal description

For any monad `m`, applying the monadic for-loop operation `forM` to the empty list `[]` with any function `f : α → m PUnit` results in the pure monadic unit value `pure .unit`.

List.forM_cons' theorem

[Monad m] : (a :: as).forM f = (f a >>= fun _ => as.forM f : m PUnit)

Full source

@[deprecated forM_cons (since := "2025-01-31")]
theorem forM_cons' [Monad m] :
    (a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) :=
  List.forM_cons

Monadic For-Loop on Cons List: `forM (a :: as) f = f a >>= fun _ => forM as f`

Informal description

For any monad `m` and any list `a :: as` of type `List α`, the monadic operation `forM` applied to the list with a function `f : α → m PUnit` is equal to first applying `f` to the head `a` and then applying `forM` to the tail `as` with the same function `f`.

List.forM_append theorem

 [Monad m] [LawfulMonad m] {l₁ l₂ : List α} {f : α → m PUnit} :
  forM (l₁ ++ l₂) f =
    (do
      forM l₁ f;
      forM l₂ f)

Full source

@[simp] theorem forM_append [Monad m] [LawfulMonad m] {l₁ l₂ : List α} {f : α → m PUnit} :
    forM (l₁ ++ l₂) f = (do forMforM l₁ f; forM l₂ f) := by
  induction l₁ <;> simp [*]

Monadic For-Loop Distributes Over List Concatenation: `forM (l₁ ++ l₂) f = (forM l₁ f; forM l₂ f)`

Informal description

For any monad `m` that satisfies the monad laws, and for any lists `l₁` and `l₂` of type `List α`, the monadic operation `forM` applied to the concatenated list `l₁ ++ l₂` with a function `f : α → m PUnit` is equal to sequentially applying `forM` to `l₁` and then to `l₂` with the same function `f`.

List.forM_map theorem

 [Monad m] [LawfulMonad m] {l : List α} {g : α → β} {f : β → m PUnit} : forM (l.map g) f = forM l (fun a => f (g a))

Full source

@[simp] theorem forM_map [Monad m] [LawfulMonad m] {l : List α} {g : α → β} {f : β → m PUnit} :
    forM (l.map g) f = forM l (fun a => f (g a)) := by
  induction l <;> simp [*]

Monadic For-Loop Commutes with List Mapping: `forM (map g l) f = forM l (f ∘ g)`

Informal description

For any monad `m` that satisfies the monad laws, any list `l` of elements of type `α`, and any functions `g : α → β` and `f : β → m PUnit`, the monadic operation `forM` applied to the mapped list `l.map g` with function `f` is equal to applying `forM` to the original list `l` with the composed function `f ∘ g`.

List.forIn'_loop_congr theorem

 [Monad m] {as bs : List α} {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
  {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs)
  (h : ∀ a m m' b, f a m b = g a m' b) : forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb

Full source

theorem forIn'_loop_congr [Monad m] {as bs : List α}
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    {b : β} (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs)
    (h : ∀ a m m' b, f a m b = g a m' b) : forIn'.loop as f xs b ha = forIn'.loop bs g xs b hb  := by
  induction xs generalizing b with
  | nil => simp [forIn'.loop]
  | cons a xs ih =>
    simp only [forIn'.loop] at *
    congr 1
    · rw [h]
    · funext s
      obtain b | b := s
      · rfl
      · simp
        rw [ih]

Congruence of Monadic List Iteration Loops with Shared Suffix

Informal description

Let $m$ be a monad, and let $as$ and $bs$ be lists of type $\alpha$. Suppose there exist lists $ys$ such that $ys \mathbin{+\kern-0.5em+} xs = as$ and $ys \mathbin{+\kern-0.5em+} xs = bs$, where $\mathbin{+\kern-0.5em+}$ denotes list concatenation. Given functions $f : (a' : \alpha) \to a' \in as \to \beta \to m (\text{ForInStep} \beta)$ and $g : (a' : \alpha) \to a' \in bs \to \beta \to m (\text{ForInStep} \beta)$, if for all $a \in \alpha$, membership proofs $m, m'$, and $b \in \beta$, we have $f(a, m, b) = g(a, m', b)$, then the loop computations $\text{forIn'}\text{.loop}\ as\ f\ xs\ b\ ha$ and $\text{forIn'}\text{.loop}\ bs\ g\ xs\ b\ hb$ are equal.

List.forIn'_cons theorem

 [Monad m] {a : α} {as : List α} (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β) :
  forIn' (a :: as) b f =
    f a mem_cons_self b >>= fun
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn' as b fun a' m b => f a' (mem_cons_of_mem a m) b

Full source

@[simp] theorem forIn'_cons [Monad m] {a : α} {as : List α}
    (f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β)) (b : β) :
    forIn' (a::as) b f = f a mem_cons_self b >>=
      fun | ForInStep.done b => pure b | ForInStep.yield b => forIn' as b fun a' m b => f a' (mem_cons_of_mem a m) b := by
  simp only [forIn', List.forIn', forIn'.loop]
  congr 1
  funext s
  obtain b | b := s
  · rfl
  · apply forIn'_loop_congr
    intros
    rfl

Monadic Iteration Decomposition for Cons List: `forIn' (a :: as) = f a >>= ...`

Informal description

Let $m$ be a monad, $a$ an element of type $\alpha$, and $as$ a list of elements of type $\alpha$. Given a function $f : (a' : \alpha) \to a' \in (a :: as) \to \beta \to m (\text{ForInStep} \beta)$ and an initial state $b : \beta$, the monadic iteration `forIn'` on the list $a :: as$ with initial state $b$ and function $f$ is equal to: 1. First applying $f$ to $a$ (using the proof that $a \in a :: as$), then 2. If the result is `ForInStep.done b'`, returning $b'$; 3. If the result is `ForInStep.yield b'`, continuing the iteration on $as$ with state $b'$ and the function $\lambda a'\, m\, b,\ f\ a'\ (\text{mem\_cons\_of\_mem}\ a\ m)\ b$.

List.forIn_cons theorem

 [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) :
  forIn (a :: as) b f =
    f a b >>= fun
      | ForInStep.done b => pure b
      | ForInStep.yield b => forIn as b f

Full source

@[simp] theorem forIn_cons [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) :
    forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f := by
  have := forIn'_cons (a := a) (as := as) (fun a' _ b => f a' b) b
  simpa only [forIn'_eq_forIn]

Monadic Iteration Decomposition for Cons List: `forIn (a :: as) = f a >>= ...`

Informal description

Let $m$ be a monad, $f : \alpha \to \beta \to m (\text{ForInStep} \beta)$ a function, $a$ an element of type $\alpha$, $as$ a list of elements of type $\alpha$, and $b$ an initial state of type $\beta$. Then the monadic iteration `forIn` on the list $a :: as$ with initial state $b$ and function $f$ is equal to: 1. First applying $f$ to $a$ and $b$, then 2. If the result is `ForInStep.done b'`, returning $b'$; 3. If the result is `ForInStep.yield b'`, continuing the iteration on $as$ with state $b'$ and function $f$.

List.forIn'_congr theorem

 [Monad m] {as bs : List α} (w : as = bs) {b b' : β} (hb : b = b') {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
  {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
  forIn' as b f = forIn' bs b' g

Full source

@[congr] theorem forIn'_congr [Monad m] {as bs : List α} (w : as = bs)
    {b b' : β} (hb : b = b')
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
    forIn' as b f = forIn' bs b' g := by
  induction bs generalizing as b b' with
  | nil =>
    subst w
    simp [hb, forIn'_nil]
  | cons b bs ih =>
    cases as with
    | nil => simp at w
    | cons a as =>
      simp only [cons.injEq] at w
      obtain ⟨rfl, rfl⟩ := w
      simp only [forIn'_cons]
      congr 1
      · simp [h, hb]
      · funext s
        obtain b | b := s
        · rfl
        · simp
          rw [ih rfl rfl]
          intro a m b
          exact h a (mem_cons_of_mem _ m) b

Congruence of Monadic Iteration over Lists: $\text{forIn'}\ as\ b\ f = \text{forIn'}\ bs\ b'\ g$ under List Equality and Function Agreement

Informal description

Let $m$ be a monad, and let $as$ and $bs$ be lists of type $\alpha$ such that $as = bs$. Given initial states $b, b' : \beta$ with $b = b'$, and functions $f : (a' : \alpha) \to a' \in as \to \beta \to m (\text{ForInStep} \beta)$ and $g : (a' : \alpha) \to a' \in bs \to \beta \to m (\text{ForInStep} \beta)$ such that for all $a \in \alpha$, membership proofs $m$, and states $b$, we have $f(a, m, b) = g(a, m, b)$. Then the monadic iterations $\text{forIn'}\ as\ b\ f$ and $\text{forIn'}\ bs\ b'\ g$ are equal.

List.forIn'_eq_foldlM theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
  forIn' l init f =
    ForInStep.value <$>
      l.attach.foldlM
        (fun b ⟨a, m⟩ =>
          match b with
          | .yield b => f a m b
          | .done b => pure (.done b))
        (ForInStep.yield init)

Full source

/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
    {l : List α} (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
    forIn' l init f = ForInStep.valueForInStep.value <$>
      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
        | .yield b => f a m b
        | .done b => pure (.done b)) (ForInStep.yield init) := by
  induction l generalizing init with
  | nil => simp
  | cons a as ih =>
    simp only [forIn'_cons, attach_cons, foldlM_cons, _root_.map_bind]
    congr 1
    funext x
    match x with
    | .done b =>
      clear ih
      dsimp
      induction as with
      | nil => simp
      | cons a as ih =>
        simp only [attach_cons, map_cons, map_map, Function.comp_def, foldlM_cons, pure_bind]
        specialize ih (fun a m b => f a (by
          simp only [mem_cons] at m
          rcases m with rfl|m
          · apply mem_cons_self
          · exact mem_cons_of_mem _ (mem_cons_of_mem _ m)) b)
        simp [ih, List.foldlM_map]
    | .yield b =>
      simp [ih, List.foldlM_map]

Monadic Iteration as Fold: $\text{forIn'} = \text{foldlM}$ on Attached List

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, $f : (a : \alpha) \to a \in l \to \beta \to m (\text{ForInStep} \beta)$ a function, and $\text{init} \in \beta$ an initial state. Then the monadic iteration `forIn'` on $l$ with initial state $\text{init}$ and function $f$ is equal to the monadic left fold of the attached list $l.\text{attach}$ (where each element is paired with its membership proof), starting with $\text{ForInStep.yield init}$ and using the operation: $$ \lambda b \langle a, m \rangle, \begin{cases} \text{ForInStep.done } b & \text{if } b = \text{ForInStep.done } b', \\ f\ a\ m\ b & \text{if } b = \text{ForInStep.yield } b'. \end{cases} $$ followed by extracting the $\text{value}$ from the resulting $\text{ForInStep}$. In symbols: $$\text{forIn'}\ l\ \text{init}\ f = \text{ForInStep.value} <\$> \text{foldlM}_\text{op}\ (\text{ForInStep.yield init})\ l.\text{attach}$$ where $\text{op}$ is the case analysis operation described above.

List.forIn'_yield_eq_foldlM theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
  forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
    l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init

Full source

/-- We can express a for loop over a list which always yields as a fold. -/
@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
    {l : List α} (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
  simp only [forIn'_eq_foldlM]
  induction l.attach generalizing init <;> simp_all

Monadic Iteration with Yield as Monadic Fold: $\text{forIn'} = \text{foldlM}$ for Yield-Only Cases

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, $f : (a : \alpha) \to a \in l \to \beta \to m \gamma$ a function producing monadic values, and $g : (a : \alpha) \to a \in l \to \beta \to \gamma \to \beta$ a state transformation function. Then the monadic iteration `forIn'` on $l$ with initial state $\text{init} \in \beta$ and function $\lambda a\ m\ b, \text{ForInStep.yield} (g\ a\ m\ b\ c) <\$> f\ a\ m\ b$ is equal to the monadic left fold of the attached list $l.\text{attach}$ (where each element is paired with its membership proof), starting with $\text{init}$ and using the operation $\lambda b\ \langle a, m\rangle, g\ a\ m\ b <\$> f\ a\ m\ b$. In symbols: $$\text{forIn'}\ l\ \text{init}\ (\lambda a\ m\ b, \text{yield} (g\ a\ m\ b\ c) <\$> f\ a\ m\ b) = \text{foldlM}_\text{op}\ \text{init}\ l.\text{attach}$$ where $\text{op}\ b\ \langle a, m\rangle = g\ a\ m\ b <\$> f\ a\ m\ b$.

List.forIn'_pure_yield_eq_foldl theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
  forIn' l init (fun a m b => pure (.yield (f a m b))) = pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init)

Full source

@[simp] theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' l init (fun a m b => pure (.yield (f a m b))) =
      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
  simp only [forIn'_eq_foldlM]
  induction l.attach generalizing init <;> simp_all

Pure Monadic Iteration Equals Pure Fold: $\text{forIn'}_{\text{pure}} = \text{pure} \circ \text{foldl}$

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, and $f : (a : \alpha) \to a \in l \to \beta \to \beta$ a function. For any initial state $\text{init} \in \beta$, the monadic iteration `forIn'` over $l$ with the pure yielding function $\lambda a\,m\,b,\ \text{pure}\,(\text{ForInStep.yield}\,(f\,a\,m\,b))$ is equal to the pure monadic value of the left fold over the attached list $l.\text{attach}$ with the initial state $\text{init}$ and the function $\lambda b\,\langle a, h\rangle,\ f\,a\,h\,b$. In symbols: $$\text{forIn'}\ l\ \text{init}\ (\lambda a\,m\,b,\ \text{pure}\,(\text{ForInStep.yield}\,(f\,a\,m\,b))) = \text{pure}\,(l.\text{attach}.\text{foldl}\,(\lambda b\,\langle a, h\rangle,\ f\,a\,h\,b)\ \text{init})$$

List.forIn'_yield_eq_foldl theorem

 {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
  forIn' (m := Id) l init (fun a m b => .yield (f a m b)) = l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init

Full source

@[simp] theorem forIn'_yield_eq_foldl
    {l : List α} (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
  simp only [forIn'_eq_foldlM]
  induction l.attach generalizing init <;> simp_all

Identity Monad Iteration Equals Fold on Attached List: $\text{forIn'}_{\text{Id}} = \text{foldl}$

Informal description

For any list $l$ of elements of type $\alpha$, any function $f : (a : \alpha) \to a \in l \to \beta \to \beta$, and any initial state $\text{init} \in \beta$, the monadic iteration `forIn'` (with the identity monad) over $l$ using the function $\lambda a\,m\,b,\ \text{ForInStep.yield}\,(f\,a\,m\,b)$ is equal to the left fold over the attached list $l.\text{attach}$ (where each element is paired with its membership proof) using the function $\lambda b\,\langle a, h\rangle,\ f\,a\,h\,b$. In symbols: $$\text{forIn'}_{\text{Id}}\ l\ \text{init}\ (\lambda a\,m\,b,\ \text{ForInStep.yield}\,(f\,a\,m\,b)) = \text{foldl}_{\text{op}}\ \text{init}\ l.\text{attach}$$ where $\text{op} = \lambda b\,\langle a, h\rangle,\ f\,a\,h\,b$.

List.forIn'_map theorem

 [Monad m] [LawfulMonad m] {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
  forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem h) y

Full source

@[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
    {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem h) y := by
  induction l generalizing init <;> simp_all

Monadic Iteration Commutes with List Mapping: $\text{forIn'}\,(\text{map}\,g\,l) = \text{forIn'}\,l \circ (\lambda f\,a\,h\,y,\ f\,(g\,a)\,(\text{mem\_map\_of\_mem}\,h)\,y)$

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, and $g : \alpha \to \beta$ a function. For any function $f : (b : \beta) \to b \in \text{map}\,g\,l \to \gamma \to m (\text{ForInStep}\,\gamma)$ and initial state $\text{init} : \gamma$, the monadic iteration $\text{forIn'}$ over the mapped list $\text{map}\,g\,l$ with function $f$ is equal to the iteration $\text{forIn'}$ over the original list $l$ with the function $\lambda a\,h\,y,\ f\,(g\,a)\,(\text{mem\_map\_of\_mem}\,h)\,y$.

List.forIn_eq_foldlM theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m (ForInStep β)) (init : β) :
  forIn l init f =
    ForInStep.value <$>
      l.foldlM
        (fun b a =>
          match b with
          | .yield b => f a b
          | .done b => pure (.done b))
        (ForInStep.yield init)

Full source

/--
We can express a for loop over a list as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
-/
theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
    {l : List α} (f : α → β → m (ForInStep β)) (init : β) :
    forIn l init f = ForInStep.valueForInStep.value <$>
      l.foldlM (fun b a => match b with
        | .yield b => f a b
        | .done b => pure (.done b)) (ForInStep.yield init) := by
  induction l generalizing init with
  | nil => simp
  | cons a as ih =>
    simp only [foldlM_cons, bind_pure_comp, forIn_cons, _root_.map_bind]
    congr 1
    funext x
    match x with
    | .done b =>
      clear ih
      dsimp
      induction as with
      | nil => simp
      | cons a as ih => simp [ih]
    | .yield b =>
      simp [ih]

Monadic Iteration as Fold: $\text{forIn} = \text{ForInStep.value} \circ \text{foldlM}$

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, $f : \alpha \to \beta \to m (\text{ForInStep} \beta)$ a function, and $\text{init} : \beta$ an initial state. Then the monadic iteration $\text{forIn}$ over $l$ with initial state $\text{init}$ and function $f$ is equal to the monadic fold $\text{foldlM}$ over $l$ where: 1. The initial state is $\text{ForInStep.yield init}$, 2. For each element $a \in l$ and current state $b$, if $b$ is $\text{ForInStep.yield b'}$, we apply $f$ to $a$ and $b'$; otherwise if $b$ is $\text{ForInStep.done b'}$, we return $\text{pure (.done b')}$, 3. The final result is wrapped in $\text{ForInStep.value}$.

List.forIn_yield_eq_foldlM theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
  forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) = l.foldlM (fun b a => g a b <$> f a b) init

Full source

/-- We can express a for loop over a list which always yields as a fold. -/
@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
    {l : List α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
      l.foldlM (fun b a => g a b <$> f a b) init := by
  simp only [forIn_eq_foldlM]
  induction l generalizing init <;> simp_all

Monadic Iteration with Yield as Monadic Fold: $\text{forIn}\,l\,\text{init}\,(\lambda a\,b,\ \text{yield}\,(g\,a\,b\,c) \text{ for } c \text{ in } f\,a\,b) = \text{foldlM}\,(\lambda b\,a,\ g\,a\,b\,c \text{ for } c \text{ in } f\,a\,b)\,\text{init}\,l$

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, $f : \alpha \to \beta \to m \gamma$ a monadic function, $g : \alpha \to \beta \to \gamma \to \beta$ a state transformation function, and $\text{init} : \beta$ an initial state. Then the monadic iteration $\text{forIn}$ over $l$ with initial state $\text{init}$ and function $\lambda a\,b,\ \text{yield}\,(g\,a\,b\,c) \text{ for } c \text{ in } f\,a\,b$ is equal to the monadic left fold $\text{foldlM}$ over $l$ with initial state $\text{init}$ and function $\lambda b\,a,\ g\,a\,b\,c \text{ for } c \text{ in } f\,a\,b$.

List.forIn_pure_yield_eq_foldl theorem

 [Monad m] [LawfulMonad m] {l : List α} (f : α → β → β) (init : β) :
  forIn l init (fun a b => pure (.yield (f a b))) = pure (f := m) (l.foldl (fun b a => f a b) init)

Full source

@[simp] theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    {l : List α} (f : α → β → β) (init : β) :
    forIn l init (fun a b => pure (.yield (f a b))) =
      pure (f := m) (l.foldl (fun b a => f a b) init) := by
  simp only [forIn_eq_foldlM]
  induction l generalizing init <;> simp_all

Pure Monadic Iteration Equals Pure Fold: $\text{forIn}\ l\ \text{init}\ (\lambda a\ b, \text{pure (.yield (f a b))}) = \text{pure (foldl}\ f\ \text{init}\ l)$

Informal description

Let $m$ be a lawful monad, $l$ a list of elements of type $\alpha$, $f : \alpha \to \beta \to \beta$ a function, and $\text{init} : \beta$ an initial state. Then the monadic iteration $\text{forIn}$ over $l$ with initial state $\text{init}$ and the pure yielding function $\lambda a\ b, \text{pure (.yield (f a b))}$ is equal to the pure monadic lift of the left fold $\text{foldl}$ over $l$ with initial state $\text{init}$ and function $f$.

List.forIn_yield_eq_foldl theorem

 {l : List α} (f : α → β → β) (init : β) :
  forIn (m := Id) l init (fun a b => .yield (f a b)) = l.foldl (fun b a => f a b) init

Full source

@[simp] theorem forIn_yield_eq_foldl
    {l : List α} (f : α → β → β) (init : β) :
    forIn (m := Id) l init (fun a b => .yield (f a b)) =
      l.foldl (fun b a => f a b) init := by
  simp only [forIn_eq_foldlM]
  induction l generalizing init <;> simp_all

Identity Monad Iteration Equals Left Fold: $\text{forIn}_{\text{Id}} = \text{foldl}$

Informal description

For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \beta \to \beta$, and any initial state $\text{init} : \beta$, the monadic iteration $\text{forIn}$ (with the identity monad) over $l$ with initial state $\text{init}$ and the function $\lambda a\ b, \text{ForInStep.yield} (f\ a\ b)$ is equal to the left fold of $l$ with initial state $\text{init}$ and function $\lambda b\ a, f\ a\ b$.

List.forIn_map theorem

 [Monad m] [LawfulMonad m] {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :
  forIn (l.map g) init f = forIn l init fun a y => f (g a) y

Full source

@[simp] theorem forIn_map [Monad m] [LawfulMonad m]
    {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :
    forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
  induction l generalizing init <;> simp_all

Monadic Iteration Commutes with List Mapping: $\text{forIn}\ (l.map\ g)\ init\ f = \text{forIn}\ l\ init\ (\lambda a\ y, f (g\ a)\ y)$

Informal description

Let $m$ be a monad satisfying the monad laws, $l$ a list of elements of type $\alpha$, $g : \alpha \to \beta$ a function, and $f : \beta \to \gamma \to m (\text{ForInStep} \gamma)$ a monadic action. Then the monadic iteration `forIn` over the mapped list $l.map\ g$ with initial state $init$ and function $f$ is equal to the monadic iteration `forIn` over the original list $l$ with initial state $init$ and the composed function $\lambda a\ y, f (g\ a)\ y$.

List.allM_eq_not_anyM_not theorem

[Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} : allM p as = (!·) <$> anyM ((!·) <$> p ·) as

Full source

theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} :
    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
  induction as with
  | nil => simp
  | cons a as ih =>
    simp only [allM, anyM, bind_map_left, _root_.map_bind]
    congr
    funext b
    split <;> simp_all

Equivalence of Monadic All and Negated Any: $\text{allM}\ p\ as = \neg \circ \text{anyM}\ (\neg \circ p)\ as$

Informal description

For any monad `m` that satisfies the monad laws, any predicate `p : α → m Bool`, and any list `as : List α`, the monadic operation `allM p as` is equivalent to applying the negation function to the result of the monadic operation `anyM (¬ ∘ p) as`.

List.anyM_pure theorem

[Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} : as.anyM (m := m) (pure <| p ·) = pure (as.any p)

Full source

@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} :
    as.anyM (m := m) (pure <| p ·) = pure (as.any p) := by
  induction as with
  | nil => simp
  | cons a as ih =>
    simp only [anyM, ih, pure_bind, all_cons]
    split <;> simp_all

Monadic Any of Pure Predicate Equals Pure of Any

Informal description

For any monad `m` that satisfies the monad laws, any predicate `p : α → Bool`, and any list `as : List α`, the monadic operation `anyM` applied to the pure version of `p` over `as` is equal to the pure version of the boolean disjunction (any) of `p` applied to `as`. In symbols: $$\text{anyM}\ (\text{pure} \circ p)\ as = \text{pure}\ (\text{any}\ p\ as)$$

List.allM_pure theorem

[Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} : as.allM (m := m) (pure <| p ·) = pure (as.all p)

Full source

@[simp] theorem allM_pure [Monad m] [LawfulMonad m] {p : α → Bool} {as : List α} :
    as.allM (m := m) (pure <| p ·) = pure (as.all p) := by
  simp [allM_eq_not_anyM_not, all_eq_not_any_not]

Monadic All of Pure Predicate Equals Pure of All

Informal description

For any monad `m` that satisfies the monad laws, any predicate `p : α → Bool`, and any list `as : List α`, the monadic operation `allM` applied to the pure version of `p` over `as` is equal to the pure version of the boolean conjunction (all) of `p` applied to `as`. In symbols: $$\text{allM}\ (\text{pure} \circ p)\ as = \text{pure}\ (\text{all}\ p\ as)$$

List.foldlM_subtype theorem

 [Monad m] {p : α → Prop} {l : List { x // p x }} {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
  (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) : l.foldlM f x = l.unattach.foldlM g x

Full source

/--
This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem foldlM_subtype [Monad m] {p : α → Prop} {l : List { x // p x }}
    {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
    l.foldlM f x = l.unattach.foldlM g x := by
  unfold unattach
  induction l generalizing x with
  | nil => simp
  | cons a l ih => simp [ih, hf]

Monadic Left Fold Equality for Subtypes: $\text{foldlM}\ f\ x\ l = \text{foldlM}\ g\ x\ l.\text{unattach}$

Informal description

Let $m$ be a monad, $p : \alpha \to \text{Prop}$ a predicate, and $l$ a list of elements of subtype $\{x \mid p(x)\}$. Given functions $f : \beta \to \{x \mid p(x)\} \to m \beta$ and $g : \beta \to \alpha \to m \beta$ such that for all $b \in \beta$, $x \in \alpha$, and proof $h$ of $p(x)$, we have $f(b, \langle x, h \rangle) = g(b, x)$, then the monadic left fold of $l$ with $f$ starting at $x$ is equal to the monadic left fold of the unattached list $l$ with $g$ starting at $x$.

List.foldlM_wfParam theorem

 [Monad m] {xs : List α} {f : β → α → m β} {init : β} : (wfParam xs).foldlM f init = xs.attach.unattach.foldlM f init

Full source

@[wf_preprocess] theorem foldlM_wfParam [Monad m] {xs : List α} {f : β → α → m β} {init : β} :
    (wfParam xs).foldlM f init = xs.attach.unattach.foldlM f init := by
  simp [wfParam]

Monadic Left Fold with Well-Founded Parameter Equals Fold of Attached List

Informal description

For any monad `m`, list `xs : List α`, function `f : β → α → m β`, and initial value `init : β`, the monadic fold operation `foldlM` applied to `wfParam xs` with `f` and `init` is equal to `foldlM` applied to the unattached version of the attached list `xs.attach` with the same function and initial value.

List.foldlM_unattach theorem

 [Monad m] {P : α → Prop} {xs : List (Subtype P)} {f : β → α → m β} {init : β} :
  xs.unattach.foldlM f init =
    xs.foldlM (init := init) fun b ⟨x, h⟩ =>
      binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <| f b (wfParam x)

Full source

@[wf_preprocess] theorem foldlM_unattach [Monad m] {P : α → Prop} {xs : List (Subtype P)} {f : β → α → m β} {init : β} :
    xs.unattach.foldlM f init = xs.foldlM (init := init) fun b ⟨x, h⟩ =>
      binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <|
      f b (wfParam x) := by
  simp [wfParam]

Equality of Monadic Left Folds for Attached and Unattached Lists

Informal description

Let $m$ be a monad, $P : \alpha \to \text{Prop}$ a predicate, and $xs$ a list of elements of subtype $\{x \mid P(x)\}$. For any function $f : \beta \to \alpha \to m \beta$ and initial value $init : \beta$, the monadic left fold of $f$ over the unattached list $xs.\text{unattach}$ starting at $init$ is equal to the monadic left fold over $xs$ with the modified function $\lambda b \langle x, h \rangle, f b x$ starting at $init$.

List.foldrM_subtype theorem

 [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
  (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) : l.foldrM f x = l.unattach.foldrM g x

Full source

/--
This lemma identifies monadic folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem foldrM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
    l.foldrM f x = l.unattach.foldrM g x := by
  unfold unattach
  induction l generalizing x with
  | nil => simp
  | cons a l ih =>
    simp [ih, hf, foldrM_cons]
    congr
    funext b
    simp [hf]

Equality of Monadic Right Folds for Subtypes with Value-Dependent Functions

Informal description

Let $m$ be a monad with lawful instances, $p : \alpha \to \text{Prop}$ be a predicate, $l$ be a list of elements of subtype $\{x \mid p x\}$, $f : \{x \mid p x\} \to \beta \to m \beta$ and $g : \alpha \to \beta \to m \beta$ be functions, and $x : \beta$ be an initial value. If for all $x$ with proof $h$ of $p(x)$ and all $b : \beta$, we have $f(\langle x, h \rangle, b) = g(x, b)$, then the monadic right fold of $f$ over $l$ with initial value $x$ is equal to the monadic right fold of $g$ over the unattached version of $l$ with the same initial value.

List.foldrM_wfParam theorem

 [Monad m] [LawfulMonad m] {xs : List α} {f : α → β → m β} {init : β} :
  (wfParam xs).foldrM f init = xs.attach.unattach.foldrM f init

Full source

@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] {xs : List α} {f : α → β → m β} {init : β} :
    (wfParam xs).foldrM f init = xs.attach.unattach.foldrM f init := by
  simp [wfParam]

Equality of Monadic Right Folds with Well-Founded Parameter

Informal description

Let $m$ be a monad with lawful instances, $\alpha$ and $\beta$ be types, $xs$ be a list of elements of type $\alpha$, $f : \alpha \to \beta \to m \beta$ be a function, and $init : \beta$ be an initial value. Then the monadic right fold of $f$ over the list $xs$ with initial value $init$ is equal to the monadic right fold of $f$ over the list obtained by first attaching and then unattaching $xs$ with the same initial value $init$.

List.foldrM_unattach theorem

 [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → β → m β} {init : β} :
  xs.unattach.foldrM f init =
    xs.foldrM (init := init) fun ⟨x, h⟩ b =>
      binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <| f (wfParam x) b

Full source

@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → β → m β} {init : β} :
    xs.unattach.foldrM f init = xs.foldrM (init := init) fun ⟨x, h⟩ b =>
      binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <|
      f (wfParam x) b := by
  simp [wfParam]

Equality of Monadic Right Folds for Unattached Subtype Lists

Informal description

Let $m$ be a lawful monad, $P : \alpha \to \text{Prop}$ be a predicate, $xs$ be a list of elements of the subtype $\{x : \alpha \mid P x\}$, $f : \alpha \to \beta \to m \beta$ be a function, and $init : \beta$ be an initial value. Then the monadic right fold of $f$ over the unattached list $xs$ with initial value $init$ is equal to the monadic right fold over $xs$ where for each element $\langle x, h \rangle$ and accumulator $b$, the function $f$ is applied to $x$ (via $\text{wfParam}$) and $b$. In symbols: $$\text{foldrM}_m\ f\ init\ (\text{unattach}\ xs) = \text{foldrM}_m\ (\lambda \langle x, h \rangle\ b \mapsto f\ x\ b)\ init\ xs$$

List.mapM_subtype theorem

 [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → m β} {g : α → m β}
  (hf : ∀ x h, f ⟨x, h⟩ = g x) : l.mapM f = l.unattach.mapM g

Full source

/--
This lemma identifies monadic maps over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
-/
@[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.mapM f = l.unattach.mapM g := by
  unfold unattach
  simp [← List.mapM'_eq_mapM]
  induction l with
  | nil => simp
  | cons a l ih => simp [ih, hf]

Monadic Map over Subtype Equals Map over Unattached List when Function Depends Only on Value

Informal description

Let $m$ be a lawful monad, $\alpha$ and $\beta$ be types, $p : \alpha \to \text{Prop}$ be a predicate, and $l$ be a list of elements of the subtype $\{x : \alpha \mid p x\}$. Given two functions $f : \{x \mid p x\} \to m \beta$ and $g : \alpha \to m \beta$ such that for all $x : \alpha$ and $h : p x$, we have $f \langle x, h \rangle = g x$, then the monadic mapping of $f$ over $l$ is equal to the monadic mapping of $g$ over the unattached version of $l$. In symbols: $$\text{mapM}_m\ f\ l = \text{mapM}_m\ g\ (\text{unattach}\ l)$$

List.mapM_wfParam theorem

[Monad m] [LawfulMonad m] {xs : List α} {f : α → m β} : (wfParam xs).mapM f = xs.attach.unattach.mapM f

Full source

@[wf_preprocess] theorem mapM_wfParam [Monad m] [LawfulMonad m] {xs : List α} {f : α → m β} :
    (wfParam xs).mapM f = xs.attach.unattach.mapM f := by
  simp [wfParam]

Monadic Mapping over Well-Founded Parameter Equals Mapping over Attached List

Informal description

Let $m$ be a monad that satisfies the monad laws, and let $xs$ be a list of elements of type $\alpha$. For any function $f : \alpha \to m \beta$, the monadic mapping of $f$ over the well-founded parameter $xs$ is equal to the monadic mapping of $f$ over the unattached version of the attached list $xs$. In other words, the following equality holds: $$ \text{mapM}_m f (\text{wfParam}\ xs) = \text{mapM}_m f (\text{unattach}\ (\text{attach}\ xs)) $$

List.mapM_unattach theorem

 [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → m β} :
  xs.unattach.mapM f = xs.mapM fun ⟨x, h⟩ => binderNameHint x f <| binderNameHint h () <| f (wfParam x)

Full source

@[wf_preprocess] theorem mapM_unattach [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → m β} :
    xs.unattach.mapM f = xs.mapM fun ⟨x, h⟩ =>
      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
  simp [wfParam]

Equality of Monadic Mapping over Unattached List and Subtype List when Function Depends Only on Value

Informal description

Let $m$ be a lawful monad, $\alpha$ and $\beta$ be types, and $P : \alpha \to \text{Prop}$ be a predicate. For any list $xs$ of elements of the subtype $\{x : \alpha \mid P x\}$ and any function $f : \alpha \to m \beta$, the monadic mapping of $f$ over the unattached version of $xs$ is equal to the monadic mapping over $xs$ where each element $\langle x, h \rangle$ is mapped to $f(x)$. In symbols: $$\text{mapM}_m\ f\ (\text{unattach}\ xs) = \text{mapM}_m\ (\lambda \langle x, h \rangle \mapsto f(x))\ xs$$

List.filterMapM_subtype theorem

 [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → m (Option β)}
  {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) : l.filterMapM f = l.unattach.filterMapM g

Full source

@[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.filterMapM f = l.unattach.filterMapM g := by
  unfold unattach
  induction l with
  | nil => simp
  | cons a l ih => simp [ih, hf, filterMapM_cons]

Equality of Filter-Map Operations on Subtype and Unattached Lists

Informal description

Let $m$ be a monad that satisfies the monad laws, and let $p : \alpha \to \text{Prop}$ be a predicate on $\alpha$. For any list $l$ of elements of the subtype $\{x \mid p x\}$, and any functions $f : \{x \mid p x\} \to m (\text{Option}\ \beta)$ and $g : \alpha \to m (\text{Option}\ \beta)$ such that $f \langle x, h \rangle = g x$ for all $x \in \alpha$ and $h : p x$, the monadic filter-map operation satisfies: \[ l.\text{filterMapM}\ f = l.\text{unattach}.\text{filterMapM}\ g \]

List.filterMapM_wfParam theorem

 [Monad m] [LawfulMonad m] {xs : List α} {f : α → m (Option β)} :
  (wfParam xs).filterMapM f = xs.attach.unattach.filterMapM f

Full source

@[wf_preprocess] theorem filterMapM_wfParam [Monad m] [LawfulMonad m]
    {xs : List α} {f : α → m (Option β)} :
    (wfParam xs).filterMapM f = xs.attach.unattach.filterMapM f := by
  simp [wfParam]

Equality of Filter-Map Operations on Attached and Unattached Lists

Informal description

Let $m$ be a monad that satisfies the monad laws, $\alpha$ and $\beta$ be types, and $f : \alpha \to m (\text{Option}\ \beta)$ be a function. For any list $xs$ of elements of type $\alpha$, the monadic filter-map operation applied to $xs$ (tracked with `wfParam`) is equal to the monadic filter-map operation applied to the unattached version of the attached list $xs$. In symbols: $$ \text{filterMapM}\ f\ (\text{wfParam}\ xs) = \text{filterMapM}\ f\ (\text{unattach}\ (\text{attach}\ xs)) $$

List.filterMapM_unattach theorem

 [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → m (Option β)} :
  xs.unattach.filterMapM f = xs.filterMapM fun ⟨x, h⟩ => binderNameHint x f <| binderNameHint h () <| f (wfParam x)

Full source

@[wf_preprocess] theorem filterMapM_unattach [Monad m] [LawfulMonad m]
    {P : α → Prop} {xs : List (Subtype P)} {f : α → m (Option β)} :
    xs.unattach.filterMapM f = xs.filterMapM fun ⟨x, h⟩ =>
      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
  simp [wfParam]

Equality of Filter-Map Operations on Unattached and Subtype Lists

Informal description

Let $m$ be a monad that satisfies the monad laws, and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$. For any list $xs$ of elements of the subtype $\{x \mid P(x)\}$ and any monadic function $f : \alpha \to m (\text{Option}\ \beta)$, the monadic filter-map operation satisfies: \[ \text{unattach}(xs).\text{filterMapM}\ f = xs.\text{filterMapM}\ (\lambda \langle x, h \rangle \mapsto f\ x) \] where $\text{unattach}$ removes the proof component from each element of the list.

List.flatMapM_subtype theorem

 [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → m (List β)} {g : α → m (List β)}
  (hf : ∀ x h, f ⟨x, h⟩ = g x) : (l.flatMapM f) = l.unattach.flatMapM g

Full source

@[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.flatMapM f) = l.unattach.flatMapM g := by
  unfold unattach
  induction l with
  | nil => simp
  | cons a l ih => simp [ih, hf]

Equality of Monadic FlatMap on Subtype and Unattached List

Informal description

Let $m$ be a monad that satisfies the monad laws, and let $p : \alpha \to \text{Prop}$ be a predicate on $\alpha$. For any list $l$ of elements of the subtype $\{x \mid p(x)\}$, and any monadic functions $f : \{x \mid p(x)\} \to m (\text{List}\ \beta)$ and $g : \alpha \to m (\text{List}\ \beta)$ such that $f(\langle x, h \rangle) = g(x)$ for all $x \in \alpha$ and $h : p(x)$, we have: $$ \text{flatMapM}_f\ l = \text{flatMapM}_g\ (\text{unattach}\ l) $$ where $\text{unattach}$ removes the proof component from each element of the list.

List.flatMapM_wfParam theorem

 [Monad m] [LawfulMonad m] {xs : List α} {f : α → m (List β)} : (wfParam xs).flatMapM f = xs.attach.unattach.flatMapM f

Full source

@[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
    {xs : List α} {f : α → m (List β)} :
    (wfParam xs).flatMapM f = xs.attach.unattach.flatMapM f := by
  simp [wfParam]

Equality of `flatMapM` with `wfParam` and `attach`/`unattach`

Informal description

For any monad `m` that satisfies the monad laws, any list `xs` of elements of type `α`, and any monadic function `f : α → m (List β)`, the following equality holds: $$ \text{flatMapM} \, f \, (\text{wfParam} \, xs) = \text{flatMapM} \, f \, (\text{unattach} \, (\text{attach} \, xs)) $$ Here, `attach` adds proofs that each element is in the original list, and `unattach` removes these proofs, returning the original list. The function `wfParam` is an identity function used for tracking parameters in well-founded recursion.

List.flatMapM_unattach theorem

 [Monad m] [LawfulMonad m] {P : α → Prop} {xs : List (Subtype P)} {f : α → m (List β)} :
  xs.unattach.flatMapM f = xs.flatMapM fun ⟨x, h⟩ => binderNameHint x f <| binderNameHint h () <| f (wfParam x)

Full source

@[wf_preprocess] theorem flatMapM_unattach [Monad m] [LawfulMonad m]
    {P : α → Prop} {xs : List (Subtype P)} {f : α → m (List β)} :
    xs.unattach.flatMapM f = xs.flatMapM fun ⟨x, h⟩ =>
      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
  simp [wfParam]

Equality of Monadic FlatMap on Unattached Subtype List and Original List

Informal description

Let $m$ be a monad that satisfies the monad laws, and let $P : \alpha \to \text{Prop}$ be a predicate on $\alpha$. For any list $xs$ of elements of the subtype $\{x \mid P(x)\}$ and any monadic function $f : \alpha \to m (\text{List}\ \beta)$, we have: $$ \text{flatMapM}_f\ (\text{unattach}\ xs) = \text{flatMapM}_{x \mapsto f(x)}\ xs $$ where $\text{unattach}$ removes the proof component from each element of the list.