Library GeoCoq.Axioms.parallel_postulates
Require Import GeoCoq.Tarski_dev.Definitions.
Section Euclid_def.
Context `{Tn:Tarski_neutral_dimensionless}.
Section Euclid_def.
Context `{Tn:Tarski_neutral_dimensionless}.
First some statements needed for equivalence proofs
between different versions of the parallel postulate.
Definition decidability_of_parallelism := ∀ A B C D,
Par A B C D ∨ ¬ Par A B C D.
Definition decidability_of_not_intersection := ∀ A B C D,
¬ (∃ I, Col I A B ∧ Col I C D) ∨
¬ ¬ (∃ I, Col I A B ∧ Col I C D).
Definition decidability_of_intersection := ∀ A B C D,
(∃ I, Col I A B ∧ Col I C D) ∨
¬ (∃ I, Col I A B ∧ Col I C D).
Definition tarski_s_parallel_postulate := ∀ A B C D T,
Bet A D T → Bet B D C → A ≠ D →
∃ X Y, Bet A B X ∧ Bet A C Y ∧ Bet X T Y.
This is uniqueness of parallel postulate.
Definition playfair_s_postulate := ∀ A1 A2 B1 B2 C1 C2 P,
Par A1 A2 B1 B2 → Col P B1 B2 →
Par A1 A2 C1 C2 → Col P C1 C2 →
Col C1 B1 B2 ∧ Col C2 B1 B2.
The sum of the angles of triangles is the flat angle.
Notice that we do not use pi here,
because defining angle measure require some continuity axioms.
A figure with three right angles is closed.
Definition bachmann_s_lotschnittaxiom := ∀ P Q R P1 R1,
P ≠ Q → Q ≠ R → Per P Q R → Per Q P P1 → Per Q R R1 →
∃ S, Col P P1 S ∧ Col R R1 S.
Transitivity of parallelism.
Definition postulate_of_transitivity_of_parallelism := ∀ A1 A2 B1 B2 C1 C2,
Par A1 A2 B1 B2 → Par B1 B2 C1 C2 →
Par A1 A2 C1 C2.
This is the converse of triangle_mid_par.
Definition midpoint_converse_postulate := ∀ A B C P Q,
¬ Col A B C →
Midpoint P B C → Par A B Q P → Col A C Q →
Midpoint Q A C.
This is the converse of l12_21_b.
The alternate interior angles between two parallel lines are congruent.
Definition alternate_interior_angles_postulate := ∀ A B C D,
TS A C B D → Par A B C D →
CongA B A C D C A.
Definition consecutive_interior_angles_postulate := ∀ A B C D P Q R,
OS B C A D → Par A B C D → SumA A B C B C D P Q R →
Bet P Q R.
If two lines are parallel, every perdenciluar to one of the lines is perpendicular to the other.
Definition perpendicular_transversal_postulate := ∀ A B C D P Q,
Par A B C D → Perp A B P Q →
Perp C D P Q.
Definition postulate_of_parallelism_of_perpendicular_transversals :=
∀ A1 A2 B1 B2 C1 C2 D1 D2,
Par A1 A2 B1 B2 → Perp A1 A2 C1 C2 → Perp B1 B2 D1 D2 →
Par C1 C2 D1 D2.
Definition universal_posidonius_postulate := ∀ A1 A2 A3 A4 B1 B2 B3 B4,
Par A1 A2 B1 B2 →
Col A1 A2 A3 → Col B1 B2 B3 → Perp A1 A2 A3 B3 →
Col A1 A2 A4 → Col B1 B2 B4 → Perp A1 A2 A4 B4 →
Cong A3 B3 A4 B4.
A variant of Playfair's postulate useful in the proofs.
Definition alternative_playfair_s_postulate := ∀ A1 A2 B1 B2 C1 C2 P,
Perp2 A1 A2 B1 B2 P → Col P B1 B2 →
Par A1 A2 C1 C2 → Col P C1 C2 →
Col C1 B1 B2 ∧ Col C2 B1 B2.
According to wikipedia:
"Proclus (410-485) wrote a commentary on The Elements where he comments on attempted proofs to deduce
the fifth postulate from the other four, in particular he notes that Ptolemy had produced a false 'proof'.
Proclus then goes on to give a false proof of his own.
However he did give a postulate which is equivalent to the fifth postulate."
Definition proclus_postulate := ∀ A B C D P Q,
Par A B C D → Col A B P → ¬ Col A B Q →
∃ Y, Col P Q Y ∧ Col C D Y.
Definition alternative_proclus_postulate := ∀ A B C D P Q,
Perp2 A B C D P → Col A B P → ¬ Col A B Q →
∃ Y, Col P Q Y ∧ Col C D Y.
Non degenerated triangles can be circumscribed.
Definition triangle_circumscription_principle := ∀ A B C,
¬ Col A B C → ∃ CC, Cong A CC B CC ∧ Cong A CC C CC.
Definition inverse_projection_postulate := ∀ A B C P Q,
Acute A B C →
Out B A P → P ≠ Q → Per B P Q →
∃ Y, Out B C Y ∧ Col P Q Y.
Definition euclid_5 := ∀ P Q R S T U,
BetS P T Q → BetS R T S → BetS Q U R → ¬ Col P Q S →
Cong P T Q T → Cong R T S T →
∃ I, BetS S Q I ∧ BetS P U I.
Definition strong_parallel_postulate := ∀ P Q R S T U,
BetS P T Q → BetS R T S → ¬ Col P R U →
Cong P T Q T → Cong R T S T →
∃ I, Col S Q I ∧ Col P U I.
Definition SPP := ∀ P Q R S T U,
BetS P T Q → BetS R T S → ¬ Col P R U →
Coplanar P Q R U →
Cong P T Q T → Cong R T S T →
∃ I, Col S Q I ∧ Col P U I.
Definition alternative_strong_parallel_postulate := ∀ A B C D P Q R,
OS B C A D → SumA A B C B C D P Q R → ¬ Bet P Q R →
∃ Y, Col B A Y ∧ Col C D Y.
Definition euclid_s_parallel_postulate := ∀ A B C D P Q R,
OS B C A D → SAMS A B C B C D → SumA A B C B C D P Q R → ¬ Bet P Q R →
∃ Y, Out B A Y ∧ Out C D Y.
There exists a triangle whose sum of angles is equal to the flat angle.
Definition postulate_of_existence_of_a_triangle_whose_angles_sum_to_two_rights :=
∃ A B C D E F, ¬ Col A B C ∧ TriSumA A B C D E F ∧ Bet D E F.
Definition posidonius_postulate :=
∃ A1 A2 B1 B2,
¬ Col A1 A2 B1 ∧ B1 ≠ B2 ∧
∀ A3 A4 B3 B4,
Col A1 A2 A3 → Col B1 B2 B3 → Perp A1 A2 A3 B3 →
Col A1 A2 A4 → Col B1 B2 B4 → Perp A1 A2 A4 B4 →
Cong A3 B3 A4 B4.
There exists two non congruent similar triangles.
Definition postulate_of_existence_of_similar_triangles :=
∃ A B C D E F,
¬ Col A B C ∧ ¬ Cong A B D E ∧
CongA A B C D E F ∧ CongA B C A E F D ∧ CongA C A B F D E.
If A, B and C are points on a circle where the line AB is a diameter of the circle, then the angle ACB is a right angle.
The circumcenter of a right triangle is the midpoint of the hypothenuse.
Definition thales_converse_postulate := ∀ A B C M,
¬ Col A B C → Midpoint M A B → Per A C B →
Cong M A M C.
Definition existential_thales_postulate :=
∃ A B C M, ¬ Col A B C ∧ Midpoint M A B ∧ Cong M A M C ∧ Per A C B.
Definition postulate_of_right_saccheri_quadrilaterals := ∀ A B C D,
Saccheri A B C D → Per A B C.
Definition postulate_of_existence_of_a_right_saccheri_quadrilateral :=
∃ A B C D, Saccheri A B C D ∧ Per A B C.
Definition postulate_of_right_lambert_quadrilaterals := ∀ A B C D,
Lambert A B C D → Per B C D.
Definition postulate_of_existence_of_a_right_lambert_quadrilateral :=
∃ A B C D, Lambert A B C D ∧ Per B C D.
Definition weak_inverse_projection_postulate := ∀ A B C D E F P Q,
Acute A B C → Per D E F → SumA A B C A B C D E F →
Out B A P → P ≠ Q → Per B P Q →
∃ Y, Out B C Y ∧ Col P Q Y.
Definition weak_tarski_s_parallel_postulate := ∀ A B C T,
Per A B C → InAngle T A B C →
∃ X Y, Out B A X ∧ Out B C Y ∧ Bet X T Y.
Definition weak_triangle_circumscription_principle := ∀ A B C A1 A2 B1 B2,
¬ Col A B C → Per A C B →
Perp_bisect A1 A2 B C → Perp_bisect B1 B2 A C →
∃ I, Col A1 A2 I ∧ Col B1 B2 I.
Definition legendre_s_parallel_postulate :=
∃ A B C,
¬ Col A B C ∧ Acute A B C ∧
∀ T,
InAngle T A B C →
∃ X Y, Out B A X ∧ Out B C Y ∧ Bet X T Y.
There exists a point and a line,
such that there is only one parallel to this line going through this point.