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.7.tar.gz
sha512=d241f37b7d6e23c5970b2a2cb1e9c7c7134ad698687c5374566277d46f3efb25648304ccdbdcc3fe6f5d8ea4ff49ed40641c0a2c25501069e10efc5e7227bffc

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: 13 Jul 2023

Dependencies (2)

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

Dev Dependencies

None

Used by (1)

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

Conflicts

None