package coq-coinduction

  1. Overview
  2. No Docs
A library for doing proofs by (enhanced) coinduction

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

  1. D
    Damien Pous

Maintainers

  1. D
    damien.pous@ens-lyon.fr

Sources

v1.8.tar.gz
sha512=13510afe8db72f43790edaa14c3ce1aa55137c03e4494b6ac1f2e19dea0a24d19ec4493afc2ad7754da5421c0ee4eb60de813d3a341c418805fcf6c0e2fb7084

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:2023-10-20

Published: 20 Oct 2023

Dependencies (1)

  1. coq >= "8.16.1" & < "8.19~"

Dev Dependencies

None

Used by (1)

  1. coq-coinduction-examples >= "1.7"

Conflicts

None