class Std.Internal.ComputableSmall (α : Type v) : Type (max (u + 1) v)

• Target : Type u
• deflate : α → Target α
• inflate : Target α → α
• deflate_inflate {a : Target α} : deflate (inflate a) = a
• inflate_deflate {a : α} : inflate (deflate a) = a

class Std.Internal.Small (α : Type v) : Prop

• h : Nonempty (ComputableSmall α)

Instances

• Std.Internal.instSmall
• Std.Internal.instSmallSigma
• Std.Internal.instSmallSubtype
• Std.Internal.instSmallSubtypeEq
• Std.Internal.instSmallSubtypeEq_1
• Std.Internal.instSmallSubtypeExistsEq

noncomputable def Std.Internal.ComputableSmall.choose (α : Type v) [small : Small α] : ComputableSmall α

Equations

• Std.Internal.ComputableSmall.choose α = Classical.ofNonempty

structure Std.Internal.USquash (α : Type v) [small : Small α] : Type u

• mk' :: (
• inner : ComputableSmall.Target α
• )

def Std.Internal.USquashOrUnit (α : Type v) : Type u

Equations

• Std.Internal.USquashOrUnit α = if x : Std.Internal.Small α then Std.Internal.USquash α else PUnit

theorem Std.Internal.uSquash_eq_uSquashOrUnit {α : Type v} [Small α] : USquash α = USquashOrUnit α

noncomputable def Std.Internal.USquash.deflate {α : Type v} [small : Small α] (x : α) : USquash α

Equations

• Std.Internal.USquash.deflate x = { inner := Std.Internal.ComputableSmall.deflate x }

noncomputable def Std.Internal.USquash.inflate {α : Type v} [small : Small α] (x : USquash α) : α

Equations

• x.inflate = Std.Internal.ComputableSmall.inflate x.inner

@[simp]

theorem Std.Internal.USquash.deflate_inflate {α : Type v} {x✝ : Small α} {x : USquash α} : deflate x.inflate = x

@[simp]

theorem Std.Internal.USquash.inflate_deflate {α : Type v} {x✝ : Small α} {x : α} : (deflate x).inflate = x

theorem Std.Internal.USquash.inflate.inj {α : Type v} {x✝ : Small α} {x y : USquash α} (h : x.inflate = y.inflate) : x = y

instance Std.Internal.instSmall {α : Type v} : Small α

instance Std.Internal.instSmallSubtype {α : Type v} [Small α] {p : α → Prop} : Small (Subtype p)

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) : Small β

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.

• small : Internal.Small (Subtype self.Property)

  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

• Std.Iterators.instFunctorHetT
• Std.Iterators.instLawfulMonadHetT
• Std.Iterators.instMonadHetT
• Std.Iterators.instMonadLiftHetTOfMonad

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

• Std.Iterators.HetT.ofPostconditionT x = { Property := x.Property, small := ⋯, operation := Std.Internal.USquash.deflate <$> x.operation }

noncomputable instance Std.Iterators.instMonadLiftHetTOfMonad (m : Type w → Type w') [Monad m] : MonadLift m (HetT 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

• Std.Iterators.HetT.lift x = liftM x

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

• Std.Iterators.HetT.pure a = { Property := fun (x : α) => a = x, small := ⋯, operation := pure (Std.Internal.USquash.deflate ⟨a, ⋯⟩) }

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

• Std.Iterators.HetT.map f x = x.pmap fun (a : α) (x : x.Property a) => f a

noncomputable def Std.Iterators.HetT.pbind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v} (x : HetT m α) (f : (a : α) → x.Property a → HetT 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] : Functor (HetT m)

Equations

• Std.Iterators.instFunctorHetT = { map := fun {α β : Type ?u.19} => Std.Iterators.HetT.map }

noncomputable instance Std.Iterators.instMonadHetT {m : Type w → Type w'} [Monad m] : Monad (HetT 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 a → m β) : 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

• x.prun f = do let a ← x.operation f a.inflate.val ⋯

@[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 a → m γ} : (lift x).prun f = do let a ← x f a True.intro

@[simp]

theorem Std.Iterators.HetT.property_ofPostconditionT {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] {x : PostconditionT m α} : (ofPostconditionT x).Property = x.Property

@[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_1 → m γ} : (ofPostconditionT x).prun f = do let a ← x.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

• Std.Iterators.HetT.liftInner n x = { Property := x.Property, small := ⋯, operation := liftM x.operation }

@[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 α} : (liftInner n x).Property = x.Property

@[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 a → m γ} : ((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 a → m β), 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 a → m β), 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 α} : HetT.map f x = x.bind (HetT.pure ∘ f)

@[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 a → m β} : (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 a → HetT 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 a → HetT m β} {g : (b : β) → (x.pbind f).Property b → m γ} : (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 b → m γ} : (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 b → m γ} : (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 α} : x.bind HetT.pure = x

@[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 : α} : HetT.map f (HetT.pure a) = HetT.pure (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 a → m β} (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)

instance Std.Iterators.instLawfulMonadHetT {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] : LawfulMonad (HetT m)

@[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)