Efficient infinite lazy lists

Stream: mathlib4

[Vasilii Nesterov]

Hi there! I am working on a new tactic that will be able to (verifiably) compute limits and asymptotics of real functions. Basically, I am implementing this paper: https://www21.in.tum.de/~eberlm/pdfs/real_asymp.pdf. For this I need efficient infinite lazy lists, which allows to reason about them (e.g. not sealed under partial). Is there something suitable for this in Lean/Mathlib? I see #7512 making Stream' efficient, but it is a draft.

[Patrick Massot]

This is great news! Thank you so much for working on this!

[Jannis Limperg]

Lean doesn't have coinductive types (except functions), so that rules out the obvious solution. I imagine your best bet would be to define an inefficient model of lazy lists in terms of functions, then override that with an efficient but unsafe implementation, using @[implementedBy] or @[csimp]. See docs#MLList for an example, though the model used there is trivial and therefore not suitable for proofs.

With that said, I would also investigate whether you can get around the lazy list requirement. In my experience, lazy lists may be elegant for certain applications, but they're never required. (At the end of the day, you only ever evaluate a finite prefix.)

[Enrico Borba]

Not to bring in a sledgehammer here, but are the ideas of the QPF paper applicable to introduce coinductive types? Not sure how "efficient" they would be, nor am I sure if this still wouldn't be "sealed" in some other way.

[Vasilii Nesterov]

I am intersted in this too. What is the status of the QpfTypes project? Are there plans to add support for conductive types to the compiler?

[Jannis Limperg]

Afaik nobody is actively working on coinductive types in any form.

[Kim Morrison]

The FRO is very keen to have coinductive predicates (not types; this is a smaller and easier target, but still useful for many applications) in Lean, but it's not on anyone's immediate roadmap.

[Enrico Borba]

Just for additional context there was some lean 4 work on QPF: https://lean-forward.github.io/pubs/keizer_msc_thesis.pdf