Lemmas about Vector.forIn' and Vector.forIn.

Monadic operations

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

@[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)

@[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

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

@[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[]

@[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

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

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

@[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

@[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

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

@[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

@[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'

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

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.

@[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.

@[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)

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

@[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

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.

@[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.

@[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)

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

@[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

@[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)

@[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?

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)

@[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)