Abstract
The GeoCoq library 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. We port a part of the GeoCoq 2.4.0 library to Isabelle/HOL: 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. The synthetic approach of the demonstrations is directly inspired by those contained in GeoCoq. The names of the lemmas and theorems used are kept as far as possible as well as the definitions.
It should be noted that T.J.M. Makarios has done some proofs in Tarski's Geometry. It uses a definition that does not quite coincide with the definition used in Geocoq and here. Furthermore, corresponding definitions in the Poincaré Disc Model development are not identical to those defined in GeoCoq.
In the last part, it is formalized that, in the neutral/absolute space, the axiom of the parallels of Tarski's system implies the Playfair axiom, the 5th postulate of Euclid and Euclid's original parallel postulate. These proofs, which are not constructive, are directly inspired by Pierre Boutry, Charly Gries, Julien Narboux and Pascal Schreck.
License
History
- April 18, 2025
- Split Tarski_Neutral.thy into 3 files:
Tarski_Neutral.thy
Tarski_Neutral_2D.thy
Tarski_Postulate_Parallels.thy
Modify ROOT
Move locale Tarski_neutral_2D and 2D-lemma to Tarski_Neutral_2D.thy
Move 2D-lemma to Tarski_Neutral_2D.thy
Move postulate-lemma to Tarski_postulate_Parallels.thy
(revision 90b76ef4bc10)
- January 31, 2021
- Initial Version
INITIAL:
CREATE: Tarski_Neutral.thy
==========================
locale Tarski_neutral_dimensionless
locale Tarski_2D
context Tarski_neutral_dimensionless
Definitions (with arity left,right)
-----------------------------------
WARNING: Perp2(1,4): GeoCoq Perp2 A B C D E :: IsaGeoCoq E Perp2 A B C D
OFSC(4,4) Cong3(3,3) Col(0,3) Bet4(0,4) BetS(0,3) FSC(4,4) IFSC(4,4)
Le(2,2) Lt(2,2) Ge(2,2) Gt(2,2) Out(1,2) Midpoint(1,2) Per(0,3) PerpAt(1,4)
Perp(2,2) Coplanar(0,4) TS(2,2) ReflectL(2,2) Reflect(2,2) InAngle(1,3)
ParStrict(2,2) Par(2,2) Plg(0,4) ParallelogramStrict(0,4)
ParallelogramFlat(0,4) Parallelogram(0,4) Rhombus(0,4) Rectangle(0,4)
Square(0,4) Lambert(0,4) OS(0,4) TSP(3,2) OSP(3,2) Saccheri(0,4)
ReflectLAt(1,4) ReflectAt(1,4) upper_dim_axiom[UpperDimAxiom](0,0)
all_coplanar_axiom[AllCoplanarAxiom](0,0) CongA(3,3) LeA(3,3) LtA(3,3)
GtA(3,3) Acute(0,3) Obtuse(0,3) OrthAt(1,4) Orth(3,3) SuppA(3,3) SumA(6,3)
TriSumA(3,3) SAMS(0,6) Inter(1,4) Perp2(1,4) QCong(0,1) TarskiLen(0,3)
QCongNull(0,1) QCongA(0,1) Ang(3,1) QCongAAcute(0,1) AngAcute(3,1)
QCongANullAcute(0,1) QCongAnNull(0,1) QCongAnFlat(0,1) IsNullAngaP(0,1)
QCongANull(0,1) AngFlat(0,1)
tarski_s_parallel_postulate[TarskiParallelPostulate](0,0)
euclid_5[Euclid5](0,0)
euclid_s_parallel_postulate[EuclidSParallelPostulate](0,0)
playfair_s_postulate[PlayFairSPostulate](0,0)
Porting Files
-------------
theories/Main/Tarski_dev/Ch02_cong.v
theories/Main/Tarski_dev/Ch03_bet.v
theories/Main/Tarski_dev/Ch04_col.v
theories/Main/Tarski_dev/Ch04_cong_bet.v
theories/Main/Tarski_dev/Ch05_bet_le.v
theories/Main/Tarski_dev/Ch06_out_lines.v
theories/Main/Tarski_dev/Ch07_midpoint.v
theories/Main/Tarski_dev/Ch08_orthogonality.v
theories/Main/Tarski_dev/Ch09_plane.v
theories/Main/Tarski_dev/Ch10_line_reflexivity.v
theories/Main/Tarski_dev/Ch10_line_reflexivity_2.v
theories/Main/Tarski_dev/Ch11_angles.v
theories/Main/Annexes/suma.v
theories/Main/Tarski_dev/Ch12_parallel.v
theories/Main/Tarski_dev/Ch12_parallel_inter_dec.v
theories/Main/Tarski_dev/Ch13_1.v
theories/Main/Tarski_dev/Ch13_2_length.v
theories/Main/Tarski_dev/Ch13_3_angles.v
theories/Main/Meta_theory/Parallel_postulates/euclid_5_original_euclid.v
theories/Main/Meta_theory/Parallel_postulates/tarski_euclid.v
theories/Main/Meta_theory/Parallel_postulates/tarski_playfair.v
(revision f5710bbb2d80)