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.5.tar.gz
sha512=433fbfc9b1f3828811fba93e176868ac190f3a861b49456adb24f8a0bee86c7454ce1f5edd143d14eda4b1a613d05ae5e746a748ea34c557695f0fa0f63af29a

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:Coinduction

Published: 30 Mar 2022

Dependencies (2)

  1. coq >= "8.15" & < "8.16~"
  2. ocaml

Dev Dependencies

None

Used by (1)

  1. coq-coinduction-examples < "1.7"

Conflicts

None