Document Open Access Logo

First-Order Guarded Coinduction in Coq

Author Łukasz Czajka

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.14.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)
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)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. A. Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006. Google Scholar
  2. A. Abel and B. Pientka. Well-founded recursion with copatterns and sized types. J. Funct. Program., 26:e2, 2016. Google Scholar
  3. A. Abel, A. Vezzosi, and T. Winterhalter. Normalization by evaluation for sized dependent types. PACMPL, 1(ICFP):33:1-33:30, 2017. Google Scholar
  4. H. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, volume 2, pages 118-310. Oxford University Press, 1992. Google Scholar
  5. T. Coquand. Infinite Objects in Type Theory. In TYPES 1993, pages 62-78, 1993. Google Scholar
  6. Ł. Czajka. A New Coinductive Confluence Proof for Infinitary Lambda Calculus. Submitted, 2018. Google Scholar
  7. Ł. Czajka. Coinduction: an elementary approach. arXiv, 2019. URL: http://arxiv.org/abs/1501.04354.
  8. Ł. Czajka and C. Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reasoning, 61(1-4):423-453, 2018. Google Scholar
  9. H. Geuvers. Inductive and coinductive types with iteration and recursion. In TYPES 1992, pages 193-217, 1992. Google Scholar
  10. E. Giménez. Codifying Guarded Definitions with Recursive Schemes. In TYPES, pages 39-59, 1994. Google Scholar
  11. J. Hughes, L. Pareto, and A. Sabry. Proving the Correctness of Reactive Systems Using Sized Types. In POPL 1996, pages 410-423, 1996. Google Scholar
  12. C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of parameterization in coinductive proof. In POPL 2013, pages 193-206, 2013. Google Scholar
  13. B. Jacobs and J. Rutten. An introduction to (co)algebras and (co)induction. In Advanced Topics in Bisimulation and Coinduction, pages 38-99. Cambridge University Press, 2011. Google Scholar
  14. D. Kozen and A. Silva. Practical coinduction. Math. Struct. in Comp. Science, 27(7):1132-1152, 2017. Google Scholar
  15. N.P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic, 51:159-172, 1991. Google Scholar
  16. J. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Google Scholar
  17. J.L. Sacchini. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In LICS 2013, pages 233-242, 2013. Google Scholar
  18. D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  19. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  20. A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 1996. Google Scholar
  21. B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Paris Diderot University, France, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact