Documentation

Std.Data.Iterators.PostConditionMonad

@[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
    @[inline]
    def Std.Iterators.PostconditionT.lift {α : Type w} {m : Type w → Type w'} [Functor m] (x : 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
      Instances For
        @[inline]
        def Std.Iterators.PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P : αProp} (x : m { α : α // P α }) :

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

        Equations
          Instances For
            @[inline]
            def Std.Iterators.PostconditionT.map {m : Type w → Type w'} [Functor m] {α β : Type w} (f : αβ) (x : 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
              Instances For
                @[inline]
                def Std.Iterators.PostconditionT.bind {m : Type w → Type w'} [Monad m] {α β : Type w} (x : PostconditionT m α) (f : αPostconditionT m β) :

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

                Equations
                  Instances For
                    @[inline]
                    def Std.Iterators.PostconditionT.pbind {m : Type w → Type w'} [Monad m] {α β : Type w} (x : PostconditionT m α) (f : Subtype x.PropertyPostconditionT m β) :

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

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

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

                        Equations
                          Instances For
                            @[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
                              Instances For
                                @[simp]
                                theorem Std.Iterators.PostconditionT.computation_pure {m : Type w → Type w'} [Monad m] {α : Type w} {x : α} :
                                @[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.map_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m] {α β : Type w} {f : αβ} {a : α} :
                                @[simp]
                                theorem Std.Iterators.PostconditionT.property_map {m : Type w → Type w'} [Functor m] {α β : Type w} {x : PostconditionT m α} {f : αβ} {b : β} :
                                @[simp]
                                theorem Std.Iterators.PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α β : Type w} {x : PostconditionT m α} {f : αβ} :
                                @[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, True.intro) <$> x