Library cong

Require Export axioms.
Require Export general_tactics.

Section T1.

Context `{M:Tarski}.

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

Lemma cong_reflexivity : forall A B,
 Cong A B A B.
Proof.
intros.
apply (cong_inner_transitivity B A A B);
apply cong_pseudo_reflexivity.
Qed.

Lemma cong_symmetry : forall A B C D : Tpoint,
 Cong A B C D -> Cong C D A B.
Proof.
intros.
eapply cong_inner_transitivity.
apply H.
apply cong_reflexivity.
Qed.

Lemma cong_transitivity : forall A B C D E F : Tpoint,
 Cong A B C D -> Cong C D E F -> Cong A B E F.
Proof.
intros.
eapply cong_inner_transitivity; eauto using cong_symmetry.
Qed.

Lemma cong_left_commutativity : forall A B C D,
 Cong A B C D -> Cong B A C D.
Proof.
intros.
eapply cong_inner_transitivity.
apply cong_symmetry.
apply cong_pseudo_reflexivity.
assumption.
Qed.

Lemma cong_right_commutativity : forall A B C D,
 Cong A B C D -> Cong A B D C.
Proof.
intros.
apply cong_symmetry.
apply cong_symmetry in H.
apply cong_left_commutativity.
assumption.
Qed.

Lemma cong_trivial_identity : forall A B : Tpoint,
 Cong A A B B.
Proof.
intros.
prolong A B E A A.

eapply cong_inner_transitivity.
apply H0.
assert(B=E).
eapply cong_identity.
apply H0.
subst.
apply cong_reflexivity.
Qed.

Lemma cong_reverse_identity : forall A C D,
 Cong A A C D -> C=D.
Proof.
intros.
apply cong_symmetry in H.
eapply cong_identity.
apply H.
Qed.

Lemma cong_commutativity : forall A B C D,
 Cong A B C D -> Cong B A D C.
Proof.
intros.
apply cong_left_commutativity.
apply cong_right_commutativity.
assumption.
Qed.

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.

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

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

Lemma five_segments_with_def : forall A B C D A' B' C' D',
 OFSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
unfold OFSC.
intros;spliter.
apply (five_segments A A' B B'); assumption.
Qed.

Axiom eq_dec_points : forall A B : Tpoint, A=B \/ ~ A=B.

Lemma cong_diff : forall A B C D : Tpoint, A <> B -> Cong A B C D -> C <> D.
Proof.
intros.
intro.
subst.
apply H.
eauto using cong_identity.
Qed.

Definition Cong_3 := fun A1 A2 A3 B1 B2 B3 => Cong A1 A2 B1 B2 /\ Cong A1 A3 B1 B3 /\ Cong A2 A3 B2 B3.

Lemma cong_3_sym : forall A B C A' B' C',
  Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
unfold Cong_3.
intuition.
Qed.

Hint Resolve cong_3_sym : Cong.

Lemma cong_3_swap : forall A B C A' B' C',
  Cong_3 A B C A' B' C' -> Cong_3 B A C B' A' C'.
Proof.
unfold Cong_3.
intuition.
Qed.

Lemma cong_3_swap_2 : forall A B C A' B' C',
  Cong_3 A B C A' B' C' -> Cong_3 A C B A' C' B'.
Proof.
unfold Cong_3.
intuition.
Qed.

Hint Resolve cong_3_swap cong_3_swap_2 : Cong3.
Hint Unfold Cong_3 : Cong3.

Lemma cong3_transitivity : forall A0 B0 C0 A1 B1 C1 A2 B2 C2,
       Cong_3 A0 B0 C0 A1 B1 C1 -> Cong_3 A1 B1 C1 A2 B2 C2 -> Cong_3 A0 B0 C0 A2 B2 C2.
unfold Cong_3.
intros.
spliter.
repeat split.
eapply cong_transitivity.
apply H.
assumption.
eapply cong_transitivity.
apply H3.
assumption.
eapply cong_transitivity.
apply H4.
assumption.
Qed.

Hint Resolve cong3_transitivity : Cong3.

Lemma l2_l1 : forall A B C A' B' C',
 Bet A B C -> Bet A' B' C' -> Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
Proof.
intros.
induction (eq_dec_points A B).
 subst B.
 assert (A'=B').
 eapply (cong_identity _ _ A).
 Cong.
 subst.
 Cong.

assert (Cong C A C' A')
 by (apply (five_segments _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity).
Cong.
Qed.

Lemma construction_unicity : forall Q A B C x y,
   ~(Q=A) -> Bet Q A x -> Cong A x B C -> Bet Q A y -> Cong A y B C -> x=y.
Proof.
intros.
assert (Cong A x A y) by
 (apply cong_transitivity with (C:=B) (D:=C);auto using cong_symmetry).

assert (Cong Q x Q y)
 by (apply (l2_l1 Q A x Q A y);Cong).

assert(OFSC Q A x y Q A x x)
 by (unfold OFSC;repeat split;Cong).

apply five_segments_with_def in H6.
apply cong_identity in H6.
assumption.
assumption.
Qed.

End T1.