Lemmas about Array.forIn' and Array.forIn. #
Monadic operations #
mapM #
theorem
Array.mapM_eq_foldlM_push
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → m β)
(l : Array α)
:
Array.mapM f l = Array.foldlM
(fun (acc : Array β) (a : α) => do
let __do_lift ← f a
pure (acc.push __do_lift))
#[] l
foldlM and foldrM #
theorem
Array.foldlM_map
{m : Type u_1 → Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{α : Type u_1}
[Monad m]
(f : β₁ → β₂)
(g : α → β₂ → m α)
(l : Array β₁)
(init : α)
:
Array.foldlM g init (Array.map f l) = Array.foldlM (fun (x : α) (y : β₁) => g x (f y)) init l
theorem
Array.foldrM_map
{m : Type u_1 → Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(f : β₁ → β₂)
(g : β₂ → α → m α)
(l : Array β₁)
(init : α)
:
Array.foldrM g init (Array.map f l) = Array.foldrM (fun (x : β₁) (y : α) => g (f x) y) init l
theorem
Array.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 : Array α)
(init : γ)
:
Array.foldlM g init (Array.filterMap f l) = Array.foldlM
(fun (x : γ) (y : α) =>
match f y with
| some b => g x b
| none => pure x)
init l
theorem
Array.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 : Array α)
(init : γ)
:
Array.foldrM g init (Array.filterMap f l) = Array.foldrM
(fun (x : α) (y : γ) =>
match f x with
| some b => g b y
| none => pure y)
init l
theorem
Array.foldlM_filter
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(p : α → Bool)
(g : β → α → m β)
(l : Array α)
(init : β)
:
Array.foldlM g init (Array.filter p l) = Array.foldlM (fun (x : β) (y : α) => if p y = true then g x y else pure x) init l
theorem
Array.foldrM_filter
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(p : α → Bool)
(g : α → β → m β)
(l : Array α)
(init : β)
:
Array.foldrM g init (Array.filter p l) = Array.foldrM (fun (x : α) (y : β) => if p x = true then g x y else pure y) init l
forM #
theorem
Array.forM_congr
{m : Type u_1 → Type u_2}
{α : Type u_3}
[Monad m]
{as bs : Array α}
(w : as = bs)
{f : α → m PUnit}
:
Array.forM f as = Array.forM f bs
@[simp]
theorem
Array.forM_map
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_4}
[Monad m]
[LawfulMonad m]
(l : Array α)
(g : α → β)
(f : β → m PUnit)
:
Array.forM f (Array.map g l) = Array.forM (fun (a : α) => f (g a)) l
forIn' #
theorem
Array.forIn'_congr
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
{as bs : Array α}
(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
Array.forIn'_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : Array α)
(f : (a : α) → a ∈ l → β → m (ForInStep β))
(init : β)
:
forIn' l init f = ForInStep.value <$> Array.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 an array as a fold,
in which whenever we reach .done b we keep that value through the rest of the fold.
@[simp]
theorem
Array.forIn'_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
(l : Array α)
(f : (a : α) → a ∈ l → β → m γ)
(g : (a : α) → a ∈ l → β → γ → β)
(init : β)
:
(forIn' l init fun (a : α) (m_1 : a ∈ l) (b : β) => (fun (c : γ) => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = Array.foldlM
(fun (b : β) (x : { x : α // x ∈ l }) =>
match x with
| ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
init l.attach
We can express a for loop over an array which always yields as a fold.
theorem
Array.forIn'_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : Array α)
(f : (a : α) → a ∈ l → β → β)
(init : β)
:
(forIn' l init fun (a : α) (m_1 : a ∈ l) (b : β) => pure (ForInStep.yield (f a m_1 b))) = pure
(Array.foldl
(fun (b : β) (x : { x : α // x ∈ l }) =>
match x with
| ⟨a, h⟩ => f a h b)
init l.attach)
@[simp]
theorem
Array.forIn'_yield_eq_foldl
{α : Type u_1}
{β : Type u_2}
(l : Array α)
(f : (a : α) → a ∈ l → β → β)
(init : β)
:
(forIn' l init fun (a : α) (m : a ∈ l) (b : β) => ForInStep.yield (f a m b)) = Array.foldl
(fun (b : β) (x : { x : α // x ∈ l }) =>
match x with
| ⟨a, h⟩ => f a h b)
init l.attach
theorem
Array.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 : Array α)
:
forIn l init f = ForInStep.value <$> Array.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 an array as a fold,
in which whenever we reach .done b we keep that value through the rest of the fold.
@[simp]
theorem
Array.forIn_yield_eq_foldlM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β γ : Type u_1}
[Monad m]
[LawfulMonad m]
(l : Array α)
(f : α → β → m γ)
(g : α → β → γ → β)
(init : β)
:
(forIn l init fun (a : α) (b : β) => (fun (c : γ) => ForInStep.yield (g a b c)) <$> f a b) = Array.foldlM (fun (b : β) (a : α) => g a b <$> f a b) init l
We can express a for loop over an array which always yields as a fold.
theorem
Array.forIn_pure_yield_eq_foldl
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(l : Array α)
(f : α → β → β)
(init : β)
:
(forIn l init fun (a : α) (b : β) => pure (ForInStep.yield (f a b))) = pure (Array.foldl (fun (b : β) (a : α) => f a b) init l)
@[simp]
theorem
Array.forIn_yield_eq_foldl
{α : Type u_1}
{β : Type u_2}
(l : Array α)
(f : α → β → β)
(init : β)
:
(forIn l init fun (a : α) (b : β) => ForInStep.yield (f a b)) = Array.foldl (fun (b : β) (a : α) => f a b) init l