Library GeoCoq.Tarski_dev.Ch12_parallel_inter_dec

Require Export GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID.

Section T13.

Context `{TE:Tarski_2D_euclidean}.

Lemma tarski_s_euclid : tarski_s_parallel_postulate.
Proof.
unfold tarski_s_parallel_postulate.
apply euclid.
Qed.

Lemma inter_dec : decidability_of_intersection.
Proof.
apply strong_parallel_postulate_implies_inter_dec.
apply strong_parallel_postulate_SPP.
cut tarski_s_parallel_postulate.
apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; tauto.
apply tarski_s_euclid.
Qed.

Lemma not_par_inter_exists : A1 B1 A2 B2,
  ¬Par A1 B1 A2 B2 X, Col X A1 B1 Col X A2 B2.
Proof.
    intros.
induction (eq_dec_points A1 B1).
subst; A2; Col.
induction (eq_dec_points A2 B2).
subst; A1; Col.
induction (inter_dec A1 B1 A2 B2).

  assumption.

  exfalso.
  apply H.
  unfold Par.
  left.
  unfold Par_strict.
  repeat split; try apply all_coplanar; assumption.
Qed.

Lemma parallel_uniqueness :
  A1 A2 B1 B2 C1 C2 P : Tpoint,
  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.
Proof.
    intros.
    apply tarski_s_euclid_implies_playfair with A1 A2 P; try assumption.
    apply tarski_s_euclid.
Qed.

Lemma par_trans : A1 A2 B1 B2 C1 C2,
  Par A1 A2 B1 B2 Par B1 B2 C1 C2 Par A1 A2 C1 C2.
Proof.
    intros.
    apply playfair_implies_par_trans with B1 B2; try assumption.
    unfold playfair_s_postulate.
    apply parallel_uniqueness.
Qed.

Lemma l12_16 : A1 A2 B1 B2 C1 C2 X,
  Par A1 A2 B1 B2 Inter A1 A2 C1 C2 X Y, Inter B1 B2 C1 C2 Y.
Proof.
    intros.
    assert(HH:= H).
    unfold Par in H.
    induction H.
      unfold Inter in H0.
      spliter.
      ex_and H0 P.
      assert(HNCol : ¬Col B1 B2 X) by (intro; unfold Par_strict in H; spliter; apply H7; X; Col).
      assert(HH1 := l8_18_existence B1 B2 X HNCol).
      ex_and HH1 X0.
      assert(HPar : ¬Par B1 B2 C1 C2).
        intro.
        assert(Par A1 A2 C1 C2) by (apply par_trans with B1 B2; assumption).
        assert(¬Par A1 A2 C1 C2).
          apply col_not_col_not_par.
             X; Col.
           P; Col.
        contradiction.
      apply not_par_inter_exists in HPar.
      ex_and HPar Y.
       Y.
      split; try Col.
       X.
      split.
        Col.
      intro.
      apply HNCol; Col.
    unfold Inter in H0.
    spliter.
    ex_and H0 P.
     X.
    split.
       P.
      split.
        Col.
      intro.
      apply H6.
      apply (col3 B1 B2); Col.
    split; try Col.
    apply par_symmetry in HH.
    unfold Par in HH.
    induction HH.
      unfold Par_strict in H7.
      spliter.
      apply False_ind.
      apply H10.
       A1.
      split; try Col.
    spliter.
    apply (col3 A1 A2); Col.
Qed.

Lemma Par_dec : A B C D, Par A B C D ¬ Par A B C D.
Proof. exact (par_trans__par_dec par_trans). Qed.

Lemma par_not_par : A B C D P Q, Par A B C D ¬Par A B P Q ¬Par C D P Q.
Proof.
intros A B C D P Q HPar HNPar.
intro HNPar'.
apply HNPar.
apply par_trans with C D; Par.
Qed.


Lemma l12_19 :
   A B C D ,
   ¬Col A B C Par A B C D Par B C D A
   Cong A B C D Cong B C D A TS B D A C TS A C B D.
Proof.
    intros.
    assert( P, Midpoint P A C) by (eapply midpoint_existence).
    ex_and H2 P.
    double B P D'.
    assert(Cong C D' A B).
      apply (l7_13 P); assumption.
    assert(Cong B C D' A).
      apply (l7_13 P); Midpoint.
    assert(Par A B C D').
      assert_diffs; apply l12_17 with P; auto.
    assert(Par C D C D').
      eapply par_trans.
        apply par_symmetry.
        apply H0.
      apply H6.
    assert(Col C D D').
      apply par_id.
      assumption.
    assert(Par B C D' A).
      assert_diffs; apply l12_17 with P; Midpoint.
    assert(Par D A D' A).
      eapply par_trans.
        apply par_symmetry.
        apply H1.
      assumption.
    assert(Col A D D').
      apply par_id.
      Par.
    assert(D = D').
      assert_diffs; apply (l6_21 A D C D); Col.
        intro.
        apply H.
        assert(Col P C D).
          apply col_permutation_2.
          apply (col_transitivity_1 _ A); Col.
        assert(Col P C D').
          apply col_permutation_2.
          apply (col_transitivity_1 _ D); Col.
        assert(Col P A D').
          apply (col_transitivity_1 _ C); Col.
        apply (col3 P D'); Col.
        intro; treat_equalities; assert_cols; Col.
    subst D'.
    split.
      Cong.
    split.
      Cong.
    assert(B D).
      intro; treat_equalities; assert_cols; Col.
    split.
      apply l12_18_c with P; Cong; Col.
    apply l12_18_d with P; Cong; Col.
Qed.

Lemma l12_20_bis :
   A B C D,
   Par A B C D Cong A B C D TS B D A C
   Par B C D A Cong B C D A TS A C B D.
Proof.
    intros.
    assert(B C) by (assert_diffs; auto).
    assert(A D) by (assert_diffs; auto).
    assert(¬ Col A B C).
      intro.
      assert(Col A B D).
        apply not_strict_par1 with C C; Col; Par.
      unfold TS in H1.
      spliter.
      contradiction.
    assert( P, Midpoint P A C) by (apply midpoint_existence).
    ex_and H5 P.
    double B P D'.
    assert(Par B C D' A).
      eapply l12_17.
        assumption.
        apply H5.
      apply l7_2.
      assumption.
    assert(Par A B C D').
      assert_diffs; apply l12_17 with P; auto.
    assert(Cong C D' A B).
      apply (l7_13 P); assumption.
    assert(Cong B C D' A).
      apply (l7_13 P); Midpoint.
    assert(Par C D C D').
      eapply par_trans.
        apply par_symmetry.
        apply H.
      assumption.
    assert(Col C D D').
      apply par_id; assumption.
    assert(Cong C D C D').
      apply (cong_transitivity _ _ A B); Cong.
    assert(D = D' Midpoint C D D').
      apply l7_20; Col.
    induction H14.
    { subst D'.
      assert(Par B C D A) by Par.
      split.
        assumption.
      assert(HH:=l12_19 A B C D H4 H H14).
      spliter.
      split; assumption.
    }
    
    exfalso.
    assert(TS A C B D).
      apply par_two_sides_two_sides; assumption.
    assert(¬ Col A C D).
      apply (par_not_col A B C D A); Col.
      apply par_not_col_strict with C; Col.
    assert(¬ Col D' A C).
      intro.
      apply H16.
      ColR.
    assert(TS A C B D').
      repeat split; Col.
       P.
      split.
        Col.
      Between.
    assert (TS A C D D').
      repeat split; Col.
       C.
      split.
        Col.
      Between.
    apply (l9_9 A C B D).
      assumption.
    apply l9_8_1 with D'; assumption.
Qed.

Lemma l12_20 :
  A B C D,
  Par A B C D Cong A B C D TS A C B D
  Par B C D A Cong B C D A TS A C B D.
Proof.
    intros.
    assert(TS B D A C).
      apply par_two_sides_two_sides.
        apply par_comm.
        assumption.
      assumption.
    assert(HH:=l12_20_bis A B C D H H0 H2).
    spliter.
    split.
      assumption.
    split.
      assumption.
    assumption.
Qed.

Lemma l12_21_a :
  A B C D,
  TS A C B D
  (Par A B C D CongA B A C D C A).
Proof.
    assert (aia : alternate_interior_angles_postulate).
    { cut tarski_s_parallel_postulate.
        apply stronger_postulates; simpl; tauto.
      apply tarski_s_euclid.
    }
    apply aia.
Qed.

Lemma l12_21 : A B C D,
 TS A C B D
 (CongA B A C D C A Par A B C D).
Proof.
    intros.
    split.
      intro.
      apply l12_21_b ; assumption.
    intro.
    apply l12_21_a; assumption.
Qed.

Lemma l12_22_a : A B C D P,
 Out P A C OS P A B D Par A B C D
 CongA B A P D C P.
Proof.
    cut ( A B C D P,
         A P Bet P A C OS P A B D Par A B C D
         CongA B A P D C P).
    { intros Haux A B C D P HOut HOS HPar.
      destruct HOut as [HAP [HCP [|]]].
        apply Haux; trivial.
      apply conga_sym, Haux; Par.
      apply col_one_side with A; Col; Side.
    }
    intros A B C D P HAP HBet HOS HPar.
    destruct (eq_dec_points A C).
    { subst C.
      apply out2__conga; [|apply out_trivial; auto].
      apply col_one_side_out with P; Side.
      apply par_id; Par.
    }
    destruct (segment_construction B A B A) as [B' []].
    assert_diffs.
    apply conga_trans with B' A C.
      apply l11_14; auto.
    apply l11_10 with B' C D A; try (apply out_trivial); auto; [|apply l6_6, bet_out; Between].
    apply l12_21_a; [|apply par_col_par_2 with B; Col].
    apply l9_2, l9_8_2 with B; [|apply col_one_side with P; Side; Col].
    assert (HNCol : ¬ Col P A B) by (apply one_side_not_col123 with D, HOS).
    assert (HNCol1 : ¬ Col B A C) by (intro; apply HNCol; ColR).
    repeat split; trivial.
      intro; apply HNCol1; ColR.
     A; Col.
Qed.

Lemma l12_22 :
   A B C D P,
  Out P A C OS P A B D
  (CongA B A P D C P Par A B C D).
Proof.
    intros.
    split; intro.
      eapply (l12_22_b _ _ _ _ P); assumption.
    apply l12_22_a; assumption.
Qed.

Lemma l12_23 :
  A B C,
  ¬Col A B C
   B', C',
  TS A C B B' TS A B C C'
      Bet B' A C' CongA A B C B A C' CongA A C B C A B'.
Proof.
    intros.
    assert( B0, Midpoint B0 A B) by (apply midpoint_existence).
    assert( C0, Midpoint C0 A C) by (apply midpoint_existence).
    ex_and H0 B0.
    ex_and H1 C0.
    prolong B C0 B' B C0.
    prolong C B0 C' C B0.
     B'.
     C'.
    assert(TS A C B B').
      apply mid_two_sides with C0; Col.
      split.
        assumption.
      Cong.
    assert(TS A B C C').
      eapply mid_two_sides with B0; Col.
      split.
        assumption.
      Cong.
    split.
      assumption.
    split.
      assumption.
    assert(Par A B' C B).
      eapply l12_17.
        intro.
        treat_equalities.
        assert(C0 = B0).
          eapply l7_17.
            2: apply H2.
          split.
            apply between_symmetry.
            assumption.
          Cong.
        treat_equalities.
        Col.
        apply H0.
      split.
        apply between_symmetry.
        assumption.
      Cong.
    assert(Par A C' B C).
      eapply l12_17.
        intro.
        treat_equalities.
        assert(C0 = B0).
          eapply l7_17.
            apply H0.
          split.
            apply between_symmetry.
            assumption.
          Cong.
        treat_equalities.
        Col.
        apply H2.
      split.
        apply between_symmetry.
        assumption.
      Cong.
    assert(Par A B' A C').
      eapply par_trans.
        apply H8.
      apply par_symmetry.
      apply par_right_comm.
      assumption.
    apply par_id in H10.
    assert(OS A C B0 C').
      eapply out_one_side_1.
        intro.
        apply H.
        assert_diffs.
        eapply (col_transitivity_1 _ B0); Col.
        apply col_trivial_2.
      apply bet_out.
        intro.
        treat_equalities.
        assert_diffs; auto.
      assumption.
    assert(OS A C B0 B).
      eapply out_one_side_1.
        intro.
        apply H.
        eapply (col_transitivity_1 _ B0); Col.
          intro.
          treat_equalities.
          Col.
        apply col_trivial_3.
      assert_diffs; apply bet_out; Between.
    assert(OS A C B C').
      eapply one_side_transitivity.
        2:apply H11.
      apply one_side_symmetry.
      assumption.
    assert(TS A C B' C').
      apply l9_2.
      eapply l9_8_2.
        apply H6.
      assumption.
    split.
      apply col_two_sides_bet with C; assumption.
    split.
      apply l9_2 in H7.
      assert(HH:= l12_21_a A C' B C H7 H9); CongA.
    apply par_symmetry in H8.
    apply invert_two_sides in H6.
    assert(HH:= l12_21_a C B A B' H6 H8); CongA.
Qed.

Lemma not_par_strict_inter_exists :
  A1 B1 A2 B2,
  ¬Par_strict A1 B1 A2 B2
   X, Col X A1 B1 Col X A2 B2.
Proof.
    intros.
    induction (eq_dec_points A1 B1).
      subst.
       A2.
      Col.
    induction (eq_dec_points A2 B2).
      subst.
       A1.
      Col.
    induction (inter_dec A1 B1 A2 B2).
      assumption.
    unfold Par_strict in H.
    exfalso.
    apply H.
    repeat split; try assumption; try apply all_coplanar.
Qed.

Lemma not_par_inter : A B A' B' X Y, ¬Par A B A' B' ( P, Col P X Y (Col P A B Col P A' B')).
Proof.
    intros.
    induction(Par_dec A B X Y).
      assert(¬ Par A' B' X Y).
        intro.
        apply H.
        apply(par_trans _ _ X Y); Par.
      assert(HH:=not_par_inter_exists A' B' X Y H1).
      ex_and HH P.
       P.
      split.
        Col.
      right.
      Col.
    assert(HH:=not_par_inter_exists A B X Y H0).
    ex_and HH P.
     P.
    split.
      Col.
    left.
    Col.
Qed.

Lemma not_par_one_not_par : A B A' B' X Y, ¬Par A B A' B' ¬Par A B X Y ¬Par A' B' X Y.
Proof.
    intros.
    assert(HH:=not_par_inter A B A' B' X Y H).
    ex_and HH P.
    induction(Par_dec A B X Y).
      right.
      intro.
      apply H.
      apply(par_trans _ _ X Y); Par.
    left.
    auto.
Qed.

Lemma col_par_par_col : A B C A' B' C', Col A B C Par A B A' B' Par B C B' C' Col A' B' C'.
Proof.
    intros.
    apply par_distincts in H0.
    apply par_distincts in H1.
    spliter.
    assert(Par A B B C).
      right.
      repeat split; Col.
    assert(Par A' B' B' C').
      apply (par_trans _ _ A' B').
        Par.
      apply (par_trans _ _ B C).
        apply (par_trans _ _ A B); Par.
      Par.
    induction H7.
      apply False_ind.
      apply H7.
       B'.
      split; Col.
    spliter.
    Col.
Qed.

Lemma trisuma__bet : A B C D E F, TriSumA A B C D E F Bet D E F.
Proof.
    apply alternate_interior__triangle.
    unfold alternate_interior_angles_postulate.
    apply l12_21_a.
Qed.

Lemma bet__trisuma : A B C D E F, Bet D E F A B B C A C D E E F
  TriSumA A B C D E F.
Proof.
    intros A B C D E F HBet; intros.
    destruct (ex_trisuma A B C) as [P [Q [R HTri]]]; auto.
    apply conga_trisuma__trisuma with P Q R; trivial.
    assert (Hd := HTri).
    apply trisuma_distincts in Hd; spliter.
    apply conga_line; auto.
    apply (trisuma__bet A B C); trivial.
Qed.

Lemma not_obtuse : ¬ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
    apply not_oah.
    right.
    assert (Hr : postulate_of_right_saccheri_quadrilaterals); [|apply Hr].
    cut alternate_interior_angles_postulate.
      apply stronger_postulates_bis; simpl; tauto.
    unfold alternate_interior_angles_postulate; apply l12_21_a.
Qed.

Lemma suma__sams : A B C D E F, SumA A B C B C A D E F SAMS D E F C A B.
Proof. exact (t22_20 not_obtuse). Qed.

End T13.