Require Export GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec.

Ltac assert_all := treat_equalities; assert_cols_perm; assert_diffs; assert_congs_perm.

Section TriangleMidpointsTheorems.

Context `{TE:Tarski_euclidean}.

Lemma col_permut132 : forall A B C, Col A B C -> Col A C B.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Col Tn A B C), @Col Tn A C B *)
Proof. exact col_permutation_5. Qed.

Lemma col_permut213 : forall A B C, Col A B C -> Col B A C.
Proof. exact col_permutation_4. Qed.

Lemma col_permut231 : forall A B C, Col A B C -> Col B C A.
Proof. exact col_permutation_1. Qed.

Lemma col_permut312 : forall A B C, Col A B C -> Col C A B.
Proof. exact col_permutation_2. Qed.

Lemma col_permut321 : forall A B C, Col A B C -> Col C B A.
Proof. exact col_permutation_3. Qed.

Lemma col123_124__col134 : forall P Q A B,
  P <> Q -> Col P Q A -> Col P Q B -> Col P A B.
Proof. exact col_transitivity_1. Qed.

Lemma col123_124__col234 : forall P Q A B,
  P <> Q -> Col P Q A -> Col P Q B -> Col Q A B.
Proof. exact col_transitivity_2. Qed.

Lemma triangle_mid_par_strict : forall A B C P Q,
 ~Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Par_strict A B Q P.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
(* Goal: @Par_strict Tn A B Q P *)
Name x the symmetric of P wrt Q.
(* Goal: @Par_strict Tn A B Q P *)
assert_all.
(* Goal: @Par_strict Tn A B Q P *)
assert (~ Col A P C) by (intro; search_contradiction).
(* Goal: @Par_strict Tn A B Q P *)
assert_diffs.
(* Goal: @Par_strict Tn A B Q P *)
assert (Parallelogram_strict A P C x) by (apply mid_plgs with Q;finish).
(* Goal: @Par_strict Tn A B Q P *)
assert (Cong A x B P) by (assert_paras_perm; assert_pars_perm; assert_all; eCong).
(* Goal: @Par_strict Tn A B Q P *)
assert (Par A x B P) by (assert_paras_perm; assert_pars_perm; apply par_col2_par with P C; finish).
(* Goal: @Par_strict Tn A B Q P *)
assert (HElim : Parallelogram A x B P \/ Parallelogram A x P B) by (apply par_cong_plg_2; assumption).

(* Goal: @Par_strict Tn A B Q P *)
induction HElim.

(* Goal: @Par_strict Tn A B Q P *)
(* Goal: @Par_strict Tn A B Q P *)
 assert_paras_perm; assert_pars_perm.
(* Goal: @Par_strict Tn A B Q P *)
(* Goal: @Par_strict Tn A B Q P *)
 Name M the intersection of the diagonals (A B) and (x P) of the parallelogram H15.
(* Goal: @Par_strict Tn A B Q P *)
(* Goal: @Par_strict Tn A B Q P *)
 treat_equalities.
(* Goal: @Par_strict Tn A P M P *)
(* Goal: @Par_strict Tn A B Q P *)
 search_contradiction.

apply par_strict_col2_par_strict with x P;
try solve[assert_paras_perm; assert_pars_perm; assert_all; Col].
(*
apply ncol134_plg__pars1423; auto; intro; apply H; assert_diffs; ColR.
*)
(* Goal: @Par_strict Tn A B x P *)
apply ncol123_plg__pars1423; auto; intro; apply H.
(* Goal: @Col Tn A B C *)
assert (P <> x) by (intro; treat_equalities; Col).
apply col_permut231; apply col123_124__col234 with P;
[| |apply col_permut231]; auto.
(* Goal: @Col Tn P C A *)
apply col_permut231; apply col123_124__col134 with Q; auto.
apply col_permut231; apply col123_124__col134 with x;
[|apply col_permut321|apply col_permut132]; auto.
Qed.

Lemma triangle_mid_par_strict_cong_aux : forall A B C P Q R,
 ~Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par_strict A B Q P  /\ Cong A R P Q /\ Cong B R P Q .
Proof with finish.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
(* Goal: @Par_strict Tn A B Q P *)
Name x the symmetric of P wrt Q.
(* Goal: @Par_strict Tn A B Q P *)
assert_all.
(* Goal: @Par_strict Tn A B Q P *)
assert (~ Col A P C) by (intro; search_contradiction).
(* Goal: @Par_strict Tn A B Q P *)
assert_diffs.
(* Goal: @Par_strict Tn A B Q P *)
assert (Parallelogram_strict A P C x) by (apply mid_plgs with Q;finish).
(* Goal: @Par_strict Tn A B Q P *)
assert_all.
assert_paras_perm.
assert_pars_perm.
assert (Cong A x B P) by eCong.
assert (Par A x B P) by (apply par_col2_par with P C; finish).
(* Goal: @Par_strict Tn A B Q P *)
assert (HElim : Parallelogram A x B P \/ Parallelogram A x P B) by (apply par_cong_plg_2; assumption).

(* Goal: @Par_strict Tn A B Q P *)
induction HElim.

 Name M the intersection of the diagonals (A B) and (x P) of the parallelogram H23.
(* Goal: @Par_strict Tn A B Q P *)
(* Goal: @Par_strict Tn A B Q P *)
 treat_equalities.
(* Goal: @Par_strict Tn A P M P *)
(* Goal: @Par_strict Tn A B Q P *)
 search_contradiction.

assert_paras_perm.
assert_pars_perm.
assert (Par P Q A B) by (assert_diffs; apply par_col_par_2 with x; finish).
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
split.

apply par_not_col_strict with x...
 intro.
 assert_cols_perm.
 apply H.
 ColR.

assert_congs_perm;split;eCong.
Qed.

Lemma triangle_par_mid : forall A B C P Q,
 ~ Col A B C ->
 Midpoint P B C ->
 Par A B Q P ->
 Col Q A C ->
 Midpoint Q A C.
Proof.
assert (H:=playfair_s_postulate_implies_midpoint_converse_postulate);
unfold midpoint_converse_postulate in H; intros; apply H with B P; Col.
(* Goal: @playfair_s_postulate Tn *)
unfold playfair_s_postulate.
(* Goal: forall (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : @Par Tn A1 A2 B1 B2) (_ : @Col Tn P B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
apply parallel_uniqueness.
Qed.

Lemma triangle_mid_par_strict_cong_1 : forall A B C P Q R,
 ~Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par_strict A B Q P  /\ Cong A R P Q.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
assert (Par_strict A B Q P /\ Cong A R P Q /\ Cong B R P Q)
  by (apply triangle_mid_par_strict_cong_aux with C; assumption).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.
(* Goal: and (@Par Tn A B Q P) (@Cong Tn B R P Q) *)
split; assumption.
Qed.

Lemma triangle_mid_par_strict_cong_2 : forall A B C P Q R,
 ~Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par_strict A B Q P  /\ Cong B R P Q.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
assert (Par_strict A B Q P /\ Cong A R P Q /\ Cong B R P Q)
  by (apply triangle_mid_par_strict_cong_aux with C; assumption).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.
(* Goal: and (@Par Tn A B Q P) (@Cong Tn B R P Q) *)
split; assumption.
Qed.

Lemma triangle_mid_par_strict_cong_simp :
 forall A B C P Q,
 ~ Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Par_strict A B Q P.
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : not (@Col Tn A B C)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C), @Par_strict Tn A B Q P *)
apply triangle_mid_par.
Qed.

Lemma triangle_mid_par_strict_cong : forall A B C P Q R,
 ~Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par_strict A B Q P /\ Par_strict A C P R /\ Par_strict B C Q R /\
 Cong A R P Q /\ Cong B R P Q /\ Cong A Q P R /\ Cong C Q P R /\ Cong B P Q R /\ Cong C P Q R.
Proof with finish.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
permutation_intro_in_hyps.
assert (Par_strict A B Q P /\ Cong A R P Q /\ Cong B R P Q)
  by (apply triangle_mid_par_strict_cong_aux with C; assumption).
assert (Par_strict A C R P /\ Cong A Q P R /\ Cong C Q P R)
  by (apply triangle_mid_par_strict_cong_aux with B; Col).
assert (Par_strict C B Q R /\ Cong C P R Q /\ Cong B P R Q)
  by (apply triangle_mid_par_strict_cong_aux with A; Col).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.

(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
split...
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
split...
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
split...
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
repeat split...
Qed.

Lemma triangle_mid_par_flat_cong_aux : forall A B C P Q R,
 B <> A ->
 Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par A B Q P /\ Cong A R P Q /\ Cong B R P Q.
Proof with finish.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.

elim (eq_dec_points A C); intro.

(* Goal: @Par_strict Tn A B Q P *)
  assert_all.
  split; try eCong.
  perm_apply (col_par)...

elim (eq_dec_points B C); intro.
(* Goal: @Par_strict Tn A B Q P *)
  assert_all.
  split; try eCong.
  perm_apply (col_par)...

elim (eq_dec_points A P); intro.
(* Goal: @Par_strict Tn A B Q P *)
  assert_all.
  assert (Col A B Q) by ColR.
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
  split.
  perm_apply (col_par).
  assert_congs_perm.
  split; eCong.

(* Goal: @Par_strict Tn A B Q P *)
Name x the symmetric of P wrt Q.

elim (eq_dec_points P x); intro.
  treat_equalities; intuition.

assert_cols.
assert (Parallelogram A P C x) by (apply mid_plg_1 with Q;finish).
(* Goal: @Par_strict Tn A B Q P *)
assert_all.
assert_pars_perm.
assert (Cong A x B P) by eCong.
assert (Par A x B P) by (apply par_col2_par with P C; finish).

(* Goal: @Par_strict Tn A B Q P *)
assert (HElim : Parallelogram A x B P \/ Parallelogram A x P B) by (apply par_cong_plg_2; assumption).

(* Goal: @Par_strict Tn A B Q P *)
induction HElim.

 Name M the intersection of the diagonals (A B) and (x P) of the parallelogram H19.
(* Goal: @Par_strict Tn A B Q P *)
(* Goal: @Par_strict Tn A B Q P *)
 treat_equalities.
(* Goal: @Par_strict Tn A P M P *)
(* Goal: @Par_strict Tn A B Q P *)
 search_contradiction.

 assert_paras_perm.
 assert_pars_perm.
 assert (Par P Q A B) by (apply par_col_par_2 with x; finish).
 assert_congs_perm.
 repeat split; try eCong...
Qed.

Lemma triangle_mid_par_flat_cong_1 : forall A B C P Q R,
 B <> A ->
 Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par A B Q P  /\ Cong A R P Q.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
assert (Par A B Q P /\ Cong A R P Q /\ Cong B R P Q)
  by (apply triangle_mid_par_flat_cong_aux with C; assumption).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.
(* Goal: and (@Par Tn A B Q P) (@Cong Tn B R P Q) *)
split; assumption.
Qed.

Lemma triangle_mid_par_flat_cong_2 : forall A B C P Q R,
 B <> A ->
 Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par A B Q P /\ Cong B R P Q.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
assert (Par A B Q P /\ Cong A R P Q /\ Cong B R P Q)
  by (apply triangle_mid_par_flat_cong_aux with C; assumption).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.
(* Goal: and (@Par Tn A B Q P) (@Cong Tn B R P Q) *)
split; assumption.
Qed.

Lemma triangle_mid_par_flat_cong : forall A B C P Q R,
 B <> A ->
 C <> A ->
 C <> B ->
 Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par A B Q P /\ Par A C P R /\ Par B C Q R /\
 Cong A R P Q /\ Cong B R P Q /\ Cong A Q P R /\ Cong C Q P R /\ Cong B P Q R /\ Cong C P Q R.
Proof with finish.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
permutation_intro_in_hyps.
(* Goal: and (@Par Tn A B Q P) (@Cong Tn B R P Q) *)
assert (Par A B Q P /\ Cong A R P Q /\ Cong B R P Q) by (apply triangle_mid_par_flat_cong_aux with C; assumption).
assert (Par A C R P /\ Cong A Q P R /\ Cong C Q P R) by (apply triangle_mid_par_flat_cong_aux with B; Col).
assert (Par C B Q R /\ Cong C P R Q /\ Cong B P R Q) by (apply triangle_mid_par_flat_cong_aux with A; Col).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
spliter.

(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
repeat split...
Qed.

Lemma triangle_mid_par_flat : forall A B C P Q,
 B <> A ->
 Col A B C ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Par A B Q P.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
elim (midpoint_existence A B); intro R; intro.
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
assert (HTMT := triangle_mid_par_flat_cong_aux A B C P Q R H H0 H1 H2 H3); spliter.
(* Goal: @Par Tn A B Q P *)
assumption.
Qed.

Lemma triangle_mid_par : forall A B C P Q,
 A <> B ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Par A B Q P.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.

elim (col_dec A B C); intro.
(* Goal: @Par Tn A B Q P *)
(* Goal: @Par Tn A B Q P *)
  apply triangle_mid_par_flat with C; finish.

(* Goal: @Par Tn A B Q P *)
  apply par_strict_par; apply triangle_mid_par_strict with C; assumption.
Qed.

Lemma triangle_mid_par_cong : forall A B C P Q R,
 B <> A ->
 C <> A ->
 C <> B ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par A B Q P /\ Par A C P R /\ Par B C Q R /\
 Cong A R P Q /\ Cong B R P Q /\ Cong A Q P R /\ Cong C Q P R /\ Cong B P Q R /\ Cong C P Q R.
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.

elim (col_dec A B C); intro.
(* Goal: @Par Tn A B Q P *)
  apply triangle_mid_par_flat_cong; assumption.

(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
  assert (HTMT := triangle_mid_par_strict_cong A B C P Q R H5 H2 H3 H4); spliter.
(* Goal: @Par Tn A B Q P *)
  repeat split; try apply par_strict_par; assumption.
Qed.


Lemma triangle_mid_par_cong_1 : forall A B C P Q R,
 C <> B ->
 Midpoint P B C ->
 Midpoint Q A C ->
 Midpoint R A B ->
 Par B C Q R /\ Cong B P Q R .
Proof.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) C B)) (_ : @Midpoint Tn P B C) (_ : @Midpoint Tn Q A C) (_ : @Midpoint Tn R A B), and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
intros.
(* Goal: and (@Par Tn B C Q R) (@Cong Tn B P Q R) *)
split.
(* Goal: @Par Tn B C Q R *)
(* Goal: @Cong Tn B P Q R *)
perm_apply (triangle_mid_par B C A Q R);finish.
(* Goal: @Cong Tn B P Q R *)
induction (col_dec A B C).
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
 assert (Par C B Q R /\ Cong B P R Q).
(* Goal: and (@Par Tn C B Q R) (@Cong Tn B P R Q) *)
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
  apply (triangle_mid_par_flat_cong_2 C B A R Q P);finish.
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
  spliter.
(* Goal: @Cong Tn B P Q R *)
  finish.
(* Goal: @Cong Tn B P Q R *)
(* Goal: @Cong Tn B P Q R *)
 assert (HTMT := triangle_mid_par_strict_cong A B C P Q R H3 H0 H1 H2); spliter.
(* Goal: @Cong Tn B P Q R *)
 finish.
Qed.

End TriangleMidpointsTheorems.