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
Instances For
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
Instances For
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
Instances For
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
Instances For
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₂)
:
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)
:
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)
: