Lemmas about vector iterators

This module provides lemmas about the interactions of Vector.iterM with IterM.step and various collectors.

theorem Vector.iterM_eq_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} : xs.iterM m = xs.iterFromIdxM m 0

theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_lt {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} (h : pos < n) : (xs.iterFromIdxM m pos).IsPlausibleStep (IterStep.yield (xs.iterFromIdxM m (pos + 1)) xs[pos])

theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdxM_of_not_lt {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} (h : ¬pos < n) : (xs.iterFromIdxM m pos).IsPlausibleStep IterStep.done

theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_pos {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} (h : 0 < n) : (xs.iterM m).IsPlausibleStep (IterStep.yield (xs.iterFromIdxM m 1) xs[0])

theorem Std.Iterators.Vector.isPlausibleStep_iterM_of_not_pos {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} (h : ¬0 < n) : (xs.iterM m).IsPlausibleStep IterStep.done

@[simp]

theorem Vector.iterFromIdxM_toArray {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : xs.toArray.iterFromIdxM m pos = xs.iterFromIdxM m pos

@[simp]

theorem Vector.iterM_toArray {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} : xs.toArray.iterM m = xs.iterM m

theorem Vector.step_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdxM m pos).step = pure (Std.Shrink.deflate (if h : pos < n then Std.PlausibleIterStep.yield (xs.iterFromIdxM m (pos + 1)) xs[pos] ⋯ else Std.PlausibleIterStep.done ⋯))

theorem Vector.step_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} {xs : Vector β n} : (xs.iterM m).step = pure (Std.Shrink.deflate (if h : 0 < n then Std.PlausibleIterStep.yield (xs.iterFromIdxM m 1) xs[0] ⋯ else Std.PlausibleIterStep.done ⋯))

theorem Vector.iterFromIdxM_equiv_iterM_drop_toList {n : Nat} {α : Type w} {xs : Vector α n} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {pos : Nat} : (xs.iterFromIdxM m pos).Equiv ((List.drop pos xs.toList).iterM m)

theorem Vector.iterM_equiv_iterM_toList {n : Nat} {α : Type w} {xs : Vector α n} {m : Type w → Type w'} [Monad m] [LawfulMonad m] : (xs.iterM m).Equiv (xs.toList.iterM m)

@[simp]

theorem Vector.toList_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} {pos : Nat} : (xs.iterFromIdxM m pos).toList = pure (List.drop pos xs.toList)

@[simp]

theorem Vector.toList_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} : (xs.iterM m).toList = pure xs.toList

@[simp]

theorem Vector.toArray_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} {pos : Nat} : (xs.iterFromIdxM m pos).toArray = pure (xs.toArray.extract pos n)

@[simp]

theorem Vector.toArray_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} : (xs.iterM m).toArray = pure xs.toArray

@[simp]

theorem Vector.toListRev_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} {pos : Nat} : (xs.iterFromIdxM m pos).toListRev = pure (List.drop pos xs.toList).reverse

@[simp]

theorem Vector.toListRev_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} : (xs.iterM m).toListRev = pure xs.toList.reverse

@[simp]

theorem Vector.length_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} {pos : Nat} : (xs.iterFromIdxM m pos).length = pure { down := n - pos }

@[simp]

theorem Vector.length_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {n : Nat} [LawfulMonad m] {xs : Vector β n} : (xs.iterM m).length = pure { down := n }