Document

# Defining Corecursive Functions in Coq Using Approximations

## File

LIPIcs.ECOOP.2022.12.pdf
• Filesize: 0.82 MB
• 24 pages

## Cite As

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 12:1-12:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.12

## Abstract

We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq’s standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq’s builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Functional constructs
##### Keywords
• corecursive function
• productiveness
• approximation
• Coq proof assistant

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. The Coq Proof Assistant. URL: https://coq.inria.fr/.
2. S. Banach. Sur les opérations dans les ensembles abstraits et leur applications aux équations intégrales. Fundam. Math., 3:133-181, 1922.
3. Y. Bertot. Filters on coinductive streams, an application to Eratosthenes' sieve. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 102-115, 2005.
4. Y. Bertot and E. Komendantskaya. Inductive and coinductive components of corecursive functions in Coq. In Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008, volume 203 of Electronic Notes in Theoretical Computer Science, pages 25-47, 2008.
5. Y. Bertot and V. Komendantsky. Fixed point semantics and partial recursion in Coq. In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain, pages 89-96, 2008.
6. J. Biendarra, J. C. Blanchette, M. Desharnais, L. Panny, A. Popescu, and D. Traytel. Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL. URL: https://isabelle.in.tum.de/doc/datatypes.pdf.
7. J. C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu, and D. Traytel. Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL. URL: https://isabelle.in.tum.de/dist/Isabelle2021/doc/corec.pdf.
8. A. Chlipala. Certified Programming with Dependent Types. MIT Press, 2013.
9. J. Forget. A Synchronous Language for Critical Embedded Systems with Multiple Real-Time Constraints. PhD thesis, Institut Supérieur de l’Aéronautique et de l’Espace, Toulouse, France, 2009.
10. S. R. Ghorpade and B. V. Limaye. A Course in Calculus and Real Analysis. Undergraduate Texts in Mathematics. Springer, 2018.
11. E. Giménez. Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, volume 996 of Lecture Notes in Computer Science, pages 39-59. Springer, 1994.
12. C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of parameterization in coinductive proof. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 193-206. ACM, 2013.
13. D. Kozen and N. Ruozzi. Applications of metric coinduction. Log. Methods Comput. Sci., 5(3), 2009.
14. The Lean Proof Assistant. URL: https://leanprover.github.io/.
15. K. Rustan M. Leino and M. Moskal. Co-induction simply - automatic co-inductive proofs in a program verifier. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 382-398. Springer, 2014.
16. C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. Available at URL: https://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf.
17. T. Uustalu and V. Vene. The essence of dataflow programming. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, volume 3780 of Lecture Notes in Computer Science, pages 2-18. Springer, 2005.
18. N. Veltri and N. van der Weide. Guarded recursion in agda via sized types. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 32:1-32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
19. G. Winskel. The Formal Semantics of Programming Languages, an introduction. MIT Press, 1993.
20. The Agda Proof Assistant. URL: https://agda.readthedocs.io/en/v2.6.2/getting-started/what-is-agda.html.
21. The Isabelle/HOL Proof Assistant. URL: https://isabelle.in.tum.de/.