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

source
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

Instances For

source
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

Instances For

source
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) ⋯

Instances For

source
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
source
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.

Instances For

source
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

Instances For

source
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
source
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) :
(fun (s : Shrink ita.Step) => Shrink.deflate (Quot.mk (fun (s₁ s₂ : ita.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) s.inflate)) <$> ita.step = (fun (s : Shrink (Quot fun (s₁ s₂ : itb.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient)) => Shrink.deflate (QuotStep.transportAlongEquiv ⋯ s.inflate)) <$> (fun (s : Shrink itb.Step) => Shrink.deflate (Quot.mk (fun (s₁ s₂ : itb.Step) => s₁.val.bundledQuotient = s₂.val.bundledQuotient) s.inflate)) <$> itb.step
source
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 : Shrink ita.Step → n γ} {g : Shrink itb.Step → n γ} (hfg : ∀ (s₁ : Shrink ita.Step) (s₂ : Shrink itb.Step), s₁.inflate.val.bundledQuotient = s₂.inflate.val.bundledQuotient → f s₁ = g s₂) :
liftM ita.step >>= f = liftM itb.step >>= g
source
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
source
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