Coinduction All the Way Up

This page is a web appendix the following paper, that appeared in Proc. LICS'16 (free pdf here).

Abstract

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.

Coq proofs

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
• Knaster-Tarski revisited with the companion
• second order coinductive reasoning about the companion
• symmetry arguments
• parametrised coinduction with the companion
• closing the gap between respectfulness and compatibility
• `rel`: properties specific to the complete lattice of binary relations
• `streams`: examples in Rutten's stream calculus
• shuffle product
• convolution product (not in the paper)
• `ccs`: examples in CCS
• up-to congruence in the full calculus of CCS (including the replication context)
• a simple example about recursive processes
• `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.