Document Open Access Logo

Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq

Author Enrico Tassi

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.29.pdf
  • Filesize: 395 kB
  • 18 pages

Document Identifiers

Author Details

Enrico Tassi
  • Université côte d'Azur - Inria, France

Cite As Get BibTex

Enrico Tassi. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.29

Abstract

We describe a procedure to derive equality tests and their correctness proofs from inductive type declarations in Coq. Programs and proofs are derived compositionally, reusing code and proofs derived previously. 
The key steps are two. First, we design appropriate induction principles for data types defined using parametric containers. Second, we develop a technique to work around the modularity limitations imposed by the purely syntactic termination check Coq performs on recursive proofs. The unary parametricity translation of inductive data types turns out to be the key to both steps.
Last but not least, we provide an implementation of the procedure for the Coq proof assistant based on the Elpi [Dunchev et al., 2015] extension language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
Keywords
  • Coq
  • Containers
  • Induction
  • Equality test
  • Parametricity translation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel. Type-based termination of generic programs. Sci. Comput. Program., 74(8):550-567, 2009. URL: https://doi.org/10.1016/j.scico.2008.01.004.
  2. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita Interactive Theorem Prover. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Automated Deduction - CADE-23, pages 64-69, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  3. Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. CIC\^: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, pages 257-271, 2006. URL: https://doi.org/10.1007/11916277_18.
  4. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly Modular (Co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 93-110, Cham, 2014. Springer International Publishing. Google Scholar
  5. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. Google Scholar
  6. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, Embeddable, λProlog Interpreter. In Proceedings of LPAR, Suva, Fiji, November 2015. URL: https://hal.inria.fr/hal-01176856.
  7. Ambrus Kaposi and András Kovács. A Syntax for Higher Inductive-Inductive Types. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, pages 20:1-20:18, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.20.
  8. Chantal Keller and Marc Lasson. Parametricity in an Impredicative Sort. In Patrick Cégielski and Arnaud Durand, editors, CSL - 26th International Workshop/21st Annual Conference of the EACSL - 2012, volume 16 of CSL, pages 381-395, Fontainebleau, France, September 2012. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.399.
  9. Assia Mahboubi and Enrico Tassi. Canonical Structures for the Working Coq User. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 19-34, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  10. Assia Mahboubi and Enrico Tassi. Mathematical Components. draft, v1-183-gb37ad7, 2018. Google Scholar
  11. Conor McBride, Healfdene Goguen, and James McKinna. A Few Constructions on Constructors. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, pages 186-200, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  12. Dale Miller. Abstract Syntax for Variable Binders: An Overview. In John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Computational Logic - CL 2000, pages 239-253, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg. Google Scholar
  13. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  14. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  15. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Google Scholar
  16. Jorge Luis Sacchini. On type-based termination and dependent pattern matching in the calculus of inductive constructions. Theses, École Nationale Supérieure des Mines de Paris, June 2011. URL: https://pastel.archives-ouvertes.fr/pastel-00622429.
  17. Tim Sheard and Simon Peyton Jones. Template Meta-programming for Haskell. SIGPLAN Not., 37(12):60-75, December 2002. URL: https://doi.org/10.1145/636517.636528.
  18. Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs '08, pages 278-293, Berlin, Heidelberg, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-71067-7_23.
  19. Enrico Tassi. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect). CoqPL, January 2018. URL: https://hal.inria.fr/hal-01637063.
  20. The Coq Development Team. The Coq Proof Assistant, version 8.8.0, April 2018. URL: https://doi.org/10.5281/zenodo.1219885.
  21. Dmitry Traytel, Andrei Popescu, and Jasmin C. Blanchette. Foundational, Compositional (Co)Datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS '12, pages 596-605, Washington, DC, USA, 2012. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2012.75.
  22. Philip Wadler. Theorems for Free! In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA '89, pages 347-359, New York, NY, USA, 1989. ACM. URL: https://doi.org/10.1145/99370.99404.
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 About DROPS Imprint Privacy Contact