Formalizing liveness properties with coinduction

Stream: CSLib

[Lef Ioannidis]

Hi folks,

This effort is very exciting! Especially hearing that non-standard (non-safety) properties like complexity are now in scope. I have myself worked on liveness properties with the goal of unifying Hoare Logic and Temporal Logic in a general structural way---our logic Ticl from OOPSLA '25 https://arxiv.org/abs/2410.14906 is a start. I am currently working on porting Ticl to Lean, and I think it can be useful in CSLib as it connects a lot of nodes in the library.

Should I be using https://github.com/alexkeizer/QpfTypes which seems to be in beta mode?
For bisimulation for example, which appears in your arxiv paper, how should one take the greatest fixpoint? Do you plan to merge Qpf in Lean, or is there some other recommended way to support coinductive relations? And more generally, do you see work on making coinduction more usuable like coq-coinduction (https://perso.ens-lyon.fr/damien.pous/cawu/) and Ticl also landing in CSLib or is it out of scope?

[Chris Henson]

Hi! I think that this is definitely in-scope for CSLib, but we have to think a bit about the encoding of coinduction.

I think that supporting QPFTypes as a dependency would be a bit difficult given its current disclaimer of being "not at all ready for serious use". Are you familiar with the work at #lean4 > Core support for coinductive predicates that is now released? I am not an expert in what this supports, but In his Lean Together talk I recall @Wojciech Różowski mentioning applications to CSLib. This was released slightly after the work on bisimulation (cc @Fabrizio Montesi), automata, etc. talked about in the arXiv paper, but I and some others have discussed using this in CSLib.

[Fabrizio Montesi]

I see @Wojciech Różowski as the way to go for many things, once it's cooked enough for what we have. Maybe it's cooked enough for some things already?

[Ching-Tsun Chou]

One thing I plan to do after my vacation is to see whether there is any applications of coinductive predicates in ωSequence and ωLanguage. But at first glance Lean's coinduction seems to work only on predicates, not on general data types. So there doesn't seem to be a direct way to use it to define (for example) infinite sequences or operations on infinite sequences (like ωSequence.flatten).

[Lef Ioannidis]

I was wondering how @Wojciech Różowski ‘s PR correlates to the FixedPoints.gfp definition in CompleteLattice, which includes the Knaster-Tarsky lemma. As far I understand we are still far from support for codata like stream, except by the Qpf extension. This also seems to be in scope for CSLib (ω sequences and traces for LTL), and something worthwhile to work on.