Lemmas about array iterators

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

theorem Array.iter_eq_toIter_iterM {β : Type w} {array : Array β} : array.iter = (array.iterM Id).toIter

theorem Array.iter_eq_iterFromIdx {β : Type w} {array : Array β} : array.iter = array.iterFromIdx 0

theorem Array.iterFromIdx_eq_toIter_iterFromIdxM {β : Type w} {array : Array β} {pos : Nat} : array.iterFromIdx pos = (array.iterFromIdxM Id pos).toIter

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

theorem Array.step_iter {β : Type w} {array : Array β} : array.iter.step = if h : 0 < array.size then Std.Iterators.PlausibleIterStep.yield (array.iterFromIdx 1) array[0] ⋯ else Std.Iterators.PlausibleIterStep.done ⋯

@[simp]

theorem Array.toList_iterFromIdx {β : Type w} {array : Array β} {pos : Nat} : (array.iterFromIdx pos).toList = List.drop pos array.toList

@[simp]

theorem Array.toList_iter {β : Type w} {array : Array β} : array.iter.toList = array.toList

@[simp]

theorem Array.toArray_iterFromIdx {β : Type w} {array : Array β} {pos : Nat} : (array.iterFromIdx pos).toArray = array.extract pos

@[simp]

theorem Array.toArray_toIter {β : Type w} {array : Array β} : array.iter.toArray = array

@[simp]

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

@[simp]

theorem Array.toListRev_toIter {β : Type w} {array : Array β} : array.iter.toListRev = array.toListRev