LIPIcs.ITP.2019.14.pdf
- Filesize: 489 kB
- 18 pages
Document
First-Order Guarded Coinduction in Coq
Author
Łukasz Czajka 
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Author Details
Cite AsGet BibTex
Łukasz Czajka. First-Order Guarded Coinduction in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 14:1-14:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.14
https://doi.org/10.4230/LIPIcs.ITP.2019.14
Abstract
We introduce two coinduction principles and two proof translations which, under certain conditions, map coinductive proofs that use our principles to guarded Coq proofs. The first principle provides an "operational" description of a proof by coinduction, which is easy to reason with informally. The second principle extends the first one to allow for direct proofs by coinduction of statements with existential quantifiers and multiple coinductive predicates in the conclusion. The principles automatically enforce the correct use of the coinductive hypothesis. We implemented the principles and the proof translations in a Coq plugin.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
- Theory of computation → Logic and verification
Keywords
- coinduction
- Coq
- guardedness
- corecursion
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads