Monadic operations #
mapM #
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.
Equations
- List.mapM' f [] = pure []
- List.mapM' f (a :: l) = do let __do_lift ← f a let __do_lift_1 ← List.mapM' f l pure (__do_lift :: __do_lift_1)
theorem
List.foldlM_cons_eq_append
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{f : α → m β}
{as : List α}
{b : β}
{bs : List β}
:
Auxiliary lemma for mapM_eq_reverse_foldlM_cons.
filterMapM #
theorem
List.filterMapM_loop_eq
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{f : α → m (Option β)}
{l : List α}
{acc : List β}
:
@[simp]
theorem
List.filterMapM_cons
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{a : α}
{l : List α}
[Monad m]
[LawfulMonad m]
{f : α → m (Option β)}
:
filterMapM f (a :: l) = do
let __do_lift ← f a
match __do_lift with
| none => filterMapM f l
| some b => do
let __do_lift ← filterMapM f l
pure (b :: __do_lift)
flatMapM #
foldlM and foldrM #
theorem
List.foldlM_filterMap
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_1}
[Monad m]
[LawfulMonad m]
{f : α → Option β}
{g : γ → β → m γ}
{l : List α}
{init : γ}
:
theorem
List.foldrM_filterMap
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_1}
[Monad m]
[LawfulMonad m]
{f : α → Option β}
{g : β → γ → m γ}
{l : List α}
{init : γ}
:
forM #
forIn' #
theorem
List.forIn'_loop_congr
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{xs : List α}
[Monad m]
{as bs : List α}
{f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
{g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
{b : β}
(ha : ∃ (ys : List α), ys ++ xs = as)
(hb : ∃ (ys : List α), ys ++ xs = bs)
(h : ∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b)
:
@[simp]
theorem
List.forIn'_cons
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
{a : α}
{as : List α}
(f : (a' : α) → a' ∈ a :: as → β → m (ForInStep β))
(b : β)
:
forIn' (a :: as) b f = do
let x ← f a ⋯ b
match x with
| ForInStep.done b => pure b
| ForInStep.yield b => forIn' as b fun (a' : α) (m : a' ∈ as) (b : β) => f a' ⋯ b
theorem
List.forIn'_congr
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[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_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b)
:
theorem
List.forIn'_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : (a : α) → a ∈ l → β → m (ForInStep β))
(init : β)
:
forIn' l init f = ForInStep.value <$> foldlM
(fun (b : ForInStep β) (x : { x : α // x ∈ l }) =>
match x with
| ⟨a, m_1⟩ =>
match b with
| ForInStep.yield b => f a m_1 b
| ForInStep.done b => pure (ForInStep.done b))
(ForInStep.yield init) l.attach
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.
@[simp]
theorem
List.forIn'_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : (a : α) → a ∈ l → β → m γ)
(g : (a : α) → a ∈ l → β → γ → β)
(init : β)
:
We can express a for loop over a list which always yields as a fold.
@[simp]
theorem
List.forIn'_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : (a : α) → a ∈ l → β → β)
(init : β)
:
@[simp]
@[simp]
theorem
List.forIn_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : α → β → m (ForInStep β))
(init : β)
:
forIn l init f = ForInStep.value <$> foldlM
(fun (b : ForInStep β) (a : α) =>
match b with
| ForInStep.yield b => f a b
| ForInStep.done b => pure (ForInStep.done b))
(ForInStep.yield init) l
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.
@[simp]
theorem
List.forIn_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : α → β → m γ)
(g : α → β → γ → β)
(init : β)
:
We can express a for loop over a list which always yields as a fold.
@[simp]
theorem
List.forIn_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{l : List α}
(f : α → β → β)
(init : β)
:
@[simp]
theorem
List.forIn_yield_eq_foldl
{α : Type u_1}
{β : Type u_2}
{l : List α}
(f : α → β → β)
(init : β)
:
(forIn l init fun (a : α) (b : β) => ForInStep.yield (f a b)) = foldl (fun (b : β) (a : α) => f a b) init l
allM and anyM #
Recognizing higher order functions using a function that only depends on the value. #
@[simp]
theorem
List.foldlM_subtype
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
{p : α → Prop}
{l : List { x : α // p x }}
{f : β → { x : α // p x } → m β}
{g : β → α → m β}
{x : β}
(hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x)
:
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.
theorem
List.foldlM_unattach
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
{P : α → Prop}
{xs : List (Subtype P)}
{f : β → α → m β}
{init : β}
:
foldlM f init xs.unattach = foldlM
(fun (b : β) (x : Subtype P) =>
match x with
| ⟨x, h⟩ => binderNameHint b f (binderNameHint x (f b) (binderNameHint h () (f b (wfParam x)))))
init xs
@[simp]
theorem
List.foldrM_subtype
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{p : α → Prop}
{l : List { x : α // p x }}
{f : { x : α // p x } → β → m β}
{g : α → β → m β}
{x : β}
(hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b)
:
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.
theorem
List.foldrM_unattach
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{P : α → Prop}
{xs : List (Subtype P)}
{f : α → β → m β}
{init : β}
:
foldrM f init xs.unattach = foldrM
(fun (x : Subtype P) (b : β) =>
match x with
| ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (binderNameHint b (f x) (f (wfParam x) b))))
init xs
@[simp]
theorem
List.mapM_subtype
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{p : α → Prop}
{l : List { x : α // p x }}
{f : { x : α // p x } → m β}
{g : α → m β}
(hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x)
:
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.
theorem
List.mapM_unattach
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{P : α → Prop}
{xs : List (Subtype P)}
{f : α → m β}
:
mapM f xs.unattach = mapM
(fun (x : Subtype P) =>
match x with
| ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
xs
theorem
List.filterMapM_wfParam
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{xs : List α}
{f : α → m (Option β)}
:
theorem
List.filterMapM_unattach
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{P : α → Prop}
{xs : List (Subtype P)}
{f : α → m (Option β)}
:
filterMapM f xs.unattach = filterMapM
(fun (x : Subtype P) =>
match x with
| ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
xs
@[simp]
theorem
List.flatMapM_unattach
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
{P : α → Prop}
{xs : List (Subtype P)}
{f : α → m (List β)}
:
flatMapM f xs.unattach = flatMapM
(fun (x : Subtype P) =>
match x with
| ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
xs