package coq-coinduction
A library and plugin for doing proofs by (enhanced) coinduction
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.tar.gz
sha512=3bfc01ac723e861495025826b3a8491960dcfd84661e10ff1a88fc97b2c588687a90e2b4bfe1eba9603d85a8ee11ea33a719d3768be512f145dbac132ce3d1a1
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 logpath:CoinductionPublished: 26 Sep 2021
On This Page