package rocq-coinduction
A library for doing proofs by (enhanced) coinduction
Install
Dune Dependency
Authors
Maintainers
Sources
v1.21.tar.gz
sha512=00364c5dfe833c732bf4d9facdd2a666bf2d77233f97a4dca37dfceb70aeddd69eaad2f05f1eb8b4b65dba30d4c37c39da9e8a40be9ee1cf72696a37234b6d50
Description
Coinductive predicates are greatest fixpoints of monotone functions. The `companion' makes it possible to enhance the associated coinduction scheme. This library provides a formalisation on enhancements based on the companion, as well as tactics in making it straightforward to perform proofs by enhanced coinduction.
Tags
keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity logpath:Coinduction date:2025-09-17Published: 19 Sep 2025
Dependencies (1)
Dev Dependencies (1)
-
rocq-core
(>= "9.0" & < "9.1~") | = "dev"
Used by (1)
-
coq-coinduction
>= "1.21"
Conflicts
None
On This Page