LIPIcs.ITP.2022.25.pdf
- Filesize: 0.77 MB
- 17 pages
Document
Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant
Author
Nicolas Magaud 
-
Part of:
Volume:
13th International Conference on Interactive Theorem Proving (ITP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-08-03
File
Document Identifiers
Author Details
Acknowledgements
We would like to thank Pascal Schreck for introducing us to the domain of (finite) projective geometry and the anonymous reviewers for their careful reading and suggestions.
Cite AsGet BibTex
Nicolas Magaud. Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.25
https://doi.org/10.4230/LIPIcs.ITP.2022.25
Abstract
We formally implement the smallest three-dimensional projective space PG(3,2) in the Coq proof assistant. This projective space features 15 points and 35 lines, related by an incidence relation. We define points and lines as two plain datatypes (one with 15 constructors for points, and one with 35 constructors for lines) and the incidence relation as a boolean function, instead of using the well-known coordinate-based approach relying on GF(2)⁴. We prove that this implementation actually verifies all the usual properties of three-dimensional projective spaces. We then use an oracle to compute some characteristic subsets of objects of PG(3,2), namely spreads and packings. We formally verify that these computed objects exactly correspond to the spreads and packings of PG(3,2). For spreads, this means identifying 56 specific sets of 5 lines among 360 360 (= 15× 14× 13× 12× 11) possible ones. We then classify them, showing that the 56 spreads of PG(3,2) are all isomorphic whereas the 240 packings of PG(3,2) can be classified into two distinct classes of 120 elements. Proving these results requires partially automating the generation of some large specification files as well as some even larger proof scripts. Overall, this work can be viewed as an example of a large-scale combination of interactive and automated specifications and proofs. It is also a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).
Subject Classification
ACM Subject Classification
- Theory of computation → Automated reasoning
- Theory of computation → Logic and verification
Keywords
- Coq
- projective geometry
- finite models
- spreads
- packings
- PG(3
- 2)
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Mickaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. Verifying SAT and SMT in Coq for a Fully Automated Decision Procedure. In International Workshop on Proof-Search in Axiomatic Theories and Type Theories (PSATTT'11), 2011.
-
Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development, Coq'Art : Thealculus of Inductive Constructions. Texts in Theoretical Computer Science, An EATCS Series. Springer-Verlag, Berlin/Heidelberg, May 2004. 469 pages.
- Anton Betten. The packings of pg(3, 3). Designs, Codes and Cryptography, 79(3):583-595, 2016. URL: https://doi.org/10.1007/s10623-015-0074-6.
- David Braun, Nicolas Magaud, and Pascal Schreck. Formalizing Some "Small" Finite Models of Projective Geometry in Coq. In Jacques Fleuriot, Dongming Wang, and Jacques Calmet, editors, Proceedings of Artificial Intelligence and Symbolic Computation 2018 (AISC'2018), number 11110 in LNAI, pages 54-69, September 2018. URL: https://hal.inria.fr/hal-01835493.
- Richard Hubert Bruck and Raj Chandra Bose. The construction of translation planes from projective spaces. Journal of Algebra, 1(1):85-102, 1964. URL: https://doi.org/10.1016/0021-8693(64)90010-9.
-
Francis Buekenhout, editor. Handbook of Incidence Geometry. North Holland, 1995.
- Frank Nelson Cole. Kirkman parades. Bull. Amer. Math. Soc., 28(9):435-437, December 1922. URL: https://projecteuclid.org:443/euclid.bams/1183485271.
- Coq development team. The Coq Proof Assistant Reference Manual, Version 8.13.2. INRIA, 2021. URL: http://coq.inria.fr.
-
Harold Scott Macdonald Coxeter. Projective Geometry. Springer Science & Business Media, 2003.
- Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Proceedings of TACAS 2008, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
- Georges Gonthier and Assia Mahboubi. A Small Scale Reflection Extension for the Coq system. Technical Report RR-6455, INRIA, 2008. URL: http://hal.inria.fr/inria-00258384/.
- Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A small scale reflection extension for the coq system. Research Report RR-6455, Inria, Saclay Ile de France, 2015. URL: https://hal.inria.fr/inria-00258384.
- John Harrison. Without loss of generality. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of LNCS, pages 43-59. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_3.
-
James William Peter Hirschfeld. Finite projective spaces of three dimensions. Oxford mathematical monographs. Clarendon Press ; New York : Oxford University Press, Oxford, 1985.
- R.H. Jeurissen. Special sets of lines in PG(3, 2). Linear Algebra and its Applications, 226-228:617-638, 1995. Honoring J.J. Seidel. URL: https://doi.org/10.1016/0024-3795(95)00200-B.
- Nicolas Magaud. Spreads and packings of pg(3,2), formally! Electronic Proceedings in Theoretical Computer Science, 352:107-115, December 2021. URL: https://doi.org/10.4204/eptcs.352.12.
- Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021. URL: https://doi.org/10.5281/zenodo.4457887.
- Brendan D. McKay. Isomorph-free exhaustive generation. Journal of Algorithms, 26(2):306-324, 1998. URL: https://doi.org/10.1006/jagm.1997.0898.
- Ronald C. Read. Every one a winner or how to avoid isomorphism search when cataloguing combinatorial configurations. In B. Alspach, P. Hell, and D.J. Miller, editors, Algorithmic Aspects of Combinatorics, volume 2 of Annals of Discrete Mathematics, pages 107-120. Elsevier, 1978. URL: https://doi.org/10.1016/S0167-5060(08)70325-X.