Library GeoCoq.Tarski_dev.Ch13_2_length

Require Export GeoCoq.Tarski_dev.Ch13_1.

Section Length_1.

Context `{T2D:Tarski_2D}.

Pappus Desargues
****************** length

Lemma lg_exists : A B, l, Q_Cong l l A B.
Proof.
    intros.
    unfold Q_Cong.
     (fun x yCong A B x y).
    split.
       A.
       B.
      intros.
      split; auto.
    Cong.
Qed.

Lemma lg_cong : l A B C D, Q_Cong l l A B l C D Cong A B C D.
Proof.
    intros.
    unfold Q_Cong in H.
    ex_and H X.
    ex_and H2 Y.
    assert(HH:= H A B).
    destruct HH.
    assert(HH:= H C D).
    destruct HH.
    apply H3 in H0.
    apply H5 in H1.
    apply cong_transitivity with X Y; Cong.
Qed.

Lemma lg_cong_lg : l A B C D, Q_Cong l l A B Cong A B C D l C D.
Proof.
    intros.
    unfold Q_Cong in H.
    ex_and H A0.
    ex_and H2 B0.
    assert(HP:= H A B).
    assert(HQ:= H C D).
    destruct HP.
    destruct HQ.
    apply H4.
    eapply cong_transitivity.
      apply H3.
      assumption.
    assumption.
Qed.

Lemma lg_sym : l A B, Q_Cong l l A B l B A.
Proof.
    intros.
    apply (lg_cong_lg l A B); Cong.
Qed.

Lemma ex_points_lg : l, Q_Cong l A, B, l A B.
Proof.
    intros.
    unfold Q_Cong in H.
    ex_and H A.
    ex_and H0 B.
    assert(HH:= H A B).
    destruct HH.
     A.
     B.
    apply H0.
    Cong.
Qed.

End Length_1.

Ltac lg_instance l A B :=
  assert(tempo_sg:= ex_points_lg l);
  match goal with
    |H: Q_Cong l |- _assert(tempo_H:=H); apply tempo_sg in tempo_H; elim tempo_H; intros A ; let tempoHP := fresh "tempo_HP" in intro tempoHP; clear tempo_H; elim tempoHP; intro B; intro; clear tempoHP
  end;
  clear tempo_sg.

Section Length_2.

Context `{T2D:Tarski_2D}.

Lemma is_len_cong : A B C D l, Len A B l Len C D l Cong A B C D.
Proof.
    intros.
    unfold Len in ×.
    spliter.
    eapply (lg_cong l); auto.
Qed.

Lemma is_len_cong_is_len : A B C D l, Len A B l Cong A B C D Len C D l.
Proof.
    intros.
    unfold Len in ×.
    spliter.
    split.
      auto.
    unfold Q_Cong in H.
    ex_and H a.
    ex_and H2 b.
    assert(HH:= H A B).
    destruct HH.
    assert(HH1:= H C D).
    destruct HH1.
    apply H3 in H1.
    apply H4.
    apply cong_transitivity with A B; trivial.
Qed.

Lemma not_cong_is_len : A B C D l , ~(Cong A B C D) Len A B l ~(l C D).
Proof.
    intros.
    unfold Len in H0.
    spliter.
    intro.
    apply H.
    apply (lg_cong l); auto.
Qed.

Lemma not_cong_is_len1 : A B C D l , ¬Cong A B C D Len A B l ¬ Len C D l.
Proof.
    intros.
    intro.
    unfold Len in ×.
    spliter.
    apply H.
    apply (lg_cong l); auto.
Qed.

Lemma lg_null_instance : l A, Q_Cong_Null l l A A.
Proof.
    intros.
    unfold Q_Cong_Null in H.
    spliter.
    unfold Q_Cong in H.
    ex_and H X.
    ex_and H1 Y.
    assert(HH:= H A A).
    destruct HH.
    ex_and H0 P.
    assert(HH:=(H P P)).
    destruct HH.
    apply H4 in H3.
    apply H1.
    apply cong_symmetry in H3.
    apply cong_reverse_identity in H3.
    subst Y.
    apply cong_trivial_identity.
Qed.

Lemma lg_null_trivial : l A, Q_Cong l l A A Q_Cong_Null l.
Proof.
    intros.
    unfold Q_Cong_Null.
    split.
      auto.
     A.
    auto.
Qed.

Lemma lg_null_dec : l, Q_Cong l Q_Cong_Null l ¬ Q_Cong_Null l.
Proof.
    intros.
    assert(HH:=H).
    unfold Q_Cong in H.
    ex_and H A.
    ex_and H0 B.
    induction(eq_dec_points A B).
      subst B.
      left.
      unfold Q_Cong_Null.
      split.
        auto.
       A.
      apply H.
      Cong.
    right.
    intro.
    unfold Q_Cong_Null in H1.
    spliter.
    ex_and H2 P.
    apply H0.
    assert(Cong A B P P).
      apply H; auto.
    apply cong_identity in H2.
    auto.
Qed.

Lemma ex_point_lg : l A, Q_Cong l B, l A B.
Proof.
    intros.
    induction(lg_null_dec l).
       A.
      apply lg_null_instance.
      auto.
      assert(HH:= H).
      unfold Q_Cong in HH.
      ex_and HH X.
      ex_and H1 Y.
      assert(HH:= another_point A).
      ex_and HH P.
      assert(HP:= H2 X Y).
      destruct HP.
      assert(l X Y).
        apply H3.
        apply cong_reflexivity.
      assert(X Y).
        intro.
        subst Y.
        apply H0.
        unfold Q_Cong_Null.
        split.
          auto.
         X.
        auto.
      assert(HH:= segment_construction_3 A P X Y H1 H6).
      ex_and HH B.
       B.
      assert(HH:= H2 A B).
      destruct HH.
      apply H9.
      Cong.
    auto.
Qed.

Lemma ex_point_lg_out : l A P, A P Q_Cong l ¬ Q_Cong_Null l B, l A B Out A B P.
Proof.
    intros.
    assert(HH:= H0).
    unfold Q_Cong in HH.
    ex_and HH X.
    ex_and H2 Y.
    assert(HP:= H3 X Y).
    destruct HP.
    assert(l X Y).
      apply H2.
      apply cong_reflexivity.
    assert(X Y).
      intro.
      subst Y.
      apply H1.
      unfold Q_Cong_Null.
      split.
        auto.
       X.
      auto.
    assert(HH:= segment_construction_3 A P X Y H H6).
    ex_and HH B.
     B.
    split.
      assert(HH:= H3 A B).
      destruct HH.
      apply H9.
      Cong.
    apply l6_6.
    auto.
Qed.

Lemma ex_point_lg_bet : l A M, Q_Cong l B : Tpoint, l M B Bet A M B.
Proof.
    intros.
    assert(HH:= H).
    unfold Q_Cong in HH.
    ex_and HH X.
    ex_and H0 Y.
    assert(HP:= H1 X Y).
    destruct HP.
    assert(l X Y).
      apply H0.
      apply cong_reflexivity.
    prolong A M B X Y.
     B.
    split; auto.
    eapply (lg_cong_lg l X Y); Cong.
Qed.

End Length_2.

Ltac lg_instance1 l A B :=
  assert(tempo_sg:= ex_point_lg l);
  match goal with
    |H: Q_Cong l |- _assert(tempo_H:=H); apply (tempo_sg A) in tempo_H; ex_elim tempo_H B; B
  end;
  clear tempo_sg.

Tactic Notation "soit" ident(A) ident(B) "de" "longueur" ident(l) := lg_instance1 l A B.

Ltac lg_instance2 l A P B :=
  assert(tempo_sg:= ex_point_lg_out l);
  match goal with
    |H: A P |- _
                        match goal with
                           |HP : Q_Cong l |- _
                                               match goal with
                                                 |HQ : ¬ Q_Cong_Null l |- _assert(tempo_HQ:=HQ);
                                                                           apply (tempo_sg A P H HP) in tempo_HQ;
                                                                           ex_and tempo_HQ B
                                               end
                        end
  end;
  clear tempo_sg.

Tactic Notation "soit" ident(B) "sur" "la" "demie" "droite" ident(A) ident(P) "/" "longueur" ident(A) ident(B) "=" ident(l) := lg_instance2 l A P B.

Section Length_3.

Context `{T2D:Tarski_2D}.

Lemma ex_points_lg_not_col : l P, Q_Cong l ¬ Q_Cong_Null l A, B, l A B ¬Col A B P.
Proof.
    intros.
    assert(HH:=another_point P).
    ex_elim HH A.
    assert(HH:= not_col_exists P A H1).
    ex_elim HH Q.
     A.
    assert(A Q).
      intro.
      subst Q.
      apply H2.
      Col.
    lg_instance2 l A Q B.
     B.
    split.
      auto.
    intro.
    apply H2.
    assert(A B).
      intro.
      subst B.
      unfold Out in H5.
      tauto; apply out_col in H5.
    apply out_col in H5.
    ColR.
Qed.

End Length_3.

Ltac lg_instance_not_col l P A B :=
  assert(tempo_sg:= ex_points_lg_not_col l P);
  match goal with
        |HP : Q_Cong l |- _match goal with
                                  |HQ : ¬ Q_Cong_Null l |- _assert(tempo_HQ:=HQ);
                                                            apply (tempo_sg HP) in tempo_HQ;
                                                            elim tempo_HQ;
                                                            intro A;
                                                            let tempo_HR := fresh "tempo_HR" in
                                                            intro tempo_HR;
                                                            elim tempo_HR;
                                                            intro B;
                                                            intro;
                                                            spliter;
                                                            clear tempo_HR tempo_HQ
                            end
  end;
  clear tempo_sg.

Tactic Notation "soit" ident(B) "sur" "la" "demie" "droite" ident(A) ident(P) "/" "longueur" ident(A) ident(B) "=" ident(l) := lg_instance2 l A P B.

Section Length_4.

Context `{T2D:Tarski_2D}.

Notation "l1 =l= l2" := (EqL l1 l2) (at level 80, right associativity).

Lemma ex_eql : l1 l2, ( A , B, Len A B l1 Len A B l2) l1 =l= l2.
Proof.
    intros.
    ex_and H A.
    ex_and H0 B.
    assert(HH:=H).
    assert(HH0:=H0).
    unfold Len in HH.
    unfold Len in HH0.
    spliter.
    unfold EqL.
    repeat split; auto.
      intro.
      assert(Len A0 B0 l1).
        unfold Len.
        split; auto.
      assert(Cong A B A0 B0).
        apply (is_len_cong _ _ _ _ l1); auto.
      assert(Len A0 B0 l2).
        apply(is_len_cong_is_len A B).
          apply H0.
        auto.
      unfold Len in H8.
      spliter.
      auto.
    intro.
    assert(Len A0 B0 l2).
      unfold Len.
      split; auto.
    assert(Cong A B A0 B0).
      apply (is_len_cong _ _ _ _ l2); auto.
    assert(Len A0 B0 l1).
      apply(is_len_cong_is_len A B).
        apply H.
      auto.
    unfold Len in H8.
    spliter.
    auto.
Qed.

Lemma all_eql : A B l1 l2, Len A B l1 Len A B l2 EqL l1 l2.
Proof.
    intros.
    apply ex_eql.
     A.
     B.
    split; auto.
Qed.

Lemma null_len : A B la lb, Len A A la Len B B lb EqL la lb.
Proof.
    intros.
    eapply (all_eql A A).
      apply H.
    eapply (is_len_cong_is_len B B); Cong.
Qed.

Require Export Setoid.

Global Instance eqL_equivalence : Equivalence EqL.
Proof.
split.
- unfold Reflexive.
  intros.
  unfold EqL.
  intros.
  tauto.
- unfold Symmetric.
  intros.
  unfold EqL in ×.
  firstorder.
- unfold Transitive.
  unfold EqL.
  intros.
  rewrite H.
  apply H0.
Qed.

Lemma ex_lg : A B, l, Q_Cong l l A B.
Proof.
    intros.
     (fun C DCong A B C D).
    unfold Q_Cong.
    split.
       A. B.
      tauto.
    Cong.
Qed.

Lemma lg_eql_lg : l1 l2, Q_Cong l1 EqL l1 l2 Q_Cong l2.
Proof.
    intros.
    unfold EqL in ×.
    unfold Q_Cong in ×.
    decompose [ex] H.
     x. x0.
    intros.
    rewrite H2.
    apply H0.
Qed.

Lemma ex_eqL : l1 l2, Q_Cong l1 Q_Cong l2 ( A, B, l1 A B l2 A B) EqL l1 l2.
Proof.
intros.
ex_and H1 A.
ex_and H2 B.
unfold EqL.
assert(HH1:= H).
assert(HH2:= H0).

unfold Q_Cong in HH1.
unfold Q_Cong in HH2.
ex_and HH1 A1.
ex_and H3 B1.
ex_and HH2 A2.
ex_and H3 B2.

repeat split; auto.
intro.
assert(HH:= H4 A0 B0).
assert(HP:= H5 A0 B0).
destruct HP.
apply H6.
assert(HP:= H4 A B).
assert(HQ:= H5 A B).
destruct HP.
destruct HQ.
apply H9 in H1.
apply H11 in H2.
destruct HH.
apply H13 in H3.
apply cong_transitivity with A B; trivial.
apply cong_transitivity with A1 B1; Cong.

intro.
assert(HH:= H4 A0 B0).
assert(HP:= H5 A0 B0).
destruct HH.
apply H6.
assert(HH:= H4 A B).
assert(HQ:= H5 A B).
destruct HH.
destruct HQ.
apply H9 in H1.
apply H11 in H2.
destruct HP.
apply H13 in H3.
apply cong_transitivity with A2 B2; trivial.
apply cong_transitivity with A B; Cong.
Qed.

End Length_4.