Duality notions in real projective plane. (English) Zbl 1494.68295
Summary: In this article, we check with the Mizar system [G. Bancerek et al., Lect. Notes Comput. Sci. 9150, 261–279 (2015; Zbl 1417.68201); J. Autom. Reasoning 61, No. 1–4, 9–32 (2018; Zbl 1433.68530)], the converse of Desargues’ theorem and the converse of Pappus’ theorem of the real projective plane. It is well known that in the projective plane, the notions of points and lines are dual [R. Hartshorne, Foundations of projective geometry. New York: W. A. Benjamin, Inc. 1967 (1967; Zbl 0152.38702); J. Richter-Gebert, Perspectives on projective geometry. Heidelberg: Springer-Verlag (2010; Zbl 1214.51001), Chapter 1; H. S. M. Coxeter, The real projective plane. 3rd ed. New York: Springer-Verlag (1993; Zbl 0772.51001)]. Some results (analytical, synthetic, combinatorial) of projective geometry are already present in some libraries Lean/Hott [U. Buchholtz and E. Rijke, in: Proceedings of the 2017 32nd annual ACM/IEEE symposium on logic in computer science, LICS 2017. Piscataway, NJ: IEEE Press. Article No. 86, 8 p. (2017; Zbl 1452.03033)], Isabelle/HOL [https://www.isa-afp.org/entries/Projective_Geometry.html], Coq [N. Magaud et al., Lect. Notes Comput. Sci. 6301, 141–162 (2011; Zbl 1302.68246); Comput. Geom. 45, No. 8, 406–424 (2012; Zbl 1248.68449); D. Braun et al., Ann. Math. Artif. Intell. 85, No. 2–4, 193–212 (2019; Zbl 1415.51007)], Agda [G. Calderón, Electron. Notes Theor. Comput. Sci. 338, 61–77 (2018; Zbl 1433.68575)], …
Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [Zbl 1302.68246] – the section on duality: “[…] For every theorem we prove, we can easily derive its dual using our function swap […]”).
In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [W. Leończuk and K. Prażmowski, “Projective spaces. I”, Formaliz. Math. 1, No. 4, 767–776 (1990)]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code.
In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [Leończuk and Prażmowski, loc. cit.] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional).
We hope that this methodology will allow us to continued more quickly the proof started in [R. Coghetto, Formaliz. Math. 26, No. 1, 21–32 (2018; Zbl 1401.51001)] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [A. Grabowski, “Tarski’s geometry modelled in Mizar computerized proof assistant” in: Proceedings of the 2016 federated conference on computer science and information systems (FedCSIS). Annals of Computer Science and Information Systems 8, 373–381 (2016; doi:10.15439/2016F290)]).
Proofs of dual statements by proof assistants have already been proposed, using an axiomatic method (for example see in [Zbl 1302.68246] – the section on duality: “[…] For every theorem we prove, we can easily derive its dual using our function swap […]”).
In our formalisation, we use an analytical rather than a synthetic approach using the definitions of Leończuk and Prażmowski of the projective plane [W. Leończuk and K. Prażmowski, “Projective spaces. I”, Formaliz. Math. 1, No. 4, 767–776 (1990)]. Our motivation is to show that it is possible by developing dual definitions to find proofs of dual theorems in a few lines of code.
In the first part, rather technical, we introduce definitions that allow us to construct the duality between the points of the real projective plane and the lines associated to this projective plane. In the second part, we give a natural definition of line concurrency and prove that this definition is dual to the definition of alignment. Finally, we apply these results to find, in a few lines, the dual properties and theorems of those defined in the article [Leończuk and Prażmowski, loc. cit.] (transitive, Vebleian, at_least_3rank, Fanoian, Desarguesian, 2-dimensional).
We hope that this methodology will allow us to continued more quickly the proof started in [R. Coghetto, Formaliz. Math. 26, No. 1, 21–32 (2018; Zbl 1401.51001)] that the Beltrami-Klein plane is a model satisfying the axioms of the hyperbolic plane (in the sense of Tarski geometry [A. Grabowski, “Tarski’s geometry modelled in Mizar computerized proof assistant” in: Proceedings of the 2016 federated conference on computer science and information systems (FedCSIS). Annals of Computer Science and Information Systems 8, 373–381 (2016; doi:10.15439/2016F290)]).
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 51A05 | General theory of linear incidence geometry and projective geometries |
| 51N15 | Projective analytic geometry |
Citations:
Zbl 1417.68201; Zbl 1433.68530; Zbl 0152.38702; Zbl 0772.51001; Zbl 1452.03033; Zbl 1302.68246; Zbl 1248.68449; Zbl 1415.51007; Zbl 1433.68575; Zbl 1401.51001; Zbl 1214.51001References:
| [1] | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:. · Zbl 1417.68201 |
| [2] | Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9-32, 2018. doi:. · Zbl 1433.68530 |
| [3] | Anthony Bordg. Projective geometry. Archive of Formal Proofs, jun 2018. |
| [4] | David Braun. Approche combinatoire pour l’automatisation en Coq des preuves formelles en géométrie d’incidence projective. PhD thesis, Université de Strasbourg, 2019. |
| [5] | Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-8. IEEE, 2017. · Zbl 1452.03033 |
| [6] | Guillermo Calderón. Formalizing constructive projective geometry in Agda. Electronic Notes in Theoretical Computer Science, 338:61-77, 2018. · Zbl 1433.68575 |
| [7] | Roland Coghetto. Klein-Beltrami model. Part I. Formalized Mathematics, 26(1):21-32, 2018. doi:. · Zbl 1401.51001 |
| [8] | Harold Scott Macdonald Coxeter. The real projective plane. Springer Science & Business Media, 1992. |
| [9] | Nikolai Vladimirovich Efimov. Géométrie supérieure. Mir, 1981. |
| [10] | Adam Grabowski. Tarski’s geometry modelled in Mizar computerized proof assistant. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11-14, 2016, pages 373-381, 2016. doi:. |
| [11] | Robin Hartshorne. Foundations of projective geometry. Citeseer, 1967. · Zbl 0152.38702 |
| [12] | Wojciech Leończuk and Krzysztof Prażmowski. Projective spaces – part I. Formalized Mathematics, 1(4):767-776, 1990. · Zbl 0741.51010 |
| [13] | Nicolas Magaud, Julien Narboux, and Pascal Schreck. Formalizing projective plane geometry in Coq. In Automated Deduction in Geometry, pages 141-162. Springer, 2008. · Zbl 1302.68246 |
| [14] | Nicolas Magaud, Julien Narboux, and Pascal Schreck. A case study in formalizing projective geometry in Coq: Desargues theorem. Computational Geometry, 45(8):406-424, 2012. · Zbl 1248.68449 |
| [15] | Jürgen Richter-Gebert. Pappos’s Theorem: Nine Proofs and Three Variations, pages 3-31. Springer Berlin Heidelberg, 2011. ISBN 978-3-642-17286-1. doi:. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
