# Lemmas about `Vector.forIn'` and `Vector.forIn`. #

## Monadic operations #

source
theorem Vector.map_toArray_inj {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {xs ys : m (Vector α n)} :
toArray <$> xs = toArray <$> ys ↔ xs = ys

### mapM #

source
@[simp]
theorem Vector.mapM_pure {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
mapM (fun (x : α) => pure (f x)) xs = pure (map f xs)
source
@[simp]
theorem Vector.mapM_map {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : α → β} {g : β → m γ} {xs : Vector α n} :
mapM g (map f xs) = mapM (g ∘ f) xs
source
theorem Vector.mapM_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) {f : α → m β} :
mapM f xs = mapM f ys
source
@[simp]
theorem Vector.mapM_mk_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → m β} :
mapM f #v[] = pure #v[]
source
@[simp]
theorem Vector.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n n' : Nat} [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} {ys : Vector α n'} :
mapM f (xs ++ ys) = do let __do_lift ← mapM f xs let __do_lift_1 ← mapM f ys pure (__do_lift ++ __do_lift_1)

### foldlM and foldrM #

source
theorem Vector.foldlM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : Nat} [Monad m] {f : β₁ → β₂} {g : α → β₂ → m α} {xs : Vector β₁ n} {init : α} :
foldlM g init (map f xs) = foldlM (fun (x : α) (y : β₁) => g x (f y)) init xs
source
theorem Vector.foldrM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : β₁ → β₂} {g : β₂ → α → m α} {xs : Vector β₁ n} {init : α} :
foldrM g init (map f xs) = foldrM (fun (x : β₁) (y : α) => g (f x) y) init xs
source
@[simp]
theorem Vector.foldlM_attachWith {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] {xs : Vector α n} {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : β → { x : α // q x } → m β} {b : β} :
foldlM f b (xs.attachWith q H) = foldlM (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => f b ⟨a, ⋯⟩) b xs.attach
source
@[simp]
theorem Vector.foldrM_attachWith {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} {q : α → Prop} (H : ∀ (a : α), a ∈ xs → q a) {f : { x : α // q x } → β → m β} {b : β} :
foldrM f b (xs.attachWith q H) = foldrM (fun (a : { x : α // x ∈ xs }) (acc : β) => f ⟨a.val, ⋯⟩ acc) b xs.attach

### forM #

source
theorem Vector.forM_congr {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} [Monad m] {as bs : Vector α n} (w : as = bs) {f : α → m PUnit} :
forM as f = forM bs f
source
@[simp]
theorem Vector.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} {n n' : Nat} [Monad m] [LawfulMonad m] {xs : Vector α n} {ys : Vector α n'} {f : α → m PUnit} :
forM (xs ++ ys) f = do forM xs f forM ys f
source
@[simp]
theorem Vector.forM_map {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_4} [Monad m] [LawfulMonad m] {xs : Vector α n} {g : α → β} {f : β → m PUnit} :
forM (map g xs) f = forM xs fun (a : α) => f (g a)

### forIn' #

source
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) :
forIn' xs b f = forIn' ys b' g
source
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.

source
@[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 : β) :
(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 a vector which always yields as a fold.

source
@[simp]
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 : β) :
(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)
source
theorem Vector.idRun_forIn'_yield_eq_foldl {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) :
(forIn' xs init fun (a : α) (m : a ∈ xs) (b : β) => ForInStep.yield <$> f a m b).run = foldl (fun (b : β) (x : { x : α // x ∈ xs }) => match x with | ⟨a, h⟩ => (f a h b).run) init xs.attach
source
@[deprecated Vector.forIn'_yield_eq_foldl (since := "2025-05-21")]
theorem Vector.forIn'_yield_eq_foldl {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} (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
source
@[simp]
theorem Vector.forIn'_map {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Vector α n} (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
source
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 : α → β → m (ForInStep β)) (init : β) :
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.

source
@[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 : β) :
(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 a vector which always yields as a fold.

source
@[simp]
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 : β) :
(forIn xs init fun (a : α) (b : β) => pure (ForInStep.yield (f a b))) = pure (foldl (fun (b : β) (a : α) => f a b) init xs)
source
theorem Vector.idRun_forIn_yield_eq_foldl {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} (f : α → β → Id β) (init : β) :
(forIn xs init fun (a : α) (b : β) => ForInStep.yield <$> f a b).run = foldl (fun (b : β) (a : α) => (f a b).run) init xs
source
@[deprecated Vector.idRun_forIn_yield_eq_foldl (since := "2025-05-21")]
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
source
@[simp]
theorem Vector.forIn_map {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) :
forIn (map g xs) init f = forIn xs init fun (a : α) (y : γ) => f (g a) y

### allM and anyM #

source
@[simp]
theorem Vector.anyM_pure {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n} :
anyM (fun (x : α) => pure (p x)) xs = pure (xs.any p)
source
@[simp]
theorem Vector.allM_pure {m : Type → Type u_1} {α : Type u_2} {n : Nat} [Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n} :
allM (fun (x : α) => pure (p x)) xs = pure (xs.all p)

### findM? and findSomeM? #

source
theorem Vector.findM?_pure {α : Type} {n : Nat} {m : Type → Type} [Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n} :
findM? (fun (x : α) => pure (p x)) xs = pure (find? p xs)
source
@[simp]
theorem Vector.findSomeM?_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] {f : α → Option β} {xs : Vector α n} :
findSomeM? (fun (x : α) => pure (f x)) xs = pure (findSome? f xs)