Library Ch08_orthogonality
Require Export Ch07_midpoint.
Require Export ColR.
Ltac not_exist_hyp_comm A B := not_exist_hyp (A≠B);not_exist_hyp (B≠A).
Ltac not_exist_hyp2 A B C D := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D].
Ltac not_exist_hyp3 A B C D E F := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D | not_exist_hyp_comm E F].
Ltac not_exist_hyp_perm_col A B C := not_exist_hyp (¬ Col A B C); not_exist_hyp (¬ Col A C B);
not_exist_hyp (¬ Col B A C); not_exist_hyp (¬ Col B C A);
not_exist_hyp (¬ Col C A B); not_exist_hyp (¬ Col C B A).
Ltac finish := match goal with
| |- Col ?A ?B ?C ⇒ Col
| |- ¬ Col ?A ?B ?C ⇒ Col
| |- Cong ?A ?B ?C ?D ⇒ Cong
| |- is_midpoint ?A ?B ?C ⇒ Midpoint
| |- ?A<>?B ⇒ apply swap_diff;assumption
| |- _ ⇒ try assumption
end.
Ltac assert_all_diffs_by_cases :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ not_exist_hyp_comm A B;induction (eq_dec_points A B);[treat_equalities;solve [finish] |idtac]
end.
Ltac assert_cols :=
repeat
match goal with
| H:Bet ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
| H:is_midpoint ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := midpoint_col X2 X1 X3 H)
| H:out ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := out_col X1 X2 X3 H)
end.
Ltac assert_bet :=
repeat
match goal with
| H:is_midpoint ?B ?A ?C |- _ ⇒ let T := fresh in not_exist_hyp (Bet A B C); assert (T := midpoint_bet A B C H)
end.
Ltac clean_reap_hyps :=
repeat
match goal with
| H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?C ?B |- _ ⇒ clear H2
| H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?B ?C |- _ ⇒ clear H2
| H:(¬Col ?A ?B ?C), H2 : ¬Col ?A ?B ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ ⇒ clear H2
| H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ ⇒ clear H2
| H:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ ⇒ clear H2
| H:(?A<>?B), H2 : (?B<>?A) |- _ ⇒ clear H2
| H:(?A<>?B), H2 : (?A<>?B) |- _ ⇒ clear H2
end.
Ltac assert_diffs :=
repeat
match goal with
| H:(¬Col ?X1 ?X2 ?X3) |- _ ⇒
let h := fresh in
not_exist_hyp3 X1 X2 X1 X3 X2 X3;
assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?A ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?B ≠ ?A |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?C ≠ ?D |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?D ≠ ?C |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?A<>?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?B<>?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?I<>?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?A<>?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?I<>?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?B<>?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:out ?A ?B ?C |- _ ⇒
let T:= fresh in (not_exist_hyp2 A B A C);
assert (T:= out_distinct A B C H);
decompose [and] T;clear T;clean_reap_hyps
end.
Ltac clean_trivial_hyps :=
repeat
match goal with
| H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ ⇒ clear H
| H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ ⇒ clear H
| H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ ⇒ clear H
| H:(Bet ?X1 ?X1 ?X2) |- _ ⇒ clear H
| H:(Bet ?X2 ?X1 ?X1) |- _ ⇒ clear H
| H:(Col ?X1 ?X1 ?X2) |- _ ⇒ clear H
| H:(Col ?X2 ?X1 ?X1) |- _ ⇒ clear H
| H:(Col ?X1 ?X2 ?X1) |- _ ⇒ clear H
| H:(is_midpoint ?X1 ?X1 ?X1) |- _ ⇒ clear H
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ ⇒
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ ⇒
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ ⇒
apply between_identity in H;smart_subst X2
| H:(is_midpoint ?X ?Y ?Y) |- _ ⇒ apply l7_3 in H; smart_subst Y
| H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := between_egality A B C H H2);smart_subst A
| H : is_midpoint ?P ?A ?P1, H2 : is_midpoint ?P ?A ?P2 |- _ ⇒
let T := fresh in not_exist_hyp (P1=P2); assert (T := symmetric_point_unicity A P P1 P2 H H2);smart_subst P1
| H : is_midpoint ?A ?P ?X, H2 : is_midpoint ?A ?Q ?X |- _ ⇒
let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9 P Q A X H H2);smart_subst P
| H : is_midpoint ?M ?A ?A |- _ ⇒
let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H);smart_subst M
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P ?P' |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2);smart_subst A
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P' ?P |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17_bis P P' A B H H2);smart_subst A
| H : is_midpoint ?A ?B ?A |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H);smart_subst A
| H : is_midpoint ?A ?A ?B |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H);smart_subst A
end.
Ltac ColR :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
treat_equalities; Col_refl tpoint col.
Ltac search_contradiction :=
match goal with
| H: ?A ≠ ?A |- _ ⇒ exfalso;apply H;reflexivity
| H: ¬ Col ?A ?B ?C |- _ ⇒ exfalso;apply H;ColR
end.
Ltac show_distinct' X Y :=
assert (X≠Y);
[intro;treat_equalities; (solve [search_contradiction])|idtac].
Ltac assert_all_diffs_by_contradiction :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ not_exist_hyp_comm A B;show_distinct' A B
end.
Ltac update_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
update_cols_gen tpoint col.
Ltac deduce_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
treat_equalities; deduce_cols_hide_gen tpoint col.
Ltac cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
cols_gen tpoint col.
Ltac tag_hyps :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
tag_hyps_gen tpoint col.
Ltac untag_hyps :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
untag_hyps_gen tpoint col.
Ltac clear_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
clear_cols_gen tpoint col.
Ltac smart_subst' := update_cols;clean.
Ltac treat_equalities_aux' :=
match goal with
| H:(?X1 = ?X2) |- _ ⇒ smart_subst'
end.
Ltac treat_equalities' :=
try treat_equalities_aux';
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ ⇒
apply cong_symmetry in H; apply cong_identity in H; smart_subst'
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ ⇒
apply cong_identity in H; smart_subst'
| H:(Bet ?X1 ?X2 ?X1) |- _ ⇒
apply between_identity in H; smart_subst'
| H:(is_midpoint ?X ?Y ?Y) |- _ ⇒ apply l7_3 in H; smart_subst'
| H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T : between_egality A B C H H2); smart_subst'
| H : is_midpoint ?P ?A ?P1, H2 : is_midpoint ?P ?A ?P2 |- _ ⇒
let T := fresh in not_exist_hyp (P1=P2); assert (T : symmetric_point_unicity A P P1 P2 H H2); smart_subst'
| H : is_midpoint ?A ?P ?X, H2 : is_midpoint ?A ?Q ?X |- _ ⇒
let T := fresh in not_exist_hyp (P=Q); assert (T : l7_9 P Q A X H H2); smart_subst'
| H : is_midpoint ?M ?A ?A |- _ ⇒
let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H); smart_subst'
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P ?P' |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2); smart_subst'
| H : is_midpoint ?A ?B ?A |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H); smart_subst'
| H : is_midpoint ?A ?A ?B |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H); smart_subst'
end.
Ltac search_contradiction' :=
match goal with
| H: ?A ≠ ?A |- _ ⇒ exfalso;apply H;reflexivity
| H: ¬ Col ?A ?B ?C |- _ ⇒ exfalso;apply H;cols
end.
Ltac show_distinct'' X Y :=
assert (X≠Y);
[intro; treat_equalities'; (solve [search_contradiction'])|idtac].
Ltac show_not_col X Y Z :=
assert (¬ Col X Y Z);
[intro; update_cols; (solve [search_contradiction'])|idtac].
Ltac assert_all_diffs_by_contradiction_aux :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ untag_hyps; not_exist_hyp_comm A B; tag_hyps; show_distinct'' A B
end.
Ltac assert_all_not_cols_by_contradiction_aux :=
repeat match goal with
| A: Tpoint, B: Tpoint, C: Tpoint |- _ ⇒ untag_hyps; not_exist_hyp_perm_col A B C; tag_hyps; show_not_col A B C
end.
Ltac assert_all_diffs_by_contradiction' :=
deduce_cols; assert_all_diffs_by_contradiction_aux; untag_hyps; clear_cols.
Ltac assert_all_not_cols_by_contradiction :=
deduce_cols; assert_all_not_cols_by_contradiction_aux; untag_hyps; clear_cols.
Ltac assert_ndc_by_contradiction :=
assert_all_diffs_by_contradiction'; assert_all_not_cols_by_contradiction.
Section T8_1.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Definition Per := fun A B C ⇒ ∃ C', is_midpoint B C C' ∧ Cong A C A C'.
Lemma Per_dec : ∀ A B C, Per A B C ∨ ¬ Per A B C.
Proof.
intros.
unfold Per.
elim (symmetric_point_construction C B);intros C' HC'.
elim (Cong_dec A C A C');intro.
left.
∃ C'.
intuition.
right.
intro.
decompose [ex and] H0;clear H0.
assert (C'=x)
by (apply symmetric_point_unicity with C B;assumption).
subst.
intuition.
Qed.
Lemma l8_2 : ∀ A B C, Per A B C → Per C B A.
Proof.
unfold Per.
intros.
ex_and H C'.
assert (∃ A', is_midpoint B A A').
apply symmetric_point_construction.
ex_and H1 A'.
∃ A'.
split.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply H0.
eapply l7_13.
apply H.
apply l7_2.
assumption.
Qed.
End T8_1.
Hint Resolve l8_2 : perp.
Ltac Perp := auto with perp.
Section T8_2.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma Per_cases :
∀ A B C,
Per A B C ∨ Per C B A →
Per A B C.
Proof.
intros.
decompose [or] H;Perp.
Qed.
Lemma Per_perm :
∀ A B C,
Per A B C →
Per A B C ∧ Per C B A.
Proof.
intros.
split; Perp.
Qed.
Lemma l8_3 : ∀ A B C A',
Per A B C → A≠B → Col B A A' → Per A' B C.
Proof.
unfold Per.
intros.
ex_and H C'.
∃ C'.
split.
assumption.
eapply l4_17 with A B;Cong;Col.
unfold is_midpoint in H.
spliter.
Cong.
Qed.
Lemma l8_4 : ∀ A B C C', Per A B C → is_midpoint B C C' → Per A B C'.
Proof.
unfold Per.
intros.
ex_and H B'.
∃ C.
split.
apply l7_2.
assumption.
assert (B' = C')
by (eapply symmetric_point_unicity;eauto).
subst B'.
Cong.
Qed.
Lemma l8_5 : ∀ A B, Per A B B.
Proof.
unfold Per.
intros.
∃ B.
split.
apply l7_3_2.
Cong.
Qed.
Lemma l8_6 : ∀ A B C A', Per A B C → Per A' B C → Bet A C A' → B=C.
Proof.
unfold Per.
intros.
ex_and H C'.
ex_and H0 C''.
assert (C'=C'')
by (eapply symmetric_point_unicity;eauto).
subst C''.
assert (C = C')
by (eapply l4_19;eauto).
subst C'.
apply l7_3.
assumption.
Qed.
End T8_2.
Hint Resolve l8_5 : perp.
Ltac let_symmetric C P A :=
let id1:=fresh in (assert (id1:(∃ A', is_midpoint P A A'));
[apply symmetric_point_construction|ex_and id1 C]).
Ltac symmetric B' A B :=
assert(sp:= symmetric_point_construction B A); ex_and sp B'.
Section T8_3.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma l8_7 : ∀ A B C, Per A B C → Per A C B → B=C.
Proof.
intros.
unfold Per in H.
ex_and H C'.
symmetric A' C A.
induction (eq_dec_points B C).
assumption.
assert (Per C' C A).
eapply l8_3.
eapply l8_2.
apply H0.
assumption.
unfold is_midpoint in H.
spliter.
unfold Col.
left.
assumption.
assert (Cong A C' A' C').
unfold Per in H4.
ex_and H4 Z.
assert (A' = Z)
by (eapply (symmetric_point_unicity A C A');auto).
subst Z.
Cong.
unfold is_midpoint in ×.
spliter.
assert (Cong A' C A' C').
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H6.
eapply cong_transitivity.
apply cong_commutativity.
apply H1.
apply cong_left_commutativity.
assumption.
assert (Per A' B C).
unfold Per.
∃ C'.
unfold is_midpoint.
repeat split;auto.
eapply l8_6.
apply H9.
unfold Per.
∃ C'.
split.
unfold is_midpoint;auto.
apply H1.
Between.
Qed.
Lemma l8_8 : ∀ A B, Per A B A → A=B.
Proof.
intros.
apply l8_7 with A.
apply l8_2.
apply l8_5.
assumption.
Qed.
Lemma l8_9 : ∀ A B C, Per A B C → Col A B C → A=B ∨ C=B.
Proof.
intros.
elim (eq_dec_points A B);intro.
tauto.
right.
eapply l8_7.
eapply l8_2.
eapply l8_5.
apply l8_3 with A; Col.
Qed.
Lemma l8_10 : ∀ A B C A' B' C', Per A B C → Cong_3 A B C A' B' C' → Per A' B' C'.
Proof.
unfold Per.
intros.
ex_and H D.
prolong C' B' D' B' C'.
∃ D'.
split.
unfold is_midpoint.
split.
assumption.
Cong.
unfold Cong_3, is_midpoint in ×.
spliter.
induction (eq_dec_points C B).
treat_equalities;Cong.
assert(OFSC C B D A C' B' D' A').
unfold OFSC.
repeat split.
assumption.
assumption.
Cong.
eapply cong_transitivity.
apply cong_symmetry.
apply H4.
eapply cong_transitivity.
apply cong_commutativity.
apply H6.
Cong.
Cong.
Cong.
assert (Cong D A D' A').
eapply five_segments_with_def.
apply H8.
assumption.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
eapply cong_transitivity.
apply H1.
Cong.
Qed.
Definition Perp_in := fun X A B C D ⇒
A≠B ∧ C≠D ∧ Col X A B ∧ Col X C D ∧ (∀ U V, Col U A B → Col V C D → Per U X V).
Lemma col_col_per_per : ∀ A X C U V,
A≠X → C≠X →
Col U A X →
Col V C X →
Per A X C →
Per U X V.
Proof.
intros.
assert (Per U X C)
by (apply (l8_3 A X C U);Col).
apply l8_2 in H4.
apply l8_2 .
apply (l8_3 C X U V);Col.
Qed.
Lemma Perp_in_dec : ∀ X A B C D, Perp_in X A B C D ∨ ¬ Perp_in X A B C D.
Proof.
intros.
unfold Perp_in.
elim (eq_dec_points A B);intro;
elim (eq_dec_points C D);intro;
elim (Col_dec X A B);intro;
elim (Col_dec X C D);intro; try
tauto.
elim (eq_dec_points B X);intro;
elim (eq_dec_points D X);intro;subst;treat_equalities.
elim (Per_dec A X C);intro.
left;repeat split;Col;intros; apply col_col_per_per with A C;Col.
right;intro;spliter;apply H3;apply H8;Col.
elim (Per_dec A X D);intro.
left;repeat split;Col;intros; apply col_col_per_per with A D;Col;ColR.
right;intro;spliter;apply H3;apply H9;Col.
elim (Per_dec B X C);intro.
left;repeat split;Col;intros; apply col_col_per_per with B C;Col;ColR.
right;intro;spliter;apply H4;apply H9;Col.
elim (Per_dec B X D);intro.
left;repeat split;Col;intros; apply col_col_per_per with B D;Col;ColR.
right;intro;spliter;apply H5;apply H10;Col.
Qed.
Definition Perp := fun A B C D ⇒ ∃ X, Perp_in X A B C D.
Lemma perp_distinct : ∀ A B C D, Perp A B C D → A ≠ B ∧ C ≠ D.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.
Lemma l8_12 : ∀ A B C D X, Perp_in X A B C D → Perp_in X C D A B.
Proof.
unfold Perp_in.
intros.
spliter.
repeat split;try assumption.
intros;eapply l8_2;eauto.
Qed.
Lemma l4_3_1 : ∀ A B C A' B' C',
Bet A B C → Bet A' B' C' → Cong A B A' B' → Cong A C A' C' → Cong B C B' C'.
Proof.
intros.
apply cong_commutativity.
eapply l4_3;eBetween;eCong.
Qed.
Lemma per_col : ∀ A B C D,
B ≠ C → Per A B C → Col B C D → Per A B D.
Proof.
unfold Per.
intros.
ex_and H0 C'.
prolong D B D' D B.
∃ D'.
assert (is_midpoint B C C').
apply H0.
induction H5.
assert (is_midpoint B D D') by
(unfold is_midpoint;split;Cong).
assert (is_midpoint B D D').
apply H7.
induction H8.
repeat split.
assumption.
Cong.
unfold Col in H1.
induction H1.
assert (Bet B C' D').
eapply l7_15.
eapply l7_3_2.
apply H0.
apply H7.
assumption.
assert (Cong C D C' D').
eapply l4_3_1.
apply H1.
apply H10.
Cong.
Cong.
assert(OFSC B C D A B C' D' A)
by (unfold OFSC;repeat split;Cong).
apply cong_commutativity.
eauto using five_segments_with_def.
induction H1.
assert (Bet C' D' B).
eapply l7_15.
apply H0.
apply H7.
apply l7_3_2.
assumption.
assert (Cong C D C' D')
by (eapply l4_3 with B B;Between;Cong).
assert(IFSC B D C A B D' C' A)
by (unfold IFSC;repeat split;Between;Cong).
apply cong_commutativity.
eauto using l4_2.
assert (Bet D' B C').
eapply l7_15.
apply H7.
eapply l7_3_2.
apply H0.
assumption.
assert (Cong C D C' D')
by (eapply l2_11 with B B;Between;Cong).
assert(OFSC C B D A C' B D' A)
by (unfold OFSC;repeat split;Between;Cong).
apply cong_commutativity.
eauto using five_segments_with_def.
Qed.
Lemma l8_13_2 : ∀ A B C D X,
A ≠ B → C ≠ D → Col X A B → Col X C D →
(∃ U, ∃ V :Tpoint, Col U A B ∧ Col V C D ∧ U≠X ∧ V≠X ∧ Per U X V) →
Perp_in X A B C D.
Proof.
intros.
ex_and H3 U.
ex_and H4 V.
unfold Perp_in.
repeat split;try assumption.
intros.
assert (Per V X U0).
eapply l8_2.
eapply l8_3.
apply H7.
assumption.
eapply col3.
apply H.
Col.
Col.
Col.
eapply per_col.
2:eapply l8_2.
2:apply H10.
auto.
eapply col3.
apply H0.
Col.
Col.
Col.
Qed.
Definition DistLn := fun A B C D ⇒
(∃ X, Col X A B ∧ ¬Col X C D) ∨ (∃ X, ¬ Col X A B ∧ Col X C D).
Lemma perBAB : ∀ A B, Per B A B → A = B.
Proof.
intros.
eapply l8_7.
apply H.
eapply l8_2.
apply l8_5.
Qed.
Lemma l8_14_1 : ∀ A B, ¬ Perp A B A B.
Proof.
intros.
unfold Perp.
intro.
ex_and H X.
unfold Perp_in in H0.
spliter.
assert (Per A X A).
apply H3.
Col.
Col.
assert (A = X).
eapply l8_7.
2: apply H4.
apply l8_2.
apply l8_5.
assert (Per B X B)
by (apply H3;Col).
assert (B = X).
eapply l8_7 with B.
2: apply H6.
apply l8_2.
apply l8_5.
apply H0.
congruence.
Qed.
Lemma l8_14_2_1a : ∀ X A B C D, Perp_in X A B C D → Perp A B C D.
Proof.
intros.
unfold Perp.
∃ X.
assumption.
Qed.
Lemma perp_in_distinct : ∀ X A B C D , Perp_in X A B C D → A ≠ B ∧ C ≠ D.
Proof.
intros.
apply l8_14_2_1a in H.
apply perp_distinct.
assumption.
Qed.
Lemma l8_14_2_1b : ∀ X A B C D Y, Perp_in X A B C D → Col Y A B → Col Y C D → X=Y.
Proof.
intros.
unfold Perp_in in H.
spliter.
eapply (H5 Y Y) in H1.
2:assumption.
apply perBAB.
assumption.
Qed.
Lemma l8_14_2_1b_bis : ∀ A B C D X, Perp A B C D → Col X A B → Col X C D → Perp_in X A B C D.
Proof.
intros.
unfold Perp in H.
ex_and H Y.
assert (Y = X)
by (eapply (l8_14_2_1b Y _ _ _ _ X) in H2;assumption).
subst Y.
assumption.
Qed.
Lemma l8_14_2_2 : ∀ X A B C D,
Perp A B C D → (∀ Y, Col Y A B → Col Y C D → X=Y) → Perp_in X A B C D.
Proof.
intros.
eapply l8_14_2_1b_bis.
assumption.
unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D) by assumption.
apply (H0 Y H2) in H3.
subst Y.
assumption.
unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D).
assumption.
apply (H0 Y H2) in H3.
subst Y.
assumption.
Qed.
Lemma l8_14_3 : ∀ A B C D X Y, Perp_in X A B C D → Perp_in Y A B C D → X=Y.
Proof.
intros.
eapply l8_14_2_1b.
apply H.
unfold Perp_in in H0.
intuition.
eapply l8_12 in H0.
unfold Perp_in in H0.
intuition.
Qed.
Lemma l8_15_1 : ∀ A B C X, A≠B → Col A B X → Perp A B C X → Perp_in X A B C X.
Proof.
intros.
eapply l8_14_2_1b_bis;Col.
Qed.
Lemma l8_15_2 : ∀ A B C X, A≠B → Col A B X → Perp_in X A B C X → Perp A B C X.
Proof.
intros.
eapply l8_14_2_1a.
apply H1.
Qed.
Lemma perp_in_per : ∀ A B C, Perp_in B A B B C→ Per A B C.
Proof.
intros.
unfold Perp_in in H.
spliter.
apply H3;Col.
Qed.
Lemma perp_sym : ∀ A B C D, Perp A B C D → Perp C D A B.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
apply l8_12.
assumption.
Qed.
Lemma perp_col0 : ∀ A B C D X Y, Perp A B C D → X ≠ Y → Col A B X → Col A B Y → Perp C D X Y.
Proof.
unfold Perp.
intros.
ex_and H X0.
∃ X0.
unfold Perp_in in ×.
spliter.
repeat split.
assumption.
assumption.
assumption.
eapply col3.
apply H.
Col.
assumption.
assumption.
intros.
eapply l8_2.
apply H6.
2:assumption.
assert(Col A X Y).
eapply col3 with A B;Col.
assert (Col B X Y).
eapply col3 with A B;Col.
eapply col3 with X Y;Col.
Qed.
Lemma l8_16_1 : ∀ A B C U X,
A≠B → Col A B X → Col A B U → U≠X → Perp A B C X → ¬ Col A B C ∧ Per C X U.
Proof.
intros.
split.
intro.
assert (Perp_in X A B C X).
eapply l8_15_1.
assumption.
assumption.
assumption.
assert (X = U).
eapply l8_14_2_1b.
apply H5.
Col.
eapply col3 with A B;Col.
intuition.
apply l8_14_2_1b_bis with C X U X;try Col.
assert (Col A X U).
eapply (col3 A B);Col.
eapply perp_col0 with A B;Col.
Qed.
Lemma per_perp_in : ∀ A B C, A ≠ B → B ≠ C → Per A B C → Perp_in B A B B C.
Proof.
intros.
unfold Perp.
repeat split.
assumption.
assumption.
Col.
Col.
intros.
eapply per_col.
apply H0.
eapply l8_2.
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H4.
apply l8_2.
assumption.
Col.
Col.
Qed.
Lemma per_perp : ∀ A B C, A ≠ B → B ≠ C → Per A B C → Perp A B B C.
Proof.
intros.
apply per_perp_in in H1.
eapply l8_14_2_1a with B;assumption.
assumption.
assumption.
Qed.
Lemma perp_left_comm : ∀ A B C D, Perp A B C D → Perp B A C D.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
unfold Perp_in in ×.
intuition.
Qed.
Lemma perp_right_comm : ∀ A B C D, Perp A B C D → Perp A B D C.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
unfold Perp_in in ×.
intuition.
Qed.
Lemma perp_comm : ∀ A B C D, Perp A B C D → Perp B A D C.
Proof.
intros.
apply perp_left_comm.
apply perp_right_comm.
assumption.
Qed.
Lemma perp_in_sym :
∀ A B C D X,
Perp_in X A B C D → Perp_in X C D A B.
Proof.
unfold Perp_in.
intros.
spliter.
repeat split.
assumption.
assumption.
assumption.
assumption.
intros.
apply l8_2.
apply H3;assumption.
Qed.
Lemma perp_in_left_comm :
∀ A B C D X,
Perp_in X A B C D → Perp_in X B A C D.
Proof.
unfold Perp_in.
intuition.
Qed.
Lemma perp_in_right_comm : ∀ A B C D X, Perp_in X A B C D → Perp_in X A B D C.
Proof.
intros.
apply perp_in_sym.
apply perp_in_left_comm.
apply perp_in_sym.
assumption.
Qed.
Lemma perp_in_comm : ∀ A B C D X, Perp_in X A B C D → Perp_in X B A D C.
Proof.
intros.
apply perp_in_left_comm.
apply perp_in_right_comm.
assumption.
Qed.
End T8_3.
Hint Resolve perp_sym perp_left_comm perp_right_comm perp_comm per_perp_in
perp_in_per perp_in_left_comm perp_in_right_comm perp_in_comm perp_in_sym : perp.
Ltac double A B A' :=
assert (mp:= symmetric_point_construction A B);
elim mp; intros A' ; intro; clear mp.
Section T8_4.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma Perp_cases :
∀ A B C D,
Perp A B C D ∨ Perp B A C D ∨ Perp A B D C ∨ Perp B A D C ∨
Perp C D A B ∨ Perp C D B A ∨ Perp D C A B ∨ Perp D C B A →
Perp A B C D.
Proof.
intros.
decompose [or] H; Perp.
Qed.
Lemma Perp_perm :
∀ A B C D,
Perp A B C D →
Perp A B C D ∧ Perp B A C D ∧ Perp A B D C ∧ Perp B A D C ∧
Perp C D A B ∧ Perp C D B A ∧ Perp D C A B ∧ Perp D C B A.
Proof.
intros.
repeat split; Perp.
Qed.
Lemma Perp_in_cases :
∀ X A B C D,
Perp_in X A B C D ∨ Perp_in X B A C D ∨ Perp_in X A B D C ∨ Perp_in X B A D C ∨
Perp_in X C D A B ∨ Perp_in X C D B A ∨ Perp_in X D C A B ∨ Perp_in X D C B A →
Perp_in X A B C D.
Proof.
intros.
decompose [or] H; Perp.
Qed.
Lemma Perp_in_perm :
∀ X A B C D,
Perp_in X A B C D →
Perp_in X A B C D ∧ Perp_in X B A C D ∧ Perp_in X A B D C ∧ Perp_in X B A D C ∧
Perp_in X C D A B ∧ Perp_in X C D B A ∧ Perp_in X D C A B ∧ Perp_in X D C B A.
Proof.
intros.
do 7 (split; Perp).
Qed.
Lemma l8_16_2 : ∀ A B C U X,
A≠B → Col A B X → Col A B U → U≠X → ¬ Col A B C → Per C X U → Perp A B C X.
Proof.
intros.
assert (C ≠ X).
intro.
subst X.
apply H3.
assumption.
unfold Perp.
∃ X.
eapply l8_13_2.
assumption.
assumption.
Col.
Col.
∃ U.
∃ C.
repeat split;
Col.
apply l8_2.
assumption.
Qed.
Lemma l8_18_unicity : ∀ A B C X Y,
¬ Col A B C → Col A B X → Perp A B C X → Col A B Y → Perp A B C Y → X=Y.
Proof.
intros.
show_distinct A B.
solve [intuition].
assert (Perp_in X A B C X)
by (eapply l8_15_1;assumption).
assert (Perp_in Y A B C Y)
by (eapply l8_15_1;assumption).
unfold Perp_in in ×.
spliter.
apply l8_7 with C;apply l8_2;[apply H14 |apply H10];Col.
Qed.
Lemma distinct : ∀ A B X C C', ¬ Col A B C → Col A B X → is_midpoint X C C' → C ≠ C'.
Proof.
intros.
intro.
subst C'.
apply H.
unfold is_midpoint in H1.
spliter.
treat_equalities.
assumption.
Qed.
Lemma l8_20_1 : ∀ A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → Per B A P.
Proof.
intros.
double B A B'.
double D A D'.
double P A P'.
induction (eq_dec_points A B).
subst B.
unfold is_midpoint in H5.
spliter.
eapply l8_2.
eapply l8_5.
assert (Per B' B C).
eapply l8_3.
apply H.
assumption.
unfold Col.
left.
apply midpoint_bet.
assumption.
assert (Per B B' C').
eapply l8_10.
apply H7.
unfold Cong_3.
repeat split.
apply cong_pseudo_reflexivity.
eapply l7_13.
unfold is_midpoint.
split.
apply H3.
apply midpoint_cong.
assumption.
assumption.
eapply l7_13.
apply l7_2.
apply H3.
assumption.
assert(is_midpoint B' D' C').
eapply symmetry_preserves_midpoint.
apply H4.
apply H3.
apply l7_2.
apply H1.
assumption.
assert(is_midpoint P' C D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H5.
apply H4.
assumption.
unfold Per.
∃ P'.
split.
assumption.
unfold Per in H7.
ex_and H7 D''.
assert (D''= D).
eapply symmetric_point_unicity.
apply H7.
apply l7_2.
assumption.
subst D''.
unfold Per in H8.
ex_and H8 D''.
assert (D' = D'').
eapply symmetric_point_unicity.
apply l7_2.
apply H9.
assumption.
subst D''.
assert (is_midpoint P C' D).
eapply symmetry_preserves_midpoint.
apply l7_2.
apply H1.
apply l7_2.
apply H5.
apply l7_2.
apply H4.
assumption.
assert (Cong C D C' D').
eapply l7_13.
apply H1.
apply l7_2.
assumption.
assert (Cong C' D C D').
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.
assert(Cong P D P' D').
eapply l7_13.
apply l7_2.
apply H5.
apply l7_2.
assumption.
assert (Cong P D P' C).
eapply cong_transitivity.
apply H16.
unfold is_midpoint in H10.
spliter.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
assert (IFSC C' P D B D' P' C B).
unfold IFSC.
repeat split.
apply midpoint_bet.
assumption.
apply midpoint_bet.
apply l7_2.
assumption.
apply cong_right_commutativity.
assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_right_commutativity.
apply midpoint_cong.
assumption.
assert (Cong P B P' B).
eapply l4_2.
apply H18.
apply cong_commutativity.
assumption.
Qed.
Lemma l8_20_2 : ∀ A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → B≠C → A≠P.
Proof.
intros.
intro.
subst P.
assert (C = D).
eapply symmetric_point_unicity.
apply H1.
assumption.
subst D.
assert (B = C).
apply l7_3.
assumption.
subst C.
absurde.
Qed.
Lemma perp_col1 : ∀ A B C D X,
C ≠ X → Perp A B C D → Col C D X → Perp A B C X.
Proof.
intros.
assert (T:=perp_distinct A B C D H0).
spliter.
unfold Perp in ×.
ex_and H0 P.
∃ P.
unfold Perp_in in ×.
spliter.
repeat split.
assumption.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_2.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_3.
assumption.
intros.
apply H7.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
apply col_permutation_5.
assumption.
apply col_permutation_1.
assumption.
Qed.
Lemma l8_18_existence : ∀ A B C, ¬ Col A B C → ∃ X, Col A B X ∧ Perp A B C X.
Proof.
intros.
prolong B A Y A C.
assert (∃ P, is_midpoint P C Y)
by (apply l7_25 with A;Cong).
ex_and H2 P.
assert (Per A P Y)
by (unfold Per;∃ C;auto using l7_2).
prolong A Y Z Y P.
prolong P Y Q Y A.
prolong Q Z Q' Q Z.
assert (is_midpoint Z Q Q')
by (unfold is_midpoint;Cong).
prolong Q' Y C' Y C.
assert (∃ X, is_midpoint X C C')
by (apply l7_25 with Y;Cong).
ex_and H13 X.
assert (OFSC A Y Z Q Q Y P A) by
(unfold OFSC;repeat split;Between;Cong).
show_distinct A Y.
intuition.
assert (Cong Z Q P A)
by (eauto using five_segments_with_def).
assert (Cong_3 A P Y Q Z Y)
by (unfold Cong_3;Cong).
assert (Per Q Z Y)
by (eauto using l8_10).
assert (Per Y Z Q) by eauto using l8_2.
show_distinct P Y.
unfold is_midpoint in ×.
spliter.
treat_equalities.
assert_cols.
Col5.
unfold Per in H19.
ex_and H19 Q''.
assert (Q' = Q'').
eapply symmetric_point_unicity.
apply H10.
assumption.
subst Q''.
assert (hy:Bet Z Y X).
apply (l7_22 Q C Q' C' Y Z X);Cong.
assert (T:=outer_transitivity_between2 C P Y Q).
assert_bet.
apply between_symmetry.
apply T;Between.
show_distinct Q Y.
intuition.
assert (Per Y X C)
by (unfold Per;∃ C';Cong).
assert_diffs.
assert (Col P Y Q).
unfold Col.
left.
assumption.
assert(Col P Y C).
unfold is_midpoint in H3.
spliter.
unfold Col.
right; right.
assumption.
assert (Col P Q C) by ColR.
assert (Col Y Q C) by ColR.
assert (Col A Y B)
by (assert_cols;Col).
assert (Col A Y Z)
by (assert_cols;Col).
assert (Col A B Z)
by ColR.
assert (Col Y B Z)
by ColR.
assert (Col Q Y P)
by Col.
assert(Q ≠ C).
intro.
subst Q.
unfold is_midpoint in ×.
spliter.
apply H.
assert (Bet B Y Z)
by (apply outer_transitivity_between2 with A;auto).
apply between_symmetry in H3.
assert (Y = P).
eapply between_egality.
apply H3.
assumption.
treat_equalities.
intuition.
assert (Col Y B Z).
eapply col_transitivity_2.
apply H15.
assumption.
assumption.
assert (Y ≠ Q').
intro.
treat_equalities.
absurde.
assert (Col Y Q' C')
by (assert_cols;Col).
assert (Q ≠ Q').
intro.
unfold OFSC, Cong_3 in ×.
spliter.
treat_equalities.
apply H.
ColR.
assert (C ≠ C').
intro.
subst C'.
apply l7_3 in H14.
subst X.
assert (Col Z Q Q')
by (assert_cols;ColR).
assert (Y ≠ Z).
intro.
subst Z.
unfold OFSC, Cong_3, is_midpoint in ×.
spliter.
treat_equalities.
intuition.
apply H.
ColR.
assert(OFSC Q Y C Z Q' Y C' Z).
unfold OFSC.
repeat split;Between;Cong.
unfold OFSC, is_midpoint in ×.
spliter.
eapply outer_transitivity_between with P;Between;Cong.
assert (Cong C Z C' Z)
by (eauto using five_segments_with_def).
assert (Col Z Y X)
by (assert_cols;Col).
assert (Y ≠ Z).
intro.
treat_equalities.
intuition.
assert(C ≠ X).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in ×.
spliter.
treat_equalities.
intuition.
assert(X ≠ Y).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in ×.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
show_distinct C' Y.
intuition.
assert (Col Y C' P ).
eapply col_transitivity_1 with C.
intuition.
unfold Col.
right;right.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
show_distinct P Q.
intuition.
assert (Col Y P Q').
eapply col_transitivity_2.
apply H10.
apply col_permutation_4.
assumption.
apply col_permutation_2.
assumption.
assert (Col Y Q Q').
eapply col_transitivity_2.
apply H20.
assumption.
apply col_permutation_4.
assumption.
assert (Col Q Y Z)
by (assert_cols;ColR).
assert (Col Y Z C)
by (assert_bet;assert_cols;ColR).
apply H.
ColR.
assert (Perp_in X Y Z C X).
eapply l8_13_2;Col.
∃ Y.
∃ C.
repeat split;Col.
assert (Col A B X) by ColR.
∃ X.
split.
assumption.
unfold Perp.
∃ X.
unfold Perp_in.
repeat split;Col.
intros.
unfold Perp_in in H52.
spliter.
apply H59;ColR.
Qed.
Lemma l8_21_aux : ∀ A B C,
A≠ B → ¬ Col A B C → ∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet C T P.
Proof.
intros.
assert (∃ X : Tpoint, Col A B X ∧ Perp A B C X).
eapply l8_18_existence.
assumption.
ex_and H1 X.
assert (Perp_in X A B C X).
eapply l8_15_1;
assumption.
assert (Per A X C).
unfold Perp_in in H3.
spliter.
apply H7.
apply col_trivial_1.
apply col_trivial_1.
assert(HH:= H4).
unfold Per in H4.
ex_and H4 C'.
double C A C''.
assert (∃ P, is_midpoint P C' C'').
eapply l7_25.
unfold is_midpoint in ×.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
apply cong_left_commutativity.
assumption;
spliter.
ex_elim H7 P.
assert (Per X A P).
eapply l8_20_1.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
apply H6.
apply l7_2.
assumption.
assert (X ≠ C).
intro.
subst C.
apply H0.
assumption.
assert (A ≠ P).
eapply l8_20_2.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
assumption.
apply l7_2.
assumption.
assumption.
assert (∃ T, Bet P T C ∧ Bet A T X).
eapply l3_17.
apply midpoint_bet.
apply l7_2.
apply H6.
apply midpoint_bet.
apply l7_2.
apply H4.
apply midpoint_bet.
apply l7_2.
apply H8.
ex_and H11 T.
induction (eq_dec_points A X).
subst X.
∃ P.
∃ T.
apply between_identity in H12.
subst T.
assert (C'= C'').
eapply symmetric_point_unicity.
apply H4.
assumption.
subst C''.
apply l7_3 in H8.
subst P.
assert (Col A C C')
by (assert_cols;ColR).
repeat split;Col;Between.
apply perp_col0 with C A;auto using perp_sym;assert_cols;Col.
∃ P.
∃ T.
repeat split.
unfold Perp.
∃ A.
unfold Perp_in.
repeat split.
assumption.
auto.
apply col_trivial_1.
apply col_trivial_3.
unfold Perp_in in H3.
spliter.
intros.
eapply per_col in H7.
apply l8_2 in H7.
eapply per_col in H7.
eapply l8_2 in H7.
apply H7.
assumption.
ColR.
assumption.
ColR.
assert_cols;ColR.
Between.
Qed.
Lemma l8_21 : ∀ A B C,
A≠ B → ∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet C T P.
Proof.
intros.
induction(Col_dec A B C).
assert (∃ C', ¬ Col A B C').
eapply l6_25.
assumption.
ex_elim H1 C'.
assert ( ∃ P : Tpoint,
(∃ T : Tpoint, Perp A B P A ∧ Col A B T ∧ Bet C' T P)).
eapply l8_21_aux.
assumption.
assumption.
ex_elim H1 P.
ex_and H3 T.
∃ P.
∃ C.
repeat split.
assumption.
assumption.
apply between_trivial2.
eapply l8_21_aux.
assumption.
assumption.
Qed.
Lemma perp_in_col : ∀ A B C D X, Perp_in X A B C D → Col A B X ∧ Col C D X.
Proof.
unfold Perp_in.
intuition.
Qed.
Lemma perp_perp_in : ∀ A B C, Perp A B C A → Perp_in A A B C A.
Proof.
intros.
apply l8_15_1.
unfold Perp in H.
ex_and H X.
unfold Perp_in in H0.
intuition.
apply col_trivial_3.
assumption.
Qed.
Lemma perp_per_1 : ∀ A B C, A≠B → Perp A B C A → Per B A C.
Proof.
intros.
assert (Perp_in A A B C A).
apply perp_perp_in.
assumption.
unfold Perp_in in H1.
spliter.
apply H5.
apply col_trivial_3.
apply col_trivial_1.
Qed.
Lemma perp_per_2 : ∀ A B C, A≠B → Perp A B A C → Per B A C.
Proof.
intros.
apply perp_right_comm in H0.
apply perp_per_1;
assumption.
Qed.
Lemma perp_col : ∀ A B C D E, A≠E → Perp A B C D → Col A B E → Perp A E C D.
Proof.
intros.
apply perp_sym.
eapply perp_col0.
apply H0.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma perp_col2 : ∀ A B C D X Y,
Perp A B X Y →
C ≠ D → Col A B C → Col A B D → Perp C D X Y.
Proof.
intros.
assert(HH:=H).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points A C).
subst A.
eapply perp_col.
assumption.
apply H.
assumption.
assert(Perp A C X Y) by (eapply perp_col;eauto).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H6.
apply col_permutation_2;
eapply col_transitivity_1.
apply H3.
assumption.
assumption.
Qed.
Lemma perp_not_eq_1 : ∀ A B C D, Perp A B C D → A≠B.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.
Lemma perp_not_eq_2 : ∀ A B C D, Perp A B C D → C≠D.
Proof.
intros.
apply perp_sym in H.
eapply perp_not_eq_1.
apply H.
Qed.
Lemma le_bet : ∀ A B C D, le C D A B → ∃ X, Bet A X B ∧ Cong A X C D.
Proof.
intros.
unfold le in H.
ex_and H Y.
∃ Y;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.
unfold Col.
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;Cong.
Qed.
Lemma diff_per_diff : ∀ A B P R ,
A ≠ B → Cong A P B R → Per B A P → Per A B R → P ≠ R.
Proof.
intros.
intro.
subst.
assert (A = B).
eapply l8_7.
apply l8_2.
apply H1.
apply l8_2.
assumption.
intuition.
Qed.
Lemma per_not_colp : ∀ A B P R, A ≠ B → A ≠ P → B ≠ R → Per B A P → Per A B R → ¬Col P A R.
Proof.
intros.
intro.
assert (Perp A B P A).
apply perp_comm.
apply per_perp.
auto.
assumption.
assumption.
assert (Perp A B B R).
apply per_perp.
assumption.
assumption.
assumption.
assert (Per B A R).
eapply per_col.
apply H0.
assumption.
Col5.
apply l8_2 in H3.
apply l8_2 in H7.
assert (A = B).
eapply l8_7.
apply H7.
assumption.
contradiction.
Qed.
Lemma per_not_col : ∀ A B C, A ≠ B → B ≠ C → Per A B C → ¬Col A B C.
Proof.
intros.
intro.
unfold Per in H1.
ex_and H1 C'.
assert (C = C' ∨ is_midpoint A C C').
eapply l7_20.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H4.
Col5.
unfold Col.
left.
apply midpoint_bet.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H1.
apply H0.
assumption.
apply H.
eapply l7_17.
apply H4.
assumption.
Qed.
Lemma per_cong : ∀ A B P R X ,
A ≠ B → A ≠ P →
Per B A P → Per A B R →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B.
Proof.
intros.
assert (Per P A B).
apply l8_2.
assumption.
double B R Q.
assert (B ≠ R).
intro.
subst R.
apply cong_identity in H3.
subst P.
absurde.
assert (Per A B Q).
eapply per_col.
apply H8.
assumption.
unfold Col.
left.
apply midpoint_bet.
assumption.
assert (Per P A X).
eapply per_col.
apply H.
assumption.
assumption.
assert (B ≠ Q).
intro.
subst Q.
apply l7_3 in H7.
subst R.
absurde.
assert (Per R B X).
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H12.
apply l8_2.
assumption.
apply col_permutation_4.
assumption.
assert (X ≠ A).
intro.
subst X.
assert (¬Col P A R).
eapply per_not_colp.
apply H.
assumption.
assumption.
assumption.
assumption.
apply H13.
unfold Col.
left.
assumption.
double P A P'.
prolong P' X R' X R.
assert (∃ M, is_midpoint M R R').
eapply l7_25.
apply cong_symmetry.
apply H16.
ex_elim H17 M.
assert (Per X M R).
unfold Per.
∃ R'.
split.
assumption.
apply cong_symmetry.
assumption.
assert (Cong X P X P').
apply l8_2 in H10.
unfold Per in H10.
ex_and H10 P''.
assert (P'=P'').
eapply symmetric_point_unicity.
apply H14.
apply H10.
subst P''.
assumption.
assert (X ≠ P').
intro.
subst P'.
apply cong_identity in H19.
subst X.
apply l7_3 in H14.
subst P.
absurde.
assert (P ≠ P').
intro.
subst P'.
eapply l7_3 in H14.
subst P.
absurde.
assert(¬Col X P P').
intro.
assert(Col X P A).
eapply col3.
apply H21.
apply col_permutation_1.
assumption.
apply col_trivial_3.
unfold Col.
right;left.
apply between_symmetry.
apply midpoint_bet.
assumption.
apply col_permutation_1 in H23.
assert (P = A ∨ X = A).
eapply l8_9.
assumption.
assumption.
induction H24.
subst P.
absurde.
apply H13.
assumption.
assert (Bet A X M).
eapply l7_22.
5:apply H14.
5:apply H18.
assumption.
assumption.
assumption.
apply cong_symmetry.
assumption.
assert (X ≠ R).
intro.
treat_equalities.
apply perBAB in H12.
treat_equalities.
unfold is_midpoint in ×.
spliter.
treat_equalities.
intuition.
assert (X ≠ R').
intro.
subst R'.
apply cong_symmetry in H16.
apply cong_identity in H16.
apply H24.
assumption.
assert (M ≠ X).
intro.
subst M.
apply H22.
eapply col_transitivity_1.
apply H24.
unfold Col.
right; right.
assumption.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
apply midpoint_bet.
assumption.
unfold Col.
right; right.
assumption.
assert (M = B).
eapply (l8_18_unicity A X R).
intro.
assert (Col A B R).
eapply col_transitivity_1.
intro.
apply H13.
apply sym_equal.
apply H28.
apply col_permutation_5.
assumption.
assumption.
eapply per_not_col.
apply H;
apply H12.
apply H8.
assumption.
assumption.
unfold Col.
left.
assumption;
eapply col_transitivity_1.
apply per_perp in H17.
apply perp_comm.
eapply perp_col.
assumption.
apply H17.
unfold Col.
right;right.
assumption.
auto.
intro.
subst M.
apply (symmetric_point_unicity R R R R') in H18.
subst R'.
apply H22.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
assumption.
unfold Col.
right; right.
assumption.
eapply l7_3_2.
apply col_permutation_5.
assumption.
apply per_perp in H10.
apply perp_comm.
eapply perp_col.
apply H13.
apply perp_comm.
eapply perp_col.
intro.
apply H13.
apply sym_equal.
apply H27.
apply perp_right_comm.
apply per_perp in H2.
apply H2.
assumption.
assumption.
assumption.
apply col_trivial_2.
auto.
intro.
apply H13.
subst X.
reflexivity.
subst M.
assert(OFSC P X R P' P' X R' P).
unfold OFSC.
repeat split.
assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_symmetry.
assumption.
apply cong_pseudo_reflexivity.
apply cong_symmetry.
assumption.
assert (Cong R P' R' P).
eapply five_segments_with_def.
apply H27.
intro.
subst X.
apply H22.
apply col_trivial_1.
assert (IFSC P' A P R R' B R P).
unfold IFSC.
repeat split.
apply between_symmetry.
apply midpoint_bet.
assumption.
apply between_symmetry.
apply midpoint_bet.
assumption.
eapply l2_11.
apply between_symmetry.
apply midpoint_bet.
apply H14.
apply between_symmetry.
apply midpoint_bet.
apply H18.
eapply cong_transitivity.
apply midpoint_cong.
apply l7_2.
apply H14.
eapply cong_transitivity.
apply H3.
apply cong_commutativity.
apply midpoint_cong.
assumption.
assumption.
assumption.
Cong.
apply cong_pseudo_reflexivity.
eapply cong_right_commutativity.
eapply l4_2.
eapply H29.
Qed.
Lemma perp_cong : ∀ A B P R X,
A ≠ B → A ≠ P →
Perp A B P A → Perp A B R B →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B.
Proof.
intros.
apply (per_cong A B P R X).
assumption.
assumption.
apply perp_per_1.
assumption.
assumption.
eapply perp_per_1.
auto.
apply perp_left_comm;auto.
assumption.
assumption.
assumption.
Qed.
Lemma midpoint_existence_aux : ∀ A B P Q T,
A≠B → Perp A B Q B → Perp A B P A →
Col A B T → Bet Q T P → le A P B Q →
∃ X : Tpoint, is_midpoint X A B.
Proof.
intros.
unfold le in H4.
ex_and H4 R.
assert (∃ X, Bet T X B ∧ Bet R X P).
eapply inner_pasch.
apply between_symmetry.
apply H3.
auto.
ex_and H6 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H6.
subst X.
Col.
assert (Col B A X).
eapply col_transitivity_2.
apply H8.
apply col_permutation_3.
assumption.
apply col_permutation_5.
unfold Col.
left; assumption.
apply col_permutation_4.
assumption.
induction(Col_dec A B P).
assert (B=A ∨ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
assumption.
apply col_permutation_4.
assumption.
induction H10.
∃ A.
subst B.
eapply l7_3_2.
subst P.
treat_equalities.
apply perp_distinct in H1.
spliter.
absurde.
assert (B ≠ R).
intro.
subst R.
treat_equalities.
apply H9.
apply col_trivial_3.
assert (¬Col A B Q).
intro.
assert (A=B ∨ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
assumption.
assumption.
induction H12.
apply H.
assumption.
subst Q.
treat_equalities.
absurde.
assert (¬Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H10.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H11.
apply col_permutation_4.
assumption.
assert (P ≠ R).
intro.
subst R.
treat_equalities.
intuition.
induction (eq_dec_points A P).
subst P.
apply perp_distinct in H1.
spliter.
absurde.
assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply perp_sym.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.
apply between_symmetry in H7.
assert (Cong A R P B).
apply (perp_cong A B P R X);
assumption.
assert (is_midpoint X A B ∧ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H9.
apply col_permutation_5.
assumption.
assumption.
assumption.
intros.
apply cong_commutativity.
apply cong_symmetry.
apply cong_right_commutativity.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
spliter.
∃ X.
assumption.
Qed.
Lemma midpoint_existence : ∀ A B, ∃ X, is_midpoint X A B.
Proof.
intros.
induction (eq_dec_points A B).
subst B.
∃ A.
apply l7_3_2.
cut(∃ Q, Perp A B B Q).
intro.
ex_elim H0 Q.
cut(∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet Q T P).
intros.
ex_elim H0 P.
ex_and H2 T.
assert (le A P B Q ∨ le B Q A P).
apply le_cases.
induction H4.
eapply midpoint_existence_aux.
assumption.
apply perp_right_comm.
apply H1.
apply H0.
apply H2.
assumption.
assumption.
assert (∃ X : Tpoint, is_midpoint X B A).
eapply (midpoint_existence_aux B A Q P T).
auto.
apply perp_left_comm.
assumption.
apply perp_comm.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
assumption.
ex_elim H5 X.
∃ X.
apply l7_2.
assumption.
eapply l8_21.
assumption.
assert (∃ P : Tpoint,
(∃ T : Tpoint, Perp B A P B ∧ Col B A T ∧ Bet A T P)) by
(apply (l8_21 B A);auto).
ex_elim H0 P.
ex_elim H1 T.
spliter.
∃ P.
apply perp_comm.
assumption.
Qed.
Lemma perp_in_id : ∀ A B C X, Perp_in X A B C A → X = A.
Proof.
intros.
assert (Perp A B C A).
unfold Perp.
∃ X.
assumption.
assert (A ≠ B ∧ C ≠ A).
apply perp_distinct.
assumption.
spliter.
assert (HH:=H0).
apply perp_perp_in in HH.
assert (l8_16_1:=l8_16_1 A B C B A).
assert (¬Col A B C ∧ Per C A B).
apply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
assumption.
spliter.
unfold Perp_in in H.
spliter.
eapply l8_18_unicity.
apply H3.
apply col_permutation_1.
assumption.
apply perp_sym.
eapply perp_col.
intro.
subst X.
assert (¬Col C A B).
apply per_not_col.
assumption.
assumption.
assumption.
apply H9.
assumption.
apply perp_sym.
apply H0.
apply col_permutation_1.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma l8_22 : ∀ A B P R X ,
A ≠ B → A ≠ P →
Per B A P → Per A B R →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B ∧ is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
assert (Cong A R P B).
apply (per_cong A B P R X);
assumption.
split.
assumption.
assert (¬ Col B A P).
eapply per_not_col.
auto.
assumption.
assumption.
apply l7_21.
intro.
apply H7.
Col.
intro.
subst R.
eapply between_identity in H5.
subst X.
apply H7.
apply col_permutation_4.
assumption.
assumption.
Cong.
Col.
unfold Col.
left.
assumption.
Qed.
Lemma l8_22_bis : ∀ A B P R X,
A ≠ B → A ≠ P →
Perp A B P A → Perp A B R B →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B ∧ is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
apply l8_22.
assumption.
assumption.
apply perp_per_1.
assumption.
assumption.
apply perp_per_1.
auto.
apply perp_left_comm.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma perp_in_perp : ∀ A B C D X, Perp_in X A B C D → Perp A B C D.
Proof.
intros.
unfold Perp.
∃ X.
assumption.
Qed.
End T8_4.
Hint Resolve perp_col perp_perp_in perp_in_perp : perp.
Section T8_5.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma perp_proj : ∀ A B C D, Perp A B C D → ¬Col A C D → ∃ X, Col A B X ∧ Perp A X C D.
Proof.
intros.
unfold Perp in H.
ex_and H X.
∃ X.
split.
unfold Perp_in in H1.
spliter.
apply col_permutation_1.
assumption.
eapply perp_col.
intro.
subst X.
unfold Perp_in in H1.
spliter.
apply H0.
assumption.
apply perp_in_perp in H1.
apply H1.
unfold Perp_in in H1.
spliter.
apply col_permutation_1.
assumption.
Qed.
Lemma l8_24 : ∀ A B P Q R T,
Perp P A A B →
Perp Q B A B →
Col A B T →
Bet P T Q →
Bet B R Q →
Cong A P B R →
∃ X, is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
unfold le in H4.
assert (∃ X, Bet T X B ∧ Bet R X P).
eapply inner_pasch.
apply H2.
assumption.
ex_and H5 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H5.
subst X.
apply col_trivial_2.
assert (Col T X B).
unfold Col.
left.
assumption.
apply col_permutation_4.
eapply col_transitivity_1.
intro.
apply H7.
apply sym_equal.
apply H9.
apply col_permutation_1.
assumption.
apply col_permutation_2.
assumption.
assert (A ≠ B).
apply perp_distinct in H.
spliter.
assumption.
assert (A ≠ P).
apply perp_distinct in H.
spliter.
auto.
induction(Col_dec A B P).
assert (B=A ∨ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
apply perp_sym.
assumption.
apply col_permutation_4.
assumption.
induction H11.
∃ A.
subst B.
absurde.
subst P.
absurde.
assert (B ≠ R).
intro.
subst R.
apply cong_identity in H4.
subst P.
absurde.
assert (Q ≠ B).
apply perp_distinct in H0.
spliter.
assumption.
assert (¬Col A B Q).
intro.
assert (A=B ∨ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
apply perp_sym.
assumption.
assumption.
induction H14.
contradiction.
subst Q.
absurde.
assert (¬Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H11.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H13.
apply col_permutation_4.
assumption.
assert (P ≠ R).
intro.
subst R.
apply between_identity in H6.
subst X.
contradiction.
induction (eq_dec_points A P).
subst P.
apply perp_distinct in H.
spliter.
absurde.
assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.
assert (Cong A R P B).
apply (perp_cong A B P R X).
assumption.
assumption.
apply perp_sym.
assumption.
assumption.
assumption.
assumption.
apply between_symmetry.
assumption.
intros.
assert (is_midpoint X A B ∧ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H10.
apply col_permutation_5.
assumption.
assumption.
assumption.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
∃ X.
assumption.
Qed.
Lemma perp_not_col2 : ∀ A B C D, Perp A B C D → ¬ Col A B C ∨ ¬ Col A B D.
Proof.
intros.
induction (Col_dec A B C).
right.
assert(Perp_in C A B C D).
apply l8_14_2_1b_bis; Col.
intro.
assert(Perp_in D A B C D).
apply l8_14_2_1b_bis; Col.
assert(C = D).
eapply l8_14_3.
apply H1.
assumption.
apply perp_not_eq_2 in H.
contradiction.
left.
assumption.
Qed.
Lemma ex_col2 : ∀ A B, ∃ C, Col A B C ∧ A ≠ C ∧ B ≠ C.
intros.
induction(eq_dec_points A B).
subst B.
assert(HH:=another_point A).
ex_and HH B.
∃ B.
split; Col.
prolong A B C A B.
∃ C.
split.
apply bet_col.
assumption.
split.
intro.
subst C.
apply between_identity in H0.
contradiction.
intro.
subst C.
apply cong_symmetry in H1.
apply cong_identity in H1.
contradiction.
Qed.
Lemma perp_in_col_perp_in : ∀ A B C D E P, C ≠ E → Col C D E → Perp_in P A B C D → Perp_in P A B C E.
intros.
unfold Perp_in in ×.
spliter.
repeat split; auto.
ColR.
intros.
apply H5.
assumption.
ColR.
Qed.
End T8_5.
Require Export ColR.
Ltac not_exist_hyp_comm A B := not_exist_hyp (A≠B);not_exist_hyp (B≠A).
Ltac not_exist_hyp2 A B C D := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D].
Ltac not_exist_hyp3 A B C D E F := first [not_exist_hyp_comm A B | not_exist_hyp_comm C D | not_exist_hyp_comm E F].
Ltac not_exist_hyp_perm_col A B C := not_exist_hyp (¬ Col A B C); not_exist_hyp (¬ Col A C B);
not_exist_hyp (¬ Col B A C); not_exist_hyp (¬ Col B C A);
not_exist_hyp (¬ Col C A B); not_exist_hyp (¬ Col C B A).
Ltac finish := match goal with
| |- Col ?A ?B ?C ⇒ Col
| |- ¬ Col ?A ?B ?C ⇒ Col
| |- Cong ?A ?B ?C ?D ⇒ Cong
| |- is_midpoint ?A ?B ?C ⇒ Midpoint
| |- ?A<>?B ⇒ apply swap_diff;assumption
| |- _ ⇒ try assumption
end.
Ltac assert_all_diffs_by_cases :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ not_exist_hyp_comm A B;induction (eq_dec_points A B);[treat_equalities;solve [finish] |idtac]
end.
Ltac assert_cols :=
repeat
match goal with
| H:Bet ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
| H:is_midpoint ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := midpoint_col X2 X1 X3 H)
| H:out ?X1 ?X2 ?X3 |- _ ⇒
not_exist_hyp (Col X1 X2 X3);let N := fresh in assert (N := out_col X1 X2 X3 H)
end.
Ltac assert_bet :=
repeat
match goal with
| H:is_midpoint ?B ?A ?C |- _ ⇒ let T := fresh in not_exist_hyp (Bet A B C); assert (T := midpoint_bet A B C H)
end.
Ltac clean_reap_hyps :=
repeat
match goal with
| H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?C ?B |- _ ⇒ clear H2
| H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?B ?C |- _ ⇒ clear H2
| H:(¬Col ?A ?B ?C), H2 : ¬Col ?A ?B ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ ⇒ clear H2
| H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ ⇒ clear H2
| H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ ⇒ clear H2
| H:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ ⇒ clear H2
| H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ ⇒ clear H2
| H:(?A<>?B), H2 : (?B<>?A) |- _ ⇒ clear H2
| H:(?A<>?B), H2 : (?A<>?B) |- _ ⇒ clear H2
end.
Ltac assert_diffs :=
repeat
match goal with
| H:(¬Col ?X1 ?X2 ?X3) |- _ ⇒
let h := fresh in
not_exist_hyp3 X1 X2 X1 X3 X2 X3;
assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?A ≠ ?B |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?B ≠ ?A |-_ ⇒
let T:= fresh in (not_exist_hyp_comm C D);
assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?C ≠ ?D |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
| H:Cong ?A ?B ?C ?D, H2 : ?D ≠ ?C |-_ ⇒
let T:= fresh in (not_exist_hyp_comm A B);
assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?A<>?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?B<>?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B I A);
assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?I<>?A |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?A<>?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I B A B);
assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?I<>?B |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B H2 H);
decompose [and] T;clear T;clean_reap_hyps
| H:is_midpoint ?I ?A ?B, H2 : ?B<>?I |- _ ⇒
let T:= fresh in (not_exist_hyp2 I A A B);
assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
decompose [and] T;clear T;clean_reap_hyps
| H:out ?A ?B ?C |- _ ⇒
let T:= fresh in (not_exist_hyp2 A B A C);
assert (T:= out_distinct A B C H);
decompose [and] T;clear T;clean_reap_hyps
end.
Ltac clean_trivial_hyps :=
repeat
match goal with
| H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ ⇒ clear H
| H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ ⇒ clear H
| H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ ⇒ clear H
| H:(Bet ?X1 ?X1 ?X2) |- _ ⇒ clear H
| H:(Bet ?X2 ?X1 ?X1) |- _ ⇒ clear H
| H:(Col ?X1 ?X1 ?X2) |- _ ⇒ clear H
| H:(Col ?X2 ?X1 ?X1) |- _ ⇒ clear H
| H:(Col ?X1 ?X2 ?X1) |- _ ⇒ clear H
| H:(is_midpoint ?X1 ?X1 ?X1) |- _ ⇒ clear H
end.
Ltac treat_equalities :=
try treat_equalities_aux;
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ ⇒
apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ ⇒
apply cong_identity in H;smart_subst X2
| H:(Bet ?X1 ?X2 ?X1) |- _ ⇒
apply between_identity in H;smart_subst X2
| H:(is_midpoint ?X ?Y ?Y) |- _ ⇒ apply l7_3 in H; smart_subst Y
| H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := between_egality A B C H H2);smart_subst A
| H : is_midpoint ?P ?A ?P1, H2 : is_midpoint ?P ?A ?P2 |- _ ⇒
let T := fresh in not_exist_hyp (P1=P2); assert (T := symmetric_point_unicity A P P1 P2 H H2);smart_subst P1
| H : is_midpoint ?A ?P ?X, H2 : is_midpoint ?A ?Q ?X |- _ ⇒
let T := fresh in not_exist_hyp (P=Q); assert (T := l7_9 P Q A X H H2);smart_subst P
| H : is_midpoint ?M ?A ?A |- _ ⇒
let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H);smart_subst M
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P ?P' |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2);smart_subst A
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P' ?P |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17_bis P P' A B H H2);smart_subst A
| H : is_midpoint ?A ?B ?A |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H);smart_subst A
| H : is_midpoint ?A ?A ?B |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H);smart_subst A
end.
Ltac ColR :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
treat_equalities; Col_refl tpoint col.
Ltac search_contradiction :=
match goal with
| H: ?A ≠ ?A |- _ ⇒ exfalso;apply H;reflexivity
| H: ¬ Col ?A ?B ?C |- _ ⇒ exfalso;apply H;ColR
end.
Ltac show_distinct' X Y :=
assert (X≠Y);
[intro;treat_equalities; (solve [search_contradiction])|idtac].
Ltac assert_all_diffs_by_contradiction :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ not_exist_hyp_comm A B;show_distinct' A B
end.
Ltac update_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
update_cols_gen tpoint col.
Ltac deduce_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
treat_equalities; deduce_cols_hide_gen tpoint col.
Ltac cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
cols_gen tpoint col.
Ltac tag_hyps :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
tag_hyps_gen tpoint col.
Ltac untag_hyps :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
untag_hyps_gen tpoint col.
Ltac clear_cols :=
let tpoint := constr:(Tpoint) in
let col := constr:(Col) in
clear_cols_gen tpoint col.
Ltac smart_subst' := update_cols;clean.
Ltac treat_equalities_aux' :=
match goal with
| H:(?X1 = ?X2) |- _ ⇒ smart_subst'
end.
Ltac treat_equalities' :=
try treat_equalities_aux';
repeat
match goal with
| H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ ⇒
apply cong_symmetry in H; apply cong_identity in H; smart_subst'
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ ⇒
apply cong_identity in H; smart_subst'
| H:(Bet ?X1 ?X2 ?X1) |- _ ⇒
apply between_identity in H; smart_subst'
| H:(is_midpoint ?X ?Y ?Y) |- _ ⇒ apply l7_3 in H; smart_subst'
| H : Bet ?A ?B ?C, H2 : Bet ?B ?A ?C |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T : between_egality A B C H H2); smart_subst'
| H : is_midpoint ?P ?A ?P1, H2 : is_midpoint ?P ?A ?P2 |- _ ⇒
let T := fresh in not_exist_hyp (P1=P2); assert (T : symmetric_point_unicity A P P1 P2 H H2); smart_subst'
| H : is_midpoint ?A ?P ?X, H2 : is_midpoint ?A ?Q ?X |- _ ⇒
let T := fresh in not_exist_hyp (P=Q); assert (T : l7_9 P Q A X H H2); smart_subst'
| H : is_midpoint ?M ?A ?A |- _ ⇒
let T := fresh in not_exist_hyp (M=A); assert (T : l7_3 M A H); smart_subst'
| H : is_midpoint ?A ?P ?P', H2 : is_midpoint ?B ?P ?P' |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := l7_17 P P' A B H H2); smart_subst'
| H : is_midpoint ?A ?B ?A |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id_2 A B H); smart_subst'
| H : is_midpoint ?A ?A ?B |- _ ⇒
let T := fresh in not_exist_hyp (A=B); assert (T := is_midpoint_id A B H); smart_subst'
end.
Ltac search_contradiction' :=
match goal with
| H: ?A ≠ ?A |- _ ⇒ exfalso;apply H;reflexivity
| H: ¬ Col ?A ?B ?C |- _ ⇒ exfalso;apply H;cols
end.
Ltac show_distinct'' X Y :=
assert (X≠Y);
[intro; treat_equalities'; (solve [search_contradiction'])|idtac].
Ltac show_not_col X Y Z :=
assert (¬ Col X Y Z);
[intro; update_cols; (solve [search_contradiction'])|idtac].
Ltac assert_all_diffs_by_contradiction_aux :=
repeat match goal with
| A: Tpoint, B: Tpoint |- _ ⇒ untag_hyps; not_exist_hyp_comm A B; tag_hyps; show_distinct'' A B
end.
Ltac assert_all_not_cols_by_contradiction_aux :=
repeat match goal with
| A: Tpoint, B: Tpoint, C: Tpoint |- _ ⇒ untag_hyps; not_exist_hyp_perm_col A B C; tag_hyps; show_not_col A B C
end.
Ltac assert_all_diffs_by_contradiction' :=
deduce_cols; assert_all_diffs_by_contradiction_aux; untag_hyps; clear_cols.
Ltac assert_all_not_cols_by_contradiction :=
deduce_cols; assert_all_not_cols_by_contradiction_aux; untag_hyps; clear_cols.
Ltac assert_ndc_by_contradiction :=
assert_all_diffs_by_contradiction'; assert_all_not_cols_by_contradiction.
Section T8_1.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Definition Per := fun A B C ⇒ ∃ C', is_midpoint B C C' ∧ Cong A C A C'.
Lemma Per_dec : ∀ A B C, Per A B C ∨ ¬ Per A B C.
Proof.
intros.
unfold Per.
elim (symmetric_point_construction C B);intros C' HC'.
elim (Cong_dec A C A C');intro.
left.
∃ C'.
intuition.
right.
intro.
decompose [ex and] H0;clear H0.
assert (C'=x)
by (apply symmetric_point_unicity with C B;assumption).
subst.
intuition.
Qed.
Lemma l8_2 : ∀ A B C, Per A B C → Per C B A.
Proof.
unfold Per.
intros.
ex_and H C'.
assert (∃ A', is_midpoint B A A').
apply symmetric_point_construction.
ex_and H1 A'.
∃ A'.
split.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply H0.
eapply l7_13.
apply H.
apply l7_2.
assumption.
Qed.
End T8_1.
Hint Resolve l8_2 : perp.
Ltac Perp := auto with perp.
Section T8_2.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma Per_cases :
∀ A B C,
Per A B C ∨ Per C B A →
Per A B C.
Proof.
intros.
decompose [or] H;Perp.
Qed.
Lemma Per_perm :
∀ A B C,
Per A B C →
Per A B C ∧ Per C B A.
Proof.
intros.
split; Perp.
Qed.
Lemma l8_3 : ∀ A B C A',
Per A B C → A≠B → Col B A A' → Per A' B C.
Proof.
unfold Per.
intros.
ex_and H C'.
∃ C'.
split.
assumption.
eapply l4_17 with A B;Cong;Col.
unfold is_midpoint in H.
spliter.
Cong.
Qed.
Lemma l8_4 : ∀ A B C C', Per A B C → is_midpoint B C C' → Per A B C'.
Proof.
unfold Per.
intros.
ex_and H B'.
∃ C.
split.
apply l7_2.
assumption.
assert (B' = C')
by (eapply symmetric_point_unicity;eauto).
subst B'.
Cong.
Qed.
Lemma l8_5 : ∀ A B, Per A B B.
Proof.
unfold Per.
intros.
∃ B.
split.
apply l7_3_2.
Cong.
Qed.
Lemma l8_6 : ∀ A B C A', Per A B C → Per A' B C → Bet A C A' → B=C.
Proof.
unfold Per.
intros.
ex_and H C'.
ex_and H0 C''.
assert (C'=C'')
by (eapply symmetric_point_unicity;eauto).
subst C''.
assert (C = C')
by (eapply l4_19;eauto).
subst C'.
apply l7_3.
assumption.
Qed.
End T8_2.
Hint Resolve l8_5 : perp.
Ltac let_symmetric C P A :=
let id1:=fresh in (assert (id1:(∃ A', is_midpoint P A A'));
[apply symmetric_point_construction|ex_and id1 C]).
Ltac symmetric B' A B :=
assert(sp:= symmetric_point_construction B A); ex_and sp B'.
Section T8_3.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma l8_7 : ∀ A B C, Per A B C → Per A C B → B=C.
Proof.
intros.
unfold Per in H.
ex_and H C'.
symmetric A' C A.
induction (eq_dec_points B C).
assumption.
assert (Per C' C A).
eapply l8_3.
eapply l8_2.
apply H0.
assumption.
unfold is_midpoint in H.
spliter.
unfold Col.
left.
assumption.
assert (Cong A C' A' C').
unfold Per in H4.
ex_and H4 Z.
assert (A' = Z)
by (eapply (symmetric_point_unicity A C A');auto).
subst Z.
Cong.
unfold is_midpoint in ×.
spliter.
assert (Cong A' C A' C').
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H6.
eapply cong_transitivity.
apply cong_commutativity.
apply H1.
apply cong_left_commutativity.
assumption.
assert (Per A' B C).
unfold Per.
∃ C'.
unfold is_midpoint.
repeat split;auto.
eapply l8_6.
apply H9.
unfold Per.
∃ C'.
split.
unfold is_midpoint;auto.
apply H1.
Between.
Qed.
Lemma l8_8 : ∀ A B, Per A B A → A=B.
Proof.
intros.
apply l8_7 with A.
apply l8_2.
apply l8_5.
assumption.
Qed.
Lemma l8_9 : ∀ A B C, Per A B C → Col A B C → A=B ∨ C=B.
Proof.
intros.
elim (eq_dec_points A B);intro.
tauto.
right.
eapply l8_7.
eapply l8_2.
eapply l8_5.
apply l8_3 with A; Col.
Qed.
Lemma l8_10 : ∀ A B C A' B' C', Per A B C → Cong_3 A B C A' B' C' → Per A' B' C'.
Proof.
unfold Per.
intros.
ex_and H D.
prolong C' B' D' B' C'.
∃ D'.
split.
unfold is_midpoint.
split.
assumption.
Cong.
unfold Cong_3, is_midpoint in ×.
spliter.
induction (eq_dec_points C B).
treat_equalities;Cong.
assert(OFSC C B D A C' B' D' A').
unfold OFSC.
repeat split.
assumption.
assumption.
Cong.
eapply cong_transitivity.
apply cong_symmetry.
apply H4.
eapply cong_transitivity.
apply cong_commutativity.
apply H6.
Cong.
Cong.
Cong.
assert (Cong D A D' A').
eapply five_segments_with_def.
apply H8.
assumption.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
eapply cong_transitivity.
apply H1.
Cong.
Qed.
Definition Perp_in := fun X A B C D ⇒
A≠B ∧ C≠D ∧ Col X A B ∧ Col X C D ∧ (∀ U V, Col U A B → Col V C D → Per U X V).
Lemma col_col_per_per : ∀ A X C U V,
A≠X → C≠X →
Col U A X →
Col V C X →
Per A X C →
Per U X V.
Proof.
intros.
assert (Per U X C)
by (apply (l8_3 A X C U);Col).
apply l8_2 in H4.
apply l8_2 .
apply (l8_3 C X U V);Col.
Qed.
Lemma Perp_in_dec : ∀ X A B C D, Perp_in X A B C D ∨ ¬ Perp_in X A B C D.
Proof.
intros.
unfold Perp_in.
elim (eq_dec_points A B);intro;
elim (eq_dec_points C D);intro;
elim (Col_dec X A B);intro;
elim (Col_dec X C D);intro; try
tauto.
elim (eq_dec_points B X);intro;
elim (eq_dec_points D X);intro;subst;treat_equalities.
elim (Per_dec A X C);intro.
left;repeat split;Col;intros; apply col_col_per_per with A C;Col.
right;intro;spliter;apply H3;apply H8;Col.
elim (Per_dec A X D);intro.
left;repeat split;Col;intros; apply col_col_per_per with A D;Col;ColR.
right;intro;spliter;apply H3;apply H9;Col.
elim (Per_dec B X C);intro.
left;repeat split;Col;intros; apply col_col_per_per with B C;Col;ColR.
right;intro;spliter;apply H4;apply H9;Col.
elim (Per_dec B X D);intro.
left;repeat split;Col;intros; apply col_col_per_per with B D;Col;ColR.
right;intro;spliter;apply H5;apply H10;Col.
Qed.
Definition Perp := fun A B C D ⇒ ∃ X, Perp_in X A B C D.
Lemma perp_distinct : ∀ A B C D, Perp A B C D → A ≠ B ∧ C ≠ D.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.
Lemma l8_12 : ∀ A B C D X, Perp_in X A B C D → Perp_in X C D A B.
Proof.
unfold Perp_in.
intros.
spliter.
repeat split;try assumption.
intros;eapply l8_2;eauto.
Qed.
Lemma l4_3_1 : ∀ A B C A' B' C',
Bet A B C → Bet A' B' C' → Cong A B A' B' → Cong A C A' C' → Cong B C B' C'.
Proof.
intros.
apply cong_commutativity.
eapply l4_3;eBetween;eCong.
Qed.
Lemma per_col : ∀ A B C D,
B ≠ C → Per A B C → Col B C D → Per A B D.
Proof.
unfold Per.
intros.
ex_and H0 C'.
prolong D B D' D B.
∃ D'.
assert (is_midpoint B C C').
apply H0.
induction H5.
assert (is_midpoint B D D') by
(unfold is_midpoint;split;Cong).
assert (is_midpoint B D D').
apply H7.
induction H8.
repeat split.
assumption.
Cong.
unfold Col in H1.
induction H1.
assert (Bet B C' D').
eapply l7_15.
eapply l7_3_2.
apply H0.
apply H7.
assumption.
assert (Cong C D C' D').
eapply l4_3_1.
apply H1.
apply H10.
Cong.
Cong.
assert(OFSC B C D A B C' D' A)
by (unfold OFSC;repeat split;Cong).
apply cong_commutativity.
eauto using five_segments_with_def.
induction H1.
assert (Bet C' D' B).
eapply l7_15.
apply H0.
apply H7.
apply l7_3_2.
assumption.
assert (Cong C D C' D')
by (eapply l4_3 with B B;Between;Cong).
assert(IFSC B D C A B D' C' A)
by (unfold IFSC;repeat split;Between;Cong).
apply cong_commutativity.
eauto using l4_2.
assert (Bet D' B C').
eapply l7_15.
apply H7.
eapply l7_3_2.
apply H0.
assumption.
assert (Cong C D C' D')
by (eapply l2_11 with B B;Between;Cong).
assert(OFSC C B D A C' B D' A)
by (unfold OFSC;repeat split;Between;Cong).
apply cong_commutativity.
eauto using five_segments_with_def.
Qed.
Lemma l8_13_2 : ∀ A B C D X,
A ≠ B → C ≠ D → Col X A B → Col X C D →
(∃ U, ∃ V :Tpoint, Col U A B ∧ Col V C D ∧ U≠X ∧ V≠X ∧ Per U X V) →
Perp_in X A B C D.
Proof.
intros.
ex_and H3 U.
ex_and H4 V.
unfold Perp_in.
repeat split;try assumption.
intros.
assert (Per V X U0).
eapply l8_2.
eapply l8_3.
apply H7.
assumption.
eapply col3.
apply H.
Col.
Col.
Col.
eapply per_col.
2:eapply l8_2.
2:apply H10.
auto.
eapply col3.
apply H0.
Col.
Col.
Col.
Qed.
Definition DistLn := fun A B C D ⇒
(∃ X, Col X A B ∧ ¬Col X C D) ∨ (∃ X, ¬ Col X A B ∧ Col X C D).
Lemma perBAB : ∀ A B, Per B A B → A = B.
Proof.
intros.
eapply l8_7.
apply H.
eapply l8_2.
apply l8_5.
Qed.
Lemma l8_14_1 : ∀ A B, ¬ Perp A B A B.
Proof.
intros.
unfold Perp.
intro.
ex_and H X.
unfold Perp_in in H0.
spliter.
assert (Per A X A).
apply H3.
Col.
Col.
assert (A = X).
eapply l8_7.
2: apply H4.
apply l8_2.
apply l8_5.
assert (Per B X B)
by (apply H3;Col).
assert (B = X).
eapply l8_7 with B.
2: apply H6.
apply l8_2.
apply l8_5.
apply H0.
congruence.
Qed.
Lemma l8_14_2_1a : ∀ X A B C D, Perp_in X A B C D → Perp A B C D.
Proof.
intros.
unfold Perp.
∃ X.
assumption.
Qed.
Lemma perp_in_distinct : ∀ X A B C D , Perp_in X A B C D → A ≠ B ∧ C ≠ D.
Proof.
intros.
apply l8_14_2_1a in H.
apply perp_distinct.
assumption.
Qed.
Lemma l8_14_2_1b : ∀ X A B C D Y, Perp_in X A B C D → Col Y A B → Col Y C D → X=Y.
Proof.
intros.
unfold Perp_in in H.
spliter.
eapply (H5 Y Y) in H1.
2:assumption.
apply perBAB.
assumption.
Qed.
Lemma l8_14_2_1b_bis : ∀ A B C D X, Perp A B C D → Col X A B → Col X C D → Perp_in X A B C D.
Proof.
intros.
unfold Perp in H.
ex_and H Y.
assert (Y = X)
by (eapply (l8_14_2_1b Y _ _ _ _ X) in H2;assumption).
subst Y.
assumption.
Qed.
Lemma l8_14_2_2 : ∀ X A B C D,
Perp A B C D → (∀ Y, Col Y A B → Col Y C D → X=Y) → Perp_in X A B C D.
Proof.
intros.
eapply l8_14_2_1b_bis.
assumption.
unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D) by assumption.
apply (H0 Y H2) in H3.
subst Y.
assumption.
unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D).
assumption.
apply (H0 Y H2) in H3.
subst Y.
assumption.
Qed.
Lemma l8_14_3 : ∀ A B C D X Y, Perp_in X A B C D → Perp_in Y A B C D → X=Y.
Proof.
intros.
eapply l8_14_2_1b.
apply H.
unfold Perp_in in H0.
intuition.
eapply l8_12 in H0.
unfold Perp_in in H0.
intuition.
Qed.
Lemma l8_15_1 : ∀ A B C X, A≠B → Col A B X → Perp A B C X → Perp_in X A B C X.
Proof.
intros.
eapply l8_14_2_1b_bis;Col.
Qed.
Lemma l8_15_2 : ∀ A B C X, A≠B → Col A B X → Perp_in X A B C X → Perp A B C X.
Proof.
intros.
eapply l8_14_2_1a.
apply H1.
Qed.
Lemma perp_in_per : ∀ A B C, Perp_in B A B B C→ Per A B C.
Proof.
intros.
unfold Perp_in in H.
spliter.
apply H3;Col.
Qed.
Lemma perp_sym : ∀ A B C D, Perp A B C D → Perp C D A B.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
apply l8_12.
assumption.
Qed.
Lemma perp_col0 : ∀ A B C D X Y, Perp A B C D → X ≠ Y → Col A B X → Col A B Y → Perp C D X Y.
Proof.
unfold Perp.
intros.
ex_and H X0.
∃ X0.
unfold Perp_in in ×.
spliter.
repeat split.
assumption.
assumption.
assumption.
eapply col3.
apply H.
Col.
assumption.
assumption.
intros.
eapply l8_2.
apply H6.
2:assumption.
assert(Col A X Y).
eapply col3 with A B;Col.
assert (Col B X Y).
eapply col3 with A B;Col.
eapply col3 with X Y;Col.
Qed.
Lemma l8_16_1 : ∀ A B C U X,
A≠B → Col A B X → Col A B U → U≠X → Perp A B C X → ¬ Col A B C ∧ Per C X U.
Proof.
intros.
split.
intro.
assert (Perp_in X A B C X).
eapply l8_15_1.
assumption.
assumption.
assumption.
assert (X = U).
eapply l8_14_2_1b.
apply H5.
Col.
eapply col3 with A B;Col.
intuition.
apply l8_14_2_1b_bis with C X U X;try Col.
assert (Col A X U).
eapply (col3 A B);Col.
eapply perp_col0 with A B;Col.
Qed.
Lemma per_perp_in : ∀ A B C, A ≠ B → B ≠ C → Per A B C → Perp_in B A B B C.
Proof.
intros.
unfold Perp.
repeat split.
assumption.
assumption.
Col.
Col.
intros.
eapply per_col.
apply H0.
eapply l8_2.
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H4.
apply l8_2.
assumption.
Col.
Col.
Qed.
Lemma per_perp : ∀ A B C, A ≠ B → B ≠ C → Per A B C → Perp A B B C.
Proof.
intros.
apply per_perp_in in H1.
eapply l8_14_2_1a with B;assumption.
assumption.
assumption.
Qed.
Lemma perp_left_comm : ∀ A B C D, Perp A B C D → Perp B A C D.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
unfold Perp_in in ×.
intuition.
Qed.
Lemma perp_right_comm : ∀ A B C D, Perp A B C D → Perp A B D C.
Proof.
unfold Perp.
intros.
ex_and H X.
∃ X.
unfold Perp_in in ×.
intuition.
Qed.
Lemma perp_comm : ∀ A B C D, Perp A B C D → Perp B A D C.
Proof.
intros.
apply perp_left_comm.
apply perp_right_comm.
assumption.
Qed.
Lemma perp_in_sym :
∀ A B C D X,
Perp_in X A B C D → Perp_in X C D A B.
Proof.
unfold Perp_in.
intros.
spliter.
repeat split.
assumption.
assumption.
assumption.
assumption.
intros.
apply l8_2.
apply H3;assumption.
Qed.
Lemma perp_in_left_comm :
∀ A B C D X,
Perp_in X A B C D → Perp_in X B A C D.
Proof.
unfold Perp_in.
intuition.
Qed.
Lemma perp_in_right_comm : ∀ A B C D X, Perp_in X A B C D → Perp_in X A B D C.
Proof.
intros.
apply perp_in_sym.
apply perp_in_left_comm.
apply perp_in_sym.
assumption.
Qed.
Lemma perp_in_comm : ∀ A B C D X, Perp_in X A B C D → Perp_in X B A D C.
Proof.
intros.
apply perp_in_left_comm.
apply perp_in_right_comm.
assumption.
Qed.
End T8_3.
Hint Resolve perp_sym perp_left_comm perp_right_comm perp_comm per_perp_in
perp_in_per perp_in_left_comm perp_in_right_comm perp_in_comm perp_in_sym : perp.
Ltac double A B A' :=
assert (mp:= symmetric_point_construction A B);
elim mp; intros A' ; intro; clear mp.
Section T8_4.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma Perp_cases :
∀ A B C D,
Perp A B C D ∨ Perp B A C D ∨ Perp A B D C ∨ Perp B A D C ∨
Perp C D A B ∨ Perp C D B A ∨ Perp D C A B ∨ Perp D C B A →
Perp A B C D.
Proof.
intros.
decompose [or] H; Perp.
Qed.
Lemma Perp_perm :
∀ A B C D,
Perp A B C D →
Perp A B C D ∧ Perp B A C D ∧ Perp A B D C ∧ Perp B A D C ∧
Perp C D A B ∧ Perp C D B A ∧ Perp D C A B ∧ Perp D C B A.
Proof.
intros.
repeat split; Perp.
Qed.
Lemma Perp_in_cases :
∀ X A B C D,
Perp_in X A B C D ∨ Perp_in X B A C D ∨ Perp_in X A B D C ∨ Perp_in X B A D C ∨
Perp_in X C D A B ∨ Perp_in X C D B A ∨ Perp_in X D C A B ∨ Perp_in X D C B A →
Perp_in X A B C D.
Proof.
intros.
decompose [or] H; Perp.
Qed.
Lemma Perp_in_perm :
∀ X A B C D,
Perp_in X A B C D →
Perp_in X A B C D ∧ Perp_in X B A C D ∧ Perp_in X A B D C ∧ Perp_in X B A D C ∧
Perp_in X C D A B ∧ Perp_in X C D B A ∧ Perp_in X D C A B ∧ Perp_in X D C B A.
Proof.
intros.
do 7 (split; Perp).
Qed.
Lemma l8_16_2 : ∀ A B C U X,
A≠B → Col A B X → Col A B U → U≠X → ¬ Col A B C → Per C X U → Perp A B C X.
Proof.
intros.
assert (C ≠ X).
intro.
subst X.
apply H3.
assumption.
unfold Perp.
∃ X.
eapply l8_13_2.
assumption.
assumption.
Col.
Col.
∃ U.
∃ C.
repeat split;
Col.
apply l8_2.
assumption.
Qed.
Lemma l8_18_unicity : ∀ A B C X Y,
¬ Col A B C → Col A B X → Perp A B C X → Col A B Y → Perp A B C Y → X=Y.
Proof.
intros.
show_distinct A B.
solve [intuition].
assert (Perp_in X A B C X)
by (eapply l8_15_1;assumption).
assert (Perp_in Y A B C Y)
by (eapply l8_15_1;assumption).
unfold Perp_in in ×.
spliter.
apply l8_7 with C;apply l8_2;[apply H14 |apply H10];Col.
Qed.
Lemma distinct : ∀ A B X C C', ¬ Col A B C → Col A B X → is_midpoint X C C' → C ≠ C'.
Proof.
intros.
intro.
subst C'.
apply H.
unfold is_midpoint in H1.
spliter.
treat_equalities.
assumption.
Qed.
Lemma l8_20_1 : ∀ A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → Per B A P.
Proof.
intros.
double B A B'.
double D A D'.
double P A P'.
induction (eq_dec_points A B).
subst B.
unfold is_midpoint in H5.
spliter.
eapply l8_2.
eapply l8_5.
assert (Per B' B C).
eapply l8_3.
apply H.
assumption.
unfold Col.
left.
apply midpoint_bet.
assumption.
assert (Per B B' C').
eapply l8_10.
apply H7.
unfold Cong_3.
repeat split.
apply cong_pseudo_reflexivity.
eapply l7_13.
unfold is_midpoint.
split.
apply H3.
apply midpoint_cong.
assumption.
assumption.
eapply l7_13.
apply l7_2.
apply H3.
assumption.
assert(is_midpoint B' D' C').
eapply symmetry_preserves_midpoint.
apply H4.
apply H3.
apply l7_2.
apply H1.
assumption.
assert(is_midpoint P' C D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H5.
apply H4.
assumption.
unfold Per.
∃ P'.
split.
assumption.
unfold Per in H7.
ex_and H7 D''.
assert (D''= D).
eapply symmetric_point_unicity.
apply H7.
apply l7_2.
assumption.
subst D''.
unfold Per in H8.
ex_and H8 D''.
assert (D' = D'').
eapply symmetric_point_unicity.
apply l7_2.
apply H9.
assumption.
subst D''.
assert (is_midpoint P C' D).
eapply symmetry_preserves_midpoint.
apply l7_2.
apply H1.
apply l7_2.
apply H5.
apply l7_2.
apply H4.
assumption.
assert (Cong C D C' D').
eapply l7_13.
apply H1.
apply l7_2.
assumption.
assert (Cong C' D C D').
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.
assert(Cong P D P' D').
eapply l7_13.
apply l7_2.
apply H5.
apply l7_2.
assumption.
assert (Cong P D P' C).
eapply cong_transitivity.
apply H16.
unfold is_midpoint in H10.
spliter.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
assert (IFSC C' P D B D' P' C B).
unfold IFSC.
repeat split.
apply midpoint_bet.
assumption.
apply midpoint_bet.
apply l7_2.
assumption.
apply cong_right_commutativity.
assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_right_commutativity.
apply midpoint_cong.
assumption.
assert (Cong P B P' B).
eapply l4_2.
apply H18.
apply cong_commutativity.
assumption.
Qed.
Lemma l8_20_2 : ∀ A B C C' D P,
Per A B C → is_midpoint P C' D → is_midpoint A C' C → is_midpoint B D C → B≠C → A≠P.
Proof.
intros.
intro.
subst P.
assert (C = D).
eapply symmetric_point_unicity.
apply H1.
assumption.
subst D.
assert (B = C).
apply l7_3.
assumption.
subst C.
absurde.
Qed.
Lemma perp_col1 : ∀ A B C D X,
C ≠ X → Perp A B C D → Col C D X → Perp A B C X.
Proof.
intros.
assert (T:=perp_distinct A B C D H0).
spliter.
unfold Perp in ×.
ex_and H0 P.
∃ P.
unfold Perp_in in ×.
spliter.
repeat split.
assumption.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_2.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_3.
assumption.
intros.
apply H7.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
apply col_permutation_5.
assumption.
apply col_permutation_1.
assumption.
Qed.
Lemma l8_18_existence : ∀ A B C, ¬ Col A B C → ∃ X, Col A B X ∧ Perp A B C X.
Proof.
intros.
prolong B A Y A C.
assert (∃ P, is_midpoint P C Y)
by (apply l7_25 with A;Cong).
ex_and H2 P.
assert (Per A P Y)
by (unfold Per;∃ C;auto using l7_2).
prolong A Y Z Y P.
prolong P Y Q Y A.
prolong Q Z Q' Q Z.
assert (is_midpoint Z Q Q')
by (unfold is_midpoint;Cong).
prolong Q' Y C' Y C.
assert (∃ X, is_midpoint X C C')
by (apply l7_25 with Y;Cong).
ex_and H13 X.
assert (OFSC A Y Z Q Q Y P A) by
(unfold OFSC;repeat split;Between;Cong).
show_distinct A Y.
intuition.
assert (Cong Z Q P A)
by (eauto using five_segments_with_def).
assert (Cong_3 A P Y Q Z Y)
by (unfold Cong_3;Cong).
assert (Per Q Z Y)
by (eauto using l8_10).
assert (Per Y Z Q) by eauto using l8_2.
show_distinct P Y.
unfold is_midpoint in ×.
spliter.
treat_equalities.
assert_cols.
Col5.
unfold Per in H19.
ex_and H19 Q''.
assert (Q' = Q'').
eapply symmetric_point_unicity.
apply H10.
assumption.
subst Q''.
assert (hy:Bet Z Y X).
apply (l7_22 Q C Q' C' Y Z X);Cong.
assert (T:=outer_transitivity_between2 C P Y Q).
assert_bet.
apply between_symmetry.
apply T;Between.
show_distinct Q Y.
intuition.
assert (Per Y X C)
by (unfold Per;∃ C';Cong).
assert_diffs.
assert (Col P Y Q).
unfold Col.
left.
assumption.
assert(Col P Y C).
unfold is_midpoint in H3.
spliter.
unfold Col.
right; right.
assumption.
assert (Col P Q C) by ColR.
assert (Col Y Q C) by ColR.
assert (Col A Y B)
by (assert_cols;Col).
assert (Col A Y Z)
by (assert_cols;Col).
assert (Col A B Z)
by ColR.
assert (Col Y B Z)
by ColR.
assert (Col Q Y P)
by Col.
assert(Q ≠ C).
intro.
subst Q.
unfold is_midpoint in ×.
spliter.
apply H.
assert (Bet B Y Z)
by (apply outer_transitivity_between2 with A;auto).
apply between_symmetry in H3.
assert (Y = P).
eapply between_egality.
apply H3.
assumption.
treat_equalities.
intuition.
assert (Col Y B Z).
eapply col_transitivity_2.
apply H15.
assumption.
assumption.
assert (Y ≠ Q').
intro.
treat_equalities.
absurde.
assert (Col Y Q' C')
by (assert_cols;Col).
assert (Q ≠ Q').
intro.
unfold OFSC, Cong_3 in ×.
spliter.
treat_equalities.
apply H.
ColR.
assert (C ≠ C').
intro.
subst C'.
apply l7_3 in H14.
subst X.
assert (Col Z Q Q')
by (assert_cols;ColR).
assert (Y ≠ Z).
intro.
subst Z.
unfold OFSC, Cong_3, is_midpoint in ×.
spliter.
treat_equalities.
intuition.
apply H.
ColR.
assert(OFSC Q Y C Z Q' Y C' Z).
unfold OFSC.
repeat split;Between;Cong.
unfold OFSC, is_midpoint in ×.
spliter.
eapply outer_transitivity_between with P;Between;Cong.
assert (Cong C Z C' Z)
by (eauto using five_segments_with_def).
assert (Col Z Y X)
by (assert_cols;Col).
assert (Y ≠ Z).
intro.
treat_equalities.
intuition.
assert(C ≠ X).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in ×.
spliter.
treat_equalities.
intuition.
assert(X ≠ Y).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in ×.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
show_distinct C' Y.
intuition.
assert (Col Y C' P ).
eapply col_transitivity_1 with C.
intuition.
unfold Col.
right;right.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
show_distinct P Q.
intuition.
assert (Col Y P Q').
eapply col_transitivity_2.
apply H10.
apply col_permutation_4.
assumption.
apply col_permutation_2.
assumption.
assert (Col Y Q Q').
eapply col_transitivity_2.
apply H20.
assumption.
apply col_permutation_4.
assumption.
assert (Col Q Y Z)
by (assert_cols;ColR).
assert (Col Y Z C)
by (assert_bet;assert_cols;ColR).
apply H.
ColR.
assert (Perp_in X Y Z C X).
eapply l8_13_2;Col.
∃ Y.
∃ C.
repeat split;Col.
assert (Col A B X) by ColR.
∃ X.
split.
assumption.
unfold Perp.
∃ X.
unfold Perp_in.
repeat split;Col.
intros.
unfold Perp_in in H52.
spliter.
apply H59;ColR.
Qed.
Lemma l8_21_aux : ∀ A B C,
A≠ B → ¬ Col A B C → ∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet C T P.
Proof.
intros.
assert (∃ X : Tpoint, Col A B X ∧ Perp A B C X).
eapply l8_18_existence.
assumption.
ex_and H1 X.
assert (Perp_in X A B C X).
eapply l8_15_1;
assumption.
assert (Per A X C).
unfold Perp_in in H3.
spliter.
apply H7.
apply col_trivial_1.
apply col_trivial_1.
assert(HH:= H4).
unfold Per in H4.
ex_and H4 C'.
double C A C''.
assert (∃ P, is_midpoint P C' C'').
eapply l7_25.
unfold is_midpoint in ×.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
apply cong_left_commutativity.
assumption;
spliter.
ex_elim H7 P.
assert (Per X A P).
eapply l8_20_1.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
apply H6.
apply l7_2.
assumption.
assert (X ≠ C).
intro.
subst C.
apply H0.
assumption.
assert (A ≠ P).
eapply l8_20_2.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
assumption.
apply l7_2.
assumption.
assumption.
assert (∃ T, Bet P T C ∧ Bet A T X).
eapply l3_17.
apply midpoint_bet.
apply l7_2.
apply H6.
apply midpoint_bet.
apply l7_2.
apply H4.
apply midpoint_bet.
apply l7_2.
apply H8.
ex_and H11 T.
induction (eq_dec_points A X).
subst X.
∃ P.
∃ T.
apply between_identity in H12.
subst T.
assert (C'= C'').
eapply symmetric_point_unicity.
apply H4.
assumption.
subst C''.
apply l7_3 in H8.
subst P.
assert (Col A C C')
by (assert_cols;ColR).
repeat split;Col;Between.
apply perp_col0 with C A;auto using perp_sym;assert_cols;Col.
∃ P.
∃ T.
repeat split.
unfold Perp.
∃ A.
unfold Perp_in.
repeat split.
assumption.
auto.
apply col_trivial_1.
apply col_trivial_3.
unfold Perp_in in H3.
spliter.
intros.
eapply per_col in H7.
apply l8_2 in H7.
eapply per_col in H7.
eapply l8_2 in H7.
apply H7.
assumption.
ColR.
assumption.
ColR.
assert_cols;ColR.
Between.
Qed.
Lemma l8_21 : ∀ A B C,
A≠ B → ∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet C T P.
Proof.
intros.
induction(Col_dec A B C).
assert (∃ C', ¬ Col A B C').
eapply l6_25.
assumption.
ex_elim H1 C'.
assert ( ∃ P : Tpoint,
(∃ T : Tpoint, Perp A B P A ∧ Col A B T ∧ Bet C' T P)).
eapply l8_21_aux.
assumption.
assumption.
ex_elim H1 P.
ex_and H3 T.
∃ P.
∃ C.
repeat split.
assumption.
assumption.
apply between_trivial2.
eapply l8_21_aux.
assumption.
assumption.
Qed.
Lemma perp_in_col : ∀ A B C D X, Perp_in X A B C D → Col A B X ∧ Col C D X.
Proof.
unfold Perp_in.
intuition.
Qed.
Lemma perp_perp_in : ∀ A B C, Perp A B C A → Perp_in A A B C A.
Proof.
intros.
apply l8_15_1.
unfold Perp in H.
ex_and H X.
unfold Perp_in in H0.
intuition.
apply col_trivial_3.
assumption.
Qed.
Lemma perp_per_1 : ∀ A B C, A≠B → Perp A B C A → Per B A C.
Proof.
intros.
assert (Perp_in A A B C A).
apply perp_perp_in.
assumption.
unfold Perp_in in H1.
spliter.
apply H5.
apply col_trivial_3.
apply col_trivial_1.
Qed.
Lemma perp_per_2 : ∀ A B C, A≠B → Perp A B A C → Per B A C.
Proof.
intros.
apply perp_right_comm in H0.
apply perp_per_1;
assumption.
Qed.
Lemma perp_col : ∀ A B C D E, A≠E → Perp A B C D → Col A B E → Perp A E C D.
Proof.
intros.
apply perp_sym.
eapply perp_col0.
apply H0.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma perp_col2 : ∀ A B C D X Y,
Perp A B X Y →
C ≠ D → Col A B C → Col A B D → Perp C D X Y.
Proof.
intros.
assert(HH:=H).
apply perp_distinct in HH.
spliter.
induction (eq_dec_points A C).
subst A.
eapply perp_col.
assumption.
apply H.
assumption.
assert(Perp A C X Y) by (eapply perp_col;eauto).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H6.
apply col_permutation_2;
eapply col_transitivity_1.
apply H3.
assumption.
assumption.
Qed.
Lemma perp_not_eq_1 : ∀ A B C D, Perp A B C D → A≠B.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.
Lemma perp_not_eq_2 : ∀ A B C D, Perp A B C D → C≠D.
Proof.
intros.
apply perp_sym in H.
eapply perp_not_eq_1.
apply H.
Qed.
Lemma le_bet : ∀ A B C D, le C D A B → ∃ X, Bet A X B ∧ Cong A X C D.
Proof.
intros.
unfold le in H.
ex_and H Y.
∃ Y;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.
unfold Col.
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;Cong.
Qed.
Lemma diff_per_diff : ∀ A B P R ,
A ≠ B → Cong A P B R → Per B A P → Per A B R → P ≠ R.
Proof.
intros.
intro.
subst.
assert (A = B).
eapply l8_7.
apply l8_2.
apply H1.
apply l8_2.
assumption.
intuition.
Qed.
Lemma per_not_colp : ∀ A B P R, A ≠ B → A ≠ P → B ≠ R → Per B A P → Per A B R → ¬Col P A R.
Proof.
intros.
intro.
assert (Perp A B P A).
apply perp_comm.
apply per_perp.
auto.
assumption.
assumption.
assert (Perp A B B R).
apply per_perp.
assumption.
assumption.
assumption.
assert (Per B A R).
eapply per_col.
apply H0.
assumption.
Col5.
apply l8_2 in H3.
apply l8_2 in H7.
assert (A = B).
eapply l8_7.
apply H7.
assumption.
contradiction.
Qed.
Lemma per_not_col : ∀ A B C, A ≠ B → B ≠ C → Per A B C → ¬Col A B C.
Proof.
intros.
intro.
unfold Per in H1.
ex_and H1 C'.
assert (C = C' ∨ is_midpoint A C C').
eapply l7_20.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H4.
Col5.
unfold Col.
left.
apply midpoint_bet.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H1.
apply H0.
assumption.
apply H.
eapply l7_17.
apply H4.
assumption.
Qed.
Lemma per_cong : ∀ A B P R X ,
A ≠ B → A ≠ P →
Per B A P → Per A B R →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B.
Proof.
intros.
assert (Per P A B).
apply l8_2.
assumption.
double B R Q.
assert (B ≠ R).
intro.
subst R.
apply cong_identity in H3.
subst P.
absurde.
assert (Per A B Q).
eapply per_col.
apply H8.
assumption.
unfold Col.
left.
apply midpoint_bet.
assumption.
assert (Per P A X).
eapply per_col.
apply H.
assumption.
assumption.
assert (B ≠ Q).
intro.
subst Q.
apply l7_3 in H7.
subst R.
absurde.
assert (Per R B X).
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H12.
apply l8_2.
assumption.
apply col_permutation_4.
assumption.
assert (X ≠ A).
intro.
subst X.
assert (¬Col P A R).
eapply per_not_colp.
apply H.
assumption.
assumption.
assumption.
assumption.
apply H13.
unfold Col.
left.
assumption.
double P A P'.
prolong P' X R' X R.
assert (∃ M, is_midpoint M R R').
eapply l7_25.
apply cong_symmetry.
apply H16.
ex_elim H17 M.
assert (Per X M R).
unfold Per.
∃ R'.
split.
assumption.
apply cong_symmetry.
assumption.
assert (Cong X P X P').
apply l8_2 in H10.
unfold Per in H10.
ex_and H10 P''.
assert (P'=P'').
eapply symmetric_point_unicity.
apply H14.
apply H10.
subst P''.
assumption.
assert (X ≠ P').
intro.
subst P'.
apply cong_identity in H19.
subst X.
apply l7_3 in H14.
subst P.
absurde.
assert (P ≠ P').
intro.
subst P'.
eapply l7_3 in H14.
subst P.
absurde.
assert(¬Col X P P').
intro.
assert(Col X P A).
eapply col3.
apply H21.
apply col_permutation_1.
assumption.
apply col_trivial_3.
unfold Col.
right;left.
apply between_symmetry.
apply midpoint_bet.
assumption.
apply col_permutation_1 in H23.
assert (P = A ∨ X = A).
eapply l8_9.
assumption.
assumption.
induction H24.
subst P.
absurde.
apply H13.
assumption.
assert (Bet A X M).
eapply l7_22.
5:apply H14.
5:apply H18.
assumption.
assumption.
assumption.
apply cong_symmetry.
assumption.
assert (X ≠ R).
intro.
treat_equalities.
apply perBAB in H12.
treat_equalities.
unfold is_midpoint in ×.
spliter.
treat_equalities.
intuition.
assert (X ≠ R').
intro.
subst R'.
apply cong_symmetry in H16.
apply cong_identity in H16.
apply H24.
assumption.
assert (M ≠ X).
intro.
subst M.
apply H22.
eapply col_transitivity_1.
apply H24.
unfold Col.
right; right.
assumption.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
apply midpoint_bet.
assumption.
unfold Col.
right; right.
assumption.
assert (M = B).
eapply (l8_18_unicity A X R).
intro.
assert (Col A B R).
eapply col_transitivity_1.
intro.
apply H13.
apply sym_equal.
apply H28.
apply col_permutation_5.
assumption.
assumption.
eapply per_not_col.
apply H;
apply H12.
apply H8.
assumption.
assumption.
unfold Col.
left.
assumption;
eapply col_transitivity_1.
apply per_perp in H17.
apply perp_comm.
eapply perp_col.
assumption.
apply H17.
unfold Col.
right;right.
assumption.
auto.
intro.
subst M.
apply (symmetric_point_unicity R R R R') in H18.
subst R'.
apply H22.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
assumption.
unfold Col.
right; right.
assumption.
eapply l7_3_2.
apply col_permutation_5.
assumption.
apply per_perp in H10.
apply perp_comm.
eapply perp_col.
apply H13.
apply perp_comm.
eapply perp_col.
intro.
apply H13.
apply sym_equal.
apply H27.
apply perp_right_comm.
apply per_perp in H2.
apply H2.
assumption.
assumption.
assumption.
apply col_trivial_2.
auto.
intro.
apply H13.
subst X.
reflexivity.
subst M.
assert(OFSC P X R P' P' X R' P).
unfold OFSC.
repeat split.
assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_symmetry.
assumption.
apply cong_pseudo_reflexivity.
apply cong_symmetry.
assumption.
assert (Cong R P' R' P).
eapply five_segments_with_def.
apply H27.
intro.
subst X.
apply H22.
apply col_trivial_1.
assert (IFSC P' A P R R' B R P).
unfold IFSC.
repeat split.
apply between_symmetry.
apply midpoint_bet.
assumption.
apply between_symmetry.
apply midpoint_bet.
assumption.
eapply l2_11.
apply between_symmetry.
apply midpoint_bet.
apply H14.
apply between_symmetry.
apply midpoint_bet.
apply H18.
eapply cong_transitivity.
apply midpoint_cong.
apply l7_2.
apply H14.
eapply cong_transitivity.
apply H3.
apply cong_commutativity.
apply midpoint_cong.
assumption.
assumption.
assumption.
Cong.
apply cong_pseudo_reflexivity.
eapply cong_right_commutativity.
eapply l4_2.
eapply H29.
Qed.
Lemma perp_cong : ∀ A B P R X,
A ≠ B → A ≠ P →
Perp A B P A → Perp A B R B →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B.
Proof.
intros.
apply (per_cong A B P R X).
assumption.
assumption.
apply perp_per_1.
assumption.
assumption.
eapply perp_per_1.
auto.
apply perp_left_comm;auto.
assumption.
assumption.
assumption.
Qed.
Lemma midpoint_existence_aux : ∀ A B P Q T,
A≠B → Perp A B Q B → Perp A B P A →
Col A B T → Bet Q T P → le A P B Q →
∃ X : Tpoint, is_midpoint X A B.
Proof.
intros.
unfold le in H4.
ex_and H4 R.
assert (∃ X, Bet T X B ∧ Bet R X P).
eapply inner_pasch.
apply between_symmetry.
apply H3.
auto.
ex_and H6 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H6.
subst X.
Col.
assert (Col B A X).
eapply col_transitivity_2.
apply H8.
apply col_permutation_3.
assumption.
apply col_permutation_5.
unfold Col.
left; assumption.
apply col_permutation_4.
assumption.
induction(Col_dec A B P).
assert (B=A ∨ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
assumption.
apply col_permutation_4.
assumption.
induction H10.
∃ A.
subst B.
eapply l7_3_2.
subst P.
treat_equalities.
apply perp_distinct in H1.
spliter.
absurde.
assert (B ≠ R).
intro.
subst R.
treat_equalities.
apply H9.
apply col_trivial_3.
assert (¬Col A B Q).
intro.
assert (A=B ∨ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
assumption.
assumption.
induction H12.
apply H.
assumption.
subst Q.
treat_equalities.
absurde.
assert (¬Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H10.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H11.
apply col_permutation_4.
assumption.
assert (P ≠ R).
intro.
subst R.
treat_equalities.
intuition.
induction (eq_dec_points A P).
subst P.
apply perp_distinct in H1.
spliter.
absurde.
assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply perp_sym.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.
apply between_symmetry in H7.
assert (Cong A R P B).
apply (perp_cong A B P R X);
assumption.
assert (is_midpoint X A B ∧ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H9.
apply col_permutation_5.
assumption.
assumption.
assumption.
intros.
apply cong_commutativity.
apply cong_symmetry.
apply cong_right_commutativity.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
spliter.
∃ X.
assumption.
Qed.
Lemma midpoint_existence : ∀ A B, ∃ X, is_midpoint X A B.
Proof.
intros.
induction (eq_dec_points A B).
subst B.
∃ A.
apply l7_3_2.
cut(∃ Q, Perp A B B Q).
intro.
ex_elim H0 Q.
cut(∃ P, ∃ T, Perp A B P A ∧ Col A B T ∧ Bet Q T P).
intros.
ex_elim H0 P.
ex_and H2 T.
assert (le A P B Q ∨ le B Q A P).
apply le_cases.
induction H4.
eapply midpoint_existence_aux.
assumption.
apply perp_right_comm.
apply H1.
apply H0.
apply H2.
assumption.
assumption.
assert (∃ X : Tpoint, is_midpoint X B A).
eapply (midpoint_existence_aux B A Q P T).
auto.
apply perp_left_comm.
assumption.
apply perp_comm.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
assumption.
ex_elim H5 X.
∃ X.
apply l7_2.
assumption.
eapply l8_21.
assumption.
assert (∃ P : Tpoint,
(∃ T : Tpoint, Perp B A P B ∧ Col B A T ∧ Bet A T P)) by
(apply (l8_21 B A);auto).
ex_elim H0 P.
ex_elim H1 T.
spliter.
∃ P.
apply perp_comm.
assumption.
Qed.
Lemma perp_in_id : ∀ A B C X, Perp_in X A B C A → X = A.
Proof.
intros.
assert (Perp A B C A).
unfold Perp.
∃ X.
assumption.
assert (A ≠ B ∧ C ≠ A).
apply perp_distinct.
assumption.
spliter.
assert (HH:=H0).
apply perp_perp_in in HH.
assert (l8_16_1:=l8_16_1 A B C B A).
assert (¬Col A B C ∧ Per C A B).
apply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
assumption.
spliter.
unfold Perp_in in H.
spliter.
eapply l8_18_unicity.
apply H3.
apply col_permutation_1.
assumption.
apply perp_sym.
eapply perp_col.
intro.
subst X.
assert (¬Col C A B).
apply per_not_col.
assumption.
assumption.
assumption.
apply H9.
assumption.
apply perp_sym.
apply H0.
apply col_permutation_1.
assumption.
apply col_trivial_3.
assumption.
Qed.
Lemma l8_22 : ∀ A B P R X ,
A ≠ B → A ≠ P →
Per B A P → Per A B R →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B ∧ is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
assert (Cong A R P B).
apply (per_cong A B P R X);
assumption.
split.
assumption.
assert (¬ Col B A P).
eapply per_not_col.
auto.
assumption.
assumption.
apply l7_21.
intro.
apply H7.
Col.
intro.
subst R.
eapply between_identity in H5.
subst X.
apply H7.
apply col_permutation_4.
assumption.
assumption.
Cong.
Col.
unfold Col.
left.
assumption.
Qed.
Lemma l8_22_bis : ∀ A B P R X,
A ≠ B → A ≠ P →
Perp A B P A → Perp A B R B →
Cong A P B R → Col A B X → Bet P X R →
Cong A R P B ∧ is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
apply l8_22.
assumption.
assumption.
apply perp_per_1.
assumption.
assumption.
apply perp_per_1.
auto.
apply perp_left_comm.
assumption.
assumption.
assumption.
assumption.
Qed.
Lemma perp_in_perp : ∀ A B C D X, Perp_in X A B C D → Perp A B C D.
Proof.
intros.
unfold Perp.
∃ X.
assumption.
Qed.
End T8_4.
Hint Resolve perp_col perp_perp_in perp_in_perp : perp.
Section T8_5.
Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.
Lemma perp_proj : ∀ A B C D, Perp A B C D → ¬Col A C D → ∃ X, Col A B X ∧ Perp A X C D.
Proof.
intros.
unfold Perp in H.
ex_and H X.
∃ X.
split.
unfold Perp_in in H1.
spliter.
apply col_permutation_1.
assumption.
eapply perp_col.
intro.
subst X.
unfold Perp_in in H1.
spliter.
apply H0.
assumption.
apply perp_in_perp in H1.
apply H1.
unfold Perp_in in H1.
spliter.
apply col_permutation_1.
assumption.
Qed.
Lemma l8_24 : ∀ A B P Q R T,
Perp P A A B →
Perp Q B A B →
Col A B T →
Bet P T Q →
Bet B R Q →
Cong A P B R →
∃ X, is_midpoint X A B ∧ is_midpoint X P R.
Proof.
intros.
unfold le in H4.
assert (∃ X, Bet T X B ∧ Bet R X P).
eapply inner_pasch.
apply H2.
assumption.
ex_and H5 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H5.
subst X.
apply col_trivial_2.
assert (Col T X B).
unfold Col.
left.
assumption.
apply col_permutation_4.
eapply col_transitivity_1.
intro.
apply H7.
apply sym_equal.
apply H9.
apply col_permutation_1.
assumption.
apply col_permutation_2.
assumption.
assert (A ≠ B).
apply perp_distinct in H.
spliter.
assumption.
assert (A ≠ P).
apply perp_distinct in H.
spliter.
auto.
induction(Col_dec A B P).
assert (B=A ∨ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
apply perp_sym.
assumption.
apply col_permutation_4.
assumption.
induction H11.
∃ A.
subst B.
absurde.
subst P.
absurde.
assert (B ≠ R).
intro.
subst R.
apply cong_identity in H4.
subst P.
absurde.
assert (Q ≠ B).
apply perp_distinct in H0.
spliter.
assumption.
assert (¬Col A B Q).
intro.
assert (A=B ∨ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
apply perp_sym.
assumption.
assumption.
induction H14.
contradiction.
subst Q.
absurde.
assert (¬Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H11.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H13.
apply col_permutation_4.
assumption.
assert (P ≠ R).
intro.
subst R.
apply between_identity in H6.
subst X.
contradiction.
induction (eq_dec_points A P).
subst P.
apply perp_distinct in H.
spliter.
absurde.
assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.
assert (Cong A R P B).
apply (perp_cong A B P R X).
assumption.
assumption.
apply perp_sym.
assumption.
assumption.
assumption.
assumption.
apply between_symmetry.
assumption.
intros.
assert (is_midpoint X A B ∧ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H10.
apply col_permutation_5.
assumption.
assumption.
assumption.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
∃ X.
assumption.
Qed.
Lemma perp_not_col2 : ∀ A B C D, Perp A B C D → ¬ Col A B C ∨ ¬ Col A B D.
Proof.
intros.
induction (Col_dec A B C).
right.
assert(Perp_in C A B C D).
apply l8_14_2_1b_bis; Col.
intro.
assert(Perp_in D A B C D).
apply l8_14_2_1b_bis; Col.
assert(C = D).
eapply l8_14_3.
apply H1.
assumption.
apply perp_not_eq_2 in H.
contradiction.
left.
assumption.
Qed.
Lemma ex_col2 : ∀ A B, ∃ C, Col A B C ∧ A ≠ C ∧ B ≠ C.
intros.
induction(eq_dec_points A B).
subst B.
assert(HH:=another_point A).
ex_and HH B.
∃ B.
split; Col.
prolong A B C A B.
∃ C.
split.
apply bet_col.
assumption.
split.
intro.
subst C.
apply between_identity in H0.
contradiction.
intro.
subst C.
apply cong_symmetry in H1.
apply cong_identity in H1.
contradiction.
Qed.
Lemma perp_in_col_perp_in : ∀ A B C D E P, C ≠ E → Col C D E → Perp_in P A B C D → Perp_in P A B C E.
intros.
unfold Perp_in in ×.
spliter.
repeat split; auto.
ColR.
intros.
apply H5.
assumption.
ColR.
Qed.
End T8_5.