package coq-coinduction

  1. Overview
  2. No Docs
A library and plugin 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.0.tar.gz
sha512=47d3a3dc7a2bbbd361131344b08133160353df3997a5df9bae4e6f91ee128b6d9212308ffd7709e9a0379abb4314e569353dba55062c61e0196bce0a4258e1c0

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 keyword:streams keyword:CCS logpath:Coinduction

Published: 28 Jul 2021

Dependencies (3)

  1. coq-aac-tactics
  2. coq >= "8.13" & < "8.15~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None