Document Open Access Logo

First-Order Guarded Coinduction in Coq

Author Łukasz Czajka

Thumbnail PDF


  • Filesize: 489 kB
  • 18 pages

Document Identifiers

Author Details

Łukasz Czajka
  • Faculty of Informatics, TU Dortmund University, Germany

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)


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
  • coinduction
  • Coq
  • guardedness
  • corecursion


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail