This module proves that the step functions of equivalent iterators behave the same under certain circumstances.

def Std.Iterators.IterStep.bundledQuotient {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] (step : IterStep (IterM m β) β) : IterStep (Quot (BundledIterM.Equiv m β)) β

This function is used in lemmas about iterator equivalence (Iter.Equiv and IterM.Equiv).

If the given step contains a successor iterator, replaces the iterator with the quotient of its bundled version.

Equations

• step.bundledQuotient = Std.Iterators.IterStep.mapIterator (Quot.mk (Std.Iterators.BundledIterM.Equiv m β) ∘ Std.Iterators.BundledIterM.ofIterM) step

def Std.Iterators.IterM.QuotStep {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] (it : IterM m β) : Type u_1

This type is used in lemmas about iterator equivalence (Iter.Equiv and IterM.Equiv).

it.QuotStep is the quotient of it.Step where two steps are identified if they agree up to equivalence of their successor iterator.

Equations

• it.QuotStep = Quot fun (s₁ s₂ : it.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient

def Std.Iterators.IterM.QuotStep.bundledQuotient {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM m β} : it.QuotStep → IterStep (Quot (BundledIterM.Equiv m β)) β

This function is used in lemmas about iterator equivalence (Iter.Equiv and IterM.Equiv).

Returns an IterStep from an IterM.QuotStep, discarding the IsPlausibleStep proof. It commutes with IterStep.bundledQuotient and Quot.mk _ : it.Step → it.QuotStep.

Equations

• Std.Iterators.IterM.QuotStep.bundledQuotient = Quot.lift (fun (s : it.Step) => s.val.bundledQuotient) ⋯

theorem Std.Iterators.IterM.Equiv.exists_step_of_step {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [Iterator α₁ m β] [Iterator α₂ m β] [Monad m] [LawfulMonad m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) (s : ita.Step) : ∃ (s' : itb.Step), s.val.bundledQuotient = s'.val.bundledQuotient

noncomputable def Std.Iterators.IterM.QuotStep.transportAlongEquiv {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [Iterator α₁ m β] [Iterator α₂ m β] [Monad m] [LawfulMonad m] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : ita.QuotStep → itb.QuotStep

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Std.Iterators.IterM.QuotStep.restrict {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Monad m] [LawfulMonad m] {it : IterM m β} (step : { s : IterStep (Quot (BundledIterM.Equiv m β)) β // ∃ (s' : it.Step), s = s'.val.bundledQuotient }) : it.QuotStep

Equations

• Std.Iterators.IterM.QuotStep.restrict step = Quot.mk (fun (s₁ s₂ : it.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) ⋯.choose

theorem Std.Iterators.IterStep.restrict_bundle {α₁ : Type u_1} {m : Type u_1 → Type u_2} {β α₂ : Type u_1} [Iterator α₁ m β] [Iterator α₂ m β] [Monad m] [LawfulMonad m] {ita : IterM m β} {step : IterStep (IterM m β) β} {h : ∃ (s : ita.Step), step.bundledQuotient = s.val.bundledQuotient} : IterM.QuotStep.restrict ⟨step.bundledQuotient, h⟩ = Quot.mk (fun (s₁ s₂ : ita.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) h.choose

theorem Std.Iterators.IterM.Equiv.step_eq {β α₁ α₂ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) : (Quot.mk fun (s₁ s₂ : ita.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) <$> ita.step = QuotStep.transportAlongEquiv ⋯ <$> (Quot.mk fun (s₁ s₂ : itb.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) <$> itb.step

theorem Std.Iterators.IterM.Equiv.lift_step_bind_congr {m : Type w → Type u_1} {n : Type w → Type u_2} {β γ α₁ α₂ : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM m β} {itb : IterM m β} (h : ita.Equiv itb) {f : ita.Step → n γ} {g : itb.Step → n γ} (hfg : ∀ (s₁ : ita.Step) (s₂ : itb.Step), s₁.val.bundledQuotient = s₂.val.bundledQuotient → f s₁ = g s₂) : liftM ita.step >>= f = liftM itb.step >>= g

theorem Std.Iterators.IterM.Equiv.liftInner_stepAsHetT_pbind_congr {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α₁ β α₂ : Type u_1} {γ : Type u_4} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM m β} {itb : IterM m β} {f : (x : IterStep (IterM m β) β) → (HetT.liftInner n ita.stepAsHetT).Property x → HetT n γ} {g : (x : IterStep (IterM m β) β) → (HetT.liftInner n itb.stepAsHetT).Property x → HetT n γ} (h : ita.Equiv itb) (hfg : ∀ (sa : IterStep (IterM m β) β) (hsa : (HetT.liftInner n ita.stepAsHetT).Property sa) (sb : IterStep (IterM m β) β) (hsb : (HetT.liftInner n itb.stepAsHetT).Property sb), sa.bundledQuotient = sb.bundledQuotient → f sa hsa = g sb hsb) : (HetT.liftInner n ita.stepAsHetT).pbind f = (HetT.liftInner n itb.stepAsHetT).pbind g

theorem Std.Iterators.IterM.Equiv.liftInner_stepAsHetT_bind_congr {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α₁ β α₂ : Type u_1} {γ : Type u_4} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α₁ m β] [Iterator α₂ m β] {ita : IterM m β} {itb : IterM m β} {f : IterStep (IterM m β) β → HetT n γ} {g : IterStep (IterM m β) β → HetT n γ} (h : ita.Equiv itb) (hfg : ∀ (sa : IterStep (IterM m β) β), ita.stepAsHetT.Property sa → ∀ (sb : IterStep (IterM m β) β), itb.stepAsHetT.Property sb → sa.bundledQuotient = sb.bundledQuotient → f sa = g sb) : (HetT.liftInner n ita.stepAsHetT).bind f = (HetT.liftInner n itb.stepAsHetT).bind g