Lemmas about Array.forIn' and Array.forIn.

Monadic operations

mapM

@[simp]

theorem Array.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : Array α} : mapM f (l₁ ++ l₂) = do let __do_lift ← mapM f l₁ let __do_lift_1 ← mapM f l₂ pure (__do_lift ++ __do_lift_1)

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} {stop : Nat} [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) (w : stop = l.size) : foldlM g init (map f l) 0 stop = foldlM (fun (x : α) (y : β₁) => g x (f y)) init l 0 stop

theorem Array.foldrM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {start : Nat} [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁) (init : α) (w : start = l.size) : foldrM g init (map f l) start = foldrM (fun (x : β₁) (y : α) => g (f x) y) init l start

theorem Array.foldlM_filterMap {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {stop : Nat} [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) (w : stop = (filterMap f l).size) : foldlM g init (filterMap f l) 0 stop = 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} {start : Nat} [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) (w : start = (filterMap f l).size) : foldrM g init (filterMap f l) start = 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} {stop : Nat} [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) (w : stop = (filter p l).size) : foldlM g init (filter p l) 0 stop = 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} {start : Nat} [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) (w : start = (filter p l).size) : foldrM g init (filter p l) start = foldrM (fun (x : α) (y : β) => if p x = true then g x y else pure y) init l

@[simp]

theorem Array.foldlM_attachWith {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] (l : Array α) {q : α → Prop} (H : ∀ (a : α), a ∈ l → q a) {f : β → { x : α // q x } → m β} {b : β} (w : stop = l.size) : foldlM f b (l.attachWith q H) 0 stop = foldlM (fun (b : β) (x : { x : α // x ∈ l }) => match x with | ⟨a, h⟩ => f b ⟨a, ⋯⟩) b l.attach

@[simp]

theorem Array.foldrM_attachWith {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : Nat} [Monad m] [LawfulMonad m] (l : Array α) {q : α → Prop} (H : ∀ (a : α), a ∈ l → q a) {f : { x : α // q x } → β → m β} {b : β} (w : start = l.size) : foldrM f b (l.attachWith q H) start = foldrM (fun (a : { x : α // x ∈ l }) (acc : β) => f ⟨a.val, ⋯⟩ acc) b l.attach

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 as f = forM bs f

@[simp]

theorem Array.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] [LawfulMonad m] (l₁ l₂ : Array α) (f : α → m PUnit) : forM (l₁ ++ l₂) f = do forM l₁ f forM l₂ f

@[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 (map g l) f = forM l fun (a : α) => f (g a)

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

Recognizing higher order functions using a function that only depends on the value.

@[simp]

theorem Array.foldlM_subtype {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] {p : α → Prop} {l : Array { x : α // p x }} {f : β → { x : α // p x } → m β} {g : β → α → m β} {x : β} (hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) (w : stop = l.size) : foldlM f x l 0 stop = foldlM g x l.unattach 0 stop

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 Array.foldrM_subtype {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : Nat} [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → β → m β} {g : α → β → m β} {x : β} (hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) (w : start = l.size) : foldrM f x l start = foldrM g x l.unattach start

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 Array.mapM_subtype {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → m β} {g : α → m β} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : mapM f l = mapM g l.unattach

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.