Library AreaMethod.examples_interactive

Require Import area_method.

Lemma midpoint_elim : O A B,
on_line_d O A B (1 / 2)
OA
B ** O / O ** A =1.
Proof.
intros.
unfold on_line_d in H.
use H.
assert (B**A + A**O = B**O) by auto with Geom.
rewrite <- H.
replace (O**A) with (- A**O).
rewrite H4.
uniformize_dir_seg.
field.
split;auto with Geom.
symmetry;auto with Geom.
Qed.

Lemma l6_15 : A B O C D r,
is_midpoint O A B
on_line_d C O A r
on_line_d D O A (1/r)
r 0
parallel A C C B
parallel D A D B
CB
DB
AC
r+1 0
harmonic A B C D.
Proof.
geoInit.
eliminate D.
replace (A ** O / O ** A) with (0-1).
eliminate C.
replace (A ** O / O ** A) with (0-1).
replace (B ** O / O ** A) with (1).
field.
repeat split;auto with field_hints.
symmetry;apply midpoint_elim;auto.
replace (A**O) with (- O**A) by (symmetry; auto with Geom).
field;auto with Geom.
intuition.
replace (A**O) with (- O**A) by (symmetry; auto with Geom).
field;auto with Geom.
intuition.
intuition.
Qed.

Lemma l_6_295 : A B C D F P Q R S,
on_foot F B A C
on_line D B F
is_midpoint P A B
is_midpoint Q B C
is_midpoint R C D
is_midpoint S D A
eq_distance S Q P R.
Proof.
geoInit.
eliminate S.
eliminate R.
repeat rewrite <- Fmult_Fplus_distr.
apply f_equal2.
auto.
apply f_equal2.
auto.
eliminate D.
eliminate F.
eliminate Q.
eliminate P.
basic_simpl.
unfold_Py.
uniformize_dir_seg.
field;decomp_all_non_zero_mult_div;solve_conds.
Qed.

Lemma l6_63 : A B C D E H,
on_foot D C A B
on_foot E B A C
inter_ll H C D B E
Py C H D = Py B H E.
Proof.
geoInit.
eliminate H.
smart_field_simplify_eq.
ring_simplify_eq.
eliminate D.
smart_field_simplify_eq.
eliminate E.
smart_field_simplify_eq.
uniformize_pys.
unfold_Py.
uniformize_signed_areas.
uniformize_dir_seg.
basic_simpl.
ring.
Qed.

Lemma l_6_273 : B C X A A1 C1,
on_perp_d A B C 1
on_foot A1 A B X
on_foot C1 C B X
eq_distance A A1 B C1.
Proof.
am_before_field.
field_simplify_eq;auto.
replace (- (2 × (2 × (2 × 2))) × S B C X × S B C X) with (- (2 × (2 × (2 × 2))) × ( S B C X × S B C X) ) by ring.
rewrite (herron_qin B C X).
unfold_Py.
uniformize_dir_seg.
field_and_conclude.
solve_conds.
unfold not;intro H1; rewrite H1 in *; basic_simpl;intuition.
Qed.

Lemma l6_144 : A B I A1 A2 B1 B2 C,
on_foot A1 B I A
on_line_d A2 A1 B (0-1)
on_foot B1 A I B
on_line_d B2 B1 A (0-1)
inter_ll C A A2 B B2
eq_angle A C I I C B.
Proof.
geoInit.
eliminate C.
smart_field_simplify_eq.
eliminate A2.
eliminate A1.
eliminate B2.
replace (1 - (0 - 1)) with 2 in × by ring.
eliminate B1.
uniformize_signed_areas.
unfold_Py;uniformize_dir_seg.
basic_simpl.
field.
solve_conds.
intro;rewrite H1 in H; basic_simpl;intuition.
intro;rewrite H1 in H0; basic_simpl;intuition.
Qed.

Lemma l_6_191 : A B C E F G O1 O2 O3 r,
1+20
r×r = (2+1)
is_midpoint E A C
on_perp_d O2 E A (r / (2+1))
is_midpoint F B C
on_perp_d O1 F C (r / (2+1))
is_midpoint G A B
on_perp_d O3 G B (r/ (2+1))
eq_distance O1 O2 O2 O3.
Proof.
geoInit.
am_before_field.
uniformize_signed_areas.
uniformize_pys.
unfold_Py.
uniformize_dir_seg.
basic_simpl.
field_simplify_eq.
ring_simplify_eq.
assert (r × r × A ** B × A ** B = ( r × r) × A ** B × A ** B).
ring.
replace (-
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 × (2 × (1 + 2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ×
r × r × A ** B × A ** B) with (-
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 × (2 × (1 + 2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ×
(r × r) × A ** B × A ** B).
2:ring.
rewrite H0.
replace (2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 × (2 × (1 + 2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ×
r × r × B ** C × B ** C)
with
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(2 ×
(2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(2 ×
(1 +
2 ×
(1 +
2 × (2 × (1 + 2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ×
(r × r) × B ** C × B ** C).
rewrite H0.
ring.
ring.
solve_conds.
Qed.