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 (Std.Shrink.deflate (if h : pos < array.size then Std.PlausibleIterStep.yield (array.iterFromIdxM m (pos + 1)) array[pos] ⋯ else Std.PlausibleIterStep.done ⋯))

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

theorem Std.Iterators.Types.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 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 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_iterM {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_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} : (array.iterM m).toListRev = pure array.toListRev

@[simp]

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

@[simp]

theorem Array.length_iterM {m : Type w → Type w'} [Monad m] {β : Type w} [LawfulMonad m] {array : Array β} : (array.iterM m).length = pure { down := array.size }