<title>Tarski's postulate of parallels implies the 5th postulate of Euclid, the postulate of Playfair and the original postulate of Euclid. - Archive of Formal Proofs

<tdclass="data"width="80%">Tarski's postulate of parallels implies the 5th postulate of Euclid, the postulate of Playfair and the original postulate of Euclid.</td>

</tr>

<tr>

<tdclass="datahead">

Author:

</td>

<tdclass="data">

Roland Coghetto (roland_coghetto /at/ hotmail /dot/ com)

</td>

</tr>

<tr>

<tdclass="datahead">Submission date:</td>

<tdclass="data">2021-01-31</td>

</tr>

<tr>

<tdclass="datahead"valign="top">Abstract:</td>

<tdclass="abstract mathjax_process">

The GeoCoq library (Main autors: Michael Beeson, Pierre Boutry,

Gabriel Braun, Charly Gries, Julien Narboux) contains a formalization

of geometry using the Coq proof assistant. It contains both proofs

about the foundations of geometry and high-level proofs in the same

style as in high-school. Some theorems also inspired by W.

Schwabhaüser, W. Szmielew and A. Tarski are also formalized with

others ITP (Metamath, Mizar) or ATP. We port a part of the GeoCoq

2.4.0 library within the Isabelle/Hol proof assistant: more precisely,

the files Chap02.v to Chap13_3.v, suma.v as well as the associated

definitions and some useful files for the demonstration of certain

parallel postulates. While the demonstrations in Coq are written in

procedural language, the transcript is done in declarative language

Isar. The synthetic approach of the demonstrations are directly

inspired by those contained in GeoCoq. Some demonstrations are

credited to G.E Martin(<<lemmabet_le__lt:>> in

Ch11_angles.thy, proved by Martin as Theorem 18.17) or Gupta H.N

(Krippen Lemma, proved by Gupta in its PhD in 1965 as Theorem 3.45).

In this work, the proofs are not contructive. The sledeghammer tool

being used to find some demonstrations. The names of the lemmas and

theorems used are kept as far as possible as well as the definitions.

A different translation has been proposed when the name was already

used in Isabel/Hol ("Len" is translated as

"TarskiLen") or that characters were not allowed in

Isabel/Hol ("anga'" in Ch13_angles.v is translated as

"angaP"). For some definitions the highlighting of a

variable has changed the order or the position of the variables

(Midpoint, Out, Inter,...). All the lemmas are valid in

absolute/neutral space defined with Tarski's axioms. It should

be noted that T.J.M. Makarios \cite{afp-Tarskis_Geometry} has begun

some demonstrations of certain proposals mainly those corresponding to

SST chapters 2 and 3. It uses a definition that does not quite

coincide with the definition used in Geocoq and here. As an example,

Makarios introduces the axiom A11 (Axiom of continuity) in the

definition of the locale "Tarski_absolute_space".

Furthermore, the definition of the locale "TarskiAbsolute"

\cite{afp-Poincare_Disc} is not not identical to the one defined in

the "Tarski_neutral_dimensionless" class of GeoCoq. Indeed

this one does not contain the axiom "upper_dimension". In

some cases particular, it is nevertheless to use the axiom

"upper_dimension". The addition of the word "_2D"

in the file indicates its presence. In the last part, it is

formalized that, in the neutral/absolute space, the axiom of the

parallels of the system of Tarski implies the Playfair axiom, the 5th

postulate of euclide and the postulate original from Euclid. These

proofs, which are not constructive, are directly inspired by Pierre

Boutry, Charly Gries, Julien Narboux and Pascal Schreck.</td>

</tr>

<tr>

<tdclass="datahead"valign="top">BibTeX:</td>

<tdclass="formatted">

<pre>@article{IsaGeoCoq-AFP,

author = {Roland Coghetto},

title = {Tarski's postulate of parallels implies the 5th postulate of Euclid, the postulate of Playfair and the original postulate of Euclid.},

@@ -88,6 +88,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour

<tr>

<tdclass="head">2021</td>

</tr>

<tr>

<tdclass="entry">

2021-01-31: <ahref="entries/IsaGeoCoq.html">Tarski's postulate of parallels implies the 5th postulate of Euclid, the postulate of Playfair and the original postulate of Euclid.</a>

<br>

Author:

Roland Coghetto

</td>

</tr>

<tr>

<tdclass="entry">

2021-01-11: <ahref="entries/JinjaDCI.html">JinjaDCI: a Java semantics with dynamic class initialization</a>