source
def Std.Shrink (α : Type u) :
Type u

Currently, `Shrink α` is just a wrapper around `α`.

In the future, `Shrink` should allow shrinking `α` into a potentially smaller universe, given a proof that `α` is actually small, just like Mathlib's `Shrink`, except that the latter's conversion functions are noncomputable. Until then, `Shrink α` is always in the same universe as `α`.

This no-op type exists so that fewer breaking changes will be needed when the real `Shrink` type is available and the iterators will be made more flexible with regard to universes.

The conversion functions `Shrink.deflate` and `Shrink.inflate` form an equivalence between `α` and `Shrink α`, but this equivalence is intentionally not definitional.

Equations

- Std.Shrink α = Std.Internal.idOpaque✝.val α

Instances For

source
@[always_inline]
def Std.Shrink.deflate {α : Type u_1} (x : α) :
Shrink α

Converts elements of `α` into elements of `Shrink α`.

Equations

- Std.Shrink.deflate x = cast ⋯ x

Instances For

source
@[always_inline]
def Std.Shrink.inflate {α : Type u_1} (x : Shrink α) :
α

Converts elements of `Shrink α` into elements of `α`.

Equations

- x.inflate = cast ⋯ x

Instances For

source
@[simp]
theorem Std.Shrink.deflate_inflate {α : Type u_1} {x : Shrink α} :
deflate x.inflate = x
source
@[simp]
theorem Std.Shrink.inflate_deflate {α : Type u_1} {x : α} :
(deflate x).inflate = x
source
theorem Std.Shrink.inflate_inj {α : Type u_1} {x y : Shrink α} :
x.inflate = y.inflate ↔ x = y
source
theorem Std.Shrink.deflate_inj {α : Type u_1} {x y : α} :
deflate x = deflate y ↔ x = y
source
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 `Init.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.

Instances For

source
theorem Std.Iterators.IterM.ext {α : Type w} {m : Type w → Type w'} {β : Type w} {x y : IterM m β} (internalState : x.internalState = y.internalState) :
x = y
source
theorem Std.Iterators.IterM.ext_iff {α : Type w} {m : Type w → Type w'} {β : Type w} {x y : IterM m β} :
x = y ↔ x.internalState = y.internalState
source
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 `Init.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.

Instances For

source
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`.

Equations

- it.toIterM = { internalState := it.internalState }

Instances For

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

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

Equations

- it.toIter = { internalState := it.internalState }

Instances For

source
@[simp]
theorem Std.Iterators.Iter.toIter_toIterM {α β : Type w} (it : Iter β) :
it.toIterM.toIter = it
source
@[simp]
theorem Std.Iterators.Iter.toIter_comp_toIterM {α β : Type w} :
IterM.toIter ∘ toIterM = id
source
@[simp]
theorem Std.Iterators.Iter.toIterM_toIter {α β : Type w} (it : IterM Id β) :
it.toIter.toIterM = it
source
@[simp]
theorem Std.Iterators.Iter.toIterM_comp_toIter {α β : Type w} :
toIterM ∘ IterM.toIter = id
source
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.

Instances For

source
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.

Equations

- (Std.Iterators.IterStep.yield it out).successor = some it
- (Std.Iterators.IterStep.skip it).successor = some it
- Std.Iterators.IterStep.done.successor = none

Instances For

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

Equations

- Std.Iterators.IterStep.mapIterator f (Std.Iterators.IterStep.yield it out) = Std.Iterators.IterStep.yield (f it) out
- Std.Iterators.IterStep.mapIterator f (Std.Iterators.IterStep.skip it) = Std.Iterators.IterStep.skip (f it)
- Std.Iterators.IterStep.mapIterator f Std.Iterators.IterStep.done = Std.Iterators.IterStep.done

Instances For

source
@[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
source
@[simp]
theorem Std.Iterators.IterStep.mapIterator_skip {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} {it : α} :
mapIterator f (skip it) = skip (f it)
source
@[simp]
theorem Std.Iterators.IterStep.mapIterator_done {α : Type u} {β : Type w} {α' : Type u'} {f : α → α'} :
mapIterator f done = done
source
@[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
source
theorem Std.Iterators.IterStep.mapIterator_comp {α : Type u} {β : Type w} {α' : Type u'} {α'' : Type u''} {f : α → α'} {g : α' → α''} :
mapIterator (g ∘ f) = mapIterator g ∘ mapIterator f
source
@[simp]
theorem Std.Iterators.IterStep.mapIterator_id {α : Type u} {β : Type w} {step : IterStep α β} :
mapIterator id step = step
source
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.

Equations

- Std.Iterators.PlausibleIterStep IsPlausibleStep = Subtype IsPlausibleStep

Instances For

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

Equations

- Std.Iterators.PlausibleIterStep.yield it' out h = ⟨Std.Iterators.IterStep.yield it' out, h⟩

Instances For

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

Equations

- Std.Iterators.PlausibleIterStep.skip it' h = ⟨Std.Iterators.IterStep.skip it', h⟩

Instances For

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

Equations

- Std.Iterators.PlausibleIterStep.done h = ⟨Std.Iterators.IterStep.done, h⟩

Instances For

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

Equations

- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.yield it' out, h⟩ yield skip done = yield it' out h
- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.skip it', h⟩ yield skip done = skip it' h
- Std.Iterators.PlausibleIterStep.casesOn ⟨Std.Iterators.IterStep.done, h⟩ yield skip done = done h

Instances For

source
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 (Shrink (PlausibleIterStep (IsPlausibleStep it)))

Instances

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

Equations

- Std.Iterators.toIterM it m β = { internalState := it }

Instances For

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

Equations

- Std.Iterators.IterM.IsPlausibleStep = Std.Iterators.Iterator.IsPlausibleStep

Instances For

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

Equations

- it.Step = Std.Iterators.PlausibleIterStep it.IsPlausibleStep

Instances For

source
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.

Equations

- it.IsPlausibleOutput out = ∃ (it' : Std.IterM m β), it.IsPlausibleStep (Std.Iterators.IterStep.yield it' out)

Instances For

source
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`.

Equations

- it'.IsPlausibleSuccessorOf it = ∃ (step : Std.Iterators.IterStep (Std.IterM m β) β), step.successor = some it' ∧ it.IsPlausibleStep step

Instances For

source
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`).

Equations

- it'.IsPlausibleSkipSuccessorOf it = it.IsPlausibleStep (Std.Iterators.IterStep.skip it')

Instances For

source
@[inline]
def Std.Iterators.IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) :
m (Shrink 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`.

Equations

- it.step = Std.Iterators.Iterator.step it

Instances For

source
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.

Equations

- it.IsPlausibleStep step = it.toIterM.IsPlausibleStep (Std.Iterators.IterStep.mapIterator Std.Iterators.Iter.toIterM step)

Instances For

source
inductive Std.Iterators.IterM.IsPlausibleIndirectOutput {α β : Type w} {m : Type w → Type w'} [Iterator α m β] :
IterM m β → β → Prop

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

- direct {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it : IterM m β} {out : β} : it.IsPlausibleOutput out → it.IsPlausibleIndirectOutput out
- indirect {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it it' : IterM m β} {out : β} : it'.IsPlausibleSuccessorOf it → it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out

Instances For

source
inductive Std.Iterators.IterM.IsPlausibleIndirectSuccessorOf {α β : Type w} {m : Type w → Type w'} [Iterator α m β] :
IterM m β → IterM m β → Prop

Asserts that an iterator `it'` could plausibly produce `it'` as a successor iterator after finitely many steps. This relation is reflexive.

- refl {α β : Type w} {m : Type w → Type w'} [Iterator α m β] (it : IterM m β) : it.IsPlausibleIndirectSuccessorOf it
- cons_right {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it'' it' it : IterM m β} (h' : it''.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it

Instances For

source
theorem Std.Iterators.IterM.IsPlausibleIndirectSuccessorOf.trans {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it'' it' it : IterM m β} (h' : it''.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleIndirectSuccessorOf it) :
it''.IsPlausibleIndirectSuccessorOf it
source
theorem Std.Iterators.IterM.IsPlausibleIndirectSuccessorOf.single {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it' it : IterM m β} (h : it'.IsPlausibleSuccessorOf it) :
it'.IsPlausibleIndirectSuccessorOf it
source
theorem Std.Iterators.IterM.IsPlausibleIndirectOutput.trans {α β : Type w} {m : Type w → Type w'} [Iterator α m β] {it' it : IterM m β} {out : β} (h : it'.IsPlausibleIndirectSuccessorOf it) (h' : it'.IsPlausibleIndirectOutput out) :
it.IsPlausibleIndirectOutput out
source
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.

Equations

- it.Step = Std.Iterators.PlausibleIterStep it.IsPlausibleStep

Instances For

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

Equations

- step.toMonadic = ⟨Std.Iterators.IterStep.mapIterator Std.Iterators.Iter.toIterM step.val, ⋯⟩

Instances For

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

Equations

- step.toPure = ⟨Std.Iterators.IterStep.mapIterator Std.Iterators.IterM.toIter step.val, ⋯⟩

Instances For

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

Equations

- it.IsPlausibleOutput out = it.toIterM.IsPlausibleOutput out

Instances For

source
theorem Std.Iterators.Iter.isPlausibleOutput_iff_exists {α β : Type w} [Iterator α Id β] {it : Iter β} {out : β} :
it.IsPlausibleOutput out ↔ ∃ (it' : Iter β), it.IsPlausibleStep (IterStep.yield it' out)
source
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`.

Equations

- it'.IsPlausibleSuccessorOf it = it'.toIterM.IsPlausibleSuccessorOf it.toIterM

Instances For

source
theorem Std.Iterators.Iter.isPlausibleSuccessorOf_iff_exists {α β : Type w} [Iterator α Id β] {it' it : Iter β} :
it'.IsPlausibleSuccessorOf it ↔ ∃ (step : IterStep (Iter β) β), step.successor = some it' ∧ it.IsPlausibleStep step
source
inductive Std.Iterators.Iter.IsPlausibleIndirectOutput {α β : Type w} [Iterator α Id β] :
Iter β → β → Prop

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

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

Instances For

source
theorem Std.Iterators.Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM {α β : Type w} [Iterator α Id β] {it : Iter β} {out : β} :
it.IsPlausibleIndirectOutput out ↔ it.toIterM.IsPlausibleIndirectOutput out
source
inductive Std.Iterators.Iter.IsPlausibleIndirectSuccessorOf {α β : Type w} [Iterator α Id β] :
Iter β → Iter β → Prop

Asserts that an iterator `it'` could plausibly produce `it'` as a successor iterator after finitely many steps. This relation is reflexive.

- refl {α β : Type w} [Iterator α Id β] (it : Iter β) : it.IsPlausibleIndirectSuccessorOf it
- cons_right {α β : Type w} [Iterator α Id β] {it'' it' it : Iter β} (h' : it''.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleSuccessorOf it) : it''.IsPlausibleIndirectSuccessorOf it

Instances For

source
theorem Std.Iterators.Iter.isPlausibleIndirectSuccessor_iff_isPlausibleIndirectSuccessor_toIterM {α β : Type w} [Iterator α Id β] {it' it : Iter β} :
it'.IsPlausibleIndirectSuccessorOf it ↔ it'.toIterM.IsPlausibleIndirectSuccessorOf it.toIterM
source
theorem Std.Iterators.Iter.IsPlausibleIndirectSuccessorOf.trans {α β : Type w} [Iterator α Id β] {it'' it' it : Iter β} (h' : it''.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleIndirectSuccessorOf it) :
it''.IsPlausibleIndirectSuccessorOf it
source
theorem Std.Iterators.Iter.IsPlausibleIndirectOutput.trans {α β : Type w} [Iterator α Id β] {it' it : Iter β} {out : β} (h : it'.IsPlausibleIndirectSuccessorOf it) (h' : it'.IsPlausibleIndirectOutput out) :
it.IsPlausibleIndirectOutput out
source
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`).

Equations

- it'.IsPlausibleSkipSuccessorOf it = it'.toIterM.IsPlausibleSkipSuccessorOf it.toIterM

Instances For

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

Equations

- it.step = it.toIterM.step.run.inflate.toPure

Instances For

source
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

Instances

source
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 β

Instances For

source
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.

Equations

- Std.Iterators.IterM.TerminationMeasures.Finite.Rel = Relation.TransGen (InvImage Std.Iterators.IterM.IsPlausibleSuccessorOf Std.Iterators.IterM.TerminationMeasures.Finite.it)

Instances For

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

- Std.Iterators.instWellFoundedRelationFiniteOfFinite = { rel := Std.Iterators.IterM.TerminationMeasures.Finite.Rel, wf := ⋯ }

source
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`).

Equations

- it.finitelyManySteps = { it := it }

Instances For

source
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`.

source
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`.

source
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`).

Equations

- it.finitelyManySteps = it.toIterM.finitelyManySteps

Instances For

source
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`.

source
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`.

source
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
source
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
source
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

Instances

source
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 β

Instances For

source
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.

Equations

- Std.Iterators.IterM.TerminationMeasures.Productive.Rel = Relation.TransGen (InvImage Std.Iterators.IterM.IsPlausibleSkipSuccessorOf Std.Iterators.IterM.TerminationMeasures.Productive.it)

Instances For

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

- Std.Iterators.instWellFoundedRelationProductiveOfProductive = { rel := Std.Iterators.IterM.TerminationMeasures.Productive.Rel, wf := ⋯ }

source
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`).

Equations

- it.finitelyManySkips = { it := it }

Instances For

source
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`.

source
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`).

Equations

- it.finitelyManySkips = it.toIterM.finitelyManySkips

Instances For

source
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`.

source
instance Std.Iterators.instProductiveOfFinite {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Finite α m] :
Productive α m
source
class Std.Iterators.LawfulDeterministicIterator {β : Type w} (α : Type w) (m : Type w → Type w') [Iterator α m β] :
Prop

This typeclass characterizes iterators that have deterministic return values. This typeclass does not guarantee that there are no monadic side effects such as exceptions.

General monadic iterators can be nondeterministic, so that `it.IsPlausibleStep step` will be true for no or more than one choice of `step`. This typeclass ensures that there is exactly one such choice.

This is an experimental instance and it should not be explicitly used downstream of the standard library.

- isPlausibleStep_eq_eq (it : IterM m β) : ∃ (step : IterStep (IterM m β) β), it.IsPlausibleStep = fun (x : IterStep (IterM m β) β) => x = step

Instances