Lemmas about vector iterators

This module provides lemmas about the interactions of Vector.iter with Iter.step and various collectors.

theorem Vector.iter_eq_toIter_iterM {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter = (xs.iterM Id).toIter

theorem Vector.iter_eq_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter = xs.iterFromIdx 0

theorem Vector.iterFromIdx_eq_toIter_iterFromIdxM {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : xs.iterFromIdx pos = (xs.iterFromIdxM Id pos).toIter

theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_lt {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} (h : pos < n) : (xs.iterFromIdx pos).IsPlausibleStep (IterStep.yield (xs.iterFromIdx (pos + 1)) xs[pos])

theorem Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_not_lt {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} (h : ¬pos < n) : (xs.iterFromIdx pos).IsPlausibleStep IterStep.done

theorem Std.Iterators.Vector.isPlausibleStep_iter_of_pos {β : Type w} {n : Nat} {xs : Vector β n} (h : 0 < n) : xs.iter.IsPlausibleStep (IterStep.yield (xs.iterFromIdx 1) xs[0])

theorem Std.Iterators.Vector.isPlausibleStep_iter_of_not_pos {β : Type w} {n : Nat} {xs : Vector β n} (h : ¬0 < n) : xs.iter.IsPlausibleStep IterStep.done

@[simp]

theorem Vector.iterFromIdx_toArray {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : xs.toArray.iterFromIdx pos = xs.iterFromIdx pos

@[simp]

theorem Vector.iter_toArray {β : Type w} {n : Nat} {xs : Vector β n} : xs.toArray.iter = xs.iter

theorem Vector.step_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdx pos).step = if h : pos < n then Std.PlausibleIterStep.yield (xs.iterFromIdx (pos + 1)) xs[pos] ⋯ else Std.PlausibleIterStep.done ⋯

theorem Vector.step_iter {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter.step = if h : 0 < n then Std.PlausibleIterStep.yield (xs.iterFromIdx 1) xs[0] ⋯ else Std.PlausibleIterStep.done ⋯

@[simp]

theorem Vector.toList_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdx pos).toList = List.drop pos xs.toList

@[simp]

theorem Vector.toList_iter {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter.toList = xs.toList

@[simp]

theorem Vector.toArray_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdx pos).toArray = xs.toArray.extract pos n

@[simp]

theorem Vector.toArray_iter {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter.toArray = xs.toArray

@[simp]

theorem Vector.toListRev_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdx pos).toListRev = (List.drop pos xs.toList).reverse

@[simp]

theorem Vector.toListRev_toIter {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter.toListRev = xs.toList.reverse

@[simp]

theorem Vector.length_iterFromIdx {β : Type w} {n : Nat} {xs : Vector β n} {pos : Nat} : (xs.iterFromIdx pos).length = n - pos

@[simp]

theorem Vector.length_iter {β : Type w} {n : Nat} {xs : Vector β n} : xs.iter.length = n

theorem Vector.iterFromIdx_equiv_iter_drop_toList {n : Nat} {α : Type w} {xs : Vector α n} {pos : Nat} : (xs.iterFromIdx pos).Equiv (List.drop pos xs.toList).iter

theorem Vector.iter_equiv_iter_toList {n : Nat} {α : Type w} {xs : Vector α n} : xs.iter.Equiv xs.toList.iter