Awesome

Paco: Coq library for Parametric Coinduction

Paco is a Coq library for parametric coinduction. For more information, please see:

• Chung-Kil Hur, Georg Neis, Derek Dreyer and Viktor Vafeiadis. The power of parameterization in coinductive proof. POPL 2013.
• Yannick Zakowski, Paul He, Chung-Kil Hur and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. CPP 2020.

Paco also supports upto techniques using "companion". See:

• Damien Pous. Coinduction All the Way Up. LICS 2016.

Minki Cho refactored the implementation to speed up the compilation time.

The current version is v4.1.2, and it's compatible with Coq 8.13 - 8.15.

Installation

# from opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-paco

# from source
cd src; make; make install          # for library files
cd webpage; make                    # for documentation

Examples

See /src/examples.v and /src/tutorial.v for examples.