Library GeoCoq.Tarski_dev.Ch06_out_lines

Require Export GeoCoq.Tarski_dev.Ch05_bet_le.

Ltac eCol := eauto with col.

Section T6_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma bet_out : A B C, B A Bet A B C Out A B C.
Proof.
    intros.
    unfold Out.
    repeat split; auto.
    intro; treat_equalities; auto.
Qed.

Lemma out_dec : P A B, Out P A B ¬ Out P A B.
Proof.
    intros.
    unfold Out.
    elim (bet_dec P A B);intro; elim (bet_dec P B A);intro; elim (eq_dec_points A P);intro; elim (eq_dec_points B P);intro; tauto.
Qed.

Lemma out_diff1 : A B C, Out A B C B A.
Proof.
    intros.
    unfold Out in H.
    spliter.
    assumption.
Qed.

Lemma out_diff2 : A B C, Out A B C C A.
Proof.
    intros.
    unfold Out in H.
    spliter.
    assumption.
Qed.

Lemma out_distinct : A B C, Out A B C B A C A.
Proof.
    intros.
    split.
      eapply out_diff1;eauto.
    eapply out_diff2;eauto.
Qed.

Lemma out_col : A B C, Out A B C Col A B C.
Proof.
    intros.
    unfold Col.
    unfold Out in H.
    spliter.
    induction H1;Between.
Qed.

Lemma l6_2 : A B C P, AP BP CP Bet A P C (Bet B P C Out P A B).
Proof.
    intros.
    unfold Out.
    split.
      intros.
      repeat split; try assumption; eapply l5_2;eBetween.
    intro; spliter; induction H5; eBetween.
Qed.

Lemma bet_out__bet : A B C P, Bet A P C Out P A B Bet B P C.
Proof.
    intros A B C P HBet HOut.
    destruct (eq_dec_points C P).
      subst; Between.
    apply (l6_2 A); trivial; destruct HOut as [HPA [HPB]]; auto.
Qed.

Lemma l6_3_1 : A B P, Out P A B (AP BP C, CP Bet A P C Bet B P C).
Proof.
    unfold Out.
    intros.
    spliter.
    repeat split; try assumption.
    induction H1.
      assert( C, Bet A P C P C) by (apply point_construction_different).
      ex_and H2 C.
       C.
      repeat split; eBetween.
    assert( C, Bet B P C P C) by (apply point_construction_different).
    ex_and H2 C.
     C.
    repeat split;eBetween.
Qed.

Lemma l6_3_2 : A B P,
  (AP BP C, CP Bet A P C Bet B P C) Out P A B.
Proof.
    intros.
    spliter.
    ex_and H1 C.
    unfold Out.
    repeat split; try assumption; eapply l5_2; eBetween.
Qed.

Lemma l6_4_1 : A B P, Out P A B Col A P B ¬ Bet A P B.
Proof.
    unfold Out.
    intros.
    spliter.
    unfold Col.
    induction H1; split.
      Between.
      intro; apply H; eapply between_equality;eauto.
      right; left; assumption.
    intro; apply H0; eapply between_equality; eBetween.
Qed.

Lemma l6_4_2 : A B P, Col A P B ¬ Bet A P B Out P A B.
Proof.
    unfold Col.
    intros.
    spliter.
    unfold Out.
    induction H.
      contradiction.
    induction (eq_dec_points A P).
      subst P; intuition.
    induction (eq_dec_points B P).
      subst P; intuition.
    induction H; repeat split; Between.
Qed.

out reflexivity. l6_5

Lemma out_trivial : P A, AP Out P A A.
Proof.
    intros.
    unfold Out.
    repeat split; Between.
Qed.

out symmetry.

Lemma l6_6 : P A B, Out P A B Out P B A.
Proof.
    unfold Out.
    intuition.
Qed.

out transitivity.

Lemma l6_7 : P A B C, Out P A B Out P B C Out P A C.
Proof.
    unfold Out.
    intros.
    spliter.
    repeat split; try assumption.
    induction H4; induction H2.
      left; eapply between_exchange4; eauto.
      eapply l5_3; eauto.
      eapply (l5_1 P B); auto.
    right; eBetween.
Qed.

Lemma bet_out_out_bet : A B C A' C',
 Bet A B C Out B A A' Out B C C' Bet A' B C'.
Proof.
    intros.
    unfold Out in ×.
    spliter.
    induction H5; induction H3.
      assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
      apply outer_transitivity_between with C; auto.
      assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
      apply between_inner_transitivity with C; assumption.
      assert(Bet A' B C) by (apply between_exchange3 with A; Between).
      apply outer_transitivity_between with C; auto.
    assert(Bet A' B C) by (apply between_exchange3 with A; Between).
    eapply between_inner_transitivity with C; assumption.
Qed.

Lemma out2_bet_out : A B C X P,
 Out B A C Out B X P Bet A X C Out B A P Out B C P.
Proof.
    intros.
    unfold Out in ×.
    spliter.
    induction H5; induction H3.
      repeat split; try assumption.
        left; eapply between_exchange4 with X; try assumption.
        apply between_inner_transitivity with C; assumption.
      apply l5_1 with X; try auto.
      apply between_exchange2 with A; assumption.
      repeat split; try assumption.
        apply l5_3 with X; try assumption.
        apply between_inner_transitivity with C; assumption.
      right; apply between_exchange4 with X; try assumption.
      apply between_exchange2 with A; assumption.
      repeat split; try assumption.
        apply l5_1 with X; try auto.
        apply between_exchange2 with C; Between.
      left; apply between_exchange4 with X; try assumption.
      apply between_inner_transitivity with A; Between.
    repeat split; try assumption.
      right; apply between_exchange4 with X; try assumption.
      apply between_exchange2 with C; Between.
    apply l5_3 with X; try assumption.
    apply between_inner_transitivity with A; Between.
Qed.

Lemma l6_11_uniqueness : A B C R X Y,
  RA BC
  Out A X R Cong A X B C
  Out A Y R Cong A Y B C
  X=Y.
Proof.
    unfold Out.
    intros.
    spliter.
    assert (Cong A X A Y) by eCong.
    induction H8; induction H6.
      apply l4_19 with A R; try assumption.
      apply l4_3 with A A; Between; Cong.
      assert (Bet A X Y) by eBetween.
      eapply between_cong; eauto.
      assert (Bet A Y X) by eBetween.
      apply sym_equal; apply between_cong with A; Cong.
    assert (Bet A X Y Bet A Y X) by (eapply l5_1; eauto).
    induction H10.
      apply between_cong with A; assumption.
    apply sym_equal; apply between_cong with A; Cong.
Qed.

Lemma l6_11_existence : A B C R,
  RA BC X, Out A X R Cong A X B C.
Proof.
    intros.
    assert ( X : Tpoint, (Bet A R X Bet A X R) Cong A X B C) by (apply (segment_construction_2);assumption).
    ex_and H1 X.
     X.
    unfold Out;repeat split; try intro;treat_equalities;intuition.
Qed.

Lemma segment_construction_3 : A B X Y, A B X Y C, Out A B C Cong A C X Y.
Proof.
    intros.
    destruct (l6_11_existence A X Y B) as [C [HC1 HC2]]; auto.
    apply l6_6 in HC1.
     C; auto.
Qed.

Lemma l6_13_1 : P A B, Out P A B Le
 P A P B Bet P A B.
Proof.
    unfold Out.
    intros.
    spliter.
    induction H2; try assumption.
    unfold Le
 in H0.
    ex_and H0 Y.
    assert(Y = A).
      apply (l6_11_uniqueness P P A B); Between; Cong.
        unfold Out; repeat split; auto.
        intro; treat_equalities; auto.
      unfold Out; repeat split; auto.
    subst Y; assumption.
Qed.

Lemma l6_13_2 : P A B, Out P A B Bet P A B Le
 P A P B.
Proof.
    intros.
    unfold Le.
     A.
    split; Cong.
Qed.

Lemma l6_16_1 : P Q S X, PQ SP Col S P Q Col X P Q Col X P S.
Proof.
    intros.
    assert((Bet P S X Bet P X S) (Bet P S X Bet S X P)) by (intro; induction H3; Between).
    unfold Col.
    induction H1;induction H2.
      right; apply H3; eapply (l5_2 Q P); Between.
      induction H2; left; eBetween.
      induction H1; left; eBetween.
    induction H1; induction H2.
      right; apply H3; eapply l5_1; eauto.
      right; right; eBetween.
      right; left; eBetween.
    right; apply H3; eapply l5_3; eBetween.
Qed.

Lemma col_transitivity_1 : P Q A B,
  PQ Col P Q A Col P Q B Col P A B.
Proof.
    intros.
    induction (eq_dec_points A P).
      subst; unfold Col; Between.
    assert (T:=l6_16_1 P Q A B).
    apply col_permutation_1; apply T; Col.
Qed.

Lemma col_transitivity_2 : P Q A B,
 PQ Col P Q A Col P Q B Col Q A B.
Proof.
    intros.
    apply (col_transitivity_1 Q P A B);Col.
Qed.

Unicity of intersection

Lemma l6_21 : A B C D P Q,
  ¬ Col A B C CD Col A B P Col A B Q Col C D P Col C D Q P=Q.
Proof.
    intros.
    elim (eq_dec_points P Q); intro; try assumption.
    cut False.
      intro; intuition.
    apply not_col_distincts in H.
    spliter.
    assert (Col C P Q) by (apply col_transitivity_1 with D; Col).
    assert (Col Q B C).
      induction (eq_dec_points Q A).
        subst; apply col_transitivity_1 with P; Col.
      apply col_transitivity_1 with P; try Col; apply col_permutation_1; apply col_transitivity_1 with A; Col.
    assert (Col A B C).
      induction (eq_dec_points Q A).
        subst Q; assumption.
      induction (eq_dec_points Q B).
        subst; apply col_permutation_2; apply col_transitivity_1 with P; try Col.
      apply col_permutation_2; apply col_transitivity_1 with Q; try Col.
    contradiction.
Qed.

End T6_1.

Hint Resolve col_transitivity_1 col_transitivity_2 out_col : col.

Section T6_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma not_col_exists : A B,
 AB C, ¬ Col A B C.
Proof.
    intros.
    assert (T:=lower_dim_ex).
    induction T.
    induction H0.
    induction H0.
    induction (Col_dec A B x).
      induction(Col_dec A B x0).
        induction(Col_dec A B x1).
          induction (eq_dec_points A x).
            assert (~(Col x x0 x1)) by (unfold Col; auto).
            treat_equalities; eCol.
          assert (Col A x x0) by eCol.
          assert (Col A x x1) by eCol.
          assert (Col A x0 x1) by eCol.
          assert (Col x x0 x1) by eCol.
          contradiction.
         x1; assumption.
       x0; assumption.
     x; assumption.
Qed.


Lemma col3 : X Y A B C,
 X Y
 Col X Y A Col X Y B Col X Y C
 Col A B C.
Proof.
    intros.
    assert (Col X A B) by (apply col_transitivity_1 with Y; assumption).
    induction(eq_dec_points C X).
      subst X; apply col_permutation_1; assumption.
    apply col_permutation_1.
    apply col_transitivity_1 with X; try assumption.
      apply col_permutation_2.
      apply col_transitivity_1 with Y; assumption.
    apply col_permutation_2.
    apply col_transitivity_1 with Y; assumption.
Qed.

Lemma out2__bet : A B C, Out A B C Out C A B Bet A B C.
Proof.
    intros A B C Hout1 Hout2.
    apply l6_4_1 in Hout2.
    destruct Hout2 as [_ Hout2].
    destruct Hout1 as [_ [_ [|]]].
    assumption.
    exfalso.
    apply Hout2.
    assumption.
Qed.

Lemma bet2_le2__le1346 : A B C A' B' C', Bet A B C Bet A' B' C' Le
 A B A' B' Le
 B C B' C'
  Le
 A C A' C'.
Proof.
  intros A B C A' B' C' HBet HBet' HleAB HleBC.

  elim(eq_dec_points A B).
  { intro.
    subst B.
    apply (le_transitivity _ _ B' C'); auto.
    apply le_comm.
     B'.
    split; Between; Cong.
  }
  intro.
  elim(eq_dec_points B C).
  { intro.
    subst C.
    apply (le_transitivity _ _ A' B'); auto.
     B'; Cong.
  }
  intro.

  assert(A' B') by (intro; subst B'; assert(A = B); auto; apply (le_zero _ _ A'); auto).
  assert(B' C') by (intro; subst C'; assert(B = C); auto; apply (le_zero _ _ B'); auto).
  destruct HleAB as [B0 []].
  assert(A' B0) by (intro; subst B0; assert(A = B); auto; apply (cong_reverse_identity A'); Cong).
  assert(HC0 := segment_construction A' B0 B C).
  destruct HC0 as [C0 []].
  assert(B0 C0) by (intro; subst C0; assert(B = C); auto; apply (cong_reverse_identity B0); auto).
   C0.
  split.
  2: apply (l2_11 _ B _ _ B0); Cong.
  apply (outer_transitivity_between2 _ B0); auto.
  assert(Bet B0 B' C') by (apply between_symmetry; apply (between_inner_transitivity _ _ _ A'); Between).
  apply l6_13_1.
  - elim(eq_dec_points B0 B').
    { intro.
      subst.
      apply (l6_2 _ _ A'); Between.
    }
    intro.
    apply (l6_7 _ _ B').
    apply (l6_2 _ _ A'); Between.
    apply bet_out; auto.
  - apply (le_transitivity _ _ B' C').
      apply (l5_6 B C B' C'); Cong.
      apply le_comm.
       B'.
      split; Between; Cong.
Qed.

Lemma bet2_le2__le2356 : A B C A' B' C', Bet A B C Bet A' B' C'
  Le A B A' B' Le A' C' A C Le B' C' B C.
Proof.
  intros A B C A' B' C' HBet HBet' HLe1 HLe2.
  elim(eq_dec_points A B).
  { intro; treat_equalities.
    apply (le_transitivity _ _ A' C'); auto.
    destruct (l5_12_a A' B' C'); auto.
  }
  intro.
  assert (AC) by (intro; treat_equalities; auto).
  destruct (l5_5_1 A B A' B' HLe1) as [B0 [HBet1 HCong1]].
  assert (AB0) by (intro; treat_equalities; auto).
  destruct HLe2 as [C0 [HBet2 HCong2]].
    assert (AC0) by (intro; treat_equalities; auto).
  assert (Bet A B0 C0).
  { apply l6_13_1.
      apply (l6_7 _ _ B); [|apply (l6_7 _ _ C)]; [apply l6_6| |apply l6_6]; apply bet_out; auto.
    apply (l5_6 A' B' A' C'); Cong.
    destruct (l5_12_a A' B' C'); auto.
  }
  apply (l5_6 B0 C0 B C); Cong; [apply (le_transitivity _ _ B C0)|].
    destruct (l5_12_a B B0 C0); eBetween.
    destruct (l5_12_a B C0 C); eBetween.
    apply cong_commutativity; apply (l4_3 _ _ A _ _ A'); Between; Cong.
Qed.

Lemma bet2_le2__le1245 : A B C A' B' C', Bet A B C Bet A' B' C'
  Le B C B' C' Le A' C' A C Le A' B' A B.
Proof.
  intros A B C A' B' C'; intros.
  apply le_comm.
  apply (bet2_le2__le2356 C _ _ C'); Le; Between.
Qed.

Lemma cong_preserves_bet : B A' A0 E D' D0,
  Bet B A' A0 Cong B A' E D' Cong B A0 E D0 Out E D' D0
  Bet E D' D0.
Proof.
    intros.
    unfold Out in H2.
    spliter.
    induction H4.
      assumption.
    assert (Le
 E D0 E D').
      eapply l5_5_2.
       D'.
      split.
        assumption.
      Cong.
    assert(Le
 E D' E D0).
      eapply l5_6.
      repeat split.
        2:apply H0.
        2:apply H1.
      eapply l5_5_2.
       A0.
      split.
        assumption.
      Cong.
    assert(Cong E D' E D0).
      apply le_anti_symmetry.
        assumption.
      assumption.
    assert(D0 = D').
      eapply between_cong.
        apply H4.
      Cong.
    subst D'.
    Between.
Qed.

Lemma out_cong_cong : B A A0 E D D0,
 Out B A A0 Out E D D0
 Cong B A E D Cong B A0 E D0
 Cong A A0 D D0.
Proof.
    intros.
    unfold Out in H.
    spliter.
    induction H4.
      assert (Bet E D D0).
        eapply cong_preserves_bet.
          2:apply H1.
          2:apply H2.
          assumption.
        assumption.
      apply cong_commutativity.
      eapply l4_3.
        apply between_symmetry.
        apply H4.
        apply between_symmetry.
        apply H5.
        Cong.
      Cong.
    assert (Bet E D0 D).
      eapply cong_preserves_bet.
        2:apply H2.
        2:apply H1.
        assumption.
      apply l6_6.
      assumption.
    eapply l4_3;eBetween;Cong.
Qed.

Lemma not_out_bet : A B C, Col A B C ¬ Out B A C Bet A B C.
Proof.
    intros.
    unfold Out in H0.
    induction (eq_dec_points A B).
      subst.
      Between.
    induction (eq_dec_points B C).
      subst.
      Between.
    unfold Col in ×.
    decompose [or] H;clear H.
      assumption.
      exfalso.
      apply H0.
      intuition.
    exfalso.
    apply H0.
    intuition.
Qed.

Lemma or_bet_out : A B C, Bet A B C Out B A C ¬Col A B C.
Proof.
    intros.
    destruct (Col_dec A B C); auto.
    destruct (out_dec B A C); auto.
    left; apply not_out_bet; trivial.
Qed.

Lemma not_bet_out : A B C,
 Col A B C ¬Bet A B C Out B A C.
Proof.
    intros.
    destruct (or_bet_out A B C) as [HBet|[HOut|HNCol]]; trivial; contradiction.
Qed.

Lemma not_bet_and_out :
  A B C,
 ¬ (Bet A B C Out B A C).
Proof.
    intros.
    intro.
    spliter.
    unfold Out in H0.
    spliter.
    induction H2.
      assert ( A = B).
        eapply between_equality.
          apply H.
        assumption.
      contradiction.
    assert(C = B).
      eapply between_equality.
        apply between_symmetry.
        apply H.
      assumption.
    contradiction.
Qed.

Lemma out_to_bet :
  A B C A' B' C',
  Col A' B' C'
 (Out B A C Out B' A' C')
  Bet A B C
  Bet A' B' C'.
Proof.
    intros.
    induction(out_dec B A C).
      unfold Out in H2.
      spliter.
      induction H4.
        assert( A = B).
          eapply between_equality.
            apply H1.
          assumption.
        contradiction.
      assert(C = B).
        apply(between_symmetry) in H4.
        eapply between_equality.
          apply between_symmetry.
          apply H1.
        apply between_symmetry.
        assumption.
      contradiction.
    destruct H0.
    assert (¬Out B' A' C').
      intro.
      apply H2.
      apply H3.
      assumption.
    apply not_out_bet.
      assumption.
    assumption.
Qed.

Lemma col_out2_col : A B C AA CC, Col A B C Out B A AA Out B C CC Col AA B CC.
Proof.
    intros.
    induction H.
      assert (Bet AA B CC).
        eapply bet_out_out_bet.
          apply H.
          assumption.
        assumption.
      unfold Col.
      left.
      assumption.
    induction H.
      assert(Out B AA CC).
        eapply l6_7.
          eapply l6_6.
          apply H0.
        apply l6_6.
        eapply l6_7.
          apply l6_6.
          apply H1.
        apply bet_out.
          unfold Out in ×.
          spliter.
          assumption.
          unfold Out in ×.
          spliter.
          assumption.
      apply col_permutation_4.
      apply out_col.
      assumption.
    assert(Out B AA CC).
      eapply l6_6.
      eapply l6_7.
        eapply l6_6.
        apply H1.
      eapply l6_6.
      eapply l6_7.
        eapply l6_6.
        apply H0.
      apply bet_out.
        unfold Out in ×.
        spliter.
        assumption.
        unfold Out in ×.
        spliter.
      apply between_symmetry.
      assumption.
    apply col_permutation_4.
    apply out_col.
    assumption.
Qed.

Lemma bet2_out_out : A B C B' C', B A B' A Out A C C' Bet A B C Bet A B' C' Out A B B'.
Proof.
    intros.
    induction(eq_dec_points B' C').
      subst C'.
      unfold Out in ×.
      spliter.
      repeat split; try assumption.
      induction H5.
        left.
        eapply between_exchange4.
          apply H2.
        assumption.
      eapply l5_3.
        apply H2.
      assumption.
    unfold Out in ×.
    spliter.
    repeat split.
      assumption.
      assumption.
    induction H6.
      assert(Bet A B C').
        eapply between_exchange4.
          apply H2.
        assumption.
      eapply l5_3.
        apply H7.
      assumption.
    assert(Bet B' C' C).
      eapply between_exchange3.
        apply H3.
      assumption.
    assert(Bet A B' C).
      eapply outer_transitivity_between.
        apply H3.
        assumption.
      assumption.
    eapply l5_3.
      apply H2.
    assumption.
Qed.

Lemma out2_out_1 : B C D X,
 Out B X C Out B X D Out B C D.
Proof.
    intros.
    unfold Out in ×.
    spliter.
    repeat split.
      assumption.
      assumption.
    induction H2; induction H4.
      eapply l5_1.
        2: apply H4.
        auto.
      assumption.
      left.
      eapply between_exchange4.
        apply H4.
      assumption.
      right.
      eapply between_exchange4.
        apply H2.
      assumption.
    eapply l5_3.
      apply H4.
    apply H2.
Qed.

Lemma out2_out_2 : B C D X,
 Out B C X Out B D X Out B C D.
Proof.
    intros.
    eapply out2_out_1.
      apply l6_6.
      apply H.
    apply l6_6.
    assumption.
Qed.

Lemma out_bet_out_1 : A B C P,
 Out P A C Bet A B C Out P A B.
Proof.
    intros.
    induction (eq_dec_points B P).
      subst P.
      apply False_ind.
      apply (not_bet_and_out A B C).
      split; assumption.
    unfold Out in ×.
    spliter.
    repeat split.
      assumption.
      assumption.
    induction H3.
      left.
      eapply between_inner_transitivity.
        apply H3.
      assumption.
    right.
    eapply between_exchange2.
      apply H3.
    apply between_symmetry.
    assumption.
Qed.

Lemma out_bet_out_2 : A B C P,
 Out P A C Bet A B C Out P B C.
Proof.
    intros.
    apply l6_6.
    eapply out_bet_out_1.
      apply l6_6.
      apply H.
    apply between_symmetry.
    assumption.
Qed.

Lemma out_bet__out : A B P Q,
 Bet P Q A Out Q A B Out P A B.
Proof.
    intros A B P Q HBet Hout.
    destruct Hout as [HAQ [HBQ [HQAB|HQBA]]]; [|apply l6_6];
      apply bet_out; eBetween; intro; treat_equalities; auto.
    apply HBQ; apply (between_equality _ _ A); Between.
Qed.

End T6_2.

Hint Resolve bet_out out_trivial l6_6 : out.