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

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

@[inline]

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

@[inline]

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

@[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 α.

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

@[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 function PostconditionT m α → PostconditionT m β, turning PostconditionT m into a monad.

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

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

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

theorem Std.Iterators.PostconditionT.run_eq_map {m : Type w → Type w'} [Monad m] {α : Type w} {x : PostconditionT m α} : x.run = Subtype.val <$> x.operation

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

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

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.operation_bind {m : Type w → Type w'} [Monad m] {α β : Type w} {x : PostconditionT m α} {f : α → PostconditionT m β} : (x.bind f).operation = do let a ← x.operation (fun (fa : Subtype (f a.val).Property) => ⟨fa.val, ⋯⟩) <$> (f a.val).operation

theorem Std.Iterators.PostconditionT.operation_bind' {m : Type w → Type w'} [Monad m] {α β : Type w} {x : PostconditionT m α} {f : α → PostconditionT m β} : (x >>= f).operation = do let a ← x.operation (fun (fa : Subtype (f a.val).Property) => ⟨fa.val, ⋯⟩) <$> (f a.val).operation

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

theorem Std.Iterators.PostconditionT.operation_bind_eq_operation_bind_mk {α β : Type w} {m : Type w → Type w'} [Monad m] {x : PostconditionT m α} {f : Subtype x.Property → m β} : x.operation >>= f = do let a ← x.operation f ⟨a.val, ⋯⟩

@[simp]

theorem Std.Iterators.PostconditionT.run_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {x : PostconditionT m α} {f : α → PostconditionT m β} : (x.bind f).run = do let x ← x.run (f x).run

@[simp]

theorem Std.Iterators.PostconditionT.run_bind' {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {x : PostconditionT m α} {f : α → PostconditionT m β} : (x >>= f).run = do let x ← x.run (f x).run

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

@[simp]

theorem Std.Iterators.PostconditionT.run_attachLift {m : Type w → Type w'} [Monad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type w} {x : m α} : (attachLift x).run = x

@[simp]

theorem Std.Iterators.PostconditionT.operation_attachLift {m : Type w → Type w'} [Monad m] [MonadAttach m] {α : Type w} {x : m α} : (attachLift x).operation = MonadAttach.attach x

instance Std.Iterators.instMonadLiftPostconditionT {m : Type w → Type w'} {n : Type w → Type w''} [MonadLift m n] : MonadLift (PostconditionT m) (PostconditionT n)

instance Std.Iterators.PostconditionT.instLawfulMonadLift {m : Type w → Type w'} {n : Type w → Type w''} [MonadLift m n] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLift m n] : LawfulMonadLift (PostconditionT m) (PostconditionT n)