Formalization of the Poincaré disc model of hyperbolic geometry. (English) Zbl 1543.68425
Summary: We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line \(\mathbb{C}P^1\) and is shown to satisfy Tarski’s axioms except for Euclid’s axiom – it is shown to satisfy it’s negation, and, moreover, to satisfy the existence of limiting parallels axiom.
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 51M09 | Elementary problems in hyperbolic and elliptic geometries |
Software:
Isabelle/HOL; Coq; Isabelle/Isar; GeoCoq; Archive Formal Proofs; Poincare_Disc; Transfer; Lifting; Complex_GeometryReferences:
| [1] | Assaf, A.: A framework for defining computational higher-order logics. Theses, École polytechnique (2015) |
| [2] | Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Mathematical Knowledge Management, MKM, Proceedings, pp. 31-43 (2006) · Zbl 1188.68258 |
| [3] | Beeson, M.: Proving Hilbert’s axioms in Tarski geometry (2014). http://www.michaelbeeson.com/research/papers/TarskiProvesHilbert.pdf |
| [4] | Beeson, M., A constructive version of Tarski’s geometry, Ann. Pure Appl. Log., 166, 11, 1199-1273 (2015) · Zbl 1392.03059 · doi:10.1016/j.apal.2015.07.006 |
| [5] | Beeson, M., Boutry, P., Braun, G., Gries, C., Narboux, J.: GeoCoq (2018). https://hal.inria.fr/hal-01912024/ |
| [6] | Beeson, M.; Wos, L., Finding proofs in Tarskian geometry, J. Autom. Reason., 58, 1, 181-207 (2017) · Zbl 1414.68100 · doi:10.1007/s10817-016-9392-2 |
| [7] | Beltrami, E.: Saggio di interpretazione della geometria Non-Euclidea. s.n. (1868) · JFM 01.0275.02 |
| [8] | Bolyai, J.: Appendix, Scientiam Spatii absolute veram exhibens: a veritate aut falsitate Axiomatis XI. Euclidei (a priori haud unquam decidenda) independentem; adjecta ad casum falsitatis, quadratura circuli geometrica. Auctore Johanne Bolyai de eadem, Geometrarum in Exercitu Caesareo Regio Austriaco Castrensium Capitaneo. Coll. Ref. (1832) · JFM 40.0521.01 |
| [9] | Borsuk, K.; Szmielew, W., Foundations of Geometry (1960), New York: North-Holland, New York · Zbl 0093.33301 |
| [10] | Boutry, P.; Braun, G.; Narboux, J., Formalization of the arithmetization of Euclidean plane geometry and applications, J. Symbol. Comput., 90, 149-168 (2019) · Zbl 1394.68349 · doi:10.1016/j.jsc.2018.04.007 |
| [11] | Boutry, P.; Gries, C.; Narboux, J., Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq, J Autom. Reason., 62, 1-68 (2019) · Zbl 1441.03011 · doi:10.1007/s10817-017-9422-8 |
| [12] | Boutry, P., Narboux, J., Schreck, P., Braun, G.: A short note about case distinctions in Tarski’s geometry. In: Botana, F., Quaresma, P. (eds.) Proceedings of the Tenth International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2014, pp. 51-65. Coimbra, Portugal (2014) |
| [13] | Braun, D.; Magaud, N.; Schreck, P., An equivalence proof between rank theory and incidence projective geometry, Proce. ADG, 2016, 62-77 (2016) |
| [14] | Braun, G., Boutry, P., Narboux, J.: From Hilbert to Tarski. In: Narboux, J., Schreck, P., Streinu, I. (eds.) Proceedings of the Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, pp. 78-96. Strasbourg, France (2016) |
| [15] | Braun, G.; Narboux, J.; Ida, T.; Fleuriot, J., From Tarski to Hilbert, Automated Deduction in Geometry (ADG 2012), 89-109 (2012), Edinburgh: Springer, Edinburgh · Zbl 1397.03019 · doi:10.1007/978-3-642-40672-0_7 |
| [16] | Braun, G.; Narboux, J., A synthetic proof of Pappus’ theorem in Tarski’s geometry, J. Autom. Reason., 58, 2, 23 (2017) · Zbl 1405.03034 · doi:10.1007/s10817-016-9374-4 |
| [17] | Brun, C., Dufourd, J.-F., Magaud, N.: Formal proof in Coq and derivation of a program in C++ to compute convex hulls. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012), volume 7993 of Lecture Notes in Computer Science, pp. 71-88. Springer Verlag, Berlin (2012) · Zbl 1396.68111 |
| [18] | Coghetto, R., Klein-Beltrami model. Part I., Formaliz. Math., 26, 1, 21-32 (2018) · Zbl 1401.51001 · doi:10.2478/forma-2018-0003 |
| [19] | Coghetto, R., Klein-Beltrami model. Part II., Formaliz. Math., 26, 1, 33-48 (2018) · Zbl 1401.51002 · doi:10.2478/forma-2018-0004 |
| [20] | Coxeter, HSM, Projective Geometry (2003), Berlin: Springer, Berlin · Zbl 1032.51002 |
| [21] | De Risi, V., The development of Euclidean axiomatics, Arch. Hist. Exact Sci., 70, 6, 591-676 (2016) · Zbl 1355.01007 · doi:10.1007/s00407-015-0173-9 |
| [22] | Dehlinger, C.; Dufourd, J-F, Formalizing generalized maps in Coq, Theor. Comput. Sci., 323, 1, 351-397 (2004) · Zbl 1078.68136 · doi:10.1016/j.tcs.2004.05.003 |
| [23] | Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry. In: Automated Deduction in Geometry (ADG 2000), volume 2061 of Lecture Notes in Computer Science, pp. 306-324 (2001) · Zbl 0985.68078 |
| [24] | Dufourd, J.-F.: A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula. In: Proceedings of the 2007 ACM Symposium on Applied Computing, SAC ’07, pp. 757-761. ACM, New York, NY, USA (2007) |
| [25] | Dufourd, J.-F., Bertot, Y.: Formal study of plane Delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving’2010 (In Federative Logic Conference: FLoC’2010), number 6172 in Lecture Notes in Computer Science, pp. 211-226. Springer (2010) · Zbl 1291.68337 |
| [26] | Fleuriot, J.; Richter-Gebert, J.; Wang, D., Nonstandard geometric proofs, Automated Deduction in Geometry (ADG 2000), 246-267 (2001), Berlin Heidelberg: Springer, Berlin Heidelberg · Zbl 0986.68125 · doi:10.1007/3-540-45410-1_15 |
| [27] | Fleuriot, J., Theorem proving in infinitesimal geometry, Log. J. IGPL, 9, 3, 447-474 (2001) · Zbl 0986.03016 · doi:10.1093/jigpal/9.3.447 |
| [28] | Fleuriot, J.: Exploring the foundations of discrete analytical geometry in Isabelle/HOL. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry (ADG 2010), volume 6877 of Lecture Notes in Computer Science, pp. 34-50. Springer (2010) · Zbl 1350.68232 |
| [29] | Freudenthal, H., K. Borsuk and Wanda Szmielew, foundations of geometry, Euclidean and Bolyai-Lobachevskian geometry, projective geometry, Bull. Am. Math. Soc., 67, 4, 342-344 (1961) · doi:10.1090/S0002-9904-1961-10606-X |
| [30] | Gauss, C.F.: Disquisitiones generales circa superficies curvas. [Mathematical tracts. Typis Dieterichianis (1828) · JFM 48.0008.01 |
| [31] | Gries, C., Narboux, J., Boutry, P.: Axiomes de continuité en géométrie neutre : une étude mécanisée en Coq. In: Magaud, N., Dargaye, Z. (eds.) Journées Francophones des Langages Applicatifs 2019, Acte des Journées Francophones des Langages Applicatifs (JFLA 2019). Les Rousses, France (2019) |
| [32] | Gupta, H.N.: Contributions to the Axiomatic Foundations of Geometry. PhD thesis, University of California, Berkley (1965) |
| [33] | Harrison, J.; Berghofer, S.; Nipkow, T.; Urban, C.; Wenzel, M., Without loss of generality, Theorem Proving in Higher Order Logics, 43-59 (2009), Berlin Heidelberg: Springer, Berlin Heidelberg · Zbl 1252.68254 · doi:10.1007/978-3-642-03359-9_3 |
| [34] | Huffman, B.; Kunčar, O.; Gonthier, G.; Norrish, M., Lifting and transfer: a modular design for quotients in Isabelle/HOL, Certified Programs and Proofs, 131-146 (2013), Cham: Springer, Cham · Zbl 1426.68284 · doi:10.1007/978-3-319-03545-1_9 |
| [35] | Kahn, G.: Constructive geometry according to Jan von Plato (1995) |
| [36] | Lobatschewsky, N.: Geometrische Untersuchungen zur Theorie der Parallellinien, pp. 159-223. Springer, Vienna (1985) |
| [37] | Lorenz, J.F.: Grundriss der Reinen und Angewandten Mathematik. Fleckeisen, Wolfenbuttel(1791) |
| [38] | Magaud, N.; Chollet, A.; Fuchs, L., Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective, Ann. Math. Artif. Intell., 74, 3-4, 309-332 (2015) · Zbl 1326.03074 · doi:10.1007/s10472-014-9434-6 |
| [39] | Magaud, N.; Narboux, J.; Schreck, P., A case study in formalizing projective geometry in Coq: Desargues theorem, Comput. Geom., 45, 8, 406-424 (2012) · Zbl 1248.68449 · doi:10.1016/j.comgeo.2010.06.004 |
| [40] | Makarios, T.J.M.: A mechanical verification of the independence of Tarski’s Euclidean axiom. Master’s thesis, Victoria University of Wellington (2012) |
| [41] | Marić, F.; Simić, D., Formalizing complex plane geometry, Ann. Math. Artif. Intell., 74, 3-4, 271-308 (2015) · Zbl 1330.68264 · doi:10.1007/s10472-014-9436-4 |
| [42] | Marić, F., Simić, D.: Complex geometry. Archive of Formal Proofs (2019). http://isa-afp.org/entries/Complex_Geometry.html, Formal proof development |
| [43] | McFarland, A.; McFarland, J.; Smith, J., Alfred Tarski: Early Work in Poland-Geometry and Teaching (2014), New York: Springer, New York · Zbl 1310.01002 |
| [44] | Meikle, L., Fleuriot, J.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In: Theorem Proving in Higher Order Logics, pp. 319-334 (2003) · Zbl 1279.68291 |
| [45] | Meikle, L., Fleuriot, J.: Mechanical theorem proving in computational geometry. In: Hong, H., Wang, D. (eds.) Automated Deduction in Geometry (ADG 2004), pp. 1-18. Springer, Berlin Heidelberg (2006) · Zbl 1159.68556 |
| [46] | Narboux, J.: Mechanical theorem proving in Tarski’s geometry. In: Eugenio, F., Roanes, L. (eds) Automated Deduction in Geometry (ADG 2006), volume 4869 of Lecture Notes in Computer Science, pp. 139-156. Springer, Pontevedra, Spain (2007) · Zbl 1195.03019 |
| [47] | Narboux, J., Janičić, P., Fleuriot, J.: Computer-assisted theorem proving in synthetic geometry. In: Sitharam, M., St. John, A., Sidman, J. (eds.) Handbook of Geometric Constraint Systems Principles, chapter 2, pp. 25-73. Chapman and Hall/CRC (2018) · Zbl 1425.68377 |
| [48] | Needham, T., Visual Complex Analysis (1998), Oxford: Oxford University Press, Oxford · Zbl 0893.30001 |
| [49] | Nipkow, T.: Programming and Proving in Isabelle/HOL (2013) |
| [50] | Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Berlin: Springer, Berlin · Zbl 0994.68131 · doi:10.1007/3-540-45949-9 |
| [51] | Pasch, M., Vorlesung über Neuere Geometrie (1976), Berlin: Springer, Berlin · Zbl 0328.50001 · doi:10.1007/978-3-642-65611-8 |
| [52] | Paulson, LC, Natural deduction as higher-order resolution, J Log Program, 3, 3, 237-258 (1986) · Zbl 0613.68035 · doi:10.1016/0743-1066(86)90015-4 |
| [53] | Paulson, LC, The foundation of a generic theorem prover, J Autom Reason, 5, 3, 363-397 (1989) · Zbl 0679.68173 · doi:10.1007/BF00248324 |
| [54] | Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R., Jackson, P. (eds.) Theorem Proving in Higher Order Logics, pp. 346-361. Springer, Berlin Heidelberg (2001) · Zbl 1005.68557 |
| [55] | Puitg, F., Dufourd, J.-F.: Formal specification and theorem proving breakthroughs in geometric modeling. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics, pp. 401-422. Springer, Berlin Heidelberg (1998) |
| [56] | Richter, W.: Formalizing Rigorous Hilbert axiomatic geometry proofs in the proof assistant Hol light. doi:10.1.1.363.2373&rep=rep1&type=pdf |
| [57] | Richter, W.; Grabowski, A.; Alama, J., Tarski geometry axioms, Formaliz. Math., 22, 2, 167-176 (2014) · Zbl 1352.51002 · doi:10.2478/forma-2014-0017 |
| [58] | Riemann, B.; Weyl, Hermann, Über die Hypothesen, welche der Geometrie zu Grunde liegen (1921), Berlin: Springer, Berlin · JFM 48.0882.06 · doi:10.1007/978-3-662-24861-4 |
| [59] | Saccheri, G.G.: Euclides ab omni naevo vindicatus. Mediolani: Ex typographia Pauli Antonio Montani (1733) |
| [60] | Schwabhäuser, W.; Szmielew, W.; Tarski, A., Metamathematische Methoden in der Geometrie (1983), Berlin: Springer, Berlin · Zbl 0564.51001 · doi:10.1007/978-3-642-69418-9 |
| [61] | Schwerdtfeger, H., Geometry of Complex Numbers: Circle Geometry, Moebius Transformation, Non-euclidean Geometry (1979), North Chelmsford: North Chelmsford, North Chelmsford · Zbl 0484.51007 |
| [62] | Scott, P.: Mechanising Hilbert’s foundations of geometry in Isabelle. Master’s thesis, University of Edinburgh (2008) |
| [63] | Scott, P., Fleuriot, J.: An investigation of Hilbert’s implicit reasoning through proof discovery in idle-time. In: Proceedings of the Seventh International Workshop on Automated Deduction in Geometry, pp. 182-200 (2010) · Zbl 1350.68244 |
| [64] | Simić, D., Marić, F., Boutry, P.: Poincaré disc model. Archive of Formal Proofs, (2019). http://isa-afp.org/entries/Poincare_Disc.html, Formal proof development |
| [65] | Stojanović Đurđević, S., Narboux, J., Janičić, P.: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry. Ann. Math. Artific. Intell. pp. 249-269 (2015) · Zbl 1327.68206 |
| [66] | Tarski, A.; Givant, S., Tarski’s system of geometry, Bull. Symbol. Log., 5, 2, 175-214 (1999) · Zbl 0932.01031 · doi:10.2307/421089 |
| [67] | von Plato, J., The axioms of constructive geometry, Ann. Pure Appl. Log., 76, 2, 169-200 (1995) · Zbl 0836.03034 · doi:10.1016/0168-0072(95)00005-2 |
| [68] | Wenzel, M.: Isabelle/Isar—a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München (2002) |
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.
