package rocq-coinduction
A library for doing proofs by (enhanced) coinduction
Install
Dune Dependency
Authors
Maintainers
Sources
v1.22.tar.gz
sha512=f3a514574fa8fd237aca9fd9cc72c5873ea41eaeae75d5c195bd312051eb3a11fcb2616e7e137cea8bdfea655ec355c39a716e4bdfa2f23b7b916a99072e5598
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: 07 May 2026
Dependencies (1)
Dev Dependencies (1)
-
rocq-core
(>= "9.2" & < "9.3") | = "dev"
Used by (1)
-
rocq-coinduction-examples
>= "1.9"
Conflicts
None
On This Page