Damien Pous' home page
This page is a web appendix the following paper, that appeared in Proc. LICS'16 (free pdf here).
We revisit coinductive proof principles from a lattice theoretic
point of view.
By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski's seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques).
The resulting theory encompasses parametrised coinduction, as recently proposed by Hur et al., and second-order reasoning, i.e., the ability to reason coinductively about the enhancements themselves. It moreover resolves an historical peculiarity about up-to context techniques.
Based on these results, we present an open-ended proof system allowing one to perform proofs on-the-fly and to neatly separate inductive and coinductive phases.
Most of the paper is formalised in the Coq proof assistant. Only the example about the pi-calculus is not covered.
The library is standalone; each module is documented; links below point to the coqdoc generated documentation. The coqdoc table of contents is here.
lattice: basic definitions and results about complete lattices
coinduction: our new abstract theory of coinduction, which covers
rel: properties specific to the complete lattice of binary relations
streams: examples in Rutten's stream calculus
ccs: examples in CCS
divergence: Hur et al.' toy example about divergence (not in the paper)
Thanks to this new theory, the library is extremely small: coqwc reports 721 lines of specifications, 622 lines of proofs, and 175 lines of comments.