Library GeoCoq.Meta_theory.Parallel_postulates.szmielew

Require Export GeoCoq.Axioms.continuity_axioms.
Require Export GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.

Section Szmielew.

Context `{T2D:Tarski_2D}.

Definition hyperbolic_plane_postulate := A1 A2 P,
  ¬ Col A1 A2 P B1 B2 C1 C2,
    Par A1 A2 B1 B2 Col P B1 B2
    Par A1 A2 C1 C2 Col P C1 C2
    ¬ Col C1 B1 B2.

Lemma aah__hpp :
  hypothesis_of_acute_saccheri_quadrilaterals
  hyperbolic_plane_postulate.
Proof.
  intros aah A1 A2 P HNCol.
  destruct (l8_18_existence A1 A2 P HNCol) as [Q [HCol1 HPerp]].
  destruct (diff_col_ex3 A1 A2 Q HCol1) as [X [HXA1 [HXA2 [HXQ HCol2]]]].
  destruct (symmetric_point_construction X Q) as [Y [HBet HCong]].
  assert_diffs.
  assert (HCol3 : Col A1 A2 Y) by ColR.
  assert (HInt : Per P Q X Per P Q Y).
    split; apply perp_per_1; auto; apply perp_sym, perp_col2 with A1 A2; Perp.
  destruct HInt as [HPer HPer'].
  destruct (per__ex_saccheri Q P X) as [B1 HSac]; auto.
  destruct (per__ex_saccheri Q P Y) as [C1 HSac']; auto.
   B1; P; C1; P; repeat split; Col.
    apply sac__par1423 in HSac; apply par_symmetry, par_col2_par_bis with Q X; Col; Par.
    apply sac__par1423 in HSac'; apply par_symmetry, par_col2_par_bis with Q Y; Col; Par.
  intro HCol.
  assert (HBet0 : Bet B1 P C1).
  { apply sac__par_strict1234 in HSac; apply sac__par_strict1234 in HSac'.
    apply col_two_sides_bet with Q; Col.
    apply l9_8_2 with X; [|apply l12_6; Par].
    apply l9_2, l9_8_2 with Y; [|apply l12_6; Par].
    repeat split; auto; try (intro; apply HNCol; ColR).
     Q; split; Col; Between.
  }
  apply (nlta B1 P C1).
  assert (HConga: CongA P Q X P Q Y) by (apply l11_16; auto).
  assert (HNCol1 : ¬ Col P Q X) by (apply per_not_col; auto).
  assert (HNCol2 : ¬ Col P Q Y) by (apply per_not_col; auto).
  assert (HNCol3 : ¬ Col Q P B1) by (apply sac__ncol123 with X; trivial).
  assert (HNCol4 : ¬ Col Q P C1) by (apply sac__ncol123 with Y; trivial).
  assert (HTS : TS Q P X Y) by (repeat split; Col; Q; split; Col).
  apply sams_lta2_suma2__lta with B1 P Q Q P C1 P Q X P Q X.
  - apply acute_per__lta; auto; apply acute_sym, (aah Q P B1 X HSac).
  - apply acute_per__lta; auto; apply (aah Q P C1 Y HSac').
  - apply (conga2_sams__sams X Q P P Q Y); CongA.
    repeat split; auto.
      right; intro; apply HNCol1; Col.
     Y; split; CongA; split; Side.
    intro HTS1; destruct HTS1 as [_ []]; assert_cols; Col.
  - assert_diffs; apply inangle__suma; repeat split; Col.
     P; split; auto.
  - assert_diffs; apply (conga3_suma__suma X Q P P Q Y X Q Y); CongA; [|apply conga_line; auto].
    apply inangle__suma; repeat split; Col.
     Q; split; auto.
Qed.

Theorem szmielew_s_theorem :
  aristotle_s_axiom
  ( P : Prop,
    (playfair_s_postulate P)
    (hyperbolic_plane_postulate ¬ P)->
    (P playfair_s_postulate)).
Proof.
intro H; intros.
assert (L := aah__hpp).
assert (HE := aristotle__acute_or_right H).
assert (HG := aristotle__greenberg H).
elim (equivalent_postulates_assuming_greenberg_s_axiom
        HG playfair_s_postulate postulate_of_right_saccheri_quadrilaterals);
unfold List.In; tauto.
Qed.

End Szmielew.