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 ⋯)

theorem Std.Iterators.ArrayIterator.stepAsHetT_iterFromIdxM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : Nat} : (array.iterFromIdxM m pos).stepAsHetT = if x : pos < array.size then pure (IterStep.yield (array.iterFromIdxM m (pos + 1)) array[pos]) else pure IterStep.done

theorem Std.Iterators.Array.iterFromIdxM_equiv_iterM_drop_toList {α : Type w} {array : Array α} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {pos : Nat} : (array.iterFromIdxM m pos).Equiv ((List.drop pos array.toList).iterM m)

theorem Std.Iterators.Array.iterM_equiv_iterM_toList {α : Type w} {array : Array α} {m : Type w → Type w'} [Monad m] [LawfulMonad m] : (array.iterM m).Equiv (array.toList.iterM m)

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