Paco: A Coq Library for Parameterized Coinduction
The Paco library provides a tactic called "pcofix", replacing Coq's primitive cofix and avoiding its syntactic guardedness checking of proof terms. We have found that pcofix yields clear performance and usability benefits, even on simple examples.
- Library Source
The power of parameterization in coinductive proof.
In Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013).
[paper: pdf] [coq script: zip]
- The power of parameterization in coinductive proof.