Library GeoCoq.Tarski_dev.Ch05_bet_le

Require Export GeoCoq.Meta_theory.Decidability.equivalence_between_decidability_properties_of_basic_relations.

Section T5.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l5_1 : A B C D,
  AB Bet A B C Bet A B D Bet A C D Bet A D C.
Proof.
apply eq_dec_implies_l5_1; apply eq_dec_points.
Qed.

Lemma l5_2 : A B C D,
  AB Bet A B C Bet A B D Bet B C D Bet B D C.
Proof.
apply eq_dec_implies_l5_2; apply eq_dec_points.
Qed.

Lemma segment_construction_2 :
   A Q B C, AQ X, (Bet Q A X Bet Q X A) Cong Q X B C.
Proof.
apply eq_dec_implies_segment_construction_2; apply eq_dec_points.
Qed.

Lemma l5_3 : A B C D,
 Bet A B D Bet A C D Bet A B C Bet A C B.
Proof.
    intros.
    assert ( P, Bet D A P AP) by (apply point_construction_different).
    ex_and H1 P.
    assert (Bet P A B) by eBetween.
    assert (Bet P A C) by eBetween.
    apply (l5_2 P);auto.
Qed.

Lemma le_bet : A B C D, Le C D A B X, Bet A X B Cong A X C D.
Proof.
    intros.
    unfold Le in H.
    ex_and H Y.
     Y;split;Cong.
Qed.

Lemma l5_5_1 : A B C D,
  Le A B C D x, Bet A B x Cong A x C D.
Proof.
    unfold Le.
    intros.
    ex_and H P.
    prolong A B x P D.
     x.
    split.
      assumption.
    eapply l2_11;eauto.
Qed.

Lemma l5_5_2 : A B C D,
 ( x, Bet A B x Cong A x C D) Le A B C D.
Proof.
    intros.
    ex_and H P.
    unfold Le.
    assert ( B' : Tpoint, Bet C B' D Cong_3 A B P C B' D) by (eapply l4_5;auto).
    ex_and H1 y.
     y.
    unfold Cong_3 in *;intuition.
Qed.

Lemma l5_6 : A B C D A' B' C' D',
 Le A B C D Cong A B A' B' Cong C D C' D' Le A' B' C' D'.
Proof.
    unfold Le.
    intros.
    spliter.
    ex_and H y.
    assert ( z : Tpoint, Bet C' z D' Cong_3 C y D C' z D') by (eapply l4_5;auto).
    ex_and H3 z.
     z.
    split.
      assumption.
    unfold Cong_3 in *; spliter.
    apply cong_transitivity with A B; try Cong.
    apply cong_transitivity with C y; assumption.
Qed.

Lemma le_reflexivity : A B, Le A B A B.
Proof.
    unfold Le.
    intros.
     B.
    split; Between; Cong.
Qed.

Lemma le_transitivity : A B C D E F, Le A B C D Le C D E F Le A B E F.
Proof.
    unfold Le.
    intros.
    ex_and H y.
    ex_and H0 z.
    assert ( P : Tpoint, Bet E P z Cong_3 C y D E P z) by (eapply l4_5;assumption).
    ex_and H3 P.
     P.
    split.
      eBetween.
    unfold Cong_3 in H4; spliter; apply cong_transitivity with C y; Cong.
Qed.

Lemma between_cong : A B C, Bet A C B Cong A C A B C=B.
Proof.
apply eq_dec_implies_between_cong; apply eq_dec_points.
Qed.

Lemma cong3_symmetry : A B C A' B' C' : Tpoint , Cong_3 A B C A' B' C' Cong_3 A' B' C' A B C.
Proof.
    unfold Cong_3.
    intros.
    intuition.
Qed.

Lemma between_cong_2 : A B D E, Bet A D B Bet A E B Cong A D A E D = E.
Proof.
    intros.
    apply cong3_bet_eq with A B; unfold Cong_3; repeat split; Cong.
    eapply (l4_2 B E A B B D A B).
    unfold IFSC; repeat split; Cong; Between.
Qed.

Lemma between_cong_3 :
   A B D E, A B Bet A B D Bet A B E Cong B D B E D = E.
Proof.
apply eq_dec_implies_between_cong_3; apply eq_dec_points.
Qed.

Lemma le_anti_symmetry : A B C D, Le A B C D Le C D A B Cong A B C D.
Proof.
    intros.
    assert ( T, Bet C D T Cong C T A B) by (apply l5_5_1;assumption).
    unfold Le in H.
    ex_and H Y.
    ex_and H1 T.
    assert (Cong C Y C T) by eCong.
    assert (Bet C Y T) by eBetween.
    assert (Y=T) by (eapply between_cong;eauto).
    subst Y.
    assert (T=D) by (eapply between_equality;eBetween).
    subst T.
    Cong.
Qed.

Lemma Cong_dec : A B C D,
  Cong A B C D ¬ Cong A B C D.
Proof.
apply eq_dec_cong_dec; apply eq_dec_points.
Qed.

Lemma bet_dec : A B C, Bet A B C ¬ Bet A B C.
Proof.
apply eq_dec_bet_dec; apply eq_dec_points.
Qed.

Lemma Col_dec : A B C, Col A B C ¬ Col A B C.
Proof.
    intros.
    unfold Col.
    elim (bet_dec A B C); intro; elim (bet_dec B C A); intro; elim (bet_dec C A B); intro; tauto.
Qed.

Lemma le_trivial : A C D, Le A A C D .
Proof.
    intros.
    unfold Le.
     C.
    split; Between; Cong.
Qed.

Lemma le_cases : A B C D, Le A B C D Le C D A B.
Proof.
    intros.
    induction(eq_dec_points A B).
      subst B; left; apply le_trivial.
    assert ( X : Tpoint, (Bet A B X Bet A X B) Cong A X C D) by (eapply (segment_construction_2 B A C D);auto).
    ex_and H0 X.
    induction H0.
      left; apply l5_5_2; X; split; assumption.
    right; unfold Le; X; split; Cong.
Qed.

Lemma le_zero : A B C, Le A B C C A=B.
Proof.
    intros.
    assert (Le C C A B) by apply le_trivial.
    assert (Cong A B C C) by (apply le_anti_symmetry;assumption).
    treat_equalities;auto.
Qed.

Lemma le_diff : A B C D, A B Le A B C D C D.
Proof.
  intros A B C D HAB HLe Heq.
  subst D; apply HAB, le_zero with C; assumption.
Qed.

Lemma lt_diff : A B C D, Lt A B C D C D.
Proof.
  intros A B C D HLt Heq.
  subst D.
  destruct HLt as [HLe HNCong].
  assert (A = B) by (apply le_zero with C; assumption).
  subst B; Cong.
Qed.

Lemma bet_cong_eq :
  A B C D,
  Bet A B C
  Bet A C D
  Cong B C A D
  C = D A = B.
Proof.
    intros.
    assert(C = D).
      assert(Le A C A D) by (eapply l5_5_2; D; split; Cong).
      assert(Le C B C A) by (eapply l5_5_2; A; split; Between; Cong).
      assert(Cong A C A D) by (eapply le_anti_symmetry; try assumption; apply l5_6 with C B C A; Cong).
      apply between_cong with A; assumption.
    split; try assumption.
    subst D; apply sym_equal.
    eapply (between_cong C); Between; Cong.
Qed.

Lemma cong__le : A B C D, Cong A B C D Le A B C D.
Proof.
  intros A B C D H.
   D.
  split.
  Between.
  Cong.
Qed.

Lemma cong__le3412 : A B C D, Cong A B C D Le C D A B.
Proof.
  intros A B C D HCong.
  apply cong__le.
  Cong.
Qed.

Lemma le1221 : A B, Le A B B A.
Proof.
  intros A B.
  apply cong__le; Cong.
Qed.

Lemma le_left_comm : A B C D, Le A B C D Le B A C D.
Proof.
  intros A B C D Hle.
  apply (le_transitivity _ _ A B); auto.
  apply le1221; auto.
Qed.

Lemma le_right_comm : A B C D, Le A B C D Le A B D C.
Proof.
  intros A B C D Hle.
  apply (le_transitivity _ _ C D); auto.
  apply le1221; auto.
Qed.

Lemma le_comm : A B C D, Le A B C D Le B A D C.
Proof.
  intros.
  apply le_left_comm.
  apply le_right_comm.
  assumption.
Qed.

Lemma ge_left_comm : A B C D, Ge A B C D Ge B A C D.
Proof.
    intros.
    unfold Ge in ×.
    apply le_right_comm.
    assumption.
Qed.

Lemma ge_right_comm : A B C D, Ge A B C D Ge A B D C.
Proof.
    intros.
    unfold Ge in ×.
    apply le_left_comm.
    assumption.
Qed.

Lemma ge_comm : A B C D, Ge A B C D Ge B A D C.
Proof.
    intros.
    apply ge_left_comm.
    apply ge_right_comm.
    assumption.
Qed.

Lemma lt_right_comm : A B C D, Lt A B C D Lt A B D C.
Proof.
    intros.
    unfold Lt in ×.
    spliter.
    split.
      apply le_right_comm.
      assumption.
    intro.
    apply H0.
    apply cong_right_commutativity.
    assumption.
Qed.

Lemma lt_left_comm : A B C D, Lt A B C D Lt B A C D.
Proof.
    intros.
    unfold Lt in ×.
    spliter.
    split.
      unfold Le in ×.
      ex_and H P.
       P.
      apply cong_left_commutativity in H1.
      split; assumption.
    intro.
    apply H0.
    apply cong_left_commutativity.
    assumption.
Qed.

Lemma lt_comm : A B C D, Lt A B C D Lt B A D C.
Proof.
    intros.
    apply lt_left_comm.
    apply lt_right_comm.
    assumption.
Qed.

Lemma gt_left_comm : A B C D, Gt A B C D Gt B A C D.
Proof.
    intros.
    unfold Gt in ×.
    apply lt_right_comm.
    assumption.
Qed.

Lemma gt_right_comm : A B C D, Gt A B C D Gt A B D C.
Proof.
    intros.
    unfold Gt in ×.
    apply lt_left_comm.
    assumption.
Qed.

Lemma gt_comm : A B C D, Gt A B C D Gt B A D C.
Proof.
    intros.
    apply gt_left_comm.
    apply gt_right_comm.
    assumption.
Qed.

Lemma cong2_lt__lt : A B C D A' B' C' D',
 Lt A B C D Cong A B A' B' Cong C D C' D' Lt A' B' C' D'.
Proof.
  intros A B C D A' B' C' D' Hlt HCong1 HCong2.
  destruct Hlt as [Hle HNCong].
  split.
  apply (l5_6 A B C D); auto.
  intro.
  apply HNCong.
  apply (cong_transitivity _ _ A' B'); auto.
  apply (cong_transitivity _ _ C' D'); Cong.
Qed.

Lemma fourth_point : A B C P, A B B C Col A B P Bet A B C
  Bet P A B Bet A P B Bet B P C Bet B C P.
Proof.
    intros.
    induction H1.
      assert(HH:= l5_2 A B C P H H2 H1).
      right; right.
      induction HH.
        right; auto.
      left; auto.
    induction H1.
      right; left.
      Between.
    left; auto.
Qed.

Lemma third_point : A B P, Col A B P Bet P A B Bet A P B Bet A B P.
Proof.
    intros.
    induction H.
      right; right.
      auto.
    induction H.
      right; left.
      Between.
    left.
    auto.
Qed.

Lemma l5_12_a : A B C, Bet A B C Le A B A C Le B C A C.
Proof.
    intros.
    split.
      unfold Le.
       B; split.
        assumption.
      apply cong_reflexivity.
    apply le_comm.
    unfold Le.
     B.
    split.
      apply between_symmetry.
      assumption.
    apply cong_reflexivity.
Qed.

Lemma bet__le1213 : A B C, Bet A B C Le A B A C.
Proof.
    intros A B C HBet.
    destruct (l5_12_a A B C HBet); trivial.
Qed.

Lemma bet__le2313 : A B C, Bet A B C Le B C A C.
Proof.
    intros A B C HBet.
    destruct (l5_12_a A B C HBet); trivial.
Qed.

Lemma bet__lt1213 : A B C, B C Bet A B C Lt A B A C.
Proof.
    intros A B C HBC HBet.
    split.
      apply bet__le1213; trivial.
    intro.
    apply HBC, between_cong with A; trivial.
Qed.

Lemma bet__lt2313 : A B C, A B Bet A B C Lt B C A C.
Proof.
    intros; apply lt_comm, bet__lt1213; Between.
Qed.

Lemma l5_12_b : A B C, Col A B C Le A B A C Le B C A C Bet A B C.
Proof.
    intros.
    unfold Col in H.
    induction H.
      assumption.
    induction H.
      assert(Le B C B A Le C A B A).
        apply l5_12_a.
          assumption.
      spliter.
      assert(Cong A B A C).
        apply le_anti_symmetry.
          assumption.
        apply le_comm.
        assumption.
      assert(C = B).
        eapply between_cong.
          apply between_symmetry.
          apply H.
        apply cong_symmetry.
        assumption.
      subst B.
      apply between_trivial.
    assert(Le B A B C Le A C B C).
      apply l5_12_a.
        apply between_symmetry.
        assumption.
    spliter.
    assert(Cong B C A C).
      apply le_anti_symmetry.
        assumption.
      assumption.
    assert(A = B).
      eapply between_cong.
        apply H.
      apply cong_symmetry.
      apply cong_commutativity.
      assumption.
    subst A.
    apply between_symmetry.
    apply between_trivial.
Qed.

Lemma bet_le_eq : A B C, Bet A B C Le A C B C A = B.
Proof.
    intros.
    assert(Le C B C A).
      eapply l5_5_2.
       A.
      split.
        apply between_symmetry.
        assumption.
      apply cong_reflexivity.
    assert(Cong A C B C).
      apply le_anti_symmetry.
        assumption.
      apply le_comm.
      assumption.
    apply sym_equal.
    eapply between_cong.
      apply between_symmetry.
      apply H.
    apply cong_commutativity.
    apply cong_symmetry.
    assumption.
Qed.

Lemma or_lt_cong_gt : A B C D, Lt A B C D Gt A B C D Cong A B C D.
Proof.
    intros.
    assert(HH:= le_cases A B C D).
    induction HH.
      induction(Cong_dec A B C D).
        right; right.
        assumption.
      left.
      unfold Lt.
      split; assumption.
    induction(Cong_dec A B C D).
      right; right.
      assumption.
    right; left.
    unfold Gt.
    unfold Lt.
    split.
      assumption.
    intro.
    apply H0.
    apply cong_symmetry.
    assumption.
Qed.

Lemma lt__le : A B C D, Lt A B C D Le A B C D.
Proof.
    intros A B C D Hlt.
    destruct Hlt.
    assumption.
Qed.

Lemma le1234_lt__lt : A B C D E F, Le A B C D Lt C D E F Lt A B E F.
Proof.
    intros A B C D E F Hle Hlt.
    destruct Hlt as [Hle' HNCong].
    split.
      apply (le_transitivity _ _ C D); auto.
    intro.
    apply HNCong.
    apply le_anti_symmetry; auto.
    apply (l5_6 A B C D); Cong.
Qed.

Lemma le3456_lt__lt : A B C D E F, Lt A B C D Le C D E F Lt A B E F.
Proof.
    intros A B C D E F Hlt Hle.
    destruct Hlt as [Hle' HNCong].
    split.
      apply (le_transitivity _ _ C D); auto.
    intro.
    apply HNCong.
    apply le_anti_symmetry; auto.
    apply (l5_6 C D E F); Cong.
Qed.

Lemma lt_transitivity : A B C D E F, Lt A B C D Lt C D E F Lt A B E F.
Proof.
    intros A B C D E F HLt1 HLt2.
    apply le1234_lt__lt with C D; try (apply lt__le); assumption.
Qed.

Lemma not_and_lt : A B C D, ¬ (Lt A B C D Lt C D A B).
Proof.
    intros A B C D.
    intro HInter.
    destruct HInter as [[Hle HNCong] []].
    apply HNCong.
    apply le_anti_symmetry; assumption.
Qed.

Lemma nlt : A B, ¬ Lt A B A B.
Proof.
    intros A B Hlt.
    apply (not_and_lt A B A B).
    split; assumption.
Qed.

Lemma le__nlt : A B C D, Le A B C D ¬ Lt C D A B.
Proof.
    intros A B C D HLe HLt.
    apply (not_and_lt A B C D); split; auto.
    split; auto.
    unfold Lt in *; spliter; auto with cong.
Qed.

Lemma cong__nlt : A B C D,
 Cong A B C D ¬ Lt A B C D.
Proof.
    intros P Q R S H.
    apply le__nlt.
    unfold Le.
     Q; split; Cong; Between.
Qed.

Lemma nlt__le : A B C D, ¬ Lt A B C D Le C D A B.
Proof.
    intros A B C D HNLt.
    destruct (le_cases A B C D); trivial.
    destruct (Cong_dec C D A B).
      apply cong__le; assumption.
    exfalso.
    apply HNLt.
    split; Cong.
Qed.

Lemma lt__nle : A B C D, Lt A B C D ¬ Le C D A B.
Proof.
  intros A B C D HLt HLe.
  generalize HLt.
  apply le__nlt; assumption.
Qed.

Lemma nle__lt : A B C D, ¬ Le A B C D Lt C D A B.
Proof.
    intros A B C D HNLe.
    destruct (le_cases A B C D).
      contradiction.
    split; trivial.
    intro.
    apply HNLe.
    apply cong__le; Cong.
Qed.

Lemma lt1123 : A B C, BC Lt A A B C.
Proof.
intros.
split.
apply le_trivial.
intro.
treat_equalities.
intuition.
Qed.

Lemma bet2_le2__le : O o A B a b, Bet a o b Bet A O B Le o a O A Le o b O B Le a b A B.
Proof.
intros.
induction(eq_dec_points A O).
treat_equalities; auto.
assert (o=a).
apply le_zero with A;auto.
subst;auto.
induction(eq_dec_points B O).
treat_equalities;auto.
assert (o=b).
apply le_zero with B;auto.
subst;auto using le_left_comm, le_right_comm.

assert(HH:= segment_construction A O b o).
ex_and HH b'.
assert(HH:= segment_construction B O a o).
ex_and HH a'.

unfold Le in H1.
ex_and H1 a''.

assert(a' = a'').
{
  apply(construction_uniqueness B O a o a' a'' H4);
  eBetween.
  Cong.
}
treat_equalities.

assert(Le B a' B A).
{
  unfold Le.
   a'.
  split; eBetween; Cong.
}

unfold Le in H2.
ex_and H2 b''.

assert(b' = b'').
{
  apply(construction_uniqueness A O b o b' b'' H3);
  eBetween.
  Cong.
}

treat_equalities.

assert(Le a' b' a' B).
{
  unfold Le.
   b'.
  split; eBetween; Cong.
}

assert(Le a' b' A B).
{
  apply(le_transitivity a' b' a' B A B); auto using le_left_comm, le_right_comm.
}

apply(l5_6 a' b' A B a b A B); Cong.
apply (l2_11 a' O b' a o b);
eBetween; Cong.
Qed.

End T5.

Hint Resolve le_reflexivity le_anti_symmetry le_trivial le_zero cong__le cong__le3412
             le1221 le_left_comm le_right_comm le_comm lt__le bet__le1213 bet__le2313 : Le.

Ltac Le := auto with Le.