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 α) : mapM f l = 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 : α) : foldlM g init (map f l) = 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 : α) : foldrM g init (map f l) = 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 : γ) : foldlM g init (filterMap f l) = 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 : γ) : foldrM g init (filterMap f l) = 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 : β) : foldlM g init (filter p l) = 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 : β) : foldrM g init (filter p l) = 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} : forM f as = 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) : forM f (map g l) = 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) : forIn' as b f = forIn' bs b' g

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 <$> 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) = 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 (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)) = foldl (fun (b : β) (x : { x : α // x ∈ l }) => match x with | ⟨a, h⟩ => f a h b) init l.attach

@[simp]

theorem Array.forIn'_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (l : Array α) (g : α → β) (f : (b : β) → b ∈ map g l → γ → m (ForInStep γ)) : forIn' (map g l) init f = forIn' l init fun (a : α) (h : a ∈ l) (y : γ) => f (g a) ⋯ y

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 <$> 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) = 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 (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)) = foldl (fun (b : β) (a : α) => f a b) init l

@[simp]

theorem Array.forIn_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (l : Array α) (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (map g l) init f = forIn l init fun (a : α) (y : γ) => f (g a) y