theorem Std.Iter.filterMapWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → Iterators.PostconditionT m (Option γ)} : filterMapWithPostcondition f it = IterM.filterMapWithPostcondition f it.toIterM

theorem Std.Iter.filterWithPostcondition_eq_toIter_filterMapWithPostcondition_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → Iterators.PostconditionT m (ULift Bool)} : filterWithPostcondition f it = IterM.filterWithPostcondition f it.toIterM

theorem Std.Iter.mapWithPostcondition_eq_toIter_mapWithPostcondition_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → Iterators.PostconditionT m γ} : mapWithPostcondition f it = IterM.mapWithPostcondition f it.toIterM

theorem Std.Iter.filterMapM_eq_toIter_filterMapM_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [MonadAttach m] {f : β → m (Option γ)} : filterMapM f it = IterM.filterMapM f it.toIterM

theorem Std.Iter.filterM_eq_toIter_filterM_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [MonadAttach m] {f : β → m (ULift Bool)} : filterM f it = IterM.filterM f it.toIterM

theorem Std.Iter.mapM_eq_toIter_mapM_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [MonadAttach m] {f : β → m γ} : mapM f it = IterM.mapM f it.toIterM

theorem Std.Iter.filterMap_eq_toIter_filterMap_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → Option γ} : filterMap f it = (IterM.filterMap f it.toIterM).toIter

theorem Std.Iter.map_eq_toIter_map_toIterM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → γ} : map f it = (IterM.map f it.toIterM).toIter

theorem Std.Iter.filter_eq_toIter_filter_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] {f : β → Bool} : filter f it = (IterM.filter f it.toIterM).toIter

theorem Std.Iter.step_filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → Iterators.PostconditionT n (Option γ)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterMapWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨none, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯)) | ⟨some out', h'⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterMapWithPostcondition f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_filterWithPostcondition {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → Iterators.PostconditionT n (ULift Bool)} [Monad n] [LawfulMonad n] [MonadLiftT m n] : (filterWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← (f out).operation match __do_lift with | ⟨{ down := false }, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯)) | ⟨{ down := true }, h'⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterWithPostcondition f it') out ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {n : Type w → Type w''} {f : β → Iterators.PostconditionT n γ} [Monad n] [LawfulMonad n] : (mapWithPostcondition f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let out' ← (f out).operation pure (Shrink.deflate (PlausibleIterStep.yield (mapWithPostcondition f it') out'.val ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (mapWithPostcondition f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_filterMapM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {β' : Type w} {f : β → n (Option β')} [Monad n] [MonadAttach n] [LawfulMonad n] [MonadLiftT m n] : (filterMapM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← MonadAttach.attach (f out) match __do_lift with | ⟨none, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapM f it') ⋯)) | ⟨some out', hf⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterMapM f it') out' ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterMapM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_filterM {α β : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {f : β → n (ULift Bool)} [Monad n] [MonadAttach n] [LawfulMonad n] [MonadLiftT m n] : (filterM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← MonadAttach.attach (f out) match __do_lift with | ⟨{ down := false }, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterM f it') ⋯)) | ⟨{ down := true }, hf⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (filterM f it') out ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (filterM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_mapM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {n : Type w → Type w''} {f : β → n γ} [Monad n] [MonadAttach n] [LawfulMonad n] : (mapM f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => do let out' ← MonadAttach.attach (f out) pure (Shrink.deflate (PlausibleIterStep.yield (mapM f it') out'.val ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (mapM f it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

theorem Std.Iter.step_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → Option γ} : (filterMap f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => match h' : f out with | none => PlausibleIterStep.skip (filterMap f it') ⋯ | some out' => PlausibleIterStep.yield (filterMap f it') out' ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (filterMap f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iter.val_step_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → Option γ} : (filterMap f it).step.val = match it.step.val with | IterStep.yield it' out => match f out with | none => IterStep.skip (filterMap f it') | some out' => IterStep.yield (filterMap f it') out' | IterStep.skip it' => IterStep.skip (filterMap f it') | IterStep.done => IterStep.done

a weaker version of step_filterMap that does not use dependent match

theorem Std.Iter.step_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} {f : β → γ} : (map f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => PlausibleIterStep.yield (map f it') (f out) ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (map f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

def Std.Iter.step_filter {α β : Type w} [Iterator α Id β] {it : Iter β} {f : β → Bool} : (filter f it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => if h' : f out = true then PlausibleIterStep.yield (filter f it') out ⋯ else PlausibleIterStep.skip (filter f it') ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (filter f it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

Equations

• ⋯ = ⋯

def Std.Iter.val_step_filter {α β : Type w} [Iterator α Id β] {it : Iter β} {f : β → Bool} : (filter f it).step.val = match it.step.val with | IterStep.yield it' out => if f out = true then IterStep.yield (filter f it') out else IterStep.skip (filter f it') | IterStep.skip it' => IterStep.skip (filter f it') | IterStep.done => IterStep.done

Equations

• ⋯ = ⋯

@[simp]

theorem Std.Iter.toList_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Option γ} : (filterMap f it).toList = List.filterMap f it.toList

@[simp]

theorem Std.Iter.toList_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} : (mapWithPostcondition f it).toList = List.mapM (fun (x : β) => (f x).run) it.toList

@[simp]

theorem Std.Iter.toList_mapM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterators.Finite α Id] {f : β → m γ} : (mapM f it).toList = List.mapM f it.toList

@[simp]

theorem Std.Iter.toList_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → γ} : (map f it).toList = List.map f it.toList

@[simp]

theorem Std.Iter.toList_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Bool} : (filter f it).toList = List.filter f it.toList

@[simp]

theorem Std.Iter.toList_filterMapWithPostcondition_filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {δ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m (Option γ)} {g : γ → Iterators.PostconditionT n (Option δ)} : (IterM.filterMapWithPostcondition g (filterMapWithPostcondition f it)).toList = (filterMapWithPostcondition (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toList

@[simp]

theorem Std.Iter.toList_mapWithPostcondition_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {δ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} {g : γ → Iterators.PostconditionT n δ} : (IterM.mapWithPostcondition g (mapWithPostcondition f it)).toList = (mapWithPostcondition (fun (b : β) => liftM (f b) >>= g) it).toList

@[simp]

theorem Std.Iter.toListRev_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Option γ} : (filterMap f it).toListRev = List.filterMap f it.toListRev

@[simp]

theorem Std.Iter.toListRev_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → γ} : (map f it).toListRev = List.map f it.toListRev

@[simp]

theorem Std.Iter.toListRev_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Bool} : (filter f it).toListRev = List.filter f it.toListRev

@[simp]

theorem Std.Iter.toArray_filterMap {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Option γ} : (filterMap f it).toArray = Array.filterMap f it.toArray

@[simp]

theorem Std.Iter.toArray_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} : (mapWithPostcondition f it).toArray = Array.mapM (fun (x : β) => (f x).run) it.toArray

@[simp]

theorem Std.Iter.toArray_mapM {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterators.Finite α Id] {f : β → m γ} : (mapM f it).toArray = Array.mapM f it.toArray

@[simp]

theorem Std.Iter.toArray_map {α β γ : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → γ} : (map f it).toArray = Array.map f it.toArray

@[simp]

theorem Std.Iter.toArray_filter {α β : Type w} [Iterator α Id β] {it : Iter β} [Iterators.Finite α Id] {f : β → Bool} : (filter f it).toArray = Array.filter f it.toArray

@[simp]

theorem Std.Iter.toArray_filterMapWithPostcondition_filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {δ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m (Option γ)} {g : γ → Iterators.PostconditionT n (Option δ)} : (IterM.filterMapWithPostcondition g (filterMapWithPostcondition f it)).toArray = (filterMapWithPostcondition (fun (b : β) => do let __do_lift ← liftM (f b) match __do_lift with | none => pure none | some fb => g fb) it).toArray

@[simp]

theorem Std.Iter.toArray_mapWithPostcondition_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {it : Iter β} {m : Type w → Type w'} {n : Type w → Type w''} {δ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterators.Finite α Id] {f : β → Iterators.PostconditionT m γ} {g : γ → Iterators.PostconditionT n δ} : (IterM.mapWithPostcondition g (mapWithPostcondition f it)).toArray = (mapWithPostcondition (fun (b : β) => liftM (f b) >>= g) it).toArray

theorem Std.Iter.forIn_filterMapWithPostcondition {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (filterMapWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run match __do_lift with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.Iter.forIn_filterMapM {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (filterMapM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) match __do_lift with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.Iter.forIn_filterMap {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {β₂ : Type w} [Monad n] [LawfulMonad n] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} : forIn (filterMap f it) init g = forIn it init fun (out : β) (acc : γ) => match f out with | some c => g c acc | none => pure (ForInStep.yield acc)

theorem Std.Iter.forIn_mapWithPostcondition {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (mapWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run g __do_lift acc

theorem Std.Iter.forIn_mapM {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} {β₂ : Type w} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} : forIn (mapM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) g __do_lift acc

theorem Std.Iter.forIn_map {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {β₂ : Type w} [Monad n] [LawfulMonad n] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} : forIn (map f it) init g = forIn it init fun (out : β) (acc : γ) => g (f out) acc

theorem Std.Iter.forIn_filterWithPostcondition {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} : forIn (filterWithPostcondition f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)

theorem Std.Iter.forIn_filterM {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} {o : Type w → Type u_1} [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} : forIn (filterM f it) init g = forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)

theorem Std.Iter.forIn_filter {α β γ : Type w} [Iterator α Id β] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} : forIn (filter f it) init g = forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else pure (ForInStep.yield acc)

theorem Std.Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (filterMapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b).run match __x with | some c => g d c | x => pure d) init it

theorem Std.Iter.foldM_filterMapM {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (filterMapM f it) = foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b) match __x with | some c => g d c | x => pure d) init it

theorem Std.Iter.foldM_mapWithPostcondition {m : Type w → Type w'} {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (mapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let c ← liftM (f b).run g d c) init it

theorem Std.Iter.foldM_mapM {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (mapM f it) = foldM (fun (d : δ) (b : β) => do let c ← liftM (f b) g d c) init it

theorem Std.Iter.foldM_filterWithPostcondition {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (filterWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b).run if __do_lift.down = true then g d b else pure d) init it

theorem Std.Iter.foldM_filterM {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter β} : IterM.foldM g init (filterM f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b) if __do_lift.down = true then g d b else pure d) init it

theorem Std.Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter β} : foldM g init (filterMap f it) = foldM (fun (d : δ) (b : β) => match f b with | some c => g d c | x => pure d) init it

theorem Std.Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter β} : foldM g init (map f it) = foldM (fun (d : δ) (b : β) => g d (f b)) init it

theorem Std.Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter β} : foldM g init (filter f it) = foldM (fun (d : δ) (b : β) => if f b = true then g d b else pure d) init it

theorem Std.Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter β} : IterM.fold g init (filterMapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __x ← (f b).run match __x with | some c => pure (g d c) | x => pure d) init it

theorem Std.Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter β} : IterM.fold g init (filterMapM f it) = foldM (fun (d : δ) (b : β) => do let __x ← f b match __x with | some c => pure (g d c) | x => pure d) init it

theorem Std.Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter β} : IterM.fold g init (mapWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let c ← (f b).run pure (g d c)) init it

theorem Std.Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter β} : IterM.fold g init (mapM f it) = foldM (fun (d : δ) (b : β) => do let c ← f b pure (g d c)) init it

theorem Std.Iter.fold_filterWithPostcondition {α β δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter β} : IterM.fold g init (filterWithPostcondition f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← (f b).run pure (if __do_lift.down = true then g d b else d)) init it

theorem Std.Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w''} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter β} : IterM.fold g init (filterM f it) = foldM (fun (d : δ) (b : β) => do let __do_lift ← f b pure (if __do_lift.down = true then g d b else d)) init it

theorem Std.Iter.fold_filterMap {α β γ δ : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Iter β} : fold g init (filterMap f it) = fold (fun (d : δ) (b : β) => match f b with | some c => g d c | x => d) init it

theorem Std.Iter.fold_map {α β γ δ : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → γ} {g : δ → γ → δ} {init : δ} {it : Iter β} : fold g init (map f it) = fold (fun (d : δ) (b : β) => g d (f b)) init it

theorem Std.Iter.fold_filter {α β δ : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {f : β → Bool} {g : δ → β → δ} {init : δ} {it : Iter β} : fold g init (filter f it) = fold (fun (d : δ) (b : β) => if f b = true then g d b else d) init it

@[simp]

theorem Std.Iter.length_map {α β β' : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → β'} : (map f it).length = it.length

@[deprecated Std.Iter.length_map (since := "2026-01-28")]

def Std.Iter.count_map {α β β' : Type u_1} [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → β'} : (map f it).length = it.length

Equations

• @Std.Iter.count_map = @Std.Iter.length_map

theorem Std.Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} : IterM.anyM p (filterMapM f it) = IterM.anyM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => p fx | none => pure { down := false }) (mapM pure it)

theorem Std.Iter.anyM_eq_anyM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter β} {p : β → m Bool} : anyM p it = ULift.down <$> IterM.anyM (fun (x : β) => ULift.up <$> p x) (mapM pure it)

This lemma expresses Iter.anyM in terms of IterM.anyM. It requires all involved types to live in Type 0.

theorem Std.Iter.anyM_mapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f : β → m β'} {p : β' → m (ULift Bool)} : IterM.anyM p (mapM f it) = IterM.anyM (fun (x : β) => do let __do_lift ← f x p __do_lift) (mapM pure it)

theorem Std.Iter.anyM_filterM {α β : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f p : β → m (ULift Bool)} : IterM.anyM p (filterM f it) = IterM.anyM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then p x else pure { down := false }) (mapM pure it)

theorem Std.Iter.anyM_filterMap {α β β' : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → Option β'} {p : β' → m Bool} : anyM p (filterMap f it) = anyM (fun (x : β) => match f x with | some fx => p fx | none => pure false) it

theorem Std.Iter.anyM_map {α β β' : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → β'} {p : β' → m Bool} : anyM p (map f it) = anyM (fun (x : β) => p (f x)) it

theorem Std.Iter.anyM_filter {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → Bool} {p : β → m Bool} : anyM p (filter f it) = anyM (fun (x : β) => if f x = true then p x else pure false) it

theorem Std.Iter.any_filterMapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (Option β')} {p : β' → Bool} : IterM.any p (filterMapM f it) = IterM.anyM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => pure { down := p fx } | none => pure { down := false }) (mapM pure it)

theorem Std.Iter.any_mapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m β'} {p : β' → Bool} : IterM.any p (mapM f it) = IterM.anyM (fun (x : β) => (fun (x : β') => { down := p x }) <$> f x) (mapM pure it)

theorem Std.Iter.any_filterM {α β : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (ULift Bool)} {p : β → Bool} : IterM.any p (filterM f it) = IterM.anyM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then pure { down := p x } else pure { down := false }) (mapM pure it)

theorem Std.Iter.any_filterMap {α β β' : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Option β'} {p : β' → Bool} : any p (filterMap f it) = any (fun (x : β) => match f x with | some fx => p fx | none => false) it

theorem Std.Iter.any_map {α β β' : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → β'} {p : β' → Bool} : any p (map f it) = any (fun (x : β) => p (f x)) it

theorem Std.Iter.allM_filterMapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} : IterM.allM p (filterMapM f it) = IterM.allM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => p fx | none => pure { down := true }) (mapM pure it)

theorem Std.Iter.allM_eq_allM_mapM_pure {α β : Type} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter β} {p : β → m Bool} : allM p it = ULift.down <$> IterM.allM (fun (x : β) => ULift.up <$> p x) (mapM pure it)

This lemma expresses Iter.allM in terms of IterM.allM. It requires all involved types to live in Type 0.

theorem Std.Iter.allM_mapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f : β → m β'} {p : β' → m (ULift Bool)} : IterM.allM p (mapM f it) = IterM.allM (fun (x : β) => do let __do_lift ← f x p __do_lift) (mapM pure it)

theorem Std.Iter.allM_filterM {α β : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {it : Iter β} {f p : β → m (ULift Bool)} : IterM.allM p (filterM f it) = IterM.allM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then p x else pure { down := true }) (mapM pure it)

theorem Std.Iter.allM_filterMap {α β β' : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → Option β'} {p : β' → m Bool} : allM p (filterMap f it) = allM (fun (x : β) => match f x with | some fx => p fx | none => pure true) it

theorem Std.Iter.allM_map {α β β' : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → β'} {p : β' → m Bool} : allM p (map f it) = allM (fun (x : β) => p (f x)) it

theorem Std.Iter.allM_filter {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [IteratorLoop α Id m] [LawfulMonad m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → Bool} {p : β → m Bool} : allM p (filter f it) = allM (fun (x : β) => if f x = true then p x else pure true) it

theorem Std.Iter.all_filterMapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (Option β')} {p : β' → Bool} : IterM.all p (filterMapM f it) = IterM.allM (fun (x : β) => do let __do_lift ← f x match __do_lift with | some fx => pure { down := p fx } | none => pure { down := true }) (mapM pure it)

theorem Std.Iter.all_mapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m β'} {p : β' → Bool} : IterM.all p (mapM f it) = IterM.allM (fun (x : β) => (fun (x : β') => { down := p x }) <$> f x) (mapM pure it)

theorem Std.Iter.all_filterM {α β : Type w} {m : Type w → Type w'} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [LawfulIteratorLoop α Id m] {it : Iter β} {f : β → m (ULift Bool)} {p : β → Bool} : IterM.all p (filterM f it) = IterM.allM (fun (x : β) => do let __do_lift ← f x if __do_lift.down = true then pure { down := p x } else pure { down := true }) (mapM pure it)

theorem Std.Iter.all_filterMap {α β β' : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → Option β'} {p : β' → Bool} : all p (filterMap f it) = all (fun (x : β) => match f x with | some fx => p fx | none => true) it

theorem Std.Iter.all_map {α β β' : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter β} {f : β → β'} {p : β' → Bool} : all p (map f it) = all (fun (x : β) => p (f x)) it