Library GeoCoq.Meta_theory.Parallel_postulates.SPP_tarski

Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section SPP_tarski.

Context `{T2D:Tarski_2D}.

Lemma impossible_case_5 : P Q R S T U I,
  BetS P T Q
  BetS R T S
  BetS Q U R
  ¬ Col P Q S
  ¬ Col P R U
  Par P R Q S
  Par P S Q R
  Bet S Q I
  Bet U I P
  False.
Proof.
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HSQI HPUI.
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
assert (HTS : TS Q S P U) by (assert_diffs; spliter; assert_cols; repeat split;
                                     Col; try ( I; Col; Between); intro; apply HNC'; ColR).
apply l9_9 in HTS; apply HTS.
apply one_side_transitivity with R.

  {
  apply l12_6; apply par_not_col_strict with P; Col; Par.
  }

  {
  assert (HQS : Q S) by (assert_diffs; assumption).
  assert (HQSQ : Col Q S Q) by Col.
  assert (HRUQ : Col R U Q) by (spliter; assert_cols; Col).
  rewrite (l9_19 Q S R U Q HQS HQSQ HRUQ).
  split; spliter; try (intro; apply HNC; assert_cols; ColR); repeat split; Between.
  }
Qed.

Lemma impossible_case_6 : P Q R S T U I,
  BetS P T Q
  BetS R T S
  BetS Q U R
  ¬ Col P Q S
  ¬ Col P R U
  Par P R Q S
  Par P S Q R
  Bet S Q I
  Bet I P U
  False.
Proof.
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HSQI HPUI.
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
apply between_symmetry in HPUI.
destruct (inner_pasch S U I Q P HSQI HPUI) as [J [HBet1 HBet2]].
assert (HParS : Par_strict P S Q U).
  {
  apply par_not_col_strict with R.

    {
    spliter; assert_cols.
    apply par_col_par with R; Par.
    ColR.
    }

    {
    spliter; assert_cols; ColR.
    }

    {
    intro; apply HNC.
    spliter; assert_cols; ColR.
    }
  }
apply HParS; J; assert_cols; Col.
Qed.

Lemma impossible_case_7 : P Q R S T U I,
  BetS P T Q
  BetS R T S
  BetS Q U R
  ¬ Col P Q S
  ¬ Col P R U
  Par P R Q S
  Par P S Q R
  Col P U I
  Bet Q I S
  False.
Proof.
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HPUI HSQI.
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
elim (eq_dec_points I S); intro HIS; treat_equalities.

  {
  assert (HParS : Par_strict Q R P I) by (apply par_not_col_strict with P; Col; Par; unfold BetS in *;
                                          spliter; assert_cols; intro; apply HNC'; ColR).
  apply HParS; U; spliter; assert_cols; Col.
  }

  {
  assert (HTS : TS P U Q S) by (assert_diffs; spliter; assert_cols; repeat split;
                                       Col; try ( I; Col; Between); intro; apply HNC; ColR).
  apply l9_9 in HTS; apply HTS.
   R; split.

    {
    spliter; assert_diffs; assert_cols.
    split; try (intro; apply HNC; ColR).
    split; try (intro; apply HNC; ColR).
     U; Col; Between.
    }

    {
    destruct HPTQ as [HPTQ HDiff1].
    destruct HQUR as [HQUR HDiff2].
    apply between_symmetry in HQUR.
    destruct (inner_pasch R P Q U T HQUR HPTQ) as [J [HPJU HRJT]].
    assert (HRJS : Bet R J S) by (spliter; eBetween).
    spliter; assert_diffs; assert_cols.
    split; try (intro; apply HNC; ColR).
    split; try (intro; apply HNC; ColR).
     J; split; Col; Between.
    }
  }
Qed.

Lemma impossible_case_8 : P Q R S T U I,
  BetS P T Q
  BetS R T S
  BetS Q U R
  ¬ Col P Q S
  ¬ Col P R U
  Par P R Q S
  Par P S Q R
  Col P U I
  Bet I S Q
  False.
Proof.
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HPUI HSQI.
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
elim HPUI; clear HPUI; intro HPUI.

  {
  assert (H : Par_strict P S Q R) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                      spliter; assert_cols; intro; apply HNC'; ColR); apply H.
  apply between_symmetry in HSQI.
  destruct (inner_pasch P Q I U S HPUI HSQI) as [J [HQJU HPJS]]; J.
  spliter; assert_diffs; assert_cols; split; Col; ColR.
  }

  {
  elim HPUI; clear HPUI; intro HPUI.

    {
    assert (H : Par_strict P S Q R) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                        spliter; assert_cols; intro; apply HNC'; ColR); apply H.
    apply between_symmetry in HSQI.
    destruct (outer_pasch U Q I P S HPUI HSQI) as [J [HQJU HPSJ]]; J.
    spliter; assert_diffs; assert_cols; split; Col; ColR.
    }

    {
    assert (H : Par_strict P R Q S) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                        spliter; assert_cols; intro; apply HNC'; ColR); apply H.
    destruct HQUR as [HQUR HDiff].
    destruct (outer_pasch Q I U R P HQUR HPUI) as [J [HQJI HRPJ]]; J.
    spliter; assert_diffs; assert_cols; split; Col.
    elim (eq_dec_points Q I); intro HQI; treat_equalities; Col; ColR.
    }
  }
Qed.

Lemma strong_parallel_postulate_implies_tarski_s_euclid_aux :
  SPP
  ( A B C D T,
   A B
   A C
   A D
   A T
   B C
   B D
   B T
   C D
   C T
   D T
   ¬ Col A B C
   Bet A D T
   Bet B D C
    B', B'', MB, X, Bet A B X Par_strict B C T X
   BetS B MB T BetS B' MB B''
   Cong B MB T MB Cong B' MB B'' MB
   Col B B' D Bet B'' T X
   B B' B'' T).
Proof.
intros HSPP A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC.
destruct (symmetric_point_construction D B) as [B' HB'].
destruct (midpoint_distinct_2 B D B' HBD HB') as [HB'D HBB'].
destruct HB' as [HBDB' HCong1].
apply between_symmetry in HADT.
apply between_symmetry in HBDB'.
destruct (outer_pasch T B' D A B HADT HBDB') as [B''' [HTB'''B' HABB''']].
destruct (midpoint_existence B T) as [MB HMB].
destruct (midpoint_distinct_1 MB B T HBT HMB) as [HBMB HMBT].
destruct HMB as [HBMBT HCong2].
destruct (symmetric_point_construction B' MB) as [B'' HB''].
assert (HB'MB : MB B').
  {
  assert (H : ¬ Col B' D MB) by (intro; apply HABC; assert_cols; ColR).
  intro; treat_equalities; apply H; Col.
  }
destruct (midpoint_distinct_2 MB B' B'' HB'MB HB'') as [HB'B'' HB''MB].
destruct HB'' as [HB'MBB'' HCong3].
assert (H1 : BetS B MB T) by (repeat split; Between).
assert (H2 : BetS B' MB B'') by (repeat split; Between).
assert (HB'T : B' T).
  {
  assert (H : ¬ Col B B' T) by (intro; apply HABC; assert_cols; ColR).
  intro; treat_equalities; apply H; Col.
  }
assert (HB'B''' : B' B''').
  {
  assert (H : ¬ Col A B B') by (intro; apply HABC; assert_cols; ColR).
  intro; treat_equalities; apply H; Col.
  }
assert (HB'''T : B''' T).
  {
  assert (H : ¬ Col A B T) by (intro; apply HABC; assert_cols; ColR).
  intro; treat_equalities; apply H; Col.
  }
assert (H3 : BetS T B''' B') by (repeat split; Between).
assert (H4 : ¬ Col B T B'') by (intro; apply HABC; assert_cols; ColR).
assert (H5 : Cong B MB T MB) by Cong.
assert (H6 : Cong B' MB B'' MB) by Cong.
destruct (HSPP B T B' B'' MB B''') as [X [HBetS HX]];
Col; try apply all_coplanar; try (intro; apply H4; assert_diffs; assert_cols; ColR).
assert (HNC : ¬ Col B B' B''') by (intro; assert_diffs; assert_cols; apply H4; ColR).
assert (HPar1 : Par B B' T B'') by (unfold BetS in *; spliter; apply l12_17 with MB; try split; Col).
assert (HPar2 : Par B B'' T B')
  by (unfold BetS in *; spliter; assert_diffs; apply l12_17 with MB; try split; Between; Cong).
elim HBetS; clear HBetS; intro HBetS.

  {
  elim HX; clear HX; intro HX.

    {
    assert (H : BetS B'' T X).
      {
      repeat split; try (intro; treat_equalities); Col.
      apply H4; assert_diffs; assert_cols; ColR.
      }
    clear HBetS; rename H into HBetS.
    assert (H : BetS B B''' X).
      {
      repeat split; try (intro; treat_equalities); Col; unfold BetS in *; spliter;
      apply H4; assert_diffs; assert_cols; ColR.
      }
    clear HX; rename H into HX.
    apply BetSEq in HBetS; destruct HBetS as [HB''TX [HB''T [HB''X HBTX]]].
     B'; B''; MB; X.
    split; unfold BetS in HX; spliter; eBetween.
    assert (HPar : Par B' B B'' T) by (apply l12_17 with MB; try split; Between; Cong).
    assert (HPar' : Par B C B'' T)
      by (apply par_symmetry; apply par_col_par with B'; Par; assert_cols; ColR).
    split.

      {
      apply par_not_col_strict with T; Col.

        {
        apply par_col_par with B''; Par.
        assert_cols; ColR.
        }

        {
        intro; apply HABC; assert_cols; ColR.
        }
      }

      {
      repeat (split; try assumption); unfold BetS in *; spliter; assert_cols; Col.
      }
    }

    {
    elim HX; clear HX; intro HX.

      {
      exfalso; apply impossible_case_5 with B T B' B'' MB B''' X; spliter; assumption.
      }

      {
      exfalso; apply impossible_case_6 with B T B' B'' MB B''' X; spliter; assumption.
      }
    }
  }

  {
  elim HBetS; clear HBetS; intro HBetS.

    {
    exfalso; apply impossible_case_7 with B T B' B'' MB B''' X; spliter; assumption.
    }

    {
    exfalso; apply impossible_case_8 with B T B' B'' MB B''' X; spliter; assumption.
    }
  }

Qed.

Lemma strong_parallel_postulate_implies_tarski_s_euclid :
  SPP
  tarski_s_parallel_postulate.
Proof.
unfold tarski_s_parallel_postulate.
intro HSPP; apply tarski_s_euclid_remove_degenerated_cases.
intros A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC.
destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A B C D T)
as [B' [B'' [MB [X [HABX [HPar' [HBet1 [HBet2 [HCong1 [HCong2 [HBB'D [HB''TX [HBB' HB''T]]]]]]]]]]]]];
destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A C B D T)
as [C' [C'' [MC [Y [HACY [HPar [HBet3 [HBet4 [HCong3 [HCong4 [HCC'D [HC''TY [HCC' HC''T]]]]]]]]]]]]];
Between; Col.
clear HBet3; clear HBet4; clear HCong3; clear HCong4;
clear MC; clear HC''TY; clear HC''T; clear HPar'.
X; Y; repeat split; try assumption.
elim (Col_dec X T Y); intro HXTY.

  {
  apply between_symmetry in HACY.
  assert (HU := outer_pasch Y B C A D HACY HBDC); destruct HU as [U [HYUB HADU]].
  apply between_symmetry in HABX.
  assert (HV := outer_pasch X Y B A U HABX HYUB); destruct HV as [V [HXVY HAUV]].
  assert (HAX : A X) by (intro; treat_equalities; Col).
  assert (HAY : A Y) by (intro; treat_equalities; Col).
  assert (HAXY : ¬ Col A X Y) by (intro; assert_cols; apply HABC; ColR).
  assert (HAU : A U) by (intro; treat_equalities; Col).
  assert (HEq : T = V) by (assert_cols; apply l6_21 with X Y A D; Col; ColR); subst; assumption.
  }

  {
  assert (HNC : ¬ Col T B'' Y) by (intro; apply HXTY; unfold BetS in *; spliter; assert_cols; ColR).
  assert (HCop : Coplanar T B B'' Y).
    {
    
    apply all_coplanar.
    }
  destruct (HSPP T B B'' B' MB Y) as [I [HCol1 HCol2]]; Cong;
  try (unfold BetS in *; spliter; repeat (split; try Between)).
  exfalso; apply HPar; I; split; Col.
  elim (eq_dec_points I B); intro HBI; subst; Col.
  unfold BetS in *; spliter; assert_cols; ColR.
  }
Qed.

End SPP_tarski.