Documentation

Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop

theorem Std.Iterators.IterM.DefaultConsumers.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {n : Type w → Type w''} [Monad n] {lift : (γ : Type w) → m γn γ} {γ : Type w} {plausible_forInStep : βγForInStep γProp} {wf : IteratorLoop.WellFounded α m plausible_forInStep} {it : IterM m β} {init : γ} {f : (b : β) → (c : γ) → n (Subtype (plausible_forInStep b c))} :
forIn lift γ plausible_forInStep wf it init f = do let __do_liftlift it.Step it.step match __do_lift with | IterStep.yield it' out, property => do let __do_liftf out init match __do_lift with | ForInStep.yield c, property => forIn lift γ plausible_forInStep wf it' c f | ForInStep.done c, property => pure c | IterStep.skip it', property => forIn lift γ plausible_forInStep wf it' init f | IterStep.done, property => pure init
theorem Std.Iterators.IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : βγn (ForInStep γ)} :
forIn it init f = DefaultConsumers.forIn (fun (x : Type w) => monadLift) γ (fun (x : β) (x : γ) (x : ForInStep γ) => True) it init fun (x1 : β) (x2 : γ) => (fun (x : ForInStep γ) => x, True.intro) <$> f x1 x2
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 n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {γ : Type w} {it : IterM m β} {init : γ} {f : βγn (ForInStep γ)} :
forIn it init f = do let __do_liftliftM it.step match __do_lift with | IterStep.yield it' out, property => do let __do_liftf 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
theorem Std.Iterators.IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] {n : Type w → Type w''} [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)
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 n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {it : IterM m β} {f : βn PUnit} :
forM it f = do let __do_liftliftM it.step match __do_lift 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
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
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 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
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 n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : γβn γ} {init : γ} {it : IterM m β} :
foldM f init it = do let __do_liftliftM it.step match __do_lift with | IterStep.yield it' out, property => do let __do_liftf init out foldM f __do_lift it' | IterStep.skip it', property => foldM f init it' | IterStep.done, property => pure init
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))
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
@[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
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_liftit.step match __do_lift 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
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
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 : β) => PUnit.unit) PUnit.unit it
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 : β) => pure PUnit.unit) PUnit.unit it
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 : PUnit) => pure (ForInStep.yield PUnit.unit)
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_liftit.step match __do_lift with | IterStep.yield it' out, property => it'.drain | IterStep.skip it', property => it'.drain | IterStep.done, property => pure PUnit.unit
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
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
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