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_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_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 : γ)
:
List.foldlM g init (filterMap f l) = List.foldlM
(fun (x : γ) (y : α) =>
match f y with
| some b => g x b
| none => pure x)
init l
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 : γ)
:
theorem
List.foldlM_filter
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(p : α → Bool)
(g : β → α → m β)
(l : List α)
(init : β)
:
List.foldlM g init (filter p l) = List.foldlM (fun (x : β) (y : α) => if p y = true then g x y else pure x) init l
@[simp]
theorem
List.foldlM_attachWith
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(l : List α)
{q : α → Prop}
(H : ∀ (a : α), a ∈ l → q a)
{f : β → { x : α // q x } → m β}
{b : β}
:
List.foldlM f b (l.attachWith q H) = List.foldlM
(fun (b : β) (x : { x : α // x ∈ l }) =>
match x with
| ⟨a, h⟩ => f b ⟨a, ⋯⟩)
b l.attach
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 <$> List.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 <$> List.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 : β)
:
(forIn l init fun (a : α) (b : β) => (fun (c : γ) => ForInStep.yield (g a b c)) <$> f a b) = List.foldlM (fun (b : β) (a : α) => g a b <$> f a b) init l
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.
@[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.
@[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.
@[simp]
@[simp]