theorem
Std.Iterators.Flatten.IsPlausibleStep.outerYield_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ it₁' : IterM m β}
{it₂' : IterM m γ}
{b : β}
(h : it₁.IsPlausibleStep (IterStep.yield it₁' b))
:
(IterM.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁' (some it₂')))
theorem
Std.Iterators.Flatten.IsPlausibleStep.outerSkip_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ it₁' : IterM m β}
(h : it₁.IsPlausibleStep (IterStep.skip it₁'))
:
(IterM.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁' none))
theorem
Std.Iterators.Flatten.IsPlausibleStep.outerDone_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
(h : it₁.IsPlausibleStep IterStep.done)
:
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerYield_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ it₂' : IterM m γ}
{b : γ}
(h : it₂.IsPlausibleStep (IterStep.yield it₂' b))
:
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (IterM.flatMapAfterM f it₁ (some it₂')) b)
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerSkip_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ it₂' : IterM m γ}
(h : it₂.IsPlausibleStep (IterStep.skip it₂'))
:
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁ (some it₂')))
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerDone_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ : IterM m γ}
(h : it₂.IsPlausibleStep IterStep.done)
:
(IterM.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfterM f it₁ none))
theorem
Std.Iterators.Flatten.IsPlausibleStep.outerYield_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ it₁' : IterM m β}
{b : β}
(h : it₁.IsPlausibleStep (IterStep.yield it₁' b))
:
(IterM.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁' (some (f b))))
theorem
Std.Iterators.Flatten.IsPlausibleStep.outerSkip_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ it₁' : IterM m β}
(h : it₁.IsPlausibleStep (IterStep.skip it₁'))
:
(IterM.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁' none))
theorem
Std.Iterators.Flatten.IsPlausibleStep.outerDone_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
(h : it₁.IsPlausibleStep IterStep.done)
:
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerYield_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ it₂' : IterM m γ}
{b : γ}
(h : it₂.IsPlausibleStep (IterStep.yield it₂' b))
:
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (IterM.flatMapAfter f it₁ (some it₂')) b)
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerSkip_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ it₂' : IterM m γ}
(h : it₂.IsPlausibleStep (IterStep.skip it₂'))
:
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁ (some it₂')))
theorem
Std.Iterators.Flatten.IsPlausibleStep.innerDone_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ : IterM m γ}
(h : it₂.IsPlausibleStep IterStep.done)
:
(IterM.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (IterM.flatMapAfter f it₁ none))
theorem
Std.Iterators.IterM.step_flatMapAfterM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
(flatMapAfterM f it₁ it₂).step = match it₂ with
| none => do
let __do_lift ← it₁.step
match __do_lift.inflate with
| ⟨IterStep.yield it₁' b, h⟩ => do
let __do_lift ← f b
pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some __do_lift)) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' none) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| some it₂ => do
let __do_lift ← it₂.step
match __do_lift.inflate with
| ⟨IterStep.yield it₂' out, h⟩ =>
pure (Shrink.deflate (PlausibleIterStep.yield (flatMapAfterM f it₁ (some it₂')) out ⋯))
| ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ (some it₂')) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ none) ⋯))
theorem
Std.Iterators.IterM.step_flatMapM
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
:
(flatMapM f it₁).step = do
let __do_lift ← it₁.step
match __do_lift.inflate with
| ⟨IterStep.yield it₁' b, h⟩ => do
let __do_lift ← f b
pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some __do_lift)) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' none) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem
Std.Iterators.IterM.step_flatMapAfter
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
(flatMapAfter f it₁ it₂).step = match it₂ with
| none => do
let __do_lift ← it₁.step
match __do_lift.inflate with
| ⟨IterStep.yield it₁' b, h⟩ =>
pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| some it₂ => do
let __do_lift ← it₂.step
match __do_lift.inflate with
| ⟨IterStep.yield it₂' out, h⟩ =>
pure (Shrink.deflate (PlausibleIterStep.yield (flatMapAfter f it₁ (some it₂')) out ⋯))
| ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁ (some it₂')) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁ none) ⋯))
theorem
Std.Iterators.IterM.step_flatMap
{α β α₂ γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
{f : β → IterM m γ}
{it₁ : IterM m β}
:
(flatMap f it₁).step = do
let __do_lift ← it₁.step
match __do_lift.inflate with
| ⟨IterStep.yield it₁' b, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem
Std.Iterators.IterM.toList_flatMapAfterM
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
(flatMapAfterM f it₁ it₂).toList = match it₂ with
| none =>
List.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toList)
it₁).toList
| some it₂ => do
let __do_lift ← it₂.toList
let __do_lift_1 ←
List.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toList)
it₁).toList
pure (__do_lift ++ __do_lift_1)
theorem
Std.Iterators.IterM.toArray_flatMapAfterM
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
(flatMapAfterM f it₁ it₂).toArray = match it₂ with
| none =>
Array.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toArray)
it₁).toArray
| some it₂ => do
let __do_lift ← it₂.toArray
let __do_lift_1 ←
Array.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toArray)
it₁).toArray
pure (__do_lift ++ __do_lift_1)
theorem
Std.Iterators.IterM.toList_flatMapM
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
:
theorem
Std.Iterators.IterM.toArray_flatMapM
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → m (IterM m γ)}
{it₁ : IterM m β}
:
theorem
Std.Iterators.IterM.toList_flatMapAfter
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
theorem
Std.Iterators.IterM.toArray_flatMapAfter
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → IterM m γ}
{it₁ : IterM m β}
{it₂ : Option (IterM m γ)}
:
theorem
Std.Iterators.IterM.toList_flatMap
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → IterM m γ}
{it₁ : IterM m β}
:
theorem
Std.Iterators.IterM.toArray_flatMap
{α α₂ β γ : Type w}
{m : Type w → Type w'}
[Monad m]
[LawfulMonad m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[Iterator α m β]
[Iterator α₂ m γ]
[Finite α m]
[Finite α₂ m]
[IteratorCollect α m m]
[IteratorCollect α₂ m m]
[LawfulIteratorCollect α m m]
[LawfulIteratorCollect α₂ m m]
{f : β → IterM m γ}
{it₁ : IterM m β}
: