Coinduction?

Stream: lean4

[Siddharth Bhat]

I'd like to reason with infinite program traces in the style of interaction trees. I see that we have a coinductive keyword, but I'm not sure how to actually declare a coinductive type :)

[Simon Hudon]

Lean does not support coinduction natively. It has to be defined as a library which is something I've been working on

[Simon Hudon]

@Jeremy Avigad, @Mario Carneiro and I wrote a paper about it so we know what we want as a foundation but the implementation has taken longer than expected

[Mario Carneiro]

Jeremy tells me that a student of @Jasmin Blanchette is working on this

[Notification Bot]

Leonardo de Moura has marked this topic as resolved.

[Notification Bot]

Leonardo de Moura has marked this topic as unresolved.

[Jasmin Blanchette]

I have an MSc student who has started looking into developing a package based on QPFs -- we just had our first meeting with Jeremy on Monday. Here's a very good student, but I doubt he will have the time to finish anything by the time he has to hand in his MSc thesis, so it's more a long-term project if anything.

[Arthur Paulino]

What's QPF?

[Johan Commelin]

https://www.andrew.cmu.edu/user/avigad/Talks/qpf.pdf presumably

[Jeremy Avigad]

Conference paper here: https://drops.dagstuhl.de/opus/volltexte/2019/11061/. Isabelle has an excellent datatype package that uses a different though more-or-less equivalent construction; see here and references: https://arxiv.org/pdf/2104.05348.pdf.

[Siddharth Bhat]

I was under the impression that quotients in lean are not computable, and hence any coinductive code written using QPFs would not be extractable into programs? or am I mistaken? :)

[Mario Carneiro]

@Siddharth Bhat That is false on both counts: Quotients in lean are computable, but the code generated for QPFs would not be making use of this anyway and would use a different reduction mechanism than the one the kernel implements (which would inspect the QPF construction itself which is not what we want).

[Siddharth Bhat]

Thanks! I didn't know either of those facts

[Julien Marquet]

I'm interested in defining coinductive types too ! Technically, I'd like to work with a variant of streams
Is there a wip implementation of https://drops.dagstuhl.de/opus/volltexte/2019/11061/pdf/LIPIcs-ITP-2019-6.pdf publicly available ? (I'd understand if people were working on this but not willing to release their work for now)
Would it be possible to define some inductive datatypes "by hand", as a workaround for the lack of meta engineering while waiting for a proper implementation of the paper ? I mean, is it reasonably feasible, or the cost of manipulating low-level data is so high that I might as well spend this time writing an implementation ?

By the way, I have some time to spend on lean4, and I'm willing to help with defining coinductive data types :)

[Sébastien Michelland]

There is a working example with a simpler model (infinite sequence of agreeing finite structures) here: https://github.com/leanprover/lean/wiki/Coinductive-Types
(But my understanding is that QPF was considered after that and superseded it)

[Julien Marquet]

This page is very interesting, thanks !
It seems to answer one of my questions: it is possible to define coinductive data types "by hand", but it's a lot of work, all the more since I actually need reflexive coinductive types...

[Alex Keizer]

I'm the student Jasmin mentioned! My work so far can be seen at https://github.com/alexkeizer/qpf4. It is very WIP, I'm still working on porting the formalizations of QPFs to lean4 so you cannot write stuff by hand using it.

[Sébastien Michelland]

I believe that goal was always to have coinductive definitions compile down to a construction like this or QPF. The Lean4 kernel is purposefully kept small so you won't have native support like in Coq.

[Alex Keizer]

Ah, I misremembered. I've actually gotten most of it to compile, so you could hand-write stuff now, but it uses sorry very liberally, so probably wouldn't recommend doing so. If anyone wants to contribute, feel free to try to provide proofs for some of those sorrys!

[Jannis Limperg]

Julien Marquet said:

Technically, I'd like to work with a variant of streams.

If you only need streams, stream A is isomorphic to Nat -> A. Coinductive types only become interesting once you have a non-degenerate tree structure.