source
theorem Std.Iterators.IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Type x → Type x'} [Monad n] {lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ} {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop} {wf : IteratorLoop.WellFounded α m plausible_forInStep} {it : IterM m β} {init : γ} {P : β → Prop} {hP : ∀ (b : β), it.IsPlausibleIndirectOutput b → P b} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
forIn' lift γ plausible_forInStep wf it init P hP f = (fun (x : Shrink it.Step → n γ) => lift (Shrink it.Step) γ x it.step) fun (s : Shrink it.Step) => match s.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out ⋯ init match __do_lift with | ⟨ForInStep.yield c, property⟩ => forIn' lift γ plausible_forInStep wf it' c P ⋯ f | ⟨ForInStep.done c, property⟩ => pure c | ⟨IterStep.skip it', h⟩ => forIn' lift γ plausible_forInStep wf it' init P ⋯ f | ⟨IterStep.done, property⟩ => pure init
source
theorem Std.Iterators.IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} :
forIn' it init f = DefaultConsumers.forIn' (fun (x x_1 : Type w) (f : x → n x_1) (x_2 : m x) => monadLift x_2 >>= f) γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) ⋯ it init it.IsPlausibleIndirectOutput ⋯ fun (x1 : β) (x2 : it.IsPlausibleIndirectOutput x1) (x3 : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f x1 x2 x3
source
theorem Std.Iterators.IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : β → γ → n (ForInStep γ)} :
forIn it init f = DefaultConsumers.forIn' (fun (x x_1 : Type w) (f : x → n x_1) (x_2 : m x) => monadLift x_2 >>= f) γ (fun (x : β) (x_1 : γ) (x_2 : ForInStep γ) => True) ⋯ it init it.IsPlausibleIndirectOutput ⋯ fun (out : β) (x : it.IsPlausibleIndirectOutput out) (acc : γ) => (fun (x : ForInStep γ) => ⟨x, True.intro⟩) <$> f out acc
source
theorem Std.Iterators.IterM.forIn'_congr {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] {ita itb : IterM m β} (w : ita = itb) {b b' : γ} (hb : b = b') {f : (a' : β) → a' ∈ ita → γ → n (ForInStep γ)} {g : (a' : β) → a' ∈ itb → γ → n (ForInStep γ)} (h : ∀ (a : β) (m_1 : a ∈ itb) (b : γ), f a ⋯ b = g a m_1 b) :
forIn' ita b f = forIn' itb b' g
source
theorem Std.Iterators.IterM.forIn_congr {γ α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n] {ita itb : IterM m β} (w : ita = itb) {b b' : γ} (hb : b = b') {f g : β → γ → n (ForInStep γ)} (h : ∀ (a : β) (b : γ), f a b = g a b) :
forIn ita b f = forIn itb b' g
source
theorem Std.Iterators.IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : (out : β) → out ∈ it → γ → n (ForInStep γ)} :
forIn' it init f = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← f out ⋯ init match __do_lift with | ForInStep.yield c => forIn' it' c fun (out_1 : β) (h'' : out_1 ∈ it') (acc : γ) => f out_1 ⋯ acc | ForInStep.done c => pure c | ⟨IterStep.skip it', h⟩ => forIn' it' init fun (out : β) (h' : out ∈ it') (acc : γ) => f out ⋯ acc | ⟨IterStep.done, property⟩ => pure init
source
theorem Std.Iterators.IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : β → γ → n (ForInStep γ)} :
forIn it init f = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← f out init match __do_lift with | ForInStep.yield c => forIn it' c f | ForInStep.done c => pure c | ⟨IterStep.skip it', property⟩ => forIn it' init f | ⟨IterStep.done, property⟩ => pure init
source
theorem Std.Iterators.IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {it : IterM m β} {f : β → n PUnit} :
forM it f = forIn it PUnit.unit fun (out : β) (x : PUnit) => do f out pure (ForInStep.yield PUnit.unit)
source
theorem Std.Iterators.IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {it : IterM m β} {f : β → n PUnit} :
forM it f = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, property⟩ => do f out forM it' f | ⟨IterStep.skip it', property⟩ => forM it' f | ⟨IterStep.done, property⟩ => pure PUnit.unit
source
theorem Std.Iterators.IterM.foldM_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM m β} :
foldM f init it = forIn it init fun (x : β) (acc : γ) => ForInStep.yield <$> f acc x
source
theorem Std.Iterators.IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ} {it : IterM m β} :
(forIn it init fun (c : β) (b : γ) => (fun (d : δ) => ForInStep.yield (g c b d)) <$> f c b) = foldM (fun (b : γ) (c : β) => g c b <$> f c b) init it
source
theorem Std.Iterators.IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM m β} :
foldM f init it = do let __do_lift ← liftM it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, property⟩ => do let __do_lift ← f init out foldM f __do_lift it' | ⟨IterStep.skip it', property⟩ => foldM f init it' | ⟨IterStep.done, property⟩ => pure init
source
theorem Std.Iterators.IterM.fold_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : IterM m β} :
fold f init it = forIn it init fun (x : β) (acc : γ) => pure (ForInStep.yield (f acc x))
source
theorem Std.Iterators.IterM.fold_eq_foldM {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : IterM m β} :
fold f init it = foldM (fun (x1 : γ) (x2 : β) => pure (f x1 x2)) init it
source
@[simp]
theorem Std.Iterators.IterM.forIn_pure_yield_eq_fold {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → γ → γ} {init : γ} {it : IterM m β} :
(forIn it init fun (c : β) (b : γ) => pure (ForInStep.yield (f c b))) = fold (fun (b : γ) (c : β) => f c b) init it
source
theorem Std.Iterators.IterM.fold_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : γ → β → γ} {init : γ} {it : IterM m β} :
fold f init it = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, property⟩ => fold f (f init out) it' | ⟨IterStep.skip it', property⟩ => fold f init it' | ⟨IterStep.done, property⟩ => pure init
source
theorem Std.Iterators.IterM.fold_hom {α β γ₁ γ₂ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁} (H : ∀ (x : γ₁) (y : β), g₂ (f x) y = f (g₁ x y)) :
fold g₂ (f init) it = f <$> fold g₁ init it
source
theorem Std.Iterators.IterM.toList_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} :
it.toList = fold (fun (l : List β) (out : β) => l ++ [out]) [] it
source
theorem Std.Iterators.IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} :
it.toArray = fold (fun (xs : Array β) (out : β) => xs.push out) #[] it
source
theorem Std.Iterators.IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {it : IterM m β} :
it.drain = fold (fun (x : PUnit) (x_1 : β) => PUnit.unit) PUnit.unit it
source
theorem Std.Iterators.IterM.drain_eq_foldM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] {it : IterM m β} :
it.drain = foldM (fun (x : PUnit) (x_1 : β) => pure PUnit.unit) PUnit.unit it
source
theorem Std.Iterators.IterM.drain_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [IteratorLoop α m m] {it : IterM m β} :
it.drain = forIn it PUnit.unit fun (x : β) (x_1 : PUnit) => pure (ForInStep.yield PUnit.unit)
source
theorem Std.Iterators.IterM.drain_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} :
it.drain = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, property⟩ => it'.drain | ⟨IterStep.skip it', property⟩ => it'.drain | ⟨IterStep.done, property⟩ => pure PUnit.unit
source
theorem Std.Iterators.IterM.drain_eq_map_toList {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} :
it.drain = (fun (x : List β) => PUnit.unit) <$> it.toList
source
theorem Std.Iterators.IterM.drain_eq_map_toListRev {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} :
it.drain = (fun (x : List β) => PUnit.unit) <$> it.toListRev
source
theorem Std.Iterators.IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM m β} :
it.drain = (fun (x : List β) => PUnit.unit) <$> it.toList
source
theorem Std.Iterators.IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} :
anyM p it = forIn it { down := false } fun (x : β) (x_1 : ULift Bool) => do let __do_lift ← p x if __do_lift.down = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })
source
theorem Std.Iterators.IterM.anyM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} :
anyM p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => do let __do_lift ← p x if __do_lift.down = true then pure { down := true } else anyM p it' | IterStep.skip it' => anyM p it' | IterStep.done => pure { down := false }
source
theorem Std.Iterators.IterM.any_eq_anyM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
any p it = anyM (fun (x : β) => pure { down := p x }) it
source
theorem Std.Iterators.IterM.anyM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → ULift Bool} :
anyM (fun (x : β) => pure (p x)) it = any (fun (x : β) => (p x).down) it
source
theorem Std.Iterators.IterM.any_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
any p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => if p x = true then pure { down := true } else any p it' | IterStep.skip it' => any p it' | IterStep.done => pure { down := false }
source
theorem Std.Iterators.IterM.any_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
any p it = forIn it { down := false } fun (x : β) (x_1 : ULift Bool) => if p x = true then pure (ForInStep.done { down := true }) else pure (ForInStep.yield { down := false })
source
theorem Std.Iterators.IterM.allM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} :
allM p it = forIn it { down := true } fun (x : β) (x_1 : ULift Bool) => do let __do_lift ← p x if __do_lift.down = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })
source
theorem Std.Iterators.IterM.allM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} :
allM p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => do let __do_lift ← p x if __do_lift.down = true then allM p it' else pure { down := false } | IterStep.skip it' => allM p it' | IterStep.done => pure { down := true }
source
theorem Std.Iterators.IterM.all_eq_allM {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
all p it = allM (fun (x : β) => pure { down := p x }) it
source
theorem Std.Iterators.IterM.allM_pure {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → ULift Bool} :
allM (fun (x : β) => pure (p x)) it = all (fun (x : β) => (p x).down) it
source
theorem Std.Iterators.IterM.all_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
all p it = do let __do_lift ← it.step match __do_lift.inflate.val with | IterStep.yield it' x => if p x = true then all p it' else pure { down := false } | IterStep.skip it' => all p it' | IterStep.done => pure { down := true }
source
theorem Std.Iterators.IterM.all_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
all p it = forIn it { down := true } fun (x : β) (x_1 : ULift Bool) => if p x = true then pure (ForInStep.yield { down := true }) else pure (ForInStep.done { down := false })
source
theorem Std.Iterators.IterM.allM_eq_not_anyM_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → m (ULift Bool)} :
allM p it = (fun (x : ULift Bool) => { down := !x.down }) <$> anyM (fun (x : β) => (fun (x : ULift Bool) => { down := !x.down }) <$> p x) it
source
theorem Std.Iterators.IterM.all_eq_not_any_not {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM m β} {p : β → Bool} :
all p it = (fun (x : ULift Bool) => { down := !x.down }) <$> any (fun (x : β) => !p x) it