Induction principle for productive iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible skip successors of `it'.

Induction principle for productive monadic iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible skip successors of `it'.

Induction principle for finite iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible successors of `it'.

Induction principle for finite monadic iterators: One can define a function f that maps every iterator it to an element of motive it by defining f it in terms of the values of f on the plausible successors of `it'.

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.

Constructor

Std.Iterators.PostconditionT.mk.{w, w'}

Fields

Property : α → Prop

operation : m (Subtype self.Property)

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

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

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

Asserts that a certain iterator it could plausibly yield the value out after an arbitrary number of steps.

Constructors

Std.Iter.IsPlausibleIndirectOutput.direct.{w} {α β : Type w}
  [Iterator α Id β] {it : Iter β} {out : β} :
  it.IsPlausibleOutput out →
    it.IsPlausibleIndirectOutput out

Std.Iter.IsPlausibleIndirectOutput.indirect.{w}
  {α β : Type w} [Iterator α Id β] {it it' : Iter β}
  {out : β} :
  it'.IsPlausibleSuccessorOf it →
    it'.IsPlausibleIndirectOutput out →
      it.IsPlausibleIndirectOutput out

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.

Constructor

Std.Iterators.HetT.mk.{w, w', v}

Fields

Property : α → Prop

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

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

A noncomputable variant of IterM.step using the HetT monad. It is used in the definition of the equivalence relations on iterators, namely IterM.Equiv and Iter.Equiv.

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

Caution: This is not a lawful monad lifting function

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.

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

A universe-heterogeneous version of Functor.map.

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

A universe-heterogeneous version of Bind.bind.

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

Equivalence relation on iterators. Equivalent iterators behave the same as long as the internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same Iterator.IsPlausibleStep relation and their step functions are the same up to equivalence of the successor iterators. This coinductive definition captures the idea that the only relevant feature of an iterator is its step function. Other information retrievable from the iterator -- for example, whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence judgement.

Equivalence relation on monadic iterators. Equivalent iterators behave the same as long as the internal state of them is not directly inspected.

Two iterators (possibly of different types) are equivalent if they have the same Iterator.IsPlausibleStep relation and their step functions are the same up to equivalence of the successor iterators. This coinductive definition captures the idea that the only relevant feature of an iterator is its step function. Other information retrievable from the iterator -- for example, whether it is a list iterator or an array iterator -- is totally irrelevant for the equivalence judgement.