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.20.tar.gz
sha512=3deb03b51aa88e6329d33f7a4eed94f243343799ecab7eabced05976541ea239e076e31de100e128b2deb58bd2f681c71232adea20db7d4c4d459fa9a4a4bf46

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-09-18

Published: 18 Sep 2024

Dependencies (1)

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

Dev Dependencies

None

Used by (1)

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

Conflicts

None