Document Open Access Logo

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description)

Authors Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.34.pdf
  • Filesize: 0.64 MB
  • 21 pages

Document Identifiers

Author Details

Cyril Cohen
  • Université Côte d'Azur, Inria, Sophia Antipolis, France
Kazuhiko Sakaguchi
  • University of Tsukuba, Japan
Enrico Tassi
  • Université Côte d'Azur, Inria, Sophia Antipolis, France

Acknowledgements

We are particularly grateful to Georges Gonthier, Assia Mahboubi and Florent Hivert for the many discussions we had that were instrumental in coining the concepts formalized here. We thank as well other developers of the Mathematical Components library and members of Dagstuhl seminar 18341, for the helpful discussions we had. We also thank many Coq developers and users who showed interest and support in this work. Finally, we thank the anonymous reviewers of this paper for their useful comments.

Cite AsGet BibTex

Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.34

Abstract

It is nowadays customary to organize libraries of machine checked proofs around hierarchies of algebraic structures. One influential example is the Mathematical Components library on top of which the long and intricate proof of the Odd Order Theorem could be fully formalized. Still, building algebraic hierarchies in a proof assistant such as Coq requires a lot of manual labor and often a deep expertise in the internals of the prover. Moreover, according to our experience, making a hierarchy evolve without causing breakage in client code is equally tricky: even a simple refactoring such as splitting a structure into two simpler ones is hard to get right. In this paper we describe HB, a high level language to build hierarchies of algebraic structures and to make these hierarchies evolve without breaking user code. The key concepts are the ones of factory, builder and abbreviation that let the hierarchy developer describe an actual interface for their library. Behind that interface the developer can provide appropriate code to ensure backward compatibility. We implement the HB language in the hierarchy-builder addon for the Coq system using the Elpi extension language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal language definitions
  • Theory of computation → Type theory
  • Theory of computation → Constraint and logic programming
  • Computing methodologies → Symbolic and algebraic manipulation
Keywords
  • Algebraic Hierarchy
  • Packed Classes
  • Coq
  • Elpi
  • Metaprogramming
  • λProlog

Metrics

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

Supplementary Materials

References

  1. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: a case study in functional analysis. accepted in the proceedings of IJCAR 2020, available at https://hal.inria.fr/hal-02463336, 2020. URL: https://hal.inria.fr/hal-02463336.
  2. Reynald Affeldt, David Nowak, and Takafumi Saikawa. A hierarchy of monadic effects for program verification using equational reasoning. In Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, pages 226-254, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_9.
  3. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. The Matita interactive theorem prover. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings, pages 64-69, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_7.
  4. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 84-98, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  5. Gerhard Betsch. On the beginnings and development of near-ring theory. In Near-rings and near-fields. Proceedings of the conference held in Fredericton, New Brunswick, July 18-24, 1993, pages 1-11. Mathematics and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, 1995. Google Scholar
  6. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41-62, 2015. URL: https://doi.org/10.1007/s11786-014-0181-1.
  7. Jacques Carette and Russell O'Connor. Theory presentation combinators. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics, pages 202-215, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  8. Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. PhD thesis, Ecole Polytechnique X, 2012. URL: https://pastel.archives-ouvertes.fr/pastel-00780446.
  9. The Coq Development Team. The Coq Proof Assistant Reference Manual, version 8.11, October 2020. URL: http://coq.inria.fr.
  10. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 378-388, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  11. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λProlog interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, pages 460-468, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_32.
  12. Erich Gamma. Design patterns: elements of reusable object-oriented software. Pearson Education India, 1995. Google Scholar
  13. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pages 327-342, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_23.
  14. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pages 163-179, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_14.
  15. Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), pages 363-371, September 2016. Google Scholar
  16. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pages 279-294. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  17. Assia Mahboubi and Enrico Tassi. Canonical structures for the working coq user. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pages 19-34, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_5.
  18. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-–381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  19. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, New York, NY, USA, 1st edition, 2012. Google Scholar
  20. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI ’88, page 199–208, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/53990.54010.
  21. Robert Pollack. Dependently typed records in type theory. Formal Aspects of Computing, 13:386–402, 2002. URL: https://doi.org/10.1007/s001650200018.
  22. Florian Rabe and Michael Kohlhase. A scalable module system. Information and Computation, 230:1-54, 2013. URL: https://doi.org/10.1016/j.ic.2013.06.001.
  23. Damien Rouhling. Formalisation Tools for Classical Analysis - A Case Study in Control Theory. PhD thesis, Université Côte d'Azur, 2019. URL: https://hal.inria.fr/tel-02333396.
  24. Amokrane Saïbi. Typing algorithm in type theory with inheritance. In 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), Paris, France, 15-17 January 1997, pages 292-301. ACM, 1997. Google Scholar
  25. Amokrane Saïbi. Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). PhD thesis, Pierre and Marie Curie University, Paris, France, 1999. URL: https://tel.archives-ouvertes.fr/tel-00523810.
  26. Kazuhiko Sakaguchi. Validating mathematical structures. accepted in the proceedings of IJCAR 2020, available at https://arxiv.org/abs/2002.00620, 2020. URL: https://arxiv.org/abs/2002.00620.
  27. Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. Mathematical Structures in Computer Science, 21(4):795-825, 2011. URL: https://doi.org/10.1017/S0960129511000119.
  28. Enrico Tassi. Coq-Elpi, Coq plugin embedding Elpi. https://github.com/LPCIC/coq-elpi, 2020. URL: https://github.com/LPCIC/coq-elpi.
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