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.9.tar.gz
sha512=93b2390ba36c5a77768b9086ea33f12fc6bc205a363b23c351729ee19037b9f0cfa772ef72b602f91506401c27b20ea0300d739444fcdb9d3954d4ec7a8c0556

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:2024-03-18

Published: 18 Mar 2024

Dependencies (1)

  1. coq >= "8.19" & < "8.20"

Dev Dependencies

None

Used by (1)

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

Conflicts

None