Library GeoCoq.Meta_theory.Parallel_postulates.universal_posidonius_postulate_par_perp_perp
Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.
Section universal_posidonius_postulate_perpendicular_transversal_postulate.
Context `{T2D:Tarski_2D}.
Lemma universal_posidonius_postulate__perpendicular_transversal_postulate :
universal_posidonius_postulate → perpendicular_transversal_postulate.
Proof.
intros HP A B C D P Q HPar HPerp1.
elim HPar; intro HParS; [|destruct HParS as [_ [_ [HC1 HC2]]]; assert_diffs;
apply perp_sym; apply perp_col0 with A B; Col; ColR].
assert (H := HPerp1); destruct H as [R HR];
apply perp_in_col in HR; destruct HR as [HC1 HC2].
assert (HEF : ∃ E F, Col A B E ∧ Col C D F ∧ Perp A B E F ∧ E ≠ R).
{
destruct (l8_18_existence A B C) as [E1 [HC3 HPerp2]];
[apply par_strict_not_col_1 with D; Par|].
destruct (l8_18_existence A B D) as [E2 [HC4 HPerp3]];
[apply par_strict_not_col_1 with C; Par|].
elim (eq_dec_points E1 R); intro; treat_equalities;
[|∃ E1, C; repeat (split; Col; Perp)].
elim (eq_dec_points E1 E2); intro; treat_equalities;
[|∃ E2, D; repeat (split; Col; Perp)].
assert (HC4 : Col E1 C D) by (apply perp_perp_col with A B; Perp).
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ E1; Col.
}
destruct HEF as [E [F [HC3 [HC4 [HPerp2 HD1]]]]].
assert (HGH : ∃ G H,
Col A B G ∧ Col C D H ∧ Perp A B G H ∧ E ≠ G ∧ F ≠ H).
{
destruct (l8_18_existence A B C) as [E1 [HC5 HPerp3]];
[apply par_strict_not_col_1 with D; Par|].
destruct (l8_18_existence A B D) as [E2 [HC6 HPerp4]];
[apply par_strict_not_col_1 with C; Par|].
elim (eq_dec_points E1 E); intro HD; treat_equalities;
[|∃ E1, C; repeat (split; Col; Perp); intro; treat_equalities; apply HD;
apply l6_21 with A B F E; assert_diffs; Col;
[elim (perp_not_col2 _ _ _ _ HPerp2); Col|
apply perp_perp_col with A B; Perp]].
elim (eq_dec_points E1 E2); intro HD'; treat_equalities;
[assert (HC7 : Col E1 C D) by (apply perp_perp_col with A B; Perp);
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ E1; Col|].
∃ E2, D; repeat (split; Col; Perp); intro; treat_equalities; apply HD'.
apply l6_21 with A B F E1; assert_diffs; Col;
[elim (perp_not_col2 _ _ _ _ HPerp2); Col|apply perp_perp_col with A B; Perp].
}
destruct HGH as [G [H [HC5 [HC6 [HPerp3 [HD2 HD3]]]]]].
assert (HSacc1 : Saccheri E F H G).
{
split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
split; [apply perp_per_1; apply perp_sym; apply perp_col0 with A B; Perp|].
split; [assert (Cong E F G H); Cong; apply HP with A B C D; Col|].
apply l12_6; apply par_strict_col2_par_strict with C D; Col.
apply par_strict_symmetry;
apply par_strict_col2_par_strict with A B; Col; Par.
}
destruct (midpoint_existence E G) as [M1 HMid1].
destruct (midpoint_existence F H) as [M2 HMid2].
assert (HLamb := mid2_sac__lam6521 _ _ _ _ _ _ HSacc1 HMid2 HMid1).
assert (HSacc2 : Saccheri E F M2 M1).
{
split; [unfold Lambert in *; spliter; Perp|].
split; [unfold Lambert in *; spliter; Perp|].
assert (HCong : Cong E F M1 M2); [|split; Cong].
{
apply HP with A B C D; Col; try solve [assert_diffs; assert_cols; ColR].
apply perp_sym; apply perp_col0 with E M1;
try solve [assert_diffs; assert_cols; Col; ColR].
apply per_perp; unfold Lambert in *; spliter; Perp.
}
apply l12_6; apply par_strict_col2_par_strict with C D; Col;
try solve [assert_diffs; assert_cols; Col; ColR].
apply par_strict_symmetry;
apply par_strict_col2_par_strict with A B; Col; Par;
assert_diffs; assert_cols; Col; ColR.
}
assert (HRAH : postulate_of_right_saccheri_quadrilaterals)
by (apply per_sac__rah with M1 M2 F E; try apply sac_perm;
unfold Lambert in *; spliter; auto).
assert (HP' : ∀ A1 A2 B1 B2 C1 C2 D1 D2,
Perp A1 A2 B1 B2 → Perp A1 A2 C1 C2 → Perp B1 B2 D1 D2 →
¬ Col A1 A2 D1 → ¬ Col B1 B2 C1 →
∃ I, Col C1 C2 I ∧ Col D1 D2 I).
{
cut bachmann_s_lotschnittaxiom.
{
clear HP; clear dependent P; clear dependent Q; clear dependent R.
intros bla A1 A2 B1 B2 C1 C2 D1 D2 HPerpAB HPerpAC HPerpBD HNCol1 HNCol2.
assert (HParA : Par_strict A1 A2 D1 D2).
apply par_not_col_strict with D1; Col; apply l12_9 with B1 B2; Perp.
assert (HParB : Par_strict B1 B2 C1 C2).
apply par_not_col_strict with C1; Col; apply l12_9 with A1 A2; Perp.
assert (HP := HPerpAC); destruct HP as [P [_ [_ [HP1 [HP2 HP3]]]]].
assert (HQ := HPerpAB); destruct HQ as [Q [_ [_ [HQ1 [HQ2 HQ3]]]]].
assert (HR := HPerpBD); destruct HR as [R [_ [_ [HR1 [HR2 HR3]]]]].
assert (HNCol3 : ¬ Col P B1 B2) by (apply par_not_col with C1 C2; Par).
assert (HNCol4 : ¬ Col R A1 A2) by (apply par_not_col with D1 D2; Par).
assert (HPQ : P ≠ Q) by (intro; subst; contradiction).
assert (HQR : Q ≠ R) by (intro; subst; contradiction).
assert (Per P Q R) by (apply HQ3; trivial).
destruct (diff_col_ex3 C1 C2 P) as [P1 [HC1P1 [HC2P1 [HPP1 HCP1]]]]; Col.
destruct (diff_col_ex3 D1 D2 R) as [R1 [HD1R1 [HD2R1 [HRR1 HDR1]]]]; Col.
destruct (bla P Q R P1 R1) as [I [HI1 HI2]]; auto.
apply HP3; Col.
apply HR3; Col.
∃ I.
split; assert_diffs; ColR.
}
{
apply weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom.
apply thales_converse_postulate__weak_triangle_circumscription_principle.
apply thales_postulate__thales_converse_postulate.
apply rah__thales_postulate; assumption.
}
}
destruct (HP' A B E F P Q C D) as [S [HC7 HC8]]; Col;
[apply perp_col0 with F M2; try (apply perp_sym; apply per_perp);
try solve [assert_diffs; assert_cols; Col; ColR];
rewrite (lam_per__rah M1 _ _ _); try apply lam_perm; assumption|
intro; destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ C; Col|
intro; apply HD1; assert (HC7 : Col Q E F)
by (apply perp_perp_col_col with P A B; Col; Perp);
elim (perp_not_col2 _ _ _ _ HPerp2); intro;
[apply l6_21 with A B E F|apply l6_21 with A B F E]; assert_diffs; Col; ColR|].
assert (HSacc3 : Saccheri E F S R).
{
split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
split; [apply perp_per_1; apply perp_col0 with P Q; try apply perp_col0 with A B; Perp;
intro; treat_equalities; destruct HParS as [_ [_ [_ HF]]];
exfalso; apply HF; ∃ S; Col|].
split; [assert (Cong E F R S); Cong; apply HP with A B C D; Col;
apply perp_col0 with P Q; Perp; intro; treat_equalities;
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ R; Col|].
apply l12_6; apply par_strict_col2_par_strict with C D; Col;
try solve [assert_diffs; assert_cols; Col; ColR];
try apply par_strict_symmetry;
try apply par_strict_col2_par_strict with A B; Col; Par.
intro; treat_equalities; assert (HC8 : Col E P Q)
by (apply perp_perp_col_col with F A B; Col; Perp).
apply HD1; elim (perp_not_col2 _ _ _ _ HPerp2); intro;
[apply l6_21 with A B E F|apply l6_21 with A B F E];
assert_diffs; Col; try ColR.
}
apply perp_col0 with S R; try solve [assert_diffs; assert_cols; Col; ColR].
apply perp_col0 with F S; try solve [assert_diffs; assert_cols; Col; ColR].
apply per_perp; try solve[apply sac_distincts in HSacc3; spliter; auto].
apply l8_2; apply HRAH with E; apply sac_perm; assumption.
Qed.
End universal_posidonius_postulate_perpendicular_transversal_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.
Section universal_posidonius_postulate_perpendicular_transversal_postulate.
Context `{T2D:Tarski_2D}.
Lemma universal_posidonius_postulate__perpendicular_transversal_postulate :
universal_posidonius_postulate → perpendicular_transversal_postulate.
Proof.
intros HP A B C D P Q HPar HPerp1.
elim HPar; intro HParS; [|destruct HParS as [_ [_ [HC1 HC2]]]; assert_diffs;
apply perp_sym; apply perp_col0 with A B; Col; ColR].
assert (H := HPerp1); destruct H as [R HR];
apply perp_in_col in HR; destruct HR as [HC1 HC2].
assert (HEF : ∃ E F, Col A B E ∧ Col C D F ∧ Perp A B E F ∧ E ≠ R).
{
destruct (l8_18_existence A B C) as [E1 [HC3 HPerp2]];
[apply par_strict_not_col_1 with D; Par|].
destruct (l8_18_existence A B D) as [E2 [HC4 HPerp3]];
[apply par_strict_not_col_1 with C; Par|].
elim (eq_dec_points E1 R); intro; treat_equalities;
[|∃ E1, C; repeat (split; Col; Perp)].
elim (eq_dec_points E1 E2); intro; treat_equalities;
[|∃ E2, D; repeat (split; Col; Perp)].
assert (HC4 : Col E1 C D) by (apply perp_perp_col with A B; Perp).
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ E1; Col.
}
destruct HEF as [E [F [HC3 [HC4 [HPerp2 HD1]]]]].
assert (HGH : ∃ G H,
Col A B G ∧ Col C D H ∧ Perp A B G H ∧ E ≠ G ∧ F ≠ H).
{
destruct (l8_18_existence A B C) as [E1 [HC5 HPerp3]];
[apply par_strict_not_col_1 with D; Par|].
destruct (l8_18_existence A B D) as [E2 [HC6 HPerp4]];
[apply par_strict_not_col_1 with C; Par|].
elim (eq_dec_points E1 E); intro HD; treat_equalities;
[|∃ E1, C; repeat (split; Col; Perp); intro; treat_equalities; apply HD;
apply l6_21 with A B F E; assert_diffs; Col;
[elim (perp_not_col2 _ _ _ _ HPerp2); Col|
apply perp_perp_col with A B; Perp]].
elim (eq_dec_points E1 E2); intro HD'; treat_equalities;
[assert (HC7 : Col E1 C D) by (apply perp_perp_col with A B; Perp);
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ E1; Col|].
∃ E2, D; repeat (split; Col; Perp); intro; treat_equalities; apply HD'.
apply l6_21 with A B F E1; assert_diffs; Col;
[elim (perp_not_col2 _ _ _ _ HPerp2); Col|apply perp_perp_col with A B; Perp].
}
destruct HGH as [G [H [HC5 [HC6 [HPerp3 [HD2 HD3]]]]]].
assert (HSacc1 : Saccheri E F H G).
{
split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
split; [apply perp_per_1; apply perp_sym; apply perp_col0 with A B; Perp|].
split; [assert (Cong E F G H); Cong; apply HP with A B C D; Col|].
apply l12_6; apply par_strict_col2_par_strict with C D; Col.
apply par_strict_symmetry;
apply par_strict_col2_par_strict with A B; Col; Par.
}
destruct (midpoint_existence E G) as [M1 HMid1].
destruct (midpoint_existence F H) as [M2 HMid2].
assert (HLamb := mid2_sac__lam6521 _ _ _ _ _ _ HSacc1 HMid2 HMid1).
assert (HSacc2 : Saccheri E F M2 M1).
{
split; [unfold Lambert in *; spliter; Perp|].
split; [unfold Lambert in *; spliter; Perp|].
assert (HCong : Cong E F M1 M2); [|split; Cong].
{
apply HP with A B C D; Col; try solve [assert_diffs; assert_cols; ColR].
apply perp_sym; apply perp_col0 with E M1;
try solve [assert_diffs; assert_cols; Col; ColR].
apply per_perp; unfold Lambert in *; spliter; Perp.
}
apply l12_6; apply par_strict_col2_par_strict with C D; Col;
try solve [assert_diffs; assert_cols; Col; ColR].
apply par_strict_symmetry;
apply par_strict_col2_par_strict with A B; Col; Par;
assert_diffs; assert_cols; Col; ColR.
}
assert (HRAH : postulate_of_right_saccheri_quadrilaterals)
by (apply per_sac__rah with M1 M2 F E; try apply sac_perm;
unfold Lambert in *; spliter; auto).
assert (HP' : ∀ A1 A2 B1 B2 C1 C2 D1 D2,
Perp A1 A2 B1 B2 → Perp A1 A2 C1 C2 → Perp B1 B2 D1 D2 →
¬ Col A1 A2 D1 → ¬ Col B1 B2 C1 →
∃ I, Col C1 C2 I ∧ Col D1 D2 I).
{
cut bachmann_s_lotschnittaxiom.
{
clear HP; clear dependent P; clear dependent Q; clear dependent R.
intros bla A1 A2 B1 B2 C1 C2 D1 D2 HPerpAB HPerpAC HPerpBD HNCol1 HNCol2.
assert (HParA : Par_strict A1 A2 D1 D2).
apply par_not_col_strict with D1; Col; apply l12_9 with B1 B2; Perp.
assert (HParB : Par_strict B1 B2 C1 C2).
apply par_not_col_strict with C1; Col; apply l12_9 with A1 A2; Perp.
assert (HP := HPerpAC); destruct HP as [P [_ [_ [HP1 [HP2 HP3]]]]].
assert (HQ := HPerpAB); destruct HQ as [Q [_ [_ [HQ1 [HQ2 HQ3]]]]].
assert (HR := HPerpBD); destruct HR as [R [_ [_ [HR1 [HR2 HR3]]]]].
assert (HNCol3 : ¬ Col P B1 B2) by (apply par_not_col with C1 C2; Par).
assert (HNCol4 : ¬ Col R A1 A2) by (apply par_not_col with D1 D2; Par).
assert (HPQ : P ≠ Q) by (intro; subst; contradiction).
assert (HQR : Q ≠ R) by (intro; subst; contradiction).
assert (Per P Q R) by (apply HQ3; trivial).
destruct (diff_col_ex3 C1 C2 P) as [P1 [HC1P1 [HC2P1 [HPP1 HCP1]]]]; Col.
destruct (diff_col_ex3 D1 D2 R) as [R1 [HD1R1 [HD2R1 [HRR1 HDR1]]]]; Col.
destruct (bla P Q R P1 R1) as [I [HI1 HI2]]; auto.
apply HP3; Col.
apply HR3; Col.
∃ I.
split; assert_diffs; ColR.
}
{
apply weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom.
apply thales_converse_postulate__weak_triangle_circumscription_principle.
apply thales_postulate__thales_converse_postulate.
apply rah__thales_postulate; assumption.
}
}
destruct (HP' A B E F P Q C D) as [S [HC7 HC8]]; Col;
[apply perp_col0 with F M2; try (apply perp_sym; apply per_perp);
try solve [assert_diffs; assert_cols; Col; ColR];
rewrite (lam_per__rah M1 _ _ _); try apply lam_perm; assumption|
intro; destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ C; Col|
intro; apply HD1; assert (HC7 : Col Q E F)
by (apply perp_perp_col_col with P A B; Col; Perp);
elim (perp_not_col2 _ _ _ _ HPerp2); intro;
[apply l6_21 with A B E F|apply l6_21 with A B F E]; assert_diffs; Col; ColR|].
assert (HSacc3 : Saccheri E F S R).
{
split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
split; [apply perp_per_1; apply perp_col0 with P Q; try apply perp_col0 with A B; Perp;
intro; treat_equalities; destruct HParS as [_ [_ [_ HF]]];
exfalso; apply HF; ∃ S; Col|].
split; [assert (Cong E F R S); Cong; apply HP with A B C D; Col;
apply perp_col0 with P Q; Perp; intro; treat_equalities;
destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; ∃ R; Col|].
apply l12_6; apply par_strict_col2_par_strict with C D; Col;
try solve [assert_diffs; assert_cols; Col; ColR];
try apply par_strict_symmetry;
try apply par_strict_col2_par_strict with A B; Col; Par.
intro; treat_equalities; assert (HC8 : Col E P Q)
by (apply perp_perp_col_col with F A B; Col; Perp).
apply HD1; elim (perp_not_col2 _ _ _ _ HPerp2); intro;
[apply l6_21 with A B E F|apply l6_21 with A B F E];
assert_diffs; Col; try ColR.
}
apply perp_col0 with S R; try solve [assert_diffs; assert_cols; Col; ColR].
apply perp_col0 with F S; try solve [assert_diffs; assert_cols; Col; ColR].
apply per_perp; try solve[apply sac_distincts in HSacc3; spliter; auto].
apply l8_2; apply HRAH with E; apply sac_perm; assumption.
Qed.
End universal_posidonius_postulate_perpendicular_transversal_postulate.