simp-based corecursive computation?

Stream: mathlib4

[Vasilii Nesterov]

Hi there! I'm working on a tactic to compute asymptotics of real functions based on this paper. The idea is to approximate functions using asymptotic series, perform computations on these series, and use the fact that a function is asymptotically equivalent to the leading term of its series. By "compute," I mean that for functions f and g with corresponding asymptotic series F and G, we can approximate f + g using F + G (where + is the operation on series), and similarly to other operations (*, /, log, exp, sin, etc.).

The most natural way to work with infinite series computationally is to implement them as a coinductive type, with operations defined corecursively. While Lean doesn't directly support coinductive types, they can be simulated (see docs#Stream' for example).

So, I think the tactic should work like this:

1. Transform an expression representing a function into an expression representing its asymptotic series
2. Apply a lemma that reduces the computation of the function's asymptotic to finding the leading term of the series
3. Compute this leading term

My main question is how to implement the third phase. My idea is to simulate lazy computation by reducing the target expression to the form destruct e, where e is an expression of some coinductive type (like Stream'). Then, reduce e to either nil, cons hd tl, or corec f a, which we know how to destruct, and then repeat until computation completed or some limit maxUnfoldSteps of destructions reached (to prevent infinite computation).

I will be happy to hear your suggestions on the tactic in general too.

[Patrick Massot]

I can’t help at all, but I want to encourage you working on this, this is great!

[Daniel Weber]

What is your question? How to do this concretely?

[Vasilii Nesterov]

I am quite new in metaprogramming. I'd like to know if my approach is adequate, is it doable? Also, maybe someone has already done something similar? Of course I will be glad to see some concrete examples!

[Daniel Weber]

https://github.com/lecopivo/SciLean SciLean has automatic differentiation, that might be similar

[Vasilii Nesterov]

My question is more about handling corecursive computation, but thank you, I'll take a look!

[Daniel Weber]

There is https://github.com/avigad/qpf for coinductive data