Document Open Access Logo

Machine-Checked Categorical Diagrammatic Reasoning

Authors Benoît Guillemet, Assia Mahboubi , Matthieu Piquerez

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2024.7.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Interactive theorem proving
  • categories
  • diagrams
  • formal proof automation

Metrics

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

Abstract

This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language, which features dedicated proof commands to automate the synthesis, and the verification, of the technical parts often eluded in the literature.

Cite As Get BibTex

Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez. Machine-Checked Categorical Diagrammatic Reasoning. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSCD.2024.7

Author Details

Benoît Guillemet
  • École normale supérieure Paris-Saclay, France
Assia Mahboubi
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France
  • Vrije Universiteit Amsterdam, The Netherlands
Matthieu Piquerez
  • Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France

Funding

This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101001995).

Acknowledgements

The authors would like to thank the anonymous reviewers for their valuable comments and suggestions.

Supplementary Materials

References

  1. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. In TPHOLs, volume 5674 of Lecture Notes in Computer Science, pages 84-98. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_8.
  2. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Log. Methods Comput. Sci., 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:8)2018.
  3. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: a formalization of homotopy type theory in coq. In CPP, pages 164-172. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018615.
  4. Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In TPCD, volume A-10 of IFIP Transactions, pages 129-156. North-Holland, 1992. Google Scholar
  5. Luc Chabassier and Bruno Barras. A graphical interface for diagrammatic proofs in proof assistants. Contributed talks in the 29th International Conference on Types for Proofs and Programs (TYPES 2023), 2023. URL: https://types2023.webs.upv.es/TYPES2023.pdf.
  6. The Mathlib Community. The lean mathematical library. In CPP, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  7. Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: a proof assistant for finitely-presented globular n-categories. CoRR, abs/2402.13179, 2024. URL: https://doi.org/10.48550/arXiv.2402.13179.
  8. Burak Ekici and Cezary Kaliszyk. Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq. Math. Comput. Sci., 14(3):533-549, 2020. URL: https://doi.org/10.1007/s11786-020-00450-8.
  9. Jason Gross, Adam Chlipala, and David I. Spivak. Experience implementing a performant category-theory library in coq. In ITP, volume 8558 of Lecture Notes in Computer Science, pages 275-291. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_18.
  10. Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez. coq-diagram-chasing. https://gitlab.inria.fr/mpiquere/coq-diagram-chasing, 2024.
  11. Markus Himmel. Diagram chasing in interactive theorem proving. Bachelorarbeit. Karlsruher Institut für Technologie, 2020. URL: https://pp.ipd.kit.edu/uploads/publikationen/himmel20bachelorarbeit.pdf.
  12. Jason Z. S. Hu and Jacques Carette. Formalizing category theory in agda. In CPP, pages 327-342. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439922.
  13. Ambroise Lafont. A categorical diagram editor to help formalising commutation proofs. https://amblafont.github.io/graph-editor/index.html, 2024. Short paper presented in the Journées Francophones des Langages Applicatifs.
  14. F. William Lawvere and Stephen H. Schanuel. Conceptual mathematics. A first introduction to categories. Cambridge: Cambridge University Press, 2nd ed. edition, 2009. Google Scholar
  15. leanprover-community/mathlib. Condensed mathematics/snake lemma. URL: https://leanprover-community.github.io/archive/stream/267928-condensed-mathematics/topic/snake.20lemma.html, 2021.
  16. Saunders Mac Lane. Homology. Class. Math. Berlin: Springer-Verlag, reprint of the 3rd corr. print. 1975 edition, 1995. Google Scholar
  17. Saunders Mac Lane. Categories for the working mathematician, volume 5 of Grad. Texts Math. New York, NY: Springer, 2nd ed edition, 1998. Google Scholar
  18. Assia Mahboubi and Matthieu Piquerez. A first order theory of diagram chasing. In CSL, volume 288 of LIPIcs, pages 38:1-38:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.38.
  19. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  20. J. Peter May. A concise course in algebraic topology. Chicago, IL: University of Chicago Press, 1999. Google Scholar
  21. Yannis Monbru. Towards automatic diagram chasing. M1 report. École Normale Supérieure Paris-Saclay, 2022. URL: https://github.com/ymonbru/Diagram-chasing/blob/main/MONBRU_Yannis_Rapport.pdf.
  22. Matthieu Piquerez. Tropical Hodge theory and applications. PhD thesis, Institut Polytechnique de Paris, November 2021. URL: https://theses.hal.science/tel-03499730#.
  23. Emily Riehl. Category Theory in Context. Dover Publications, 2017. URL: https://math.jhu.edu/~eriehl/context.pdf.
  24. The Coq Development Team. The coq proof assistant, June 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  25. Amin Timany and Bart Jacobs. Category theory in coq 8.5. In FSCD, volume 52 of LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.30.
  26. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. Unimath - A computer-checked library of univalent mathematics. available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.10849216.
  27. John Wiegley. Category theory 1.0.0. https://github.com/jwiegley/category-theory/, 2022.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact