Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 1/2021

30-04-2020

Formalization of the Poincaré Disc Model of Hyperbolic Geometry

Authors: Danijela Simić, Filip Marić, Pierre Boutry

Published in: Journal of Automated Reasoning | Issue 1/2021

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.
previous article Formalization of Euler–Lagrange Equation Set Based on Variational Calculus in HOL Light
next article HO in Coq

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
We use the numbering of theorems as of the tenth edition.
 
3
To highlight the fact that all of the axioms except for Euclid’s axiom indeed defines a neutral geometry we provide figures both in the Euclidean model and a non-Euclidean model, namely the Poincaré disc model. The figure on the left hand side illustrates the validity of the axiom in Euclidean geometry. The figure on the right hand side either depicts the validity of the statement in the Poincaré disc model or exhibits a counter-example.
 
4
From this example it can be seen that the lifting must be done in two stages (one for the subtype and the other for the quotient type). However, to simplify the presentation, in the rest of the paper we shall show only the initial and the final definition.
 
5
Note that such claim is slightly imprecise. In a strictly typed setting the value of the cross ratio is a number in the extended complex plane \(\mathbb {C}{}P^1\). If different from \(\infty _h\), then it can be converted to an ordinary complex number and we claim that its imaginary part is equal to 0. Formally we claim that is_real (to_complex (cross_ratio u \(i_1\) v \(i_2\))), where is_real x \(\equiv \) Im x = 0. For simplicity, we shall sometimes make such simplifications.
 
6
There already exists tools that translate proofs from one proof assistant to another [1].
 
7
there is no development about real closed fields in Isabelle/HOL. This is the reason that motivated us to avoid the restriction of predicates f and g to FOL predicates.
 
Literature
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)
3.
4.
5.
6.
7.
Beltrami, E.: Saggio di interpretazione della geometria Non-Euclidea. s.n. (1868)
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)
9.
Borsuk, K., Szmielew, W.: Foundations of Geometry. North-Holland, New York (1960)MATH
10.
Boutry, P., Braun, G., Narboux, J.: Formalization of the arithmetization of Euclidean plane geometry and applications. J. Symbol. Comput. 90, 149–168 (2019) MathSciNetMATHCrossRef
11.
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.: From Tarski to Hilbert. In: Ida, T., Fleuriot, J. (eds.) Automated Deduction in Geometry (ADG 2012). Lecture Notes in Computer Science, vol. 7993, pp. 89–109. Springer, Edinburgh (2012)CrossRef
16.
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)
18.
19.
20.
Coxeter, H.S.M.: Projective Geometry. Springer, Berlin (2003)MATH
21.
22.
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)
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)
26.
Fleuriot, J.: Nonstandard geometric proofs. In: Richter-Gebert, J., Wang, D. (eds.) Automated Deduction in Geometry (ADG 2000), pp. 246–267. Springer, Berlin Heidelberg (2001)CrossRef
27.
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)
29.
Freudenthal, H., et al.: K. Borsuk and Wanda Szmielew, foundations of geometry, Euclidean and Bolyai-Lobachevskian geometry, projective geometry. Bull. Am. Math. Soc. 67(4), 342–344 (1961)CrossRef
30.
Gauss, C.F.: Disquisitiones generales circa superficies curvas. [Mathematical tracts. Typis Dieterichianis (1828)
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.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 43–59. Springer, Berlin Heidelberg (2009)CrossRef
34.
Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs, pp. 131–146. Springer, Cham (2013)MATHCrossRef
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)MathSciNetMATHCrossRef
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)MathSciNetMATHCrossRef
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.
42.
43.
McFarland, A., McFarland, J., Smith, J. (eds.): Alfred Tarski: Early Work in Poland-Geometry and Teaching. Springer, New York (2014)MATH
44.
Meikle, L., Fleuriot, J.: Formalizing Hilbert’s Grundlagen in Isabelle/Isar. In: Theorem Proving in Higher Order Logics, pp. 319–334 (2003)
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)
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)
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)
48.
Needham, T.: Visual Complex Analysis. Oxford University Press, Oxford (1998)MATH
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, vol. 2283. Springer, Berlin (2002)MATHCrossRef
51.
52.
53.
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)
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.
57.
Richter, W., Grabowski, A., Alama, J.: Tarski geometry axioms. Formaliz. Math. 22(2), 167–176 (2014)MATHCrossRef
58.
Riemann, B., Weyl, Hermann: Über die Hypothesen, welche der Geometrie zu Grunde liegen. Springer, Berlin (1921)MATHCrossRef
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. Springer, Berlin (1983)MATHCrossRef
61.
Schwerdtfeger, H.: Geometry of Complex Numbers: Circle Geometry, Moebius Transformation, Non-euclidean Geometry. North Chelmsford, North Chelmsford (1979)MATH
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)
64.
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)
66.
67.
68.
Wenzel, M.: Isabelle/Isar—a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München (2002)
Metadata
Title
Formalization of the Poincaré Disc Model of Hyperbolic Geometry
Authors
Danijela Simić
Filip Marić
Pierre Boutry
Publication date
30-04-2020
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 1/2021
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-020-09551-2

Premium Partner

    Image Credits