Definition of iterators

This module defines iterators and what it means for an iterator to be finite and productive.

structure Std.Iterators.IterM {α : Type w} (m : Type w → Type w') (β : Type w) : Type w

An iterator that sequentially emits values of type β in the monad m. It may be finite or infinite.

See the root module Std.Data.Iterators for a more comprehensive overview over the iterator framework.

See Std.Data.Iterators.Producers for ways to iterate over common data structures. By convention, the monadic iterator associated with an object can be obtained via dot notation. For example, List.iterM IO creates an iterator over a list in the monad IO.

See Std.Data.Iterators.Consumers for ways to use an iterator. For example, it.toList will convert a provably finite iterator it into a list and it.allowNontermination.toList will do so even if finiteness cannot be proved. It is also always possible to manually iterate using it.step, relying on the termination measures it.finitelyManySteps and it.finitelyManySkips.

See Iter for a more convenient interface in case that no monadic effects are needed (m = Id).

Internally, IterM m β wraps an element of type α containing state information. The type α determines the implementation of the iterator using a typeclass mechanism. The concrete typeclass implementing the iterator is Iterator α m β.

When using combinators, α can become very complicated. It is an implicit parameter of α so that the pretty printer will not print this large type by default. If a declaration returns an iterator, the following will not work:

def x : IterM IO Nat := [1, 2, 3].iterM IO

Instead the declaration type needs to be completely omitted:

def x := [1, 2, 3].iterM IO

-- if you want to ensure that `x` is an iterator in `IO` emitting `Nat`
def x := ([1, 2, 3].iterM IO : IterM IO Nat)

• internalState : α

  Internal implementation detail of the iterator.

structure Std.Iterators.Iter {α : Type w} (β : Type w) : Type w

An iterator that sequentially emits values of type β. It may be finite or infinite.

See the root module Std.Data.Iterators for a more comprehensive overview over the iterator framework.

See Std.Data.Iterators.Producers for ways to iterate over common data structures. By convention, the monadic iterator associated with an object can be obtained via dot notation. For example, List.iterM IO creates an iterator over a list in the monad IO.

See Std.Data.Iterators.Consumers for ways to use an iterator. For example, it.toList will convert a provably finite iterator it into a list and it.allowNontermination.toList will do so even if finiteness cannot be proved. It is also always possible to manually iterate using it.step, relying on the termination measures it.finitelyManySteps and it.finitelyManySkips.

See IterM for iterators that operate in a monad.

Internally, Iter β wraps an element of type α containing state information. The type α determines the implementation of the iterator using a typeclass mechanism. The concrete typeclass implementing the iterator is Iterator α m β.

When using combinators, α can become very complicated. It is an implicit parameter of α so that the pretty printer will not print this large type by default. If a declaration returns an iterator, the following will not work:

def x : Iter Nat := [1, 2, 3].iter

Instead the declaration type needs to be completely omitted:

def x := [1, 2, 3].iter

-- if you want to ensure that `x` is an iterator emitting `Nat`
def x := ([1, 2, 3].iter : Iter Nat)

• internalState : α

  Internal implementation detail of the iterator.

def Std.Iterators.Iter.toIterM {α β : Type w} (it : Iter β) : IterM Id β

Converts a pure iterator (Iter β) into a monadic iterator (IterM Id β) in the identity monad Id.

def Std.Iterators.IterM.toIter {α β : Type w} (it : IterM Id β) : Iter β

Converts a monadic iterator (IterM Id β) over Id into a pure iterator (Iter β).

@[simp]

theorem Std.Iterators.Iter.toIter_toIterM {α β : Type w} (it : Iter β) : it.toIterM.toIter = it

@[simp]

theorem Std.Iterators.Iter.toIter_comp_toIterM {α β : Type w} : IterM.toIter ∘ toIterM = id

@[simp]

theorem Std.Iterators.Iter.toIterM_toIter {α β : Type w} (it : IterM Id β) : it.toIter.toIterM = it

@[simp]

theorem Std.Iterators.Iter.toIterM_comp_toIter {α β : Type w} : toIterM ∘ IterM.toIter = id

inductive Std.Iterators.IterStep (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)

IterStep α β represents a step taken by an iterator (Iter β or IterM m β).

• yield {α : Sort u_1} {β : Sort u_2} (it : α) (out : β) : IterStep α β

  IterStep.yield it out describes the situation that an iterator emits out and provides it as the succeeding iterator.

• skip {α : Sort u_1} {β : Sort u_2} (it : α) : IterStep α β

  IterStep.skip it describes the situation that an iterator does not emit anything in this iteration and provides it' as the succeeding iterator.

  Allowing skip steps is necessary to generate efficient code from a loop over an iterator.

• done {α : Sort u_1} {β : Sort u_2} : IterStep α β

  IterStep.done describes the situation that an iterator has finished and will neither emit more values nor cause any monadic effects. In this case, no succeeding iterator is provided.

def Std.Iterators.IterStep.successor {α : Type u} {β : Type w} : IterStep α β → Option α

Returns the succeeding iterator stored in an iterator step or none if the step is .done and the iterator has finished.

@[inline]

def Std.Iterators.IterStep.mapIterator {α : Type u} {β : Type w} {α' : Type u'} (f : α → α') : IterStep α β → IterStep α' β

If present, applies f to the iterator of an IterStep and replaces the iterator with the result of the application of f.

@[simp]

theorem Std.Iterators.IterStep.mapIterator_yield {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} {it : α} {out : β} : mapIterator f (yield it out) = yield (f it) out

@[simp]

theorem Std.Iterators.IterStep.mapIterator_skip {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} {it : α} : mapIterator f (skip it) = skip (f it)

@[simp]

theorem Std.Iterators.IterStep.mapIterator_done {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} : mapIterator f done = done

@[simp]

theorem Std.Iterators.IterStep.mapIterator_mapIterator {α : Type u} {β : Type w} {α' : Type u'} {α'' : Type u''} {f : α → α'} {g : α' → α''} {step : IterStep α β} : mapIterator g (mapIterator f step) = mapIterator (g ∘ f) step

@[simp]

theorem Std.Iterators.IterStep.mapIterator_id {α : Type u} {β : Type w} {step : IterStep α β} : mapIterator id step = step

def Std.Iterators.PlausibleIterStep {α : Type u} {β : Type w} (IsPlausibleStep : IterStep α β → Prop) : Type (max 0 u w)

A variant of IterStep that bundles the step together with a proof that it is "plausible". The plausibility predicate will later be chosen to assert that a state is a plausible successor of another state. Having this proof bundled up with the step is important for termination proofs.

See IterM.Step and Iter.Step for the concrete choice of the plausibility predicate.

@[match_pattern]

def Std.Iterators.PlausibleIterStep.yield {α : Type u} {β : Type w} {IsPlausibleStep : IterStep α β → Prop} (it' : α) (out : β) (h : IsPlausibleStep (IterStep.yield it' out)) : PlausibleIterStep IsPlausibleStep

Match pattern for the yield case. See also IterStep.yield.

@[match_pattern]

def Std.Iterators.PlausibleIterStep.skip {α : Type u} {β : Type w} {IsPlausibleStep : IterStep α β → Prop} (it' : α) (h : IsPlausibleStep (IterStep.skip it')) : PlausibleIterStep IsPlausibleStep

Match pattern for the skip case. See also IterStep.skip.

@[match_pattern]

def Std.Iterators.PlausibleIterStep.done {α : Type u} {β : Type w} {IsPlausibleStep : IterStep α β → Prop} (h : IsPlausibleStep IterStep.done) : PlausibleIterStep IsPlausibleStep

Match pattern for the done case. See also IterStep.done.

@[reducible, inline]

abbrev Std.Iterators.PlausibleIterStep.casesOn {α : Type u} {β : Type w} {IsPlausibleStep : IterStep α β → Prop} {motive : PlausibleIterStep IsPlausibleStep → Sort x} (s : PlausibleIterStep IsPlausibleStep) (yield : (it' : α) → (out : β) → (h : IsPlausibleStep (IterStep.yield it' out)) → motive ⟨IterStep.yield it' out, h⟩) (skip : (it' : α) → (h : IsPlausibleStep (IterStep.skip it')) → motive ⟨IterStep.skip it', h⟩) (done : (h : IsPlausibleStep IterStep.done) → motive ⟨IterStep.done, h⟩) : motive s

A more convenient cases eliminator for PlausibleIterStep.

class Std.Iterators.Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) : Type (max w w')

The typeclass providing the step function of an iterator in Iter (α := α) β or IterM (α := α) m β.

In order to allow intrinsic termination proofs when iterating with the step function, the step object is bundled with a proof that it is a "plausible" step for the given current iterator.

• IsPlausibleStep : IterM m β → IterStep (IterM m β) β → Prop
• step (it : IterM m β) : m (PlausibleIterStep (IsPlausibleStep it))

@[inline]

def Std.Iterators.toIterM {α : Type w} (it : α) (m : Type w → Type w') (β : Type w) : IterM m β

Converts wraps the state of an iterator into an IterM object.

@[simp]

theorem Std.Iterators.toIterM_internalState {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (it : IterM m β) : toIterM it.internalState m β = it

@[simp]

theorem Std.Iterators.internalState_toIterM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (it : α) : (toIterM it m β).internalState = it

@[reducible, inline]

abbrev Std.Iterators.IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] : IterM m β → IterStep (IterM m β) β → Prop

Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means is up to the Iterator instance but it should be strong enough to allow termination proofs.

@[reducible, inline]

abbrev Std.Iterators.IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) : Type w

The type of the step object returned by IterM.step, containing an IterStep and a proof that this is a plausible step for the given iterator.

def Std.Iterators.IterM.IsPlausibleOutput {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (out : β) : Prop

Asserts that a certain output value could plausibly be emitted by the given iterator in its next step.

def Std.Iterators.IterM.IsPlausibleSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it' it : IterM m β) : Prop

Asserts that a certain iterator it' could plausibly be the directly succeeding iterator of another given iterator it.

def Std.Iterators.IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it' it : IterM m β) : Prop

Asserts that a certain iterator it' could plausibly be the directly succeeding iterator of another given iterator it while no value is emitted (see IterStep.skip).

@[inline]

def Std.Iterators.IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) : m it.Step

Makes a single step with the given iterator it, potentially emitting a value and providing a succeeding iterator. If this function is used recursively, termination can sometimes be proved with the termination measures it.finitelyManySteps and it.finitelyManySkips.

def Std.Iterators.Iter.IsPlausibleStep {α β : Type w} [Iterator α Id β] (it : Iter β) (step : IterStep (Iter β) β) : Prop

Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means is up to the Iterator instance but it should be strong enough to allow termination proofs.

def Std.Iterators.Iter.Step {α β : Type w} [Iterator α Id β] (it : Iter β) : Type w

The type of the step object returned by Iter.step, containing an IterStep and a proof that this is a plausible step for the given iterator.

@[inline]

def Std.Iterators.Iter.Step.toMonadic {α β : Type w} [Iterator α Id β] {it : Iter β} (step : it.Step) : it.toIterM.Step

Converts an Iter.Step into an IterM.Step.

@[inline]

def Std.Iterators.IterM.Step.toPure {α β : Type w} [Iterator α Id β] {it : IterM Id β} (step : it.Step) : it.toIter.Step

Converts an IterM.Step into an Iter.Step.

@[simp]

theorem Std.Iterators.IterM.Step.toPure_yield {α β : Type w} [Iterator α Id β] {it it' : IterM Id β} {out : β} {h : it.IsPlausibleStep (IterStep.yield it' out)} : toPure ⟨IterStep.yield it' out, h⟩ = PlausibleIterStep.yield it'.toIter out h

@[simp]

theorem Std.Iterators.IterM.Step.toPure_skip {α β : Type w} [Iterator α Id β] {it it' : IterM Id β} {h : it.IsPlausibleStep (IterStep.skip it')} : toPure ⟨IterStep.skip it', h⟩ = PlausibleIterStep.skip it'.toIter h

@[simp]

theorem Std.Iterators.IterM.Step.toPure_done {α β : Type w} [Iterator α Id β] {it : IterM Id β} {h : it.IsPlausibleStep IterStep.done} : toPure ⟨IterStep.done, h⟩ = PlausibleIterStep.done h

def Std.Iterators.Iter.IsPlausibleOutput {α β : Type w} [Iterator α Id β] (it : Iter β) (out : β) : Prop

Asserts that a certain output value could plausibly be emitted by the given iterator in its next step.

def Std.Iterators.Iter.IsPlausibleSuccessorOf {α β : Type w} [Iterator α Id β] (it' it : Iter β) : Prop

Asserts that a certain iterator it' could plausibly be the directly succeeding iterator of another given iterator it.

def Std.Iterators.Iter.IsPlausibleSkipSuccessorOf {α β : Type w} [Iterator α Id β] (it' it : Iter β) : Prop

Asserts that a certain iterator it' could plausibly be the directly succeeding iterator of another given iterator it while no value is emitted (see IterStep.skip).

@[inline]

def Std.Iterators.Iter.step {α β : Type w} [Iterator α Id β] (it : Iter β) : it.Step

Makes a single step with the given iterator it, potentially emitting a value and providing a succeeding iterator. If this function is used recursively, termination can sometimes be proved with the termination measures it.finitelyManySteps and it.finitelyManySkips.

class Std.Iterators.Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop

Finite α m asserts that IterM (α := α) m terminates after finitely many steps. Technically, this means that the relation of plausible successors is well-founded. Given this typeclass, termination proofs for well-founded recursion over an iterator it can use it.finitelyManySteps as a termination measure.

• wf : WellFounded IterM.IsPlausibleSuccessorOf

structure Std.Iterators.IterM.TerminationMeasures.Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over finite iterators. See also IterM.finitelyManySteps and Iter.finitelyManySteps.

• it : IterM m β

def Std.Iterators.IterM.TerminationMeasures.Finite.Rel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] : Finite α m → Finite α m → Prop

The relation of plausible successors on IterM.TerminationMeasures.Finite. It is well-founded if there is a Finite instance.

instance Std.Iterators.instWellFoundedRelationFiniteOfFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] : WellFoundedRelation (IterM.TerminationMeasures.Finite α m)

def Std.Iterators.IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] (it : IterM m β) : TerminationMeasures.Finite α m

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

theorem Std.Iterators.IterM.TerminationMeasures.Finite.rel_of_yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it it' : IterM m β} {out : β} (h : it.IsPlausibleStep (IterStep.yield it' out)) : { it := it' }.Rel { it := it }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with IterM.finitelyManySteps.

theorem Std.Iterators.IterM.TerminationMeasures.Finite.rel_of_skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it it' : IterM m β} (h : it.IsPlausibleStep (IterStep.skip it')) : { it := it' }.Rel { it := it }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with IterM.finitelyManySteps.

def Std.Iterators.Iter.finitelyManySteps {α β : Type w} [Iterator α Id β] [Finite α Id] (it : Iter β) : IterM.TerminationMeasures.Finite α Id

Termination measure to be used in well-founded recursive functions recursing over a finite iterator (see also Finite).

theorem Std.Iterators.Iter.TerminationMeasures.Finite.rel_of_yield {α β : Type w} [Iterator α Id β] {it it' : Iter β} {out : β} (h : it.IsPlausibleStep (IterStep.yield it' out)) : { it := it'.toIterM }.Rel { it := it.toIterM }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with IterM.finitelyManySteps.

theorem Std.Iterators.Iter.TerminationMeasures.Finite.rel_of_skip {α β : Type w} [Iterator α Id β] {it it' : Iter β} (h : it.IsPlausibleStep (IterStep.skip it')) : { it := it'.toIterM }.Rel { it := it.toIterM }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with IterM.finitelyManySteps.

theorem Std.Iterators.IterM.isPlausibleSuccessorOf_of_yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it' it : IterM m β} {out : β} (h : it.IsPlausibleStep (IterStep.yield it' out)) : it'.IsPlausibleSuccessorOf it

theorem Std.Iterators.IterM.isPlausibleSuccessorOf_of_skip {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] {it it' : IterM m β} (h : it.IsPlausibleStep (IterStep.skip it')) : it'.IsPlausibleSuccessorOf it

class Std.Iterators.Productive (α : Type u_1) (m : Type u_1 → Type u_2) {β : Type u_1} [Iterator α m β] : Prop

Productive α m asserts that IterM (α := α) m terminates or emits a value after finitely many skips. Technically, this means that the relation of plausible successors during skips is well-founded. Given this typeclass, termination proofs for well-founded recursion over an iterator it can use it.finitelyManySkips as a termination measure.

• wf : WellFounded IterM.IsPlausibleSkipSuccessorOf

structure Std.Iterators.IterM.TerminationMeasures.Productive (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Type w

This type is a wrapper around IterM so that it becomes a useful termination measure for recursion over productive iterators. See also IterM.finitelyManySkips and Iter.finitelyManySkips.

• it : IterM m β

def Std.Iterators.IterM.TerminationMeasures.Productive.Rel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] : Productive α m → Productive α m → Prop

The relation of plausible successors while skipping on IterM.TerminationMeasures.Productive. It is well-founded if there is a Productive instance.

instance Std.Iterators.instWellFoundedRelationProductiveOfProductive {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Productive α m] : WellFoundedRelation (IterM.TerminationMeasures.Productive α m)

def Std.Iterators.IterM.finitelyManySkips {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Productive α m] (it : IterM m β) : TerminationMeasures.Productive α m

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

theorem Std.Iterators.IterM.TerminationMeasures.Productive.rel_of_skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it it' : IterM m β} (h : it.IsPlausibleStep (IterStep.skip it')) : { it := it' }.Rel { it := it }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with IterM.finitelyManySkips.

def Std.Iterators.Iter.finitelyManySkips {α β : Type w} [Iterator α Id β] [Productive α Id] (it : Iter β) : IterM.TerminationMeasures.Productive α Id

Termination measure to be used in well-founded recursive functions recursing over a productive iterator (see also Productive).

theorem Std.Iterators.Iter.TerminationMeasures.Productive.rel_of_skip {α β : Type w} [Iterator α Id β] {it it' : Iter β} (h : it.IsPlausibleStep (IterStep.skip it')) : { it := it'.toIterM }.Rel { it := it.toIterM }

This theorem is used by a decreasing_trivial extension. It powers automatic termination proofs with Iter.finitelyManySkips.

instance Std.Iterators.instProductiveOfFinite {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Finite α m] : Productive α m