Abstract
We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues’ property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The perspector is the point at which the three lines connecting the vertices of two perspective triangles concur.
- 2.
Computer setup: Intel(R) Core(TM) i5-4460 CPU @ 3.20 GHz with 16G of memory.
- 3.
An interactive representation of pg(3, 2) can be viewed on wolfram web site: http://demonstrations.wolfram.com/15PointProjectiveSpace/.
- 4.
Fully-specified functions can be automatically defined using the proof search capabilities of Coq.
References
Armand, M., Grégoire, G., Keller, B., Théry, L., Werner, B.: 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 2011) (2011)
Batten, L.M.: Combinatorics of Finite Geometries. Cambridge University Press, Cambridge (1997)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5
Braun, D., Magaud, N., Schreck, P.: An equivalence proof between rank theory and incidence projective geometry. In: Automated Deduction in Geometry (ADG 2016), pp. 62–77 (2016)
Buekenhout, F. (ed.): Handbook of Incidence Geometry. North Holland, Amsterdam (1995)
Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.6. LogiCal Project (2017)
Coxeter, H.S.M.: Projective Geometry. Springer, New York (2003)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Hall, M.: Projective planes. Trans. Am. Math. Soc. 54(2), 229–277 (1943)
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_1
Magaud, N., Narboux, J., Schreck, P.: Formalizing projective plane geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS (LNAI), vol. 6301, pp. 141–162. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21046-4_7
Magaud, N., Narboux, J., Schreck, P.: A case study in formalizing projective geometry in Coq: Desargues theorem. Comput. Geom.: Theor. Appl. 45(8), 406–424 (2012)
Mahboubi, A., Tassi, E.: Mathematical Components. Draft (2016)
Michelucci, D., Schreck, P.: Incidence constraints: a combinatorial approach. Int. J. Comput. Geom. Appl. 16(5), 443–460 (2006)
Moulton, F.R.: A simple non-desarguesian plane geometry. Trans. Am. Math. Soc. 3(2), 192–195 (1902)
Oxley, J.G.: Matroid Theory, vol. 3. Oxford University Press, Oxford (2006)
Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337 (2009)
Tebbi, T., Gross, J.: A profiler for Ltac. In: Coq PL Workshop 2015 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Braun, D., Magaud, N., Schreck, P. (2018). Formalizing Some “Small” Finite Models of Projective Geometry in Coq. In: Fleuriot, J., Wang, D., Calmet, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2018. Lecture Notes in Computer Science(), vol 11110. Springer, Cham. https://doi.org/10.1007/978-3-319-99957-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-99957-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99956-2
Online ISBN: 978-3-319-99957-9
eBook Packages: Computer ScienceComputer Science (R0)