Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add coinduction to the Coq Platform #380

Open
palmskog opened this issue Oct 20, 2023 · 0 comments
Open

Add coinduction to the Coq Platform #380

palmskog opened this issue Oct 20, 2023 · 0 comments

Comments

@palmskog
Copy link
Collaborator

Coinduction is a Coq plugin and library for automation of proofs about coinductive relations. The plugin is in principle agnostic towards the underlying representation of these relations, e.g., if they involve positive coinductive types or negative coinductive types. One of the main advantages of using the plugin over, e.g., Coq's builtin cofix tactic is that users need not concern themselves with the cofix guard condition, which is typically only checked at Qed time by Coq. Coinduction is notably used in the Ctrees library (described in this paper).

Coinduction is part of Coq's CI and is maintained by @damien-pous. However, both myself and @YaZko could potentially help out with maintenance issues related to the Platform. In particular, I can help out with opam packaging.

I propose that coinduction is included in the Coq Platform. It fills an important niche and could help more people use coinductive relations effectively in their Coq developments. Coinduction currently has no dependencies besides Coq and Stdlib.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant