Library bet

Require Export cong.

Section T2.

Context `{M:Tarski}.

Ltac prolong A B x C D :=
 assert (sg:= segment_construction A B C D);
 ex_and sg x.

Definition Col (A B C : Tpoint) : Prop := Bet A B C \/ Bet B C A \/ Bet C A B.

Lemma bet_col : forall A B C, Bet A B C -> Col A B C.
Proof.
intros;unfold Col;auto.
Qed.

Lemma between_trivial : forall A B : Tpoint, Bet A B B.
Proof.
intros.
prolong A B x B B.
assert (x = B)
 by (apply cong_identity in H0;auto).
subst;assumption.
Qed.

Lemma between_symmetry : forall A B C : Tpoint, Bet A B C -> Bet C B A.
Proof.
intros.
assert (Bet B C C).
apply between_trivial.
assert(exists x, Bet B x B /\ Bet C x A)
 by (eapply inner_pasch;eauto).
ex_and H1 x.
apply between_identity in H1.
subst;assumption.
Qed.

Lemma between_trivial2 : forall A B : Tpoint, Bet A A B.
Proof.
intros.
apply between_symmetry.
apply between_trivial.
Qed.

Lemma between_egality : forall A B C : Tpoint, Bet A B C -> Bet B A C -> A = B.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet A x A)
 by (apply (inner_pasch A B C);assumption).
ex_and H1 x.
apply between_identity in H1.
apply between_identity in H2.
congruence.
Qed.


Ltac assert_cols :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Col ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X2 ?X1) |- _ => clear H
end.

Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.

Ltac treat_equalities_aux :=
  match goal with
   | H:(?X1 = ?X2) |- _ => smart_subst X2
end.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);apply cong_symmetry;assumption|idtac];smart_subst X2
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);assumption|idtac];smart_subst X2
   | H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.

Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].

Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.

Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.

Lemma between_inner_transitivity : forall A B C D, Bet A B D -> Bet B C D -> Bet A B C.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet C x A).
eapply inner_pasch;eauto.
ex_and H1 x.
Between.
Qed.

Lemma between_exchange3 : forall A B C D, Bet A B C -> Bet A C D -> Bet B C D.
Proof.
intros.
assert (exists x, Bet C x C /\ Bet B x D)
 by (eapply inner_pasch;eBetween).
ex_and H1 x.
Between.
Qed.

Lemma outer_transitivity_between2 : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
Proof.
intros.
prolong A C x C D.
assert (x = D).
 apply (construction_unicity B C C D);
 try assumption.
 apply (between_exchange3 A B C x); assumption.
 apply cong_reflexivity.

subst x;assumption.
Qed.

Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 : Between.

Lemma between_exchange2 : forall A B C D, Bet A B D -> Bet B C D -> Bet A C D.
intros.
induction (eq_dec_points B C);eBetween.
Qed.

Hint Resolve between_exchange2 : Between.

Lemma outer_transitivity_between : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A B D.
eBetween.
Qed.

Lemma between_exchange4 : forall A B C D, Bet A B C -> Bet A C D -> Bet A B D.
eBetween.
Qed.

Hint Resolve outer_transitivity_between between_exchange4.

Definition Bet_4 := fun A1 A2 A3 A4 =>
   Bet A1 A2 A3 /\ Bet A2 A3 A4 /\ Bet A1 A3 A4 /\ Bet A1 A2 A4.

Lemma l_3_9_4 : forall A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 -> Bet_4 A4 A3 A2 A1.
Proof.
unfold Bet_4.
intros;spliter;Between.
Qed.

Lemma two_distinct_points : exists x, exists y: Tpoint, x <> y.
Proof.
assert (ld:=lower_dim).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
unfold Col in H.
induction (eq_dec_points A B).
subst A.
exists B.
exists C.
Between.

firstorder.
Qed.

Lemma point_construction_different : forall A B, exists C, Bet A B C /\ B <> C.
Proof.
intros.
assert (tdp := two_distinct_points).
ex_elim tdp x.
ex_elim H y.
prolong A B E x y.
exists E.
show_distinct B E.
apply cong_symmetry in H1.
apply cong_identity in H1.
intuition.
intuition.
Qed.

Lemma another_point : forall A: Tpoint, exists B, A<>B.
Proof.
intros.
assert (pcd := point_construction_different A A).
ex_and pcd B.
exists B;assumption.
Qed.

Lemma l3_17 : forall A B C A' B' P,
               Bet A B C -> Bet A' B' C -> Bet A P A' -> exists Q, Bet P Q C /\ Bet B Q B'.
Proof.
intros.
assert (exists Q', Bet B' Q' A /\ Bet P Q' C)
 by (eapply inner_pasch;eBetween).
ex_and H2 x.
assert (exists y, Bet x y C /\ Bet B y B')
 by (eapply inner_pasch;eBetween).
ex_and H4 y.
exists y;eBetween.
Qed.

End T2.