Monadic operations #
mapM #
Alternate (non-tail-recursive) form of mapM for proofs.
Note that we can not have this as the main definition and replace it using a @[csimp] lemma,
because they are only 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)
Instances For
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.
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]
(f : α → β → m (ForInStep β))
(init : β)
(l : List α)
:
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.
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 #
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 β)
:
(fun (init : β) => foldlM f init xs.unattach) = fun (init : β) =>
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 β)
:
(fun (init : β) => foldrM f init xs.unattach) = fun (init : β) =>
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