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.