scan combinator for iterators

Stream: lean4

[cmlsharp]

I noticed there is no Std Iterator combinator for scan (like fold but it accumulates the partial results) so [1,2,3].iter.scan (. + .) 0 |>.toList would be [0,1,3,6]. You can see this in Haskell, Rust for example. I have an implementation that I believe works which I could package into a PR, but I had a bit of trouble precisely determining what i ought to include in the IsPlausibleStep definition, so i would appreciate some feedback/sanity checking if possible. I'm also decently new to Lean.

Implementation here

[Paul Reichert]

Hi, @cmlsharp, thanks for your suggestion. I think scan is a welcome addition to the standard library, so I'd be happy to see a PR for this combinator.

In Lean, we can only reason about code that provably terminates*, so while you can execute [1,2,3].iter.scan (. + .) 0 |>.toList, you will not be able to prove anything about the returned list without proving that [1,2,3].iter.scan (. + .) 0 is a finite iterator.

The IsPlausibleStep predicate is needed for proving that your iterator is finite by providing an Std.Iterators.Finite instance. It should simply be as strong as possible. Proving finiteness of it.scan f init given that it is finite (and productiveness given that it is productive), you will usually notice if your IsPlausibleStep predicate is too weak. In your case, I'm optimistic that it's strong enough since you have included all the proofs from the branches done (h, hs, hp) in it.

Before we can add scan to the standard library, the PR should include Std.Iterators.Finite and Std.Iterators.Productive instances for scan and there should be lemmas analogous to Std.Data.Iterators.Lemmas.Combinators.Drop, so that we have verified the basic properties of the iterator. Optionally -- and depending on how much time you are willing to invest -- you could also try implementing a generalization that takes a monadic accumulation function scanM similarly to foldM or mapM.

*) slight oversimplification