Specify and reason about all values produced by iterator

Stream: Is there code for X?

[Qiyuan Zhao]

Is there any approach to specifying and reasoning about the collection of all values produced by an iterator? For example, is there a way to specify that "the iterator never produces the same value twice" or "the iterator produces all possible values of this type"? I searched on Loogle and didn't find any related definitions. It seems that one indirect way to do so is to specify over the iterator.toList, but I'm not sure if that's a good one.

[Matt Diamond]

When you say "iterator" are you referring to iterated function application (docs#Nat.iterate)?

[Qiyuan Zhao]

Oh sorry, I forgot to mention that the "iterator" here refers to the iterators in Std.Data.Iterators.

[Paul Reichert]

As long as you're only working on finite iterators (and if your iterators don't have side effects; Iter not IterM), then I'd say specifying these kinds of behaviors using toList is a robust solution. Does that restriction apply to your use case?

We still need to find out how such properties can conveniently be verified for non-finite or monadic iterators. The iterators have complicated dependent types and have an ill-behaved equality and we can't change that for efficiency reasons. One approach I'd like to try out in the future is to introduce noncomputable, bundled iterators. On these, it becomes easier to apply equational reasoning, and we might provide a library for LTL-style predicates on these. But this is very much an open question.

[Jakub Nowak]

For the "the iterator produces all possible values of this type", maybe something like this?

def Std.Iter.IsComplete [Iterator α Id β] (it : Iter (α := α) β) : Prop :=
  ∀ b, it.IsPlausibleIndirectOutput b

[Paul Reichert]

That generally works, but such predicates relying on IsPlausibleIndirectOutput don't compose well. We can't express (it.filter f).IsComplete in terms of it.IsComplete or even IsPlausibleIndirectOutput (I think, at least not easily). This is where the LTL idea comes from. (We'd also want a way to apply the same predicate on iterators of different types, which is difficult to achieve without bundled iterators.)

If you're only interested in finite iterators, I'd go with the toList-based formulation because you will get API lemmas that compose better.