Lemmas about array iterators

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

theorem Array.iterM_eq_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {array : Array β} : array.iterM m = array.iterFromIdxM m 0

theorem Array.step_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} {array : Array β} {pos : Nat} : (array.iterFromIdxM m pos).step = pure (if h : pos < array.size then Std.Iterators.PlausibleIterStep.yield (array.iterFromIdxM m (pos + 1)) array[pos] ⋯ else Std.Iterators.PlausibleIterStep.done ⋯)

theorem Array.step_iterM {m : Type w → Type w'} [Monad m] {β : Type w} {array : Array β} : (array.iterM m).step = pure (if h : 0 < array.size then Std.Iterators.PlausibleIterStep.yield (array.iterFromIdxM m 1) array[0] ⋯ else Std.Iterators.PlausibleIterStep.done ⋯)

@[simp]

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

@[simp]

theorem Array.toList_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} : (array.iterM m).toList = pure array.toList

@[simp]

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

@[simp]

theorem Array.toArray_toIterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} : (array.iterM m).toArray = pure array

@[simp]

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

@[simp]

theorem Array.toListRev_toIterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} : (array.iterM m).toListRev = pure array.toListRev