Library cong_bet

Require Export bet.

Section T3.

Context `{M:Tarski}.

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) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H;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.

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

Definition IFSC := fun A B C D A' B' C' D' =>
   Bet A B C /\ Bet A' B' C' /\
   Cong A C A' C' /\ Cong B C B' C' /\
   Cong A D A' D' /\ Cong C D C' D'.

Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
             cong_left_commutativity cong_right_commutativity
             cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.

Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.

Lemma l4_2 : forall A B C D A' B' C' D', IFSC A B C D A' B' C' D' -> Cong B D B' D'.
Proof.
unfold IFSC.
intros.
spliter.

induction (eq_dec_points A C).

treat_equalities;assumption.

assert (exists E, Bet A C E /\ C <> E)
 by apply point_construction_different.
ex_and H6 E.
prolong A' C' E' C E.

assert (Cong E D E' D')
 by (
  apply (five_segments_with_def A C E D A' C' E' D');[
  unfold OFSC; repeat split;Cong|
  assumption]).

apply (five_segments_with_def E C B D E' C' B' D').
unfold OFSC.
repeat split; try solve [eBetween| Cong ].
auto.
Qed.

Lemma l4_3 : forall A B C A' B' C',
  Bet A B C -> Bet A' B' C' -> Cong A C A' C' -> Cong B C B' C' -> Cong A B A' B'.
Proof.
intros.
apply cong_commutativity.
apply (l4_2 A B C A A' B' C' A').
unfold IFSC.
repeat split;Cong.
Qed.

Lemma l4_5 : forall A B C A' C',
  Bet A B C -> Cong A C A' C' ->
  exists B', Bet A' B' C' /\ Cong_3 A B C A' B' C'.
Proof.
intros.
unfold Cong_3.

assert (exists D', Bet C' A' D' /\ A' <> D')
 by (apply point_construction_different).
ex_and H1 x'.
prolong x' A' B' A B.
prolong x' B' C'' B C.

assert (Bet A' B' C'') by eBetween.

assert (C'' = C').
eapply (construction_unicity x' A' ).

auto.
eBetween.

apply (l2_l1 A' B' C'' A B C);Between.

eBetween.
Cong.

subst C''.
exists B'.
Cong.
Qed.

Lemma l4_6 : forall A B C A' B' C', Bet A B C -> Cong_3 A B C A' B' C' -> Bet A' B' C'.
Proof.
unfold Cong_3.
intros.
assert (exists B'', Bet A' B'' C' /\ Cong_3 A B C A' B'' C')
  by (eapply l4_5;intuition).
ex_and H1 x.
unfold Cong_3 in *;spliter.

assert (Cong_3 A' x C' A' B' C')
 by (unfold Cong_3;repeat split;eCong).
unfold Cong_3 in H7;spliter.

assert (IFSC A' x C' x A' x C' B')
 by (unfold IFSC;repeat split;Cong).
assert (Cong x x x B')
 by (eapply l4_2;apply H10).
Between.
Qed.

Lemma cong3_bet_eq : forall A B C x,
 Bet A B C -> Cong_3 A B C A x C -> x = B.
Proof.
unfold Cong_3.
intros.
spliter.
assert (IFSC A B C B A B C x)
 by (unfold IFSC;intuition).
assert (Cong B B B x)
 by (apply (l4_2 _ _ _ _ _ _ _ _ H3)).
Between.
Qed.

End T3.