Documentation

Std.Data.Iterators.Lemmas.Equivalence.HetT

class Std.Internal.ComputableSmall (α : Type v) :
Type (max (u + 1) v)
Instances
    structure Std.Internal.USquash (α : Type v) [small : Small α] :
    noncomputable def Std.Internal.USquash.deflate {α : Type v} [small : Small α] (x : α) :
    Equations
    noncomputable def Std.Internal.USquash.inflate {α : Type v} [small : Small α] (x : USquash α) :
    α
    Equations
    @[simp]
    theorem Std.Internal.USquash.deflate_inflate {α : Type v} {x✝ : Small α} {x : USquash α} :
    @[simp]
    theorem Std.Internal.USquash.inflate_deflate {α : Type v} {x✝ : Small α} {x : α} :
    theorem Std.Internal.USquash.inflate.inj {α : Type v} {x✝ : Small α} {x y : USquash α} (h : x.inflate = y.inflate) :
    x = y
    instance Std.Internal.instSmallSubtype {α : Type v} [Small α] {p : αProp} :
    instance Std.Internal.instSmallSubtypeEq {α : Type v} {x : α} :
    Small { x_1 : α // x = x_1 }
    instance Std.Internal.instSmallSubtypeEq_1 {α : Type v} {x : α} :
    Small { x_1 : α // x_1 = x }
    def Std.Internal.Small.of_surjective (α : Type v) {β : Type w} (f : αβ) [Small α] (h : ∀ (b : β), (a : α), f a = b) :
    Equations
    • =
    instance Std.Internal.instSmallSubtypeExistsEq {α : Type v} {β : Type w} {f : αβ} [Small α] :
    Small { b : β // (a : α), f a = b }
    theorem Std.Internal.Small.map {α : Type v} {β : Type w} (P : αProp) (f : (a : α) → P aβ) [Small { a : α // P a }] :
    Small { b : β // (a : α), (h : P a), f a h = b }
    instance Std.Internal.instSmallSigma {α : Type v} {β : αType w} [Small α] [∀ (a : α), Small (β a)] :
    Small ((a : α) × β a)
    theorem Std.Internal.Small.pbind {α : Type v} {β : Type w} (P : αProp) (Q : (a : α) → P aβProp) (i₁ : Small { a : α // P a }) (i₂ : ∀ (a : α) (h : P a), Small { b : β // Q a h b }) :
    Small { b : β // (a : α), (h : P a), Q a h b }
    theorem Std.Internal.Small.bind {α : Type v} {β : Type w} (P : αProp) (Q : αβProp) (i₁ : Small { a : α // P a }) (i₂ : ∀ (a : α), Small { b : β // Q a b }) :
    Small { b : β // (a : α), P a Q a b }
    structure Std.Iterators.HetT (m : Type w → Type w') (α : Type v) :
    Type (max v w')

    If m is a monad, then HetT m is a monad that has two features:

    • It generalizes m to arbitrary universes.
    • It tracks a postcondition property that holds for the monadic return value, similarly to PostconditionT.

    This monad is noncomputable and is merely a vehicle for more convenient proofs, especially proofs about the equivalence of iterators, because it avoids universe issues and spares users the work to handle the postconditions manually.

    Caution: Just like PostconditionT, this is not a lawful monad transformer. To lift from m to HetT m, use HetT.lift.

    Because this monad is fundamentally universe-polymorphic, it is recommended for consistency to always use the methods HetT.pure, HetT.map and HetT.bind instead of the homogeneous versions Pure.pure, Functor.map and Bind.bind.

    • Property : αProp

      A predicate that holds for the return value(s) of the m-monadic operation.

    • A proof that the possible return values are equivalent to a w-small type.

    • operation : m (Internal.USquash (Subtype self.Property))

      The actual monadic operation. Its return value is bundled together with a proof that it satisfies Property and squashed so that it fits into the monad m.

    Instances For
    noncomputable def Std.Iterators.HetT.ofPostconditionT {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : PostconditionT m α) :
    HetT m α

    Converts PostconditionT m α to HetT m α, preserving the postcondition property.

    Equations
    noncomputable instance Std.Iterators.instMonadLiftHetTOfMonad (m : Type w → Type w') [Monad m] :
    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Std.Iterators.HetT.lift {α : Type w} {m : Type w → Type w'} [Monad m] (x : m α) :
    HetT m α

    Lifts x : m α into HetT m α with the trivial postcondition.

    Caution: This is not a lawful monad lifting function

    Equations
    noncomputable def Std.Iterators.HetT.pure {m : Type w → Type w'} [Pure m] {α : Type v} (a : α) :
    HetT m α

    A universe-heterogeneous version of Pure.pure. Given a : α, it returns an element of HetT m α with the postcondition (a = ·).

    Equations
    noncomputable def Std.Iterators.HetT.pmap {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (x : HetT m α) (f : (a : α) → x.Property aβ) :
    HetT m β

    A generalization of HetT.map that provides the postcondition property to the mapping function.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Std.Iterators.HetT.map {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} (f : αβ) (x : HetT m α) :
    HetT m β

    A universe-heterogeneous version of Functor.map.

    Equations
    noncomputable def Std.Iterators.HetT.pbind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : HetT m α) (f : (a : α) → x.Property aHetT m β) :
    HetT m β

    A generalization of HetT.bind that provides the postcondition property to the mapping function.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Std.Iterators.HetT.bind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : HetT m α) (f : αHetT m β) :
    HetT m β

    A universe-heterogeneous version of Bind.bind.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable instance Std.Iterators.instFunctorHetT {m : Type w → Type w'} [Functor m] :
    Equations
    noncomputable instance Std.Iterators.instMonadHetT {m : Type w → Type w'} [Monad m] :
    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def Std.Iterators.HetT.prun {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (x : HetT m α) (f : (a : α) → x.Property am β) :
    m β

    Applies the given function to the result of the contained m-monadic operation with a proof that the postcondition property holds, returning another operation in m.

    Equations
    @[simp]
    theorem Std.Iterators.HetT.property_lift {α : Type w} {m : Type w → Type w'} [Monad m] {x : m α} :
    (lift x).Property = fun (x : α) => True
    @[simp]
    theorem Std.Iterators.HetT.prun_lift {α γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {x : m α} {f : (a : α) → (lift x).Property am γ} :
    (lift x).prun f = do let ax f a True.intro
    @[simp]
    @[simp]
    theorem Std.Iterators.HetT.prun_ofPostconditionT {m : Type u_1 → Type u_2} {α γ : Type u_1} [Monad m] [LawfulMonad m] {x : PostconditionT m α} {f : (x_1 : α) → (ofPostconditionT x).Property x_1m γ} :
    (ofPostconditionT x).prun f = do let ax.operation f a.val
    noncomputable def Std.Iterators.HetT.liftInner {α : Type u_1} {m : Type w → Type w'} (n : Type w → Type w'') [MonadLiftT m n] (x : HetT m α) :
    HetT n α

    If the monad m is liftable to n, lifts HetT m α to HetT n α.

    Equations
    @[simp]
    theorem Std.Iterators.HetT.property_liftInner {α : Type u_1} {m : Type w → Type w'} {n : Type w → Type w''} [MonadLiftT m n] {x : HetT m α} :
    @[simp]
    theorem Std.Iterators.HetT.prun_liftInner {α : Type u_1} {γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {x : HetT m α} {f : (a : α) → (liftInner n x).Property am γ} :
    ((liftInner n x).prun fun (a : α) (ha : (liftInner n x).Property a) => liftM (f a ha)) = liftM (x.prun f)
    theorem Std.Iterators.HetT.ext {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type v} {x y : HetT m α} (h : x.Property = y.Property) (h' : ∀ (β : Type w) (f : (a : α) → x.Property am β), x.prun f = y.prun fun (a : α) (ha : y.Property a) => f a ) :
    x = y
    theorem Std.Iterators.HetT.ext_iff {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type v} {x y : HetT m α} :
    x = y (h : x.Property = y.Property), ∀ (β : Type w) (f : (a : α) → x.Property am β), x.prun f = y.prun fun (a : α) (ha : y.Property a) => f a
    @[simp]
    theorem Std.Iterators.HetT.map_eq_pure_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : αβ} {x : HetT m α} :
    @[simp]
    theorem Std.Iterators.HetT.property_pure {m : Type w → Type w'} {α : Type u} [Monad m] [LawfulMonad m] {x : α} :
    (HetT.pure x).Property = fun (x_1 : α) => x = x_1
    @[simp]
    theorem Std.Iterators.HetT.prun_pure {m : Type w → Type w'} {α : Type u} {β : Type w} [Monad m] [LawfulMonad m] {x : α} {f : (a : α) → (HetT.pure x).Property am β} :
    (HetT.pure x).prun f = f x
    @[simp]
    theorem Std.Iterators.HetT.property_pbind {m : Type w → Type w'} {α : Type u} {β : Type v} [Monad m] [LawfulMonad m] {x : HetT m α} {f : (a : α) → x.Property aHetT m β} :
    (x.pbind f).Property = fun (b : β) => (a : α), (h : x.Property a), (f a h).Property b
    @[simp]
    theorem Std.Iterators.HetT.prun_pbind {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [Monad m] [LawfulMonad m] {x : HetT m α} {f : (a : α) → x.Property aHetT m β} {g : (b : β) → (x.pbind f).Property bm γ} :
    (x.pbind f).prun g = x.prun fun (a : α) (ha : x.Property a) => (f a ha).prun fun (b : β) (hb : (f a ha).Property b) => g b
    @[simp]
    theorem Std.Iterators.HetT.property_bind {m : Type w → Type w'} {α : Type u} {β : Type v} [Monad m] [LawfulMonad m] {x : HetT m α} {f : αHetT m β} :
    (x.bind f).Property = fun (b : β) => (a : α), x.Property a (f a).Property b
    @[simp]
    theorem Std.Iterators.HetT.prun_bind {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [Monad m] [LawfulMonad m] {x : HetT m α} {f : αHetT m β} {g : (b : β) → (x.bind f).Property bm γ} :
    (x.bind f).prun g = x.prun fun (a : α) (ha : x.Property a) => (f a).prun fun (b : β) (hb : (f a).Property b) => g b
    theorem Std.Iterators.HetT.bind_eq_pbind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} (x : HetT m α) (f : αHetT m β) :
    x.bind f = x.pbind fun (a : α) (x : x.Property a) => f a
    @[simp]
    theorem Std.Iterators.HetT.property_pmap {m : Type w → Type w'} {α : Type u} {β : Type v} [Monad m] [LawfulMonad m] {x : HetT m α} {f : (a : α) → x.Property aβ} :
    (x.pmap f).Property = fun (b : β) => (a : α), (h : x.Property a), f a h = b
    @[simp]
    theorem Std.Iterators.HetT.prun_pmap {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [Monad m] [LawfulMonad m] {x : HetT m α} {f : (a : α) → x.Property aβ} {g : (b : β) → (x.pmap f).Property bm γ} :
    (x.pmap f).prun g = x.prun fun (a : α) (ha : x.Property a) => g (f a ha)
    @[simp]
    theorem Std.Iterators.HetT.pure_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : αHetT m β} {a : α} :
    (HetT.pure a).bind f = f a
    @[simp]
    theorem Std.Iterators.HetT.bind_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {x : HetT m α} :
    @[simp]
    theorem Std.Iterators.HetT.bind_assoc {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x} {x : HetT m α} {f : αHetT m β} {g : βHetT m γ} :
    (x.bind f).bind g = x.bind fun (a : α) => (f a).bind g
    @[simp]
    theorem Std.Iterators.HetT.map_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : αβ} {a : α} :
    @[simp]
    theorem Std.Iterators.HetT.comp_map {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x} {f : αβ} {g : βγ} {x : HetT m α} :
    HetT.map (g f) x = HetT.map g (HetT.map f x)
    theorem Std.Iterators.HetT.prun_congr {m : Type w → Type w'} {α : Type u} {β : Type w} [Monad m] [LawfulMonad m] {x y : HetT m α} {f : (a : α) → x.Property am β} (h : x = y) :
    x.prun f = y.prun fun (a : α) (ha : y.Property a) => f a
    theorem Std.Iterators.HetT.pmap_congr {m : Type w → Type w'} {α : Type u} {β : Type v} [Monad m] [LawfulMonad m] {x y : HetT m α} {f : (a : α) → x.Property aβ} (h : x = y) :
    x.pmap f = y.pmap fun (a : α) (ha : y.Property a) => f a
    theorem Std.Iterators.HetT.pmap_map {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x} {x : HetT m α} {f : αβ} {g : (b : β) → (HetT.map f x).Property bγ} :
    (HetT.map f x).pmap g = x.pmap fun (a : α) (ha : x.Property a) => g (f a)
    theorem Std.Iterators.HetT.map_pmap {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {γ : Type x} {x : HetT m α} {f : (a : α) → x.Property aβ} {g : βγ} :
    HetT.map g (x.pmap f) = x.pmap fun (a : α) (ha : x.Property a) => g (f a ha)
    @[simp]
    theorem Std.Iterators.HetT.property_map {m : Type w → Type w'} [Functor m] {α : Type u} {β : Type v} {x : HetT m α} {f : αβ} {b : β} :
    (HetT.map f x).Property b (a : α), f a = b x.Property a
    @[simp]
    theorem Std.Iterators.HetT.liftInner_bind {m : Type w → Type w'} {n : Type w → Type w''} {α : Type u} {β : Type v} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] [LawfulMonad m] [LawfulMonad n] {x : HetT m α} {f : αHetT m β} :
    liftInner n (x.bind f) = (liftInner n x).bind fun (a : α) => liftInner n (f a)