Library GeoCoq.Tarski_dev.Ch02_cong

Require Export GeoCoq.Axioms.tarski_axioms.

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

Section T1_1.

Context `{Tn:Tarski_neutral_dimensionless}.

Lemma cong_reflexivity : 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 : 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 : 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 : 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 : 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_3421 : A B C D,
 Cong A B C D Cong C D B A.
Proof.
    auto using cong_symmetry, cong_right_commutativity.
Qed.

Lemma cong_4312 : A B C D,
 Cong A B C D Cong D C A B.
Proof.
    auto using cong_symmetry, cong_right_commutativity.
Qed.

Lemma cong_4321 : A B C D,
 Cong A B C D Cong D C B A.
Proof.
    auto using cong_symmetry, cong_right_commutativity.
Qed.

Lemma cong_trivial_identity : 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 : 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 : 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.

End T1_1.

Hint Resolve cong_commutativity cong_3421 cong_4312 cong_4321 cong_reverse_identity cong_trivial_identity
             cong_left_commutativity cong_right_commutativity
             cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.

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

Section T1_2.

Context `{Tn:Tarski_neutral_dimensionless}.


Lemma not_cong_2134 : A B C D, ¬ Cong A B C D ¬ Cong B A C D.
Proof.
auto with cong.
Qed.

Lemma not_cong_1243 : A B C D, ¬ Cong A B C D ¬ Cong A B D C.
Proof.
auto with cong.
Qed.

Lemma not_cong_2143 : A B C D, ¬ Cong A B C D ¬ Cong B A D C.
Proof.
auto with cong.
Qed.

Lemma not_cong_3412 : A B C D, ¬ Cong A B C D ¬ Cong C D A B.
Proof.
auto with cong.
Qed.

Lemma not_cong_4312 : A B C D, ¬ Cong A B C D ¬ Cong D C A B.
Proof.
auto with cong.
Qed.

Lemma not_cong_3421 : A B C D, ¬ Cong A B C D ¬ Cong C D B A.
Proof.
auto with cong.
Qed.

Lemma not_cong_4321 : A B C D, ¬ Cong A B C D ¬ Cong D C B A.
Proof.
auto with cong.
Qed.

End T1_2.

Hint Resolve not_cong_2134 not_cong_1243 not_cong_2143
             not_cong_3412 not_cong_4312 not_cong_3421 not_cong_4321 : cong.

Section T1_3.

Context `{Tn:Tarski_neutral_dimensionless}.

Definition OFSC 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_segment_with_def : A B C D A' B' C' D',
 OFSC A B C D A' B' C' D' AB Cong C D C' D'.
Proof.
    unfold OFSC.
    intros;spliter.
    apply (five_segment A A' B B'); assumption.
Qed.

Lemma cong_diff : 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.

Lemma cong_diff_2 : A B C D ,
 B A Cong A B C D C D.
Proof.
    intros.
    intro;subst.
    apply H.
    symmetry.
    eauto using cong_identity, cong_symmetry.
Qed.

Lemma cong_diff_3 : A B C D ,
 C D Cong A B C D A B.
Proof.
    intros.
    intro;subst.
    apply H.
    eauto using cong_identity, cong_symmetry.
Qed.

Lemma cong_diff_4 : A B C D ,
 D C Cong A B C D A B.
Proof.
    intros.
    intro;subst.
    apply H.
    symmetry.
    eauto using cong_identity, cong_symmetry.
Qed.

Definition Cong_3 A B C A' B' C' := Cong A B A' B' Cong A C A' C' Cong B C B' C'.

Lemma cong_3_sym : 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.

Lemma cong_3_swap : 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 : 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.

Lemma cong3_transitivity : 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.
Proof.
    unfold Cong_3.
    intros.
    spliter.
    repeat split; eCong.
Qed.

End T1_3.

Hint Resolve cong_3_sym : cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : cong3.
Hint Unfold Cong_3 : cong3.

Section T1_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma eq_dec_points : A B : Tpoint, A=B ¬ A=B.
Proof. exact point_equality_decidability. Qed.

Lemma l2_11 : 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') by
     (apply (cong_identity A' B' A); Cong).
      subst; Cong.
    apply cong_commutativity; apply (five_segment A A' B B' C C' A A'); Cong.
Qed.

Lemma bet_cong3 : A B C A' B', Bet A B C Cong A B A' B' C', Cong_3 A B C A' B' C'.
Proof.
    intros.
    assert ( x, Bet A' B' x Cong B' x B C) by (apply segment_construction).
    ex_and H1 x.
    assert (Cong A C A' x).
      eapply l2_11.
        apply H.
        apply H1.
        assumption.
      Cong.
     x;unfold Cong_3; repeat split;Cong.
Qed.

Lemma construction_uniqueness : 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 eCong.
    assert (Cong Q X Q Y) by (apply (l2_11 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_segment_with_def in H6; try assumption.
    apply cong_identity with X; Cong.
Qed.

Lemma Cong_cases :
  A B C D,
 Cong A B C D Cong A B D C Cong B A C D Cong B A D C
 Cong C D A B Cong C D B A Cong D C A B Cong D C B A
 Cong A B C D.
Proof.
    intros.
    decompose [or] H;clear H; Cong.
Qed.

Lemma Cong_perm :
  A B C D,
 Cong A B C D
 Cong A B C D Cong A B D C Cong B A C D Cong B A D C
 Cong C D A B Cong C D B A Cong D C A B Cong D C B A.
Proof.
    intros.
    repeat split; Cong.
Qed.

End T1_4.