This module proves that the step functions of equivalent iterators behave the same under certain circumstances.
def
Std.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.
Instances For
@[reducible, inline]
abbrev
Std.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.
Instances For
def
Std.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.
Instances For
theorem
Std.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.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
theorem
Std.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₂)
:
theorem
Std.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 β) β) → (Iterators.HetT.liftInner n ita.stepAsHetT).Property x → Iterators.HetT n γ}
{g : (x : IterStep (IterM m β) β) → (Iterators.HetT.liftInner n itb.stepAsHetT).Property x → Iterators.HetT n γ}
(h : ita.Equiv itb)
(hfg :
∀ (sa : IterStep (IterM m β) β) (hsa : (Iterators.HetT.liftInner n ita.stepAsHetT).Property sa)
(sb : IterStep (IterM m β) β) (hsb : (Iterators.HetT.liftInner n itb.stepAsHetT).Property sb),
sa.bundledQuotient = sb.bundledQuotient → f sa hsa = g sb hsb)
:
(Iterators.HetT.liftInner n ita.stepAsHetT).pbind f = (Iterators.HetT.liftInner n itb.stepAsHetT).pbind g
theorem
Std.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 β) β → Iterators.HetT n γ}
{g : IterStep (IterM m β) β → Iterators.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)
:
(Iterators.HetT.liftInner n ita.stepAsHetT).bind f = (Iterators.HetT.liftInner n itb.stepAsHetT).bind g