@[unbox]

structure Std.Iterators.PostconditionT (m : Type w → Type w') (α : Type w) : Type (max w w')

PostconditionT m α represents an operation in the monad m together with a intrinsic proof that some postcondition holds for the α valued monadic result. It consists of a predicate P about α and an element of m ({ a // P a }) and is a helpful tool for intrinsic verification, notably termination proofs, in the context of iterators.

PostconditionT m is a monad if m is. However, note that PostconditionT m α is a structure, so that the compiler will generate inefficient code from recursive functions returning PostconditionT m α. Optimizations for ReaderT, StateT etc. aren't applicable for structures.

Moreover, PostconditionT m α is not a well-behaved monad transformer because PostconditionT.lift neither commutes with pure nor with bind.

• Property : α → Prop

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

• operation : m (Subtype self.Property)

  The actual monadic operation. Its return value is bundled together with a proof that it satisfies Property.

Instances For

• Std.Iterators.instFunctorPostconditionT
• Std.Iterators.instLawfulMonadPostconditionT
• Std.Iterators.instMonadPostconditionT

@[inline]

def Std.Iterators.PostconditionT.lift {α : Type w} {m : Type w → Type w'} [Functor m] (x : m α) : PostconditionT m α

Lifts an operation from m to PostconditionT m without asserting any nontrivial postcondition.

Caution: lift is not a lawful lift function. For example, pure a : PostconditionT m α is not the same as PostconditionT.lift (pure a : m α).

Equations

• Std.Iterators.PostconditionT.lift x = { Property := fun (x : α) => True, operation := (fun (x : α) => ⟨x, True.intro⟩) <$> x }

@[inline]

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

Equations

• Std.Iterators.PostconditionT.pure a = { Property := fun (y : α) => a = y, operation := pure ⟨a, ⋯⟩ }

@[inline]

def Std.Iterators.PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P : α → Prop} (x : m { α : α // P α }) : PostconditionT m α

Lifts a monadic value from m { a : α // P a } to a value PostconditionT m α.

Equations

• Std.Iterators.PostconditionT.liftWithProperty x = { Property := P, operation := x }

@[inline]

def Std.Iterators.PostconditionT.map {m : Type w → Type w'} [Functor m] {α β : Type w} (f : α → β) (x : PostconditionT m α) : PostconditionT m β

Given a function f : α → β, returns a a function PostconditionT m α → PostconditionT m β, turning PostconditionT m into a functor.

The postcondition of the x.map f states that the return value is the image under f of some a : α satisfying the x.Property.

Equations

• Std.Iterators.PostconditionT.map f x = { Property := fun (b : β) => ∃ (a : Subtype x.Property), f a.val = b, operation := (fun (a : Subtype x.Property) => ⟨f a.val, ⋯⟩) <$> x.operation }

@[inline]

def Std.Iterators.PostconditionT.bind {m : Type w → Type w'} [Monad m] {α β : Type w} (x : PostconditionT m α) (f : α → PostconditionT m β) : PostconditionT m β

Given a function α → PostconditionT m β, returns a a function PostconditionT m α → PostconditionT m β, turning PostconditionT m into a monad.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.PostconditionT.pbind {m : Type w → Type w'} [Monad m] {α β : Type w} (x : PostconditionT m α) (f : Subtype x.Property → PostconditionT m β) : PostconditionT m β

A version of bind that provides a proof of the previous postcondition to the mapping function.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Iterators.PostconditionT.liftMap {m : Type w → Type w'} [Monad m] {α β : Type w} (f : α → β) (x : m α) : PostconditionT m β

Lifts an operation from m to PostConditionT m and then applies PostconditionT.map.

Equations

• Std.Iterators.PostconditionT.liftMap f x = { Property := fun (b : β) => ∃ (a : α), f a = b, operation := (fun (a : α) => ⟨f a, ⋯⟩) <$> x }

@[inline]

def Std.Iterators.PostconditionT.run {m : Type w → Type w'} [Monad m] {α : Type w} (x : PostconditionT m α) : m α

Converts an operation from PostConditionT m to m, discarding the postcondition.

Equations

• x.run = (fun (a : Subtype x.Property) => a.val) <$> x.operation

instance Std.Iterators.instFunctorPostconditionT {m : Type w → Type w'} [Functor m] : Functor (PostconditionT m)

Equations

• Std.Iterators.instFunctorPostconditionT = { map := fun {α β : Type ?u.20} => Std.Iterators.PostconditionT.map }

instance Std.Iterators.instMonadPostconditionT {m : Type w → Type w'} [Monad m] : Monad (PostconditionT m)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Iterators.PostconditionT.pure_eq_pure {m : Type w → Type w'} [Monad m] {α : Type w} {a : α} : pure a = PostconditionT.pure a

@[simp]

theorem Std.Iterators.PostconditionT.property_pure {m : Type w → Type w'} [Monad m] {α : Type w} {x : α} : (pure x).Property = fun (x_1 : α) => x = x_1

@[simp]

theorem Std.Iterators.PostconditionT.operation_pure {m : Type w → Type w'} [Monad m] {α : Type w} {x : α} : (pure x).operation = pure ⟨x, ⋯⟩

theorem Std.Iterators.PostconditionT.ext {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type w} {x y : PostconditionT m α} (h : x.Property = y.Property) (h' : (fun (p : Subtype x.Property) => ⟨p.val, ⋯⟩) <$> x.operation = y.operation) : x = y

theorem Std.Iterators.PostconditionT.ext_iff {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type w} {x y : PostconditionT m α} : x = y ↔ ∃ (h : x.Property = y.Property), (fun (p : Subtype x.Property) => ⟨p.val, ⋯⟩) <$> x.operation = y.operation

@[simp]

theorem Std.Iterators.PostconditionT.map_eq_pure_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {f : α → β} {x : PostconditionT m α} : PostconditionT.map f x = x.bind (pure ∘ f)

@[simp]

theorem Std.Iterators.PostconditionT.pure_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {f : α → PostconditionT m β} {a : α} : (pure a).bind f = f a

@[simp]

theorem Std.Iterators.PostconditionT.bind_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α : Type w} {x : PostconditionT m α} : x.bind pure = x

@[simp]

theorem Std.Iterators.PostconditionT.bind_assoc {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β γ : Type w} {x : PostconditionT m α} {f : α → PostconditionT m β} {g : β → PostconditionT m γ} : (x.bind f).bind g = x.bind fun (a : α) => (f a).bind g

@[simp]

theorem Std.Iterators.PostconditionT.map_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {f : α → β} {a : α} : PostconditionT.map f (pure a) = pure (f a)

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

@[simp]

theorem Std.Iterators.PostconditionT.property_map {m : Type w → Type w'} [Functor m] {α β : Type w} {x : PostconditionT m α} {f : α → β} {b : β} : (PostconditionT.map f x).Property b ↔ ∃ (a : α), f a = b ∧ x.Property a

@[simp]

theorem Std.Iterators.PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α β : Type w} {x : PostconditionT m α} {f : α → β} : (PostconditionT.map f x).operation = (fun (a : Subtype x.Property) => ⟨f a.val, ⋯⟩) <$> x.operation

@[simp]

theorem Std.Iterators.PostconditionT.property_lift {m : Type w → Type w'} [Functor m] {α : Type w} {x : m α} : (lift x).Property = fun (x : α) => True

@[simp]

theorem Std.Iterators.PostconditionT.operation_lift {m : Type w → Type w'} [Functor m] {α : Type w} {x : m α} : (lift x).operation = (fun (x_1 : α) => ⟨x_1, ⋯⟩) <$> x