Formalization of the arithmetization of Euclidean plane geometry and applications.

*(English)*Zbl 1394.68349Summary: This paper describes the formalization of the arithmetization of Euclidean plane geometry in the Coq proof assistant. As a basis for this work, Tarski’s system of geometry was chosen for its well-known metamathematical properties. This work completes our formalization of the two-dimensional results contained in the book by W. Schwabhäuser et al. [Metamathematische Methoden in der Geometrie. Teil I: Ein axiomatischer Aufbau der euklidischen Geometrie. Berlin etc.: Springer-Verlag (1983; Zbl 0564.51001)]. We defined the arithmetic operations geometrically and proved that they verify the properties of an ordered field. Then, we introduced Cartesian coordinates, and provided characterizations of the main geometric predicates. In order to prove the characterization of the segment congruence relation, we provided a synthetic formal proof of two crucial theorems in geometry, namely the intercept and Pythagoras’ theorems. To obtain the characterizations of the geometric predicates, we adopted an original approach based on bootstrapping: we used an algebraic prover to obtain new characterizations of the predicates based on already proven ones. The arithmetization of geometry paves the way for the use of algebraic automated deduction methods in synthetic geometry. Indeed, without a “back-translation” from algebra to geometry, algebraic methods only prove theorems about polynomials and not geometric statements. However, thanks to the arithmetization of geometry, the proven statements correspond to theorems of any model of Tarski’s Euclidean geometry axioms. To illustrate the concrete use of this formalization, we derived from Tarski’s system of geometry a formal proof of the nine-point circle theorem using the Gröbner basis method. Moreover, we solve a challenge proposed by Beeson: we prove that, given two points, an equilateral triangle based on these two points can be constructed in Euclidean Hilbert planes. Finally, we derive the axioms for another automated deduction method: the area method.

##### MSC:

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

03B30 | Foundations of classical theories (including reverse mathematics) |

03B35 | Mechanization of proofs and logical operations |

51M04 | Elementary problems in Euclidean geometries |

68W30 | Symbolic computation and algebraic computation |

##### Keywords:

formalization; geometry; Coq; arithmetization; intercept theorem; Pythagoras’ theorem; area method
Full Text:
DOI

##### References:

[1] | Beeson, Michael, Proof and computation in geometry, (Ida, Tetsuo; Fleuriot, Jacques, Automated Deduction in Geometry (ADG 2012), Lecture Notes in Artificial Intelligence, vol. 7993, (2013), Springer Heidelberg), 1-30 · Zbl 1397.03018 |

[2] | Beeson, Michael, A constructive version of Tarski’s geometry, Ann. Pure Appl. Logic, 166, 11, 1199-1273, (2015) · Zbl 1392.03059 |

[3] | Beeson, Michael; Wos, Larry, Finding proofs in Tarskian geometry, J. Autom. Reason., 58, 1, 181-207, (2017) · Zbl 1414.68100 |

[4] | Bell, John L., Hilbert’s ϵ-operator in intuitionistic type theories, Math. Log. Q., 39, 1, 323-337, (1993) · Zbl 0802.03005 |

[5] | Birkhoff, George D., A set of postulates for plane geometry, based on scale and protractor, Ann. Math., 329-345, (1932) · Zbl 0004.12602 |

[6] | Borsuk, Karol; Szmielew, Wanda, Foundations of geometry, (1960), North-Holland · Zbl 0093.33301 |

[7] | Botana, Francisco; Hohenwarter, Markus; Janičić, Predrag; Kovács, Zoltán; Petrović, Ivan; Recio, Tomás; Weitzhofer, Simon, Automated theorem proving in geogebra: current achievements, J. Autom. Reason., 55, 1, 39-59, (2015) · Zbl 1356.68181 |

[8] | Botana, Francisco; Recio, Tomas, On the unavoidable uncertainty of truth in dynamic geometry proving, Math. Comput. Sci., 10, 1, 5-25, (2016) · Zbl 1357.68197 |

[9] | Boutry, Pierre; Narboux, Julien; Schreck, Pascal; Braun, Gabriel, A short note about case distinctions in Tarski’s geometry, (Botana, Francisco; Quaresma, Pedro, Proceedings of the 10th Int. Workshop on Automated Deduction in Geometry, Proceedings of ADG 2014, vol. TR 2014/01, (2014), University of Coimbra Coimbra, Portugal), 51-65 |

[10] | Boutry, Pierre; Narboux, Julien; Schreck, Pascal; Braun, Gabriel, Using small scale automation to improve both accessibility and readability of formal proofs in geometry, (Botana, Francisco; Quaresma, Pedro, Proceedings of the 10th Int. Workshop on Automated Deduction in Geometry, Proceedings of ADG 2014, vol. TR 2014/01, (July 2014), University of Coimbra Coimbra, Portugal), 31-49 |

[11] | Boutry, Pierre, Narboux, Julien, Schreck, Pascal, 2015. A reflexive tactic for automated generation of proofs of incidence to an affine variety. https://hal.inria.fr/hal-01216750. Unpublished. |

[12] | Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal, Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using coq, J. Autom. Reason, (2017) |

[13] | Braun, Gabriel; Boutry, Pierre; Narboux, Julien, From Hilbert to Tarski, (Eleventh International Workshop on Automated Deduction in Geometry, Proceedings of ADG 2016, Strasbourg, France, (June 2016)), 19 |

[14] | Braun, Gabriel; Narboux, Julien, From Tarski to Hilbert, (Ida, Tetsuo; Fleuriot, Jacques, Post-proceedings of Automated Deduction in Geometry 2012, Edinburgh, United Kingdom, September 2012, Lecture Notes in Computer Science, vol. 7993, (2012), Springer), 89-109 · Zbl 1397.03019 |

[15] | Chen, Xiaoyu; Wang, Dongming, Formalization and specification of geometric knowledge objects, Math. Comput. Sci., 7, 4, 439-454, (2013) · Zbl 1319.68214 |

[16] | Chou, Shang-Ching; Gao, Xiao-Shan; Zhang, Jing-Zhong, Machine proofs in geometry, (1994), World Scientific Singapore · Zbl 0941.68503 |

[17] | Cohen, Cyril; Mahboubi, Assia, Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Log. Methods Comput. Sci., 8, 1, 1-40, (2012) · Zbl 1241.68096 |

[18] | Dehlinger, Christophe; Dufourd, Jean-François; Schreck, Pascal, Higher-order intuitionistic formalization and proofs in Hilbert’s elementary geometry, (Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 2061, (2001), Springer), 306-324 · Zbl 0985.68078 |

[19] | Descartes, René, La géométrie, (1925), Open Court Chicago, First published as an appendix to the Discours de la Méthode, 1637 · JFM 25.1048.01 |

[20] | Durdević, Sana Stojanović; Narboux, Julien; Janičić, Predrag, Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry, Ann. Math. Artif. Intell., 25, (2015) · Zbl 1327.68206 |

[21] | Euclid; Heath, T. L.; Densmore, D., Euclid’s elements: all thirteen books complete in one volume: the Thomas L. heath translation, (2002), Green Lion Press · Zbl 1026.01024 |

[22] | Fuchs, Laurent; Théry, Laurent, A formalization of Grassmann-Cayley algebra in COQ and its application to theorem proving in projective geometry, 51-67, (2011), Springer Berlin, Heidelberg · Zbl 1350.68233 |

[23] | Genevaux, Jean-David; Narboux, Julien; Schreck, Pascal, Formalization of Wu’s simple method in coq, (Jouannaud, Jean-Pierre; Shao, Zhong, CPP 2011 First International Conference on Certified Programs and Proofs, Kenting, Taiwan, December 2011, Lecture Notes in Computer Science, vol. 7086, (2011), Springer-Verlag), 71-86 · Zbl 1350.68234 |

[24] | Grégoire, Benjamin; Pottier, Loïc; Théry, Laurent, Proof certificates for algebra and their application to automatic geometry theorem proving, (Post-Proceedings of Automated Deduction in Geometry (ADG 2008), Lecture Notes in Artificial Intelligence, vol. 6701, (2011)) · Zbl 1302.68242 |

[25] | Gupta, Haragauri Narayan, Contributions to the axiomatic foundations of geometry, (1965), University of California Berkley, PhD thesis |

[26] | Hilbert, David, Foundations of geometry, (1960), Open Court La Salle, Illinois, Second English edition, translated from the tenth German edition by Leo Unger. Original publication date, 1899 |

[27] | Janičić, Predrag, GCLC - A tool for constructive Euclidean geometry and more than that, (Takayama, Nobuki; Iglesias, Andres; Gutierrez, Jaime, Proceedings of International Congress of Mathematical Software (ICMS 2006), Lecture Notes in Computer Science, vol. 4151, (2006), Springer-Verlag), 58-73 · Zbl 1230.51024 |

[28] | Janičić, Predrag; Narboux, Julien; Quaresma, Pedro, The area method: a recapitulation, J. Autom. Reason., 48, 4, 489-532, (2012) · Zbl 1242.68281 |

[29] | Klein, Felix, A comparative review of recent researches in geometry, Bull. New York Math. Soc., 2, 10, 215-249, (1893) · JFM 25.0871.02 |

[30] | Makarios, Timothy James McKenzie, A mechanical verification of the independence of Tarski’s Euclidean axiom, (2012), Victoria University of Wellington, Master Thesis |

[31] | Klein, Felix, Vergleichende betrachtungen über neuere geometrische forschungen, Math. Ann., 43, 1, 63-100, (1893) · JFM 25.0871.01 |

[32] | Marić, Filip; Petrović, Danijela, Formalizing complex plane geometry, Ann. Math. Artif. Intell., 74, 3-4, 271-308, (2015) · Zbl 1330.68264 |

[33] | Marić, Filip; Petrović, Ivan; Petrović, Danijela; Janičić, Predrag, Formalization and implementation of algebraic methods in geometry, (Quaresma, Pedro; Back, Ralph-Johan, Proceedings First Workshop on CTP Components for Educational Software, Wrocław, Poland, 31th July 2011, Electronic Proceedings in Theoretical Computer Science, vol. 79, (2012), Open Publishing Association), 63-81 |

[34] | Mathis, P.; Schreck, P., Determining automatically compass and straightedge unconstructibility in triangles, (Davenport, James H.; Ghourabi, Fadoua, 7th International Symposium on Symbolic Computation, EPiC Series in Computing, vol. 39, (2016), EasyChair), 130-142, Issn 2040-557X |

[35] | Meikle, Laura I.; Fleuriot, Jacques D., Formalizing Hilbert’s grundlagen in isabelle/isar, 319-334, (2003), Springer Berlin Heidelberg Berlin, Heidelberg · Zbl 1279.68291 |

[36] | Millman, Richard S.; Parker, George D., Geometry: A metric approach with models, (1991), Springer Science & Business Media · Zbl 0724.51001 |

[37] | Moise, E. E., Elementary geometry from an advanced standpoint, (1990), Addison-Wesley · Zbl 0797.51002 |

[38] | Narboux, Julien, A decision procedure for geometry in coq, (Konrad, Slind; Annett, Bunker; Ganesh, Gopalakrishnan, Proceedings of TPHOLs’2004, Lecture Notes in Computer Science, vol. 3223, (2004), Springer-Verlag) · Zbl 1099.68734 |

[39] | Narboux, Julien, Mechanical theorem proving in Tarski’s geometry, (Botana, Francisco; Lozano, Eugenio Roanes, Post-Proceedings of Automated Deduction in Geometry 2006, Pontevedra, Spain, Lecture Notes in Computer Science, vol. 4869, (2007), Springer), 139-156 · Zbl 1195.03019 |

[40] | Narboux, Julien; Braun, David, Towards a certified version of the encyclopedia of triangle centers, Math. Comput. Sci., 10, 1, 17, (2016) · Zbl 1343.51001 |

[41] | Pambuccian, Victor, Zur existenz gleichseitiger dreiecke in h-ebenen, J. Geom., 63, 1, 147-153, (1998) · Zbl 0931.51006 |

[42] | Richter, William; Grabowski, Adam; Alama, Jesse, Tarski geometry axioms, Formaliz. Math., 22, 2, 167-176, (2014) · Zbl 1352.51002 |

[43] | School Mathematics Study Group, Mathematics for high school: geometry. Teacher’s commentary, (1961), Yale University Press New Haven |

[44] | Schwabhäuser, Wolfram; Szmielew, Wanda; Tarski, Alfred, Metamathematische methoden in der geometrie, (1983), Springer-Verlag Berlin · Zbl 1237.51003 |

[45] | Sozeau, Matthieu, A new look at generalized rewriting in type theory, J. Formaliz. Reason., 2, 1, 41-62, (2010) · Zbl 1205.68364 |

[46] | Tarski, Alfred; Givant, Steven, Tarski’s system of geometry, Bull. Symb. Log., 5, 2, (1999) · Zbl 0932.01031 |

[47] | Wu, Wen-Tsün, Mechanical theorem proving in geometries, (1994), Springer-Verlag · Zbl 0831.03003 |

[48] | Ye, Zheng; Chou, Shang-Ching; Gao, Xiao-Shan, An introduction to Java geometry expert, (International Workshop on Automated Deduction in Geometry, Lecture Notes in Computer Science, vol. 6301, (2008), Springer), 189-195 · Zbl 1302.68247 |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.