Library GeoCoq.Highschool.orthocenter

Require Import GeoCoq.Highschool.circumcenter.

Section Orthocenter.

Context `{TE:Tarski_2D_euclidean}.

Definition is_orthocenter H A B C :=
 ¬ Col A B C ∧ Perp A H B C ∧ Perp B H A C ∧ Perp C H A B.

Lemma construct_intersection : ∀ A B C X1 X2 X3,
 ¬ Col A B C →
 Par A C B X1 → Par A B C X2 → Par B C A X3 →
 ∃ E, Col E A X3 ∧ Col E B X1.
Proof with finish.
intros A B C X1 X2 X3 HNC HPar1 HPar2 HPar3.
apply not_par_inter_exists.
intro HNPar; apply HNC.
assert (HFalsePar : Par B C A C)
  by (apply (par_trans B C B X1 A C); finish; apply (par_trans B C A X3 B); finish).
apply par_id_2...
Qed.

Lemma not_col_par_col2_diff : ∀ A B C D E F,
  ¬ Col A B C → Par A B C D → Col C D E → Col A E F → A ≠ E.
Proof.
intros A B C D E F HNC HPar HC1 HC2.
intro; subst.
apply HNC; apply not_strict_par1 with D E; finish.
Qed.

Lemma construct_triangle : ∀ A B C,
  ¬ Col A B C → ∃ D, ∃ E, ∃ F,
  Col B D F ∧ Col A E F ∧ Col C D E ∧
  Par A B C D ∧ Par A C B D ∧ Par B C A E ∧
  Par A B C E ∧ Par A C B F ∧ Par B C A F ∧
  D ≠ E ∧ D ≠ F ∧ E ≠ F.
Proof.
intros A B C HNC.
assert_diffs; rename H2 into HAB; rename H1 into HBC; rename H4 into HAC.

elim (parallel_existence1 A B C HAB);intros X1 HX1.
elim (parallel_existence1 A C B HAC);intros X2 HX2.
elim (parallel_existence1 B C A HBC);intros X3 HX3.

assert (T : ∃ D, Col D B X2 ∧ Col D C X1) by (apply construct_intersection with A X3; finish); DecompExAnd T D.
assert (T : ∃ E, Col E A X3 ∧ Col E C X1) by (apply construct_intersection with B X2; finish); DecompExAnd T E.
assert (T : ∃ F, Col F A X3 ∧ Col F B X2) by (apply construct_intersection with C X1; finish); DecompExAnd T F.

assert (A ≠ E) by (apply not_col_par_col2_diff with B C X1 X3; finish).
assert (A ≠ F) by (apply not_col_par_col2_diff with C B X2 X3; finish).
assert (B ≠ D) by (apply not_col_par_col2_diff with A C X1 X2; finish).
assert (B ≠ F) by (apply not_col_par_col2_diff with C A X3 X2; finish).
assert (C ≠ D) by (apply not_col_par_col2_diff with A B X2 X1; finish).
assert (C ≠ E) by (apply not_col_par_col2_diff with B A X3 X1; finish).

assert (Par A B C D) by (apply par_col_par with X1; finish).
assert (Par A C B D) by (apply par_col_par with X2; finish).
assert (Par B C A E) by (apply par_col_par with X3; finish).
assert (Par A B C E) by (apply par_col_par with X1; finish).
assert (Par A C B F) by (apply par_col_par with X2; finish).
assert (Par B C A F) by (apply par_col_par with X3; finish).

assert (¬ (D = E ∧ D = F)).

  intro; spliter; treat_equalities.
  assert_paras_perm.
  assert_nparas_perm.
  permutation_intro_in_hyps.
  contradiction.

∃ D; ∃ E; ∃ F.
assert_diffs.
repeat split; finish; try ColR.

intro; subst.
assert (E ≠ F) by (intro; subst; intuition).
apply HNC; apply col_permutation_1; apply not_strict_par1 with E A; sfinish.

intro; subst.
assert (E ≠ F) by (intro; subst; intuition).
apply HNC; apply col_permutation_2; apply not_strict_par1 with E C; sfinish.

intro; subst.
assert (D ≠ F) by (intro; subst; intuition).
apply HNC; apply not_strict_par1 with D B; sfinish.
Qed.

Lemma diff_not_col_col_par4_mid: ∀ A B C D E,
  D ≠ E → ¬ Col A B C → Col C D E → Par A B C D →
  Par A B C E → Par A E B C → Par A C B D → Midpoint C D E.
Proof.
intros A B C D E HD HNC HC HPar1 HPar2 HPar3 HPar4.
assert (HPara1 : Parallelogram_strict A B C E) by (apply parallel_2_plg; finish).
assert (HPara2 : Parallelogram_strict C A B D) by (apply parallel_2_plg; finish).
assert_congs_perm.
apply cong_col_mid; Col; eCong.
Qed.

Lemma altitude_is_perp_bisect : ∀ A B C O A1 E F,
  A ≠ O → E ≠ F → Perp A A1 B C → Col O A1 A → Col A E F → Par B C A E → Midpoint A E F →
  Perp_bisect A O E F.
Proof with finish.
intros.
apply perp_mid_perp_bisect...
apply perp_sym.
apply par_perp_perp with B C.
apply par_col_par with A...
apply perp_col1 with A1...
Qed.

Lemma altitude_intersect:
 ∀ A A1 B B1 C C1 O: Tpoint,
 ¬ Col A B C →
 Perp A A1 B C → Perp B B1 A C → Perp C C1 A B →
 Col O A A1 → Col O B B1 →
 Col O C C1.
Proof with finish.
intros A A1 B B1 C C1 O HNC HPerp1 HPerp2 HPerp3 HC1 HC2.
assert (HT := HNC).
apply construct_triangle in HT.
destruct HT as [D [E [F HT]]].
spliter.

assert (Midpoint A E F) by (apply diff_not_col_col_par4_mid with B C; finish).
assert (Midpoint B D F) by (apply diff_not_col_col_par4_mid with A C; finish).
assert (Midpoint C D E) by (apply diff_not_col_col_par4_mid with A B; finish).

assert_diffs.
elim (eq_dec_points A O); intro.

  treat_equalities; apply col_permutation_4; apply perp_perp_col with A B...
  apply perp_right_comm; apply perp_col1 with B1...

elim (eq_dec_points B O); intro.

  treat_equalities; apply col_permutation_4; apply perp_perp_col with A B...
  apply perp_col1 with A1...

elim (eq_dec_points C O); intro.

  subst; Col.

assert (Perp_bisect A O E F) by (apply altitude_is_perp_bisect with B C A1; finish).
assert (Perp_bisect B O D F) by (apply altitude_is_perp_bisect with A C B1; finish).

assert (Perp O C D E).

  apply circumcenter_intersect with F A B; finish.
  apply perp_bisect_sym_1; assumption.
  apply perp_bisect_sym_1; assumption.

assert (Perp C1 C D E).

  apply perp_sym; apply par_perp_perp with A B...
  apply par_symmetry; apply par_col_par_2 with C...

apply col_permutation_2; apply perp_perp_col with D E...
Qed.

Lemma is_orthocenter_cases :
  ∀ A B C G,
  is_orthocenter G A B C ∨
  is_orthocenter G A C B ∨
  is_orthocenter G B A C ∨
  is_orthocenter G B C A ∨
  is_orthocenter G C A B ∨
  is_orthocenter G C B A →
  is_orthocenter G A B C.
Proof.
intros.
decompose [or] H;clear H;
unfold is_orthocenter in *;spliter;
repeat (split; finish).
Qed.

Lemma is_orthocenter_perm : ∀ A B C G,
 is_orthocenter G A B C →
 is_orthocenter G A B C ∧ is_orthocenter G A C B ∧
 is_orthocenter G B A C ∧ is_orthocenter G B C A ∧
 is_orthocenter G C A B ∧ is_orthocenter G C B A.
Proof.
intros.
unfold is_orthocenter in ×.
spliter.
repeat split;finish.
Qed.

Lemma is_orthocenter_perm_1 : ∀ A B C G,
 is_orthocenter G A B C → is_orthocenter G A C B.
Proof.
intros.
apply is_orthocenter_perm in H;intuition.
Qed.

Lemma is_orthocenter_perm_2 : ∀ A B C G,
 is_orthocenter G A B C → is_orthocenter G B A C.
Proof.
intros.
apply is_orthocenter_perm in H;intuition.
Qed.

Lemma is_orthocenter_perm_3 : ∀ A B C G,
 is_orthocenter G A B C → is_orthocenter G B C A.
Proof.
intros.
apply is_orthocenter_perm in H;intuition.
Qed.

Lemma is_orthocenter_perm_4 : ∀ A B C G,
 is_orthocenter G A B C → is_orthocenter G C A B.
Proof.
intros.
apply is_orthocenter_perm in H;intuition.
Qed.

Lemma is_orthocenter_perm_5 : ∀ A B C G,
 is_orthocenter G A B C → is_orthocenter G C B A.
Proof.
intros.
apply is_orthocenter_perm in H;intuition.
Qed.

Lemma orthocenter_per :
 ∀ A B C H,
 Per A B C →
 is_orthocenter H A B C →
 H=B.
Proof.
intros.
unfold is_orthocenter in *;spliter.
assert_diffs.
assert (Perp A B B C) by (apply per_perp;finish).
assert (Par A H A B)
 by (apply l12_9 with B C;auto).
assert (Col A B H)
 by (perm_apply (par_id A B H)).

assert (Par C H B C)
 by (apply l12_9 with A B;finish).
assert (Col B C H)
 by (perm_apply (par_id C B H)).
apply l6_21 with A B C B;finish.
Qed.

Lemma orthocenter_col :
 ∀ A B C H,
 Col H B C →
 is_orthocenter H A B C →
 H = B ∨ H = C.
Proof.
intros.
unfold is_orthocenter in ×.
spliter.
assert (Perp_at H B C A H).
apply l8_14_2_1b_bis;finish.
induction (eq_dec_points B H).
subst;auto.
assert (Perp A H B H)
 by (apply (perp_col1 A H B C H);finish).
assert (Par A H A C)
  by (apply l12_9 with B H;finish).
assert (Col H A C)
  by (perm_apply (par_id A C H)).
assert (H=C).
assert_diffs.
apply l6_21 with B C A C;finish.
subst.
auto.
Qed.

End Orthocenter.