Lemmas about Vector.forIn' and Vector.forIn. #
Monadic operations #
mapM #
foldlM and foldrM #
theorem
Vector.foldlM_filterMap
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_1}
{n : Nat}
[Monad m]
[LawfulMonad m]
(f : α → Option β)
(g : γ → β → m γ)
(xs : Vector α n)
(init : γ)
:
Array.foldlM g init (Array.filterMap f xs.toArray) = foldlM
(fun (x : γ) (y : α) =>
match f y with
| some b => g x b
| none => pure x)
init xs
theorem
Vector.foldrM_filterMap
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_1}
{n : Nat}
[Monad m]
[LawfulMonad m]
(f : α → Option β)
(g : β → γ → m γ)
(xs : Vector α n)
(init : γ)
:
Array.foldrM g init (Array.filterMap f xs.toArray) = foldrM
(fun (x : α) (y : γ) =>
match f x with
| some b => g b y
| none => pure y)
init xs
theorem
Vector.foldlM_filter
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{n : Nat}
[Monad m]
[LawfulMonad m]
(p : α → Bool)
(g : β → α → m β)
(xs : Vector α n)
(init : β)
:
theorem
Vector.foldrM_filter
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{n : Nat}
[Monad m]
[LawfulMonad m]
(p : α → Bool)
(g : α → β → m β)
(xs : Vector α n)
(init : β)
:
forM #
forIn' #
theorem
Vector.forIn'_congr
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β : Type u_1}
[Monad m]
{xs ys : Vector α n}
(w : xs = ys)
{b b' : β}
(hb : b = b')
{f : (a' : α) → a' ∈ xs → β → m (ForInStep β)}
{g : (a' : α) → a' ∈ ys → β → m (ForInStep β)}
(h : ∀ (a : α) (m_1 : a ∈ ys) (b : β), f a ⋯ b = g a m_1 b)
:
theorem
Vector.forIn'_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(xs : Vector α n)
(f : (a : α) → a ∈ xs → β → m (ForInStep β))
(init : β)
:
forIn' xs init f = ForInStep.value <$> foldlM
(fun (b : ForInStep β) (x : { x : α // x ∈ xs }) =>
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) xs.attach
We can express a for loop over a vector as a fold,
in which whenever we reach .done b we keep that value through the rest of the fold.
@[simp]
theorem
Vector.forIn'_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
(xs : Vector α n)
(f : (a : α) → a ∈ xs → β → m γ)
(g : (a : α) → a ∈ xs → β → γ → β)
(init : β)
:
We can express a for loop over a vector which always yields as a fold.
theorem
Vector.forIn'_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(xs : Vector α n)
(f : (a : α) → a ∈ xs → β → β)
(init : β)
:
theorem
Vector.forIn_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
{n : Nat}
[Monad m]
[LawfulMonad m]
(f : α → β → m (ForInStep β))
(init : β)
(xs : Vector α n)
:
forIn xs 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) xs
We can express a for loop over a vector as a fold,
in which whenever we reach .done b we keep that value through the rest of the fold.
@[simp]
theorem
Vector.forIn_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
(xs : Vector α n)
(f : α → β → m γ)
(g : α → β → γ → β)
(init : β)
:
We can express a for loop over a vector which always yields as a fold.
theorem
Vector.forIn_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{n : Nat}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(xs : Vector α n)
(f : α → β → β)
(init : β)
:
@[simp]
theorem
Vector.forIn_yield_eq_foldl
{α : Type u_1}
{n : Nat}
{β : Type u_2}
(xs : Vector α n)
(f : α → β → β)
(init : β)
:
(forIn xs init fun (a : α) (b : β) => ForInStep.yield (f a b)) = foldl (fun (b : β) (a : α) => f a b) init xs