CoinductionExamples

Examples on how to use the rocq-coinduction library, a library for doing proofs by (enhanced) coinduction based on the notion of 'companion', from the paper: Coinduction All the Way Up. Damien Pous. In Proc. LICS, 2016.

• a formalisation of Hur et al's toy example on divergence
• a formalisation of Rutten's stream calculus
• a formalisation of Milner's calculus of communicating systems (CCS)
• a formalisation of automata and regular expression equivalence
• an example on how to use the companion to avoid the need for generalized parameterized coinduction

Modules

• divergence.v : Hur et al's example on divergence
• streams.v : Rutten's stream calculus
• ccs.v : Milner's CCS, strong and weak bisimilarity
• automata.v : Automata equivalence, regular expressions
• gpaco.v : generalized paco via the companion

Meta

• Author(s):
  • Damien Pous (initial)
• Rocq-community maintainer(s):
  • Damien Pous (@damien-pous)
• License: GNU LGPL
• Additional dependencies: rocq-coinduction, and rocq-aac-tactics + rocq-relation-algebra for the CCS example
• Rocq namespace: CoinductionExamples
• Related publication(s):
  • Coinduction All the Way Up doi:10.1145/2933575.2934564

Building and installation instructions

The easiest way to install the latest released version of CoinductionExamples is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install rocq-coinduction-examples

To instead build and install manually, do:

git clone https://github.com/damien-pous/coinduction-examples.git
cd coinduction-examples
make
make install

Compatibility

to see how to port code from coq-coinduction v1.6 to v1.7, check the following commit 7afec25f051cc4b45820c333bfd4b4689d86abef