Library perp_bisect
Require Export Ch12_parallel.
Section PerpBisect_1.
Context `{MT:Tarski_2D}.
Context `{EqDec:EqDecidability Tpoint}.
Section PerpBisect_1.
Context `{MT:Tarski_2D}.
Context `{EqDec:EqDecidability Tpoint}.
PQ is the perpendicular bisector of segment AB
Definition perp_bisect P Q A B :=
∃ I, Perp_in I P Q A B ∧ is_midpoint I A B.
Lemma perp_bisect_sym_1 :
∀ P Q A B,
perp_bisect P Q A B →
perp_bisect Q P A B.
Proof.
intros.
unfold perp_bisect in ×.
elim H;intros.
∃ x.
intuition; Perp.
Qed.
Lemma perp_bisect_sym_2 :
∀ P Q A B,
perp_bisect P Q A B →
perp_bisect P Q B A.
Proof.
intros.
unfold perp_bisect in ×.
elim H;intros.
∃ x.
intuition; Perp.
Qed.
Lemma perp_bisect_sym_3 : ∀ A B C D,
perp_bisect A B C D →
perp_bisect B A D C.
Proof.
intros.
apply perp_bisect_sym_1.
apply perp_bisect_sym_2.
trivial.
Qed.
Lemma perp_in_per_1 :
∀ A B C D X,
Perp_in X A B C D →
Per A X C.
Proof.
intros.
unfold Perp_in in ×.
decompose [and] H.
apply H5;
Col.
Qed.
Lemma perp_in_per_2 :
∀ A B C D X,
Perp_in X A B C D →
Per A X D.
Proof.
intros.
unfold Perp_in in ×.
decompose [and] H.
apply H5;
Col.
Qed.
Lemma perp_in_per_3 :
∀ A B C D X,
Perp_in X A B C D →
Per B X C.
Proof.
intros.
unfold Perp_in in ×.
decompose [and] H.
apply H5;
Col.
Qed.
Lemma perp_in_per_4 :
∀ A B C D X,
Perp_in X A B C D →
Per B X D.
Proof.
intros.
unfold Perp_in in ×.
decompose [and] H.
apply H5;
Col.
Qed.
Lemma perp_bisect_perp :
∀ P Q A B,
perp_bisect P Q A B →
Perp P Q A B.
Proof.
intros.
unfold perp_bisect in ×.
decompose [and ex] H;clear H.
unfold Perp.
∃ x.
assumption.
Qed.
End PerpBisect_1.
Hint Resolve perp_in_per_1 perp_in_per_2 perp_in_per_3 perp_in_per_4 : perp.
Hint Resolve perp_bisect_perp : perp_bisect.
Section PerpBisect_2.
Context `{MT:Tarski_2D}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma perp_bisect_cong_1 :
∀ P Q A B,
perp_bisect P Q A B →
Cong A P B P.
Proof.
intros.
unfold perp_bisect in H.
elim H;intros I;intros;clear H.
decompose [and] H0;clear H0.
assert (Cong P A P B).
apply (per_double_cong P I A B);
eauto with perp.
Cong.
Qed.
Lemma perp_bisect_cong_2 :
∀ P Q A B,
perp_bisect P Q A B →
Cong A Q B Q.
Proof.
intros.
unfold perp_bisect in H.
elim H;intros I;intros;clear H.
decompose [and] H0;clear H0.
assert (Cong Q A Q B).
apply (per_double_cong Q I A B);
eauto with perp.
Cong.
Qed.
End PerpBisect_2.
Hint Resolve perp_bisect_cong_1 perp_bisect_cong_2 : perp_bisect.
Section PerpBisect_3.
Context `{MT:Tarski_2D}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma perp_bisect_cong :
∀ P Q A B,
perp_bisect P Q A B →
Cong A P B P ∧ Cong A Q B Q.
Proof.
intros.
split.
eauto using perp_bisect_cong_1.
eauto using perp_bisect_cong_2.
Qed.
Lemma perp_bisect_conc :
∀ A A1 B B1 C C1 O: Tpoint,
¬ Col A B C →
perp_bisect O A1 B C → perp_bisect O B1 A C → perp_bisect O C1 A B →
Cong A O B O → Cong B O C O →
Cong A O C O.
Proof.
intros.
apply (cong_transitivity A O B O C O); assumption.
Qed.
Lemma cong_perp_bisect :
∀ P Q A B,
P ≠ Q → A ≠ B →
Cong A P B P →
Cong A Q B Q →
perp_bisect P Q A B.
Proof.
intros.
unfold perp_bisect.
elim (midpoint_existence A B).
intros I HI.
∃ I.
split;try assumption.
assert (Per P I A)
by (unfold Per;∃ B;Cong).
show_distinct A I.
unfold is_midpoint in ×.
spliter.
treat_equalities.
intuition.
show_distinct B I.
unfold is_midpoint in ×.
spliter.
treat_equalities.
intuition.
induction(eq_dec_points P I).
subst.
eapply l8_13_2;Col.
apply midpoint_col;auto.
∃ Q. ∃ B;repeat split;Col.
unfold Per.
∃ A.
split.
Midpoint.
Cong.
eapply l8_13_2.
assumption.
assumption.
apply upper_dim with A B;Cong.
unfold is_midpoint in ×.
spliter;Cong.
apply midpoint_col;auto.
∃ P.
∃ A.
repeat split;Col.
Qed.
Definition is_on_perp_bisect P A B := Cong A P P B.
Lemma perp_bisect_is_on_perp_bisect :
∀ A B C P,
is_on_perp_bisect P A B →
is_on_perp_bisect P B C →
is_on_perp_bisect P A C.
Proof.
intros.
unfold is_on_perp_bisect in ×.
eCong.
Qed.
Lemma perp_mid_perp_bisect : ∀ A B C D,
is_midpoint C A B → Perp C D A B →
perp_bisect C D A B.
Proof with finish.
intros.
∃ C...
split...
assert_cols; apply l8_14_2_1b_bis...
Qed.
End PerpBisect_3.
Section Euclid.
Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma triangle_circumscription_implies_inter_dec :
(∀ A B C, ¬ Col A B C → ∃ CC, Cong A CC B CC ∧ Cong A CC C CC) →
∀ A B C D, (∃ I, Col I A B ∧ Col I C D) ∨ ¬ (∃ I, Col I A B ∧ Col I C D).
Proof.
intros HTC A B C D.
elim (eq_dec_points A B); intro HAB; elim (eq_dec_points C D); intro HCD.
- left; ∃ A; subst; split; finish.
- left; ∃ C; subst; split; finish.
- left; ∃ A; subst; split; finish.
- assert (HAC := midpoint_existence A C).
destruct HAC as [M Hmid].
elim (eq_dec_points A C); intro HAC.
× treat_equalities.
left; ∃ M; split; finish.
× elim (Col_dec M A B); intro HCol1;
elim (Col_dec M C D); intro HCol2.
+ assert_diffs; assert_cols.
left; ∃ M; split; finish.
+ assert_diffs; assert_cols.
left; ∃ C; split; finish; ColR.
+ assert_diffs; assert_cols.
left; ∃ A; split; finish; ColR.
+ elim (l10_2_existence_spec A B M); intros M1 HM1;
elim (l10_2_existence_spec C D M); intros M2 HM2.
elim (Col_dec M1 M M2); intro HCol3.
{
destruct HM1 as [[M3 [Hmid1 HCol4]] HElim1].
destruct HM2 as [[M4 [Hmid2 HCol5]] HElim2].
elim (eq_dec_points M M1); intro HMM1;
elim (eq_dec_points M M2); intro HMM2.
- treat_equalities.
assert_diffs; assert_cols.
left; ∃ A; split; finish; ColR.
- treat_equalities.
assert_diffs; assert_cols.
left; ∃ C; split; finish; ColR.
- treat_equalities.
assert_diffs; assert_cols.
left; ∃ A; split; finish; ColR.
- right.
elim HElim1; clear HElim1; intro HElim1;
elim HElim2; clear HElim2; intro HElim2.
× assert (HPerp : Perp A B M M2) by (apply perp_col1 with M1; finish).
assert (HPar : Par A B C D) by (apply l12_9 with M M2; unfold coplanar; finish; trivial).
elim HPar; clear HPar; intro HPar.
+ unfold Par_strict in HPar; intuition.
+ destruct HPar as [Hclear1 [Hclear2 [HCol6 HCol7]]]; clear Hclear1; clear Hclear2.
assert_diffs; assert_cols.
exfalso; apply HCol1; ColR.
× intuition.
× intuition.
× intuition.
}
{
left.
assert (H := HTC M1 M M2 HCol3).
destruct H as [I [HI1 HI2]].
assert (HPerp1 := HM1).
assert (HPerp2 := HM2).
destruct HPerp1 as [Hclear HPerp1]; clear Hclear.
destruct HPerp2 as [Hclear HPerp2]; clear Hclear.
assert (HCong1 : Cong M1 A M A) by (apply is_image_spec_col_cong with A B; finish).
assert (HCong2 : Cong M2 C M C) by (apply is_image_spec_col_cong with C D; finish).
elim HPerp1; clear HPerp1; intro HPerp1;
elim HPerp2; clear HPerp2; intro HPerp2.
- elim (eq_dec_points A I); intro HAI;
elim (eq_dec_points C I); intro HCI.
× subst; ∃ I; split; finish.
× subst.
assert (HPer3 : Perp I C M M2)
by (apply perp_bisect_perp; apply cong_perp_bisect; assert_diffs; finish; eCong).
∃ I.
split; finish.
apply col_permutation_2.
apply perp_perp_col with M M2; finish.
× subst.
assert (HPer3 : Perp I A M M1)
by (apply perp_bisect_perp; apply cong_perp_bisect; assert_diffs; finish; eCong).
∃ I.
split; finish.
apply col_permutation_2.
apply perp_perp_col with M M1; finish.
× assert (HPer3 : Perp I A M M1)
by (apply perp_bisect_perp; apply cong_perp_bisect; assert_diffs; finish; eCong).
assert (HPer4 : Perp I C M M2)
by (apply perp_bisect_perp; apply cong_perp_bisect; assert_diffs; finish; eCong).
∃ I.
split.
apply col_permutation_2.
apply perp_perp_col with M M1; finish.
apply col_permutation_2.
apply perp_perp_col with M M2; finish.
- assert_diffs; subst; intuition.
- assert_diffs; subst; intuition.
- assert_diffs; subst; intuition.
}
Qed.
End Euclid.