Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section tarski_playfair.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma tarski_s_euclid_implies_playfair :
 tarski_s_parallel_postulate ->
 playfair_s_postulate.
Proof.
assert (HAux:  tarski_s_parallel_postulate ->
  forall A1 A2 B1 B2 C1 C2 P, ~ Col P A1 A2 ->
  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).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  {
(* Goal: forall (_ : @tarski_s_parallel_postulate Tn) (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : not (@Col Tn P A1 A2)) (_ : @Par Tn A1 A2 B1 B2) (_ : @Col Tn P B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
intros HTE; intros.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
apply par_distincts in H0.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
apply par_distincts in H2.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
assert(HPar1 : Par_strict A1 A2 B1 B2) by (apply (par_not_col_strict _ _ _ _ P); Col; intro; apply H; Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
assert(HPar2 : Par_strict A1 A2 C1 C2) by (apply (par_not_col_strict _ _ _ _ P); Col; intro; apply H; Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
elim (line_dec B1 B2 C1 C2); intro HLine.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assumption.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert (HLineNew : ~ Col C1 B1 B2 \/ ~ Col C2 B1 B2) by (induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2);tauto).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  clear HLine; rename HLineNew into HLine.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HC' : exists C', Col C1 C2 C' /\ TS B1 B2 A1 C').
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    {
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    assert (Coplanar A1 A2 P A1) by (exists A1; left; split; Col).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    apply par__coplanar in H0.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    apply par__coplanar in H2.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    assert (Coplanar A1 A2 P B1) by (apply coplanar_perm_1, col_cop__cop with B2; Col).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    assert (Coplanar A1 A2 P B2) by (apply coplanar_perm_1, col_cop__cop with B1; Col; Cop).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    assert (Coplanar A1 A2 P C1) by (apply coplanar_perm_1, col_cop__cop with C2; Col).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Col Tn C1 C2 C') (@TS Tn B1 B2 A1 C')) *)
    assert (Coplanar A1 A2 P C2) by (apply coplanar_perm_1, col_cop__cop with C1; Col; Cop).
    elim HLine; clear HLine; intro HNC;
    [destruct (cop_not_par_other_side B1 B2 C1 C2 P A1) as [C' [HCol HTS]]|
     destruct (cop_not_par_other_side B1 B2 C2 C1 P A1) as [C' [HCol HTS]]];
    try exists C'; Col; try (intro; apply HPar1; exists A1; Col);
(* Goal: @Col Tn A1 A1 A2 *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    apply coplanar_pseudo_trans with A1 A2 P; Col.
    }
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  ex_and HC' C'.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  unfold TS in H9.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert (~ Col A1 B1 B2) by (spliter; auto).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  ex_and H12 B.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  double C' P C.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  unfold Midpoint in H14.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HD : exists D, Bet B D C /\ Bet P D A1) by (apply inner_pasch with C'; Between).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  ex_and HD D.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(C' <> P) by (intro; subst C'; contradiction).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert (Par A1 A2 C' P) by (apply par_col2_par with C1 C2; Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HPar3 : Par_strict A1 A2 C' P) by (apply (par_not_col_strict _ _ _ _ P); Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(B <> P).
(* Goal: not (@eq (@Tpoint Tn) P C) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    intro.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    subst B.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    apply (par_not_col _ _ _ _ A1) in HPar3.
(* Goal: False *)
(* Goal: @Col Tn A1 A1 A2 *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      apply HPar3; Col.
(* Goal: @Col Tn A1 A1 A2 *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      Col.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(P <> C).
(* Goal: not (@eq (@Tpoint Tn) P C) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    intro.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    treat_equalities.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    absurde.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col B P B1) by ColR.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col B P B2) by ColR.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col C' P C1) by ColR.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col C P C1) by (assert_cols;ColR).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col C' P C2) by ColR.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Col C P C2) by (assert_cols;ColR).

  assert(~Col B P C)
    by (intro;apply H11;assert_cols;ColR).

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(P <> D) by (intro; subst D; apply bet_col in H16; contradiction).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HE := HTE P B C D A1 H17 H16 H29).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  ex_and HE X; ex_and H30 Y.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Hx := l12_6 A1 A2 P X).

  assert (P<>X)
    by (intro;treat_equalities;intuition).

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Par_strict A1 A2 P X) by (apply (par_strict_col2_par_strict _ _ B1 B2); Col; apply col3 with B P; Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  apply Hx in H34.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Hy := l12_6 A1 A2 P Y).

  assert (P<>Y)
    by (intro;treat_equalities;intuition).

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HPar4 : Par_strict A1 A2 P Y) by (apply (par_strict_col2_par_strict _ _ C1 C2); Col; apply (col3 C P); Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  apply Hy in HPar4.
  assert(HOS : OS A1 A2 X Y)
     by (apply one_side_transitivity with P; try assumption; unfold OS in *; ex_and H34 Z; exists Z; split; assumption).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(Ho := HOS).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  unfold OS in HOS.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  ex_and HOS Z.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  unfold TS in H36.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  unfold TS in H37.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  assert(HTS : TS A1 A2 X Y) by (unfold TS; repeat split; try assumption; exists A1; split; Col).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  apply l9_9 in HTS.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  contradiction.
  }
(* Goal: forall _ : @tarski_s_parallel_postulate Tn, @playfair_s_postulate Tn *)
intros HTE A1; intros.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
assert( A1 <> A2 /\ B1 <> B2) by (apply par_distinct;auto).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
assert( A1 <> A2 /\ C1 <> C2) by (apply par_distinct;auto).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
clear H4.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
induction(col_dec P A1 A2).
  (** If P is one line A1A2 then line A1A2=B1B2=C1C2 and we can conclude. *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  induction H.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    exfalso.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    apply H.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X C1 C2)) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    exists P.
(* Goal: @Col Tn A1 A1 A2 *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    split; Col.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    induction H1.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      exfalso.
(* Goal: False *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      apply H1.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X C1 C2)) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      exists P.
(* Goal: @Col Tn A1 A1 A2 *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      split; Col.

(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      spliter.
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
      split;ColR.
  (** In the other case we use the previous lemma. *)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  apply (HAux HTE A1 A2 _ _ _ _ P); auto.
Qed.

End tarski_playfair.