A library for doing proofs by (enhanced) coinduction.
It is based on the notion of 'companion' from the paper Coinduction All the Way Up. Damien Pous. In Proc. LICS, 2016.
It contains:
Examples on how to use the library may be found in the associated coq-coinduction-examples package:
lattice.v
: complete lattices, monotone functions in such latticestower.v
: abstract theory of coinduction via tower inductionrel.v
: tools for the complete lattice of binary relationstactics.v
: tactics for coinductive predicates/relationscompanion.v
: abstract theory of the companion (no longer used)tests.v
: sanity checksall.v
: single module to load the library (despite the name, excludes companion and tests)Coinduction
The easiest way to install the latest released version of Coinduction is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-coinduction
To instead build and install manually, do:
git clone https://github.com/damien-pous/coinduction.git
cd coinduction
make
make install