Lemmas about Array.forIn' and Array.forIn.

Monadic operations

mapM

@[simp]

theorem Array.mapM_id {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Id β} : mapM f xs = map f xs

@[simp]

theorem Array.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) {xs ys : Array α} : mapM f (xs ++ ys) = do let __do_lift ← mapM f xs let __do_lift_1 ← mapM f ys 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 β) (xs : Array α) : mapM f xs = foldlM (fun (acc : Array β) (a : α) => do let __do_lift ← f a pure (acc.push __do_lift)) #[] xs

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 α) (xs : Array β₁) (init : α) (w : stop = xs.size) : foldlM g init (map f xs) 0 stop = foldlM (fun (x : α) (y : β₁) => g x (f y)) init xs 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 α) (xs : Array β₁) (init : α) (w : start = xs.size) : foldrM g init (map f xs) start = foldrM (fun (x : β₁) (y : α) => g (f x) y) init xs 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 γ) (xs : Array α) (init : γ) (w : stop = (filterMap f xs).size) : foldlM g init (filterMap f xs) 0 stop = foldlM (fun (x : γ) (y : α) => match f y with | some b => g x b | none => pure x) init xs

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 γ) (xs : Array α) (init : γ) (w : start = (filterMap f xs).size) : foldrM g init (filterMap f xs) start = foldrM (fun (x : α) (y : γ) => match f x with | some b => g b y | none => pure y) init xs

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 β) (xs : Array α) (init : β) (w : stop = (filter p xs).size) : foldlM g init (filter p xs) 0 stop = foldlM (fun (x : β) (y : α) => if p y = true then g x y else pure x) init xs

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 β) (xs : Array α) (init : β) (w : start = (filter p xs).size) : foldrM g init (filter p xs) start = foldrM (fun (x : α) (y : β) => if p x = true then g x y else pure y) init xs

@[simp]

theorem Array.foldlM_attachWith {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] (xs : Array α) {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : β → { x : α // q x } → m β} {b : β} (w : stop = xs.size) : foldlM f b (xs.attachWith q H) 0 stop = foldlM (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => f b ⟨a, ⋯⟩) b xs.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] (xs : Array α) {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : { x : α // q x } → β → m β} {b : β} (w : start = xs.size) : foldrM f b (xs.attachWith q H) start = foldrM (fun (a : { x : α // x ∈ xs }) (acc : β) => f ⟨a.val, ⋯⟩ acc) b xs.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] (xs ys : Array α) (f : α → m PUnit) : forM (xs ++ ys) f = do forM xs f forM ys f

@[simp]

theorem Array.forM_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] [LawfulMonad m] (xs : Array α) (g : α → β) (f : β → m PUnit) : forM (map g xs) f = forM xs 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] (xs : Array α) (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 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] (xs : Array α) (f : (a : α) → a ∈ xs → β → m γ) (g : (a : α) → a ∈ xs → β → γ → β) (init : β) : (forIn' xs init fun (a : α) (m_1 : a ∈ xs) (b : β) => (fun (c : γ) => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) = foldlM (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b) init xs.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] (xs : Array α) (f : (a : α) → a ∈ xs → β → β) (init : β) : (forIn' xs init fun (a : α) (m_1 : a ∈ xs) (b : β) => pure (ForInStep.yield (f a m_1 b))) = pure (foldl (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => f a h b) init xs.attach)

@[simp]

theorem Array.forIn'_yield_eq_foldl {α : Type u_1} {β : Type u_2} (xs : Array α) (f : (a : α) → a ∈ xs → β → β) (init : β) : (forIn' xs init fun (a : α) (m : a ∈ xs) (b : β) => ForInStep.yield (f a m b)) = foldl (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => f a h b) init xs.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] (xs : Array α) (g : α → β) (f : (b : β) → b ∈ map g xs → γ → m (ForInStep γ)) : forIn' (map g xs) init f = forIn' xs init fun (a : α) (h : a ∈ xs) (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 : β) (xs : Array α) : 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 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] (xs : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn xs 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 xs

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] (xs : Array α) (f : α → β → β) (init : β) : (forIn xs init fun (a : α) (b : β) => pure (ForInStep.yield (f a b))) = pure (foldl (fun (b : β) (a : α) => f a b) init xs)

@[simp]

theorem Array.forIn_yield_eq_foldl {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β → β) (init : β) : (forIn xs init fun (a : α) (b : β) => ForInStep.yield (f a b)) = foldl (fun (b : β) (a : α) => f a b) init xs

@[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] (xs : Array α) (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (map g xs) init f = forIn xs init fun (a : α) (y : γ) => f (g a) y

theorem List.filterM_toArray {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) : Array.filterM p l.toArray = toArray <$> filterM p l

@[simp]

theorem List.filterM_toArray' {m : Type → Type u_1} {α : Type} {stop : Nat} [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) (w : stop = l.length) : Array.filterM p l.toArray 0 stop = toArray <$> filterM p l

Variant of filterM_toArray with a side condition for the stop position.

theorem List.filterRevM_toArray {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) : Array.filterRevM p l.toArray = toArray <$> filterRevM p l

@[simp]

theorem List.filterRevM_toArray' {m : Type → Type u_1} {α : Type} {start : Nat} [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) (w : start = l.length) : Array.filterRevM p l.toArray start = toArray <$> filterRevM p l

Variant of filterRevM_toArray with a side condition for the start position.

theorem List.filterMapM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) : Array.filterMapM f l.toArray = toArray <$> filterMapM f l

@[simp]

theorem List.filterMapM_toArray' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) (w : stop = l.length) : Array.filterMapM f l.toArray 0 stop = toArray <$> filterMapM f l

Variant of filterMapM_toArray with a side condition for the stop position.

@[simp]

theorem List.flatMapM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) : Array.flatMapM f l.toArray = toArray <$> flatMapM (fun (a : α) => Array.toList <$> f a) l

theorem Array.filterM_congr {m : Type → Type u_1} {α : Type} [Monad m] {as bs : Array α} (w : as = bs) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) : filterM p as = filterM q bs

theorem Array.filterRevM_congr {m : Type → Type u_1} {α : Type} [Monad m] {as bs : Array α} (w : as = bs) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) : filterRevM p as = filterRevM q bs

theorem Array.filterMapM_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {as bs : Array α} (w : as = bs) {f g : α → m (Option β)} (h : ∀ (a : α), f a = g a) : filterMapM f as = filterMapM g bs

theorem Array.flatMapM_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {as bs : Array α} (w : as = bs) {f g : α → m (Array β)} (h : ∀ (a : α), f a = g a) : flatMapM f as = flatMapM g bs

theorem Array.toList_filterM {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (xs : Array α) (p : α → m Bool) : toList <$> filterM p xs = List.filterM p xs.toList

theorem Array.toList_filterRevM {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] (xs : Array α) (p : α → m Bool) : toList <$> filterRevM p xs = List.filterRevM p xs.toList

theorem Array.toList_filterMapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → m (Option β)) : toList <$> filterMapM f xs = List.filterMapM f xs.toList

theorem Array.toList_flatMapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → m (Array β)) : toList <$> flatMapM f xs = List.flatMapM (fun (a : α) => toList <$> f a) xs.toList

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} {xs : 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 = xs.size) : foldlM f x xs 0 stop = foldlM g x xs.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.

theorem Array.foldlM_wfParam {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (xs : Array α) (f : β → α → m β) : (fun (init : β) => foldlM f init (wfParam xs)) = fun (init : β) => foldlM f init xs.attach.unattach

theorem Array.foldlM_unattach {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (P : α → Prop) (xs : Array (Subtype P)) (f : β → α → m β) : (fun (init : β) => foldlM f init xs.unattach) = fun (init : β) => foldlM (fun (b : β) (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint b f (binderNameHint x (f b) (binderNameHint h () (f b (wfParam x))))) init xs

@[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} {xs : 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 = xs.size) : foldrM f x xs start = foldrM g x xs.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.

theorem Array.foldrM_wfParam {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → β → m β) : (fun (init : β) => foldrM f init (wfParam xs)) = fun (init : β) => foldrM f init xs.attach.unattach

theorem Array.foldrM_unattach {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → β → m β) : (fun (init : β) => foldrM f init xs.unattach) = fun (init : β) => foldrM (fun (x : Subtype P) (b : β) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (binderNameHint b (f x) (f (wfParam x) b)))) init xs

@[simp]

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

theorem Array.mapM_wfParam {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → m β) : mapM f (wfParam xs) = mapM f xs.attach.unattach

theorem Array.mapM_unattach {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → m β) : mapM f xs.unattach = mapM (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs

@[simp]

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

theorem Array.filterMapM_wfParam {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → m (Option β)) : filterMapM f (wfParam xs) = filterMapM f xs.attach.unattach

theorem Array.filterMapM_unattach {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → m (Option β)) : filterMapM f xs.unattach = filterMapM (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs

@[simp]

theorem Array.flatMapM_subtype {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → m (Array β)} {g : α → m (Array β)} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : flatMapM f xs = flatMapM g xs.unattach

theorem Array.flatMapM_wfParam {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (f : α → m (Array β)) : flatMapM f (wfParam xs) = flatMapM f xs.attach.unattach

theorem Array.flatMapM_unattach {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → m (Array β)) : flatMapM f xs.unattach = flatMapM (fun (x : Subtype P) => match x with | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x)))) xs