Library exercises
Require Import triangle_midpoints_theorems.
Section Exercises.
Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Context `{InterDec:InterDecidability Tpoint Col}.
Lemma Per_mid_rectangle : ∀ A B C I J K,
A ≠ B →
B ≠ C →
Per B A C →
is_midpoint I B C →
is_midpoint J A C →
is_midpoint K A B →
Rectangle A J I K.
Proof.
intros.
assert_diffs.
assert_cols.
elim (eq_dec_points A C); intro; apply plg_per_rect.
treat_equalities.
assert (HM : ∃ M : Tpoint, is_midpoint M J I) by (apply midpoint_existence); decompose [ex] HM; repeat split; intuition; ∃ x; intuition.
treat_equalities; intuition.
assert( Par A B J I ∧ Par A C I K ∧ Par B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_cong; intuition).
spliter.
elim (Col_dec A B C); intro; assert_diffs.
apply parallelogram_to_plg; unfold Parallelogram; right; unfold Parallelogram_flat; repeat split.
ColR.
ColR.
assumption.
assumption.
right; intro; subst; assert (B = C) by (apply symmetric_point_unicity with A K; assumption); contradiction.
apply pars_par_plg.
assert (Par_strict A B J I ∧ Par_strict A C I K ∧ Par_strict B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_strict_cong; intuition).
spliter.
apply par_strict_symmetry; apply par_strict_col_par_strict with C; intuition; apply par_strict_symmetry; apply par_strict_right_comm; assumption; Col.
Par.
Col.
assert (Par_strict A B J I ∧ Par_strict A C I K ∧ Par_strict B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_strict_cong; intuition).
spliter.
apply par_symmetry; apply par_col_par with B; intuition; apply par_symmetry; apply par_strict_par; assumption.
left; apply l8_3 with B; try apply l8_2; try apply l8_3 with C; try apply l8_2; try assumption; intuition; Col.
Qed.
End Exercises.
Section Exercises.
Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Context `{InterDec:InterDecidability Tpoint Col}.
Lemma Per_mid_rectangle : ∀ A B C I J K,
A ≠ B →
B ≠ C →
Per B A C →
is_midpoint I B C →
is_midpoint J A C →
is_midpoint K A B →
Rectangle A J I K.
Proof.
intros.
assert_diffs.
assert_cols.
elim (eq_dec_points A C); intro; apply plg_per_rect.
treat_equalities.
assert (HM : ∃ M : Tpoint, is_midpoint M J I) by (apply midpoint_existence); decompose [ex] HM; repeat split; intuition; ∃ x; intuition.
treat_equalities; intuition.
assert( Par A B J I ∧ Par A C I K ∧ Par B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_cong; intuition).
spliter.
elim (Col_dec A B C); intro; assert_diffs.
apply parallelogram_to_plg; unfold Parallelogram; right; unfold Parallelogram_flat; repeat split.
ColR.
ColR.
assumption.
assumption.
right; intro; subst; assert (B = C) by (apply symmetric_point_unicity with A K; assumption); contradiction.
apply pars_par_plg.
assert (Par_strict A B J I ∧ Par_strict A C I K ∧ Par_strict B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_strict_cong; intuition).
spliter.
apply par_strict_symmetry; apply par_strict_col_par_strict with C; intuition; apply par_strict_symmetry; apply par_strict_right_comm; assumption; Col.
Par.
Col.
assert (Par_strict A B J I ∧ Par_strict A C I K ∧ Par_strict B C J K ∧
Cong A K I J ∧ Cong B K I J ∧ Cong A J I K ∧ Cong C J I K ∧ Cong B I J K ∧ Cong C I J K)
by (apply triangle_mid_par_strict_cong; intuition).
spliter.
apply par_symmetry; apply par_col_par with B; intuition; apply par_symmetry; apply par_strict_par; assumption.
left; apply l8_3 with B; try apply l8_2; try apply l8_3 with C; try apply l8_2; try assumption; intuition; Col.
Qed.
End Exercises.