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

Section Szmielew.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Definition hyperbolic_plane_postulate := forall A1 A2 P,
  ~ Col A1 A2 P -> exists 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.
(* Goal: forall _ : @hypothesis_of_acute_saccheri_quadrilaterals Tn, hyperbolic_plane_postulate *)
  intros aah A1 A2 P HNCol.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct (l8_18_existence A1 A2 P HNCol) as [Q [HCol1 HPerp]].
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct (diff_col_ex3 A1 A2 Q HCol1) as [X [HXA1 [HXA2 [HXQ HCol2]]]].
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct (symmetric_point_construction X Q) as [Y [HBet HCong]].
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  assert (HCol3 : Col A1 A2 Y) by ColR.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  assert (HInt : Per P Q X /\ Per P Q Y).
(* Goal: and (@Per Tn P Q X) (@Per Tn P Q Y) *)
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
    split; apply perp_per_1; auto; apply perp_sym, perp_col2 with A1 A2; Perp.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct HInt as [HPer HPer'].
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct (per__ex_saccheri Q P X) as [B1 HSac]; auto.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  destruct (per__ex_saccheri Q P Y) as [C1 HSac']; auto.
(* Goal: @ex (@Tpoint Tn) (fun B1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun B2 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C1 : @Tpoint Tn => @ex (@Tpoint Tn) (fun C2 : @Tpoint Tn => and (@Par Tn A1 A2 B1 B2) (and (@Col Tn P B1 B2) (and (@Par Tn A1 A2 C1 C2) (and (@Col Tn P C1 C2) (not (@Col Tn C1 B1 B2))))))))) *)
  exists B1; exists P; exists C1; exists P; repeat split; Col.
(* Goal: @Par Tn A1 A2 B1 P *)
(* Goal: @Par Tn A1 A2 C1 P *)
(* Goal: not (@Col Tn C1 B1 P) *)
    apply sac__par1423 in HSac; apply par_symmetry, par_col2_par_bis with Q X; Col; Par.
(* Goal: @Par Tn A1 A2 C1 P *)
(* Goal: not (@Col Tn C1 B1 P) *)
    apply sac__par1423 in HSac'; apply par_symmetry, par_col2_par_bis with Q Y; Col; Par.
(* Goal: not (@Col Tn C1 B1 P) *)
  intro HCol.
(* Goal: False *)
  assert (HBet0 : Bet B1 P C1).
(* Goal: @Bet Tn B1 P C1 *)
(* Goal: False *)
  { apply sac__par_strict1234 in HSac; apply sac__par_strict1234 in HSac'.
(* Goal: @Bet Tn B1 P C1 *)
    apply col_two_sides_bet with Q; Col.
(* Goal: @TS Tn P Q B1 C1 *)
    apply l9_8_2 with X; [|apply l12_6; Par].
(* Goal: @TS Tn P Q X C1 *)
    apply l9_2, l9_8_2 with Y; [|apply l12_6; Par].
(* Goal: @TS Tn P Q Y X *)
    repeat split; auto; try (intro; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P Q) (@Bet Tn Y T X)) *)
    exists Q; split; Col; Between.
  }
(* Goal: False *)
  apply (nlta B1 P C1).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HConga: CongA P Q X P Q Y) by (apply l11_16; auto).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HNCol1 : ~ Col P Q X) by (apply per_not_col; auto).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HNCol2 : ~ Col P Q Y) by (apply per_not_col; auto).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HNCol3 : ~ Col Q P B1) by (apply sac__ncol123 with X; trivial).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HNCol4 : ~ Col Q P C1) by (apply sac__ncol123 with Y; trivial).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  assert (HTS : TS Q P X Y) by (repeat split; Col; exists Q; split; Col).
(* Goal: @LtA Tn B1 P C1 B1 P C1 *)
  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.
(* Goal: @SAMS Tn X Q P P Q Y *)
    repeat split; auto.
(* Goal: or (@Out Tn Q P Y) (not (@Bet Tn X Q P)) *)
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn P Q J P Q Y) (and (not (@OS Tn Q P X J)) (and (not (@TS Tn X Q P J)) (@Coplanar Tn X Q P J)))) *)
      right; intro; apply HNCol1; Col.
(* Goal: @ex (@Tpoint Tn) (fun J : @Tpoint Tn => and (@CongA Tn P Q J P Q Y) (and (not (@OS Tn Q P X J)) (and (not (@TS Tn X Q P J)) (@Coplanar Tn X Q P J)))) *)
    exists Y; split; CongA; repeat split; Side; Cop.
(* Goal: not (@TS Tn X Q P Y) *)
    intro HTS1; destruct HTS1 as [_ []]; assert_cols; Col.
  - assert_diffs; apply inangle__suma; repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn B1 X C1) (or (@eq (@Tpoint Tn) X P) (@Out Tn P X Q))) *)
    exists P; split; auto.
  - assert_diffs; apply (conga3_suma__suma X Q P P Q Y X Q Y); CongA; [|apply conga_line; auto].
(* Goal: @SumA Tn X Q P P Q Y X Q Y *)
    apply inangle__suma; repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Bet Tn X X0 Y) (or (@eq (@Tpoint Tn) X0 Q) (@Out Tn Q X0 P))) *)
    exists Q; split; auto.
Qed.

Theorem szmielew_s_theorem :
  aristotle_s_axiom ->
  (forall P : Prop,
    (playfair_s_postulate -> P) ->
    (hyperbolic_plane_postulate -> ~ P)->
    (P <-> playfair_s_postulate)).
Proof.
(* Goal: forall (_ : @aristotle_s_axiom Tn) (P : Prop) (_ : forall _ : @playfair_s_postulate Tn, P) (_ : forall _ : hyperbolic_plane_postulate, not P), iff P (@playfair_s_postulate Tn) *)
intro H; intros.
(* Goal: iff P (@playfair_s_postulate Tn) *)
assert (L := aah__hpp).
(* Goal: iff P (@playfair_s_postulate Tn) *)
assert (HE := aristotle__acute_or_right H).
(* Goal: iff P (@playfair_s_postulate Tn) *)
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.