Library AreaMethod.freepoints
For the first time, we need decidability of the parallel predicate
Lemma parallel_dec : ∀ A B C D, parallel A B C D ∨ ¬ parallel A B C D.
Proof.
intros.
apply classic.
Qed.
Ltac cases_parallel A B C D := elim (parallel_dec A B C D);intros.
Definition Det3 (x1 x2 x3 y1 y2 y3 z1 z2 z3 : F) : F :=
x1 × (y2 × z3) - x1 × (y3 × z2) - x2 × (y1 × z3) + x2 × (y3 × z1) +
x3 × (y1 × z2) - x3 × (y2 × z1).
Lemma freepoint_elimination_aux : ∀ O U V B Y:Point, ¬ Col O U V →
S O B Y = 1/ (S O U V) × (S O B V × S O U Y + S O B U × S O Y V).
Proof with Geometry.
intros.
cases_parallel U V O Y.
rename H into T.
assert (O**Y / U**V = S U O Y / S O V U).
apply l2_15...
assert (S O B Y = S O B O + (O**Y/U**V) × S4 O U B V).
apply elim_area_on_parallel.
unfold on_parallel;repeat split...
eauto with Geom.
rewrite H in H1.
basic_simpl.
unfold S4 in ×.
assert (parallel O Y U V).
Geometry.
unfold parallel, S4 in ×.
IsoleVarRing (S O Y V) H2.
rewrite H2.
rewrite H1.
uniformize_signed_areas.
field.
split...
assert (∃ W, inter_ll W U V O Y).
apply inter_ll_ex...
DecompEx H1 W.
cases_equality W O.
subst W.
unfold inter_ll in ×.
intuition.
rename H1 into Hdiff.
assert (S B O W = 1 / S4 U O V Y × (S U O Y × S B O V + S V Y O × S B O U)).
apply elim_area_inter_ll...
replace (S4 U O V Y) with (- S4 O U Y V) in H1.
2:Geometry.
replace ((S U O Y × S B O V + S V Y O × S B O U)) with
(S O B V × S O U Y + S O B U × S O Y V) in H1.
2:uniformize_signed_areas;field.
unfold inter_ll in *;DecompAndAll.
assert (O ** W / O ** Y = S O U V / S4 O U Y V).
apply co_side_ter...
cases_col B O W.
cases_equality V W.
subst W.
assert (Col O Y B).
eapply col_trans_1 with (B:=V)...
unfold Col in ×.
uniformize_signed_areas.
rewrite H4.
rewrite H5.
rewrite H7.
ring.
cases_equality O B.
subst B.
basic_simpl.
ring.
cases_col V O B.
assert (Col O Y B).
eapply col_trans_1 with (B:= W)...
assert (Col O Y V).
eapply col_trans_1 with (B:= B)...
unfold Col in ×.
uniformize_signed_areas.
rewrite H9.
rewrite H10.
rewrite H11.
ring.
assert (U**W/V**W = S U O B / S V O B).
apply co_side...
cases_col V O Y.
cases_equality Y O.
subst Y.
basic_simpl.
ring.
assert (Col Y W V).
eapply col_trans_1 with (B:= O)...
assert (Col W U Y).
eapply col_trans_1 with (B:= V)...
cases_equality Y W.
subst W.
clear H13 H12 H5.
assert (Col O V B).
eapply col_trans_1 with (B:= Y)...
unfold Col in ×.
uniformize_signed_areas.
rewrite H4.
replace (S V O B) with (-0).
rewrite H11.
ring.
rewrite <- H5.
ring.
assert (Col Y U O).
eapply col_trans_1 with (B:= W)...
assert (Col O U V).
eapply col_trans_1 with (B:= Y)...
intuition.
assert (U**W/V**W = S U O Y / S V O Y).
apply co_side...
rewrite H10 in H12.
assert (Col O B Y).
eapply col_trans_1 with (B:= W)...
rewrite H13.
uniformize_signed_areas.
RewriteVar (S O B U) H12.
2:Geometry.
field.
split...
Second case
assert (O**Y / O**W = S B O Y / S B O W).
apply A6...
assert (O**Y / O**W = S4 O U Y V / S O U V).
replace (O ** Y / O ** W) with (1/(O ** W / O ** Y)).
rewrite H2.
field.
Geometry.
repeat apply nonzeromult...
field.
split...
unfold not;intro.
assert (O=Y).
Geometry.
subst Y.
assert (parallel U V O O)...
rewrite H7 in H8.
set (S O B V × S O U Y + S O B U × S O Y V) in ×.
rewrite H1 in H8.
replace (S B O Y) with (-S O B Y) in H8.
2:Geometry.
RewriteVar (S O B Y) H8.
field;split...
apply nonzeromult...
apply nonzerodiv...
unfold not;intro.
rewrite H9 in H1.
basic_simpl.
assert (Col O Y B).
eapply col_trans_1 with (B:=W)...
Geometry.
Qed.
Lemma free_points_area_elimination :
∀ O U V A B Y : Point,
S O U V ≠ 0 →
S A B Y =
Det3 (S O U A) (S O V A) 1 (S O U B) (S O V B) 1 (S O U Y) (S O V Y) 1 /
S O U V.
Proof with Geometry.
intros.
unfold Det3.
replace (S A B Y) with (S A B O + S A O Y + S O B Y)...
replace (S A O Y) with (- S O A Y).
2:symmetry;Geometry.
replace (S O A Y) with (1/ (S O U V) × (S O A V × S O U Y + S O A U × S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S O B Y) with (1/ (S O U V) × (S O B V × S O U Y + S O B U × S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S A B O) with (S O A B).
2:Geometry.
replace (S O A B) with (1/ (S O U V) × (S O A V × S O U B + S O A U × S O B V)).
2:symmetry;eapply freepoint_elimination_aux...
uniformize_signed_areas.
field...
Qed.
Lemma free_points_ratio_elimination_1 : ∀ O U V A B C D : Point,
parallel A B C D →
C≠D →
S O U V ≠ 0 →
S U A B ≠ 0 →
A**B / C**D = (S O U A × S O V B + S O U A × S O U V - S O V A × S O U B -
S O U B × S O U V) /
(S O U A × S O V D - S O U A × S O V C + S O V A × S O U C -
S O V A × S O U D + S O U V × S O U C - S O U V × S O U D).
Proof.
intros.
cases_equality A B.
subst.
basic_simpl;intuition.
assert (A**B / C**D = (S O A B + S O U A - S O U B) / (S U C D - S A C D)
∧ (S U C D - S A C D) ≠ 0 ).
elim (on_line_dex_spec_strong_f A B C D H H3).
intros D' Hn. decompose [and] Hn;clear Hn.
rewrite <- H6.
assert (A≠D').
intro;subst; basic_simpl; auto with Geom.
assert (¬ Col U A D').
intro.
assert (Col A B U).
eapply (col_trans_1);eauto with Geom.
assert (Col U A B); auto with Geom.
rewrite (A6 A B D' U H5 H8) by auto with Geom.
rewrite (A5 U A B O).
assert (S U A D' = S U C D - S A C D) by
(apply (l2_12a_strong_3 A D' D C U);auto).
split.
uniformize_signed_areas.
rewrite H9; field; rewrite <- H9; auto with Geom.
rewrite <- H9;auto with Geom.
use H4.
rewrite H5.
rewrite (free_points_area_elimination O U V O A B) in × by assumption.
rewrite (free_points_area_elimination O U V U C D) in × by assumption.
rewrite (free_points_area_elimination O U V A C D) in × by assumption.
unfold Det3 in ×.
replace (S O V U) with (- S O U V) in × by auto with Geom.
basic_simpl.
field.
split;auto.
clear H5.
replace ((0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D) / S O U V -
(S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D) / S O U V
)
with ((0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D - (S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D)) / S O U V) in H6 by (field;auto).
replace (0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D -
(S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D)) with (S O U A × S O V D - S O U A × S O V C + S O V A × S O U C - S O V A × S O U D +
S O U V × S O U C - S O U V × S O U D) in H6 by ring.
intro Hx; rewrite Hx in H6; clear Hx.
basic_simpl;
intuition.
Qed.
Lemma free_point_ratio_elimination_2 : ∀ O U V A B C D : Point,
parallel A B C D →
C≠D →
S O U V ≠ 0 →
S V A B ≠ 0 →
A**B / C**D = (S O V A × S O U B + S O V A × S O V U - S O U A × S O V B -
S O V B × S O V U) /
(S O V A × S O U D - S O V A × S O U C + S O U A × S O V C -
S O U A × S O V D + S O V U × S O V C - S O V U × S O V D).
Proof.
intros.
assert (S O V U ≠ 0).
intro; apply H1;uniformize_signed_areas;auto with Geom.
rewrite (free_points_ratio_elimination_1 O V U A B C D) by auto.
reflexivity.
Qed.
Lemma free_points_ratio_elimination_3 : ∀ O U V A B C D : Point,
parallel A B C D →
A≠B →
C≠D →
S O U V ≠ 0 →
S U C D ≠ 0 →
A**B / C**D = (S O U C × S O V B - S O U C × S O V A + S O V C × S O U A -
S O V C × S O U B + S O U V × S O U A - S O U V × S O U B)/
(S O U C × S O V D + S O U C × S O U V - S O V C × S O U D -
S O U D × S O U V).
Proof.
intros.
assert (A**B / C**D = (S U A B - S C A B) / (S O C D + S O U C - S O U D)
∧ (S O C D + S O U C - S O U D) ≠ 0 ).
assert (parallel C D A B) by auto with Geom.
elim (on_line_dex_spec_strong_f C D A B H4 H1).
intros D' Hn. decompose [and] Hn;clear Hn.
rewrite <- H7.
assert (C≠D').
intro;subst; basic_simpl; auto with Geom.
rewrite (A6 C D' D U H1) by auto with Geom.
rewrite (A5 U C D O).
assert (T:=A5 U C D O).
assert (S U C D' = S U A B - S C A B) by
(apply (l2_12a_strong_3 C D' B A U);auto).
split.
uniformize_signed_areas.
rewrite H9.
field.
replace (S O C D + S U C O - - S U O D)
with (S U C O + S U O D + S O C D) by ring.
rewrite <- T;auto.
replace (S O C D + S O U C - S O U D)
with (S U C O + S U O D + S O C D)
by (uniformize_signed_areas;ring).
rewrite <- T;auto.
use H4.
rewrite H5.
rewrite (free_points_area_elimination O U V U A B) in × by assumption.
rewrite (free_points_area_elimination O U V C A B) in × by assumption.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
replace (S O V U) with (- S O U V) in × by auto with Geom.
basic_simpl.
field.
split;auto.
clear H5.
replace ((S O U C × S O V D - S O V C × S O U D) / S O U V + S O U C - S O U D)
with ((S O U C × S O V D + S O U C × S O U V - S O V C × S O U D - S O U D × S O U V) / (S O U V))
in H6 by (field;auto).
intro.
rewrite H4 in H6.
basic_simpl;
intuition.
Qed.
Lemma free_points_ratio_elimination_4 : ∀ O U V A B C D : Point,
parallel A B C D →
A≠B →
C≠D →
S O U V ≠ 0 →
S V C D ≠ 0 →
A**B / C**D = (S O V C × S O U B - S O V C × S O U A + S O U C × S O V A -
S O U C × S O V B + S O V U × S O V A - S O V U × S O V B) /
(S O V C × S O U D + S O V C × S O V U - S O U C × S O V D -
S O V D × S O V U).
intros.
assert (S O V U ≠ 0).
intro; assert (Col O U V) by auto with Geom;intuition.
rewrite (free_points_ratio_elimination_3 O V U A B C D) by auto.
reflexivity.
Qed.
Lemma free_points_ratio_elimination_5 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col A C D →
A**B / C**D = (S O U C × S O V A - S O U C × S O V B - S O V A × S O U B +
S O V B × S O U A - S O V C × S O U A + S O V C × S O U B) /
(S O U C × S O V A - S O U C × S O V D - S O V A × S O U D -
S O V C × S O U A + S O V C × S O U D + S O U A × S O V D) .
Proof.
intros.
rewrite (l2_15 A B C D) by auto with Geom.
assert (¬ Col A D C) by auto with Geom.
unfold Col in H3.
rewrite (free_points_area_elimination O U V C A B) in × by assumption.
rewrite (free_points_area_elimination O U V A D C) in × by assumption.
unfold Det3 in ×.
field.
split;auto.
basic_simpl.
replace (S O U A × S O V D - S O U A × S O V C - S O V A × S O U D +
S O V A × S O U C + S O U D × S O V C - S O V D × S O U C)
with (S O U C × S O V A - S O U C × S O V D - S O V A × S O U D - S O V C × S O U A +
S O V C × S O U D + S O U A × S O V D) in × by ring.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_6 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col O A C →
Col A C D →
A**B / C**D = (S O U A × S O V B - S O V A × S O U B) /
(S O U C × S O V D - S O V C × S O U D).
Proof.
intros.
assert (¬ Col O C D).
intro.
assert (Col C A O).
apply (col_trans_1 C D A O );auto with Geom.
intuition.
assert (Col B C D).
cut (Col C D B).
auto with Geom.
apply (par_col_col_1 C D A B); auto with Geom.
rewrite <- (l2_7 C D A B O);auto.
unfold Col in H4.
rewrite (free_points_area_elimination O U V O A B) in × by assumption.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
field.
split;auto.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_6_non_zero_denom: ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col O A C →
Col A C D →
S O U C × S O V D - S O V C × S O U D ≠ 0.
Proof.
intros.
assert (¬ Col O C D).
intro.
assert (Col C A O).
apply (col_trans_1 C D A O );auto with Geom.
intuition.
unfold Col in H4.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_7 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col U A C →
Col A C D →
A**B / C**D =
(S O U V × (S O U B - S O U A) - S O U A × S O V B + S O U B × S O V A) /
(S O U V × (S O U D - S O U C) - S O U C × S O V D + S O U D × S O V C).
Proof.
intros.
rewrite (free_points_ratio_elimination_6 U O V A B C D) by auto with Geom.
assert (S U O C × S U V D - S U V C × S U O D ≠ 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).
rewrite (free_points_area_elimination O U V U V A) in × by assumption.
rewrite (free_points_area_elimination O U V U V B) in × by assumption.
rewrite (free_points_area_elimination O U V U V C) in × by assumption.
rewrite (free_points_area_elimination O U V U V D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
replace (S O V U) with (- S O U V) in × by auto with Geom.
replace (S U O A) with (- S O U A) in × by auto with Geom.
replace (S U O B) with (- S O U B) in × by auto with Geom.
replace (S U O C) with (- S O U C) in × by auto with Geom.
replace (S U O D) with (- S O U D) in × by auto with Geom.
basic_simpl.
set (xc := S O U C) in ×.
set (xa := S O U A) in ×.
set (xb := S O U B) in ×.
set (xd := S O U D) in ×.
set (yc := S O V C) in ×.
set (ya := S O V A) in ×.
set (yb := S O V B) in ×.
set (yd := S O V D) in ×.
set (X := S O U V) in ×.
field.
repeat split;auto.
replace ((0 - - (X × X) - X × xd + X × yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X × X) - X × xc + X × yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc × (X - xd + yd)) - - ((X - xc + yc) × xd))
with (X × (xd - xc) - xc × yd + xd × yc) in H4 by ring.
auto.
replace (- (xc × ((0 - - (X × X) - X × xd + X × yd) / X)) -
- ((0 - - (X × X) - X × xc + X × yc) / X × xd))
with ((- (xc × (- - (X × X) - X × xd + X × yd)) -
- ((- - (X × X) - X × xc + X × yc) × xd)) / X) in H4
by (field;auto).
intro Hx; rewrite Hx in ×.
replace (0 / X) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_7_non_zero_denom :
∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col U A C →
Col A C D →
(S O U V × (S O U D - S O U C) - S O U C × S O V D + S O U D × S O V C) ≠ 0.
Proof.
intros.
assert (S U O C × S U V D - S U V C × S U O D ≠ 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).
rewrite (free_points_area_elimination O U V U V C) in × by assumption.
rewrite (free_points_area_elimination O U V U V D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
replace (S O V U) with (- S O U V) in × by auto with Geom.
replace (S U O A) with (- S O U A) in × by auto with Geom.
replace (S U O B) with (- S O U B) in × by auto with Geom.
replace (S U O C) with (- S O U C) in × by auto with Geom.
replace (S U O D) with (- S O U D) in × by auto with Geom.
basic_simpl.
set (xc := S O U C) in ×.
set (xa := S O U A) in ×.
set (xb := S O U B) in ×.
set (xd := S O U D) in ×.
set (yc := S O V C) in ×.
set (ya := S O V A) in ×.
set (yb := S O V B) in ×.
set (yd := S O V D) in ×.
set (X := S O U V) in ×.
replace ((0 - - (X × X) - X × xd + X × yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X × X) - X × xc + X × yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc × (X - xd + yd)) - - ((X - xc + yc) × xd))
with (X × (xd - xc) - xc × yd + xd × yc) in H4 by ring.
auto.
Qed.
Lemma free_points_ratio_elimination_8 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col V A C →
Col A C D →
A**B / C**D =
( S O U V × (S O V B - S O V A) + S O V A × S O U B - S O V B × S O U A) /
( S O U V × (S O V D - S O V C) + S O V C × S O U D - S O V D × S O U C).
Proof.
intros.
rewrite (free_points_ratio_elimination_7 O V U A B C D) by auto with Geom.
replace (S O V U) with (- S O U V) by auto with Geom.
field.
replace (- S O U V) with (S O V U) by auto with Geom.
split.
replace (S O U V) with (- S O V U) by auto with Geom.
replace (- S O V U × (S O V D - S O V C) + S O V C × S O U D - S O V D × S O U C)
with (- (S O V U × (S O V D - S O V C) - S O V C × S O U D + S O V D × S O U C))
by ring.
Lemma aux: ∀ x, x≠0 → -x≠0.
Proof.
auto with field_hints.
Qed.
apply aux.
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
Qed.
apply A6...
assert (O**Y / O**W = S4 O U Y V / S O U V).
replace (O ** Y / O ** W) with (1/(O ** W / O ** Y)).
rewrite H2.
field.
Geometry.
repeat apply nonzeromult...
field.
split...
unfold not;intro.
assert (O=Y).
Geometry.
subst Y.
assert (parallel U V O O)...
rewrite H7 in H8.
set (S O B V × S O U Y + S O B U × S O Y V) in ×.
rewrite H1 in H8.
replace (S B O Y) with (-S O B Y) in H8.
2:Geometry.
RewriteVar (S O B Y) H8.
field;split...
apply nonzeromult...
apply nonzerodiv...
unfold not;intro.
rewrite H9 in H1.
basic_simpl.
assert (Col O Y B).
eapply col_trans_1 with (B:=W)...
Geometry.
Qed.
Lemma free_points_area_elimination :
∀ O U V A B Y : Point,
S O U V ≠ 0 →
S A B Y =
Det3 (S O U A) (S O V A) 1 (S O U B) (S O V B) 1 (S O U Y) (S O V Y) 1 /
S O U V.
Proof with Geometry.
intros.
unfold Det3.
replace (S A B Y) with (S A B O + S A O Y + S O B Y)...
replace (S A O Y) with (- S O A Y).
2:symmetry;Geometry.
replace (S O A Y) with (1/ (S O U V) × (S O A V × S O U Y + S O A U × S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S O B Y) with (1/ (S O U V) × (S O B V × S O U Y + S O B U × S O Y V)).
2:symmetry;eapply freepoint_elimination_aux...
replace (S A B O) with (S O A B).
2:Geometry.
replace (S O A B) with (1/ (S O U V) × (S O A V × S O U B + S O A U × S O B V)).
2:symmetry;eapply freepoint_elimination_aux...
uniformize_signed_areas.
field...
Qed.
Lemma free_points_ratio_elimination_1 : ∀ O U V A B C D : Point,
parallel A B C D →
C≠D →
S O U V ≠ 0 →
S U A B ≠ 0 →
A**B / C**D = (S O U A × S O V B + S O U A × S O U V - S O V A × S O U B -
S O U B × S O U V) /
(S O U A × S O V D - S O U A × S O V C + S O V A × S O U C -
S O V A × S O U D + S O U V × S O U C - S O U V × S O U D).
Proof.
intros.
cases_equality A B.
subst.
basic_simpl;intuition.
assert (A**B / C**D = (S O A B + S O U A - S O U B) / (S U C D - S A C D)
∧ (S U C D - S A C D) ≠ 0 ).
elim (on_line_dex_spec_strong_f A B C D H H3).
intros D' Hn. decompose [and] Hn;clear Hn.
rewrite <- H6.
assert (A≠D').
intro;subst; basic_simpl; auto with Geom.
assert (¬ Col U A D').
intro.
assert (Col A B U).
eapply (col_trans_1);eauto with Geom.
assert (Col U A B); auto with Geom.
rewrite (A6 A B D' U H5 H8) by auto with Geom.
rewrite (A5 U A B O).
assert (S U A D' = S U C D - S A C D) by
(apply (l2_12a_strong_3 A D' D C U);auto).
split.
uniformize_signed_areas.
rewrite H9; field; rewrite <- H9; auto with Geom.
rewrite <- H9;auto with Geom.
use H4.
rewrite H5.
rewrite (free_points_area_elimination O U V O A B) in × by assumption.
rewrite (free_points_area_elimination O U V U C D) in × by assumption.
rewrite (free_points_area_elimination O U V A C D) in × by assumption.
unfold Det3 in ×.
replace (S O V U) with (- S O U V) in × by auto with Geom.
basic_simpl.
field.
split;auto.
clear H5.
replace ((0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D) / S O U V -
(S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D) / S O U V
)
with ((0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D - (S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D)) / S O U V) in H6 by (field;auto).
replace (0 - - (S O U V × S O U C) - S O U V × S O U D + S O U C × S O V D -
S O V C × S O U D -
(S O U A × S O V C - S O U A × S O V D - S O V A × S O U C +
S O V A × S O U D + S O U C × S O V D - S O V C × S O U D)) with (S O U A × S O V D - S O U A × S O V C + S O V A × S O U C - S O V A × S O U D +
S O U V × S O U C - S O U V × S O U D) in H6 by ring.
intro Hx; rewrite Hx in H6; clear Hx.
basic_simpl;
intuition.
Qed.
Lemma free_point_ratio_elimination_2 : ∀ O U V A B C D : Point,
parallel A B C D →
C≠D →
S O U V ≠ 0 →
S V A B ≠ 0 →
A**B / C**D = (S O V A × S O U B + S O V A × S O V U - S O U A × S O V B -
S O V B × S O V U) /
(S O V A × S O U D - S O V A × S O U C + S O U A × S O V C -
S O U A × S O V D + S O V U × S O V C - S O V U × S O V D).
Proof.
intros.
assert (S O V U ≠ 0).
intro; apply H1;uniformize_signed_areas;auto with Geom.
rewrite (free_points_ratio_elimination_1 O V U A B C D) by auto.
reflexivity.
Qed.
Lemma free_points_ratio_elimination_3 : ∀ O U V A B C D : Point,
parallel A B C D →
A≠B →
C≠D →
S O U V ≠ 0 →
S U C D ≠ 0 →
A**B / C**D = (S O U C × S O V B - S O U C × S O V A + S O V C × S O U A -
S O V C × S O U B + S O U V × S O U A - S O U V × S O U B)/
(S O U C × S O V D + S O U C × S O U V - S O V C × S O U D -
S O U D × S O U V).
Proof.
intros.
assert (A**B / C**D = (S U A B - S C A B) / (S O C D + S O U C - S O U D)
∧ (S O C D + S O U C - S O U D) ≠ 0 ).
assert (parallel C D A B) by auto with Geom.
elim (on_line_dex_spec_strong_f C D A B H4 H1).
intros D' Hn. decompose [and] Hn;clear Hn.
rewrite <- H7.
assert (C≠D').
intro;subst; basic_simpl; auto with Geom.
rewrite (A6 C D' D U H1) by auto with Geom.
rewrite (A5 U C D O).
assert (T:=A5 U C D O).
assert (S U C D' = S U A B - S C A B) by
(apply (l2_12a_strong_3 C D' B A U);auto).
split.
uniformize_signed_areas.
rewrite H9.
field.
replace (S O C D + S U C O - - S U O D)
with (S U C O + S U O D + S O C D) by ring.
rewrite <- T;auto.
replace (S O C D + S O U C - S O U D)
with (S U C O + S U O D + S O C D)
by (uniformize_signed_areas;ring).
rewrite <- T;auto.
use H4.
rewrite H5.
rewrite (free_points_area_elimination O U V U A B) in × by assumption.
rewrite (free_points_area_elimination O U V C A B) in × by assumption.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
replace (S O V U) with (- S O U V) in × by auto with Geom.
basic_simpl.
field.
split;auto.
clear H5.
replace ((S O U C × S O V D - S O V C × S O U D) / S O U V + S O U C - S O U D)
with ((S O U C × S O V D + S O U C × S O U V - S O V C × S O U D - S O U D × S O U V) / (S O U V))
in H6 by (field;auto).
intro.
rewrite H4 in H6.
basic_simpl;
intuition.
Qed.
Lemma free_points_ratio_elimination_4 : ∀ O U V A B C D : Point,
parallel A B C D →
A≠B →
C≠D →
S O U V ≠ 0 →
S V C D ≠ 0 →
A**B / C**D = (S O V C × S O U B - S O V C × S O U A + S O U C × S O V A -
S O U C × S O V B + S O V U × S O V A - S O V U × S O V B) /
(S O V C × S O U D + S O V C × S O V U - S O U C × S O V D -
S O V D × S O V U).
intros.
assert (S O V U ≠ 0).
intro; assert (Col O U V) by auto with Geom;intuition.
rewrite (free_points_ratio_elimination_3 O V U A B C D) by auto.
reflexivity.
Qed.
Lemma free_points_ratio_elimination_5 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col A C D →
A**B / C**D = (S O U C × S O V A - S O U C × S O V B - S O V A × S O U B +
S O V B × S O U A - S O V C × S O U A + S O V C × S O U B) /
(S O U C × S O V A - S O U C × S O V D - S O V A × S O U D -
S O V C × S O U A + S O V C × S O U D + S O U A × S O V D) .
Proof.
intros.
rewrite (l2_15 A B C D) by auto with Geom.
assert (¬ Col A D C) by auto with Geom.
unfold Col in H3.
rewrite (free_points_area_elimination O U V C A B) in × by assumption.
rewrite (free_points_area_elimination O U V A D C) in × by assumption.
unfold Det3 in ×.
field.
split;auto.
basic_simpl.
replace (S O U A × S O V D - S O U A × S O V C - S O V A × S O U D +
S O V A × S O U C + S O U D × S O V C - S O V D × S O U C)
with (S O U C × S O V A - S O U C × S O V D - S O V A × S O U D - S O V C × S O U A +
S O V C × S O U D + S O U A × S O V D) in × by ring.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_6 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col O A C →
Col A C D →
A**B / C**D = (S O U A × S O V B - S O V A × S O U B) /
(S O U C × S O V D - S O V C × S O U D).
Proof.
intros.
assert (¬ Col O C D).
intro.
assert (Col C A O).
apply (col_trans_1 C D A O );auto with Geom.
intuition.
assert (Col B C D).
cut (Col C D B).
auto with Geom.
apply (par_col_col_1 C D A B); auto with Geom.
rewrite <- (l2_7 C D A B O);auto.
unfold Col in H4.
rewrite (free_points_area_elimination O U V O A B) in × by assumption.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
field.
split;auto.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_6_non_zero_denom: ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col O A C →
Col A C D →
S O U C × S O V D - S O V C × S O U D ≠ 0.
Proof.
intros.
assert (¬ Col O C D).
intro.
assert (Col C A O).
apply (col_trans_1 C D A O );auto with Geom.
intuition.
unfold Col in H4.
rewrite (free_points_area_elimination O U V O C D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
intro Hx; rewrite Hx in ×.
replace (0 / S O U V) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_7 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col U A C →
Col A C D →
A**B / C**D =
(S O U V × (S O U B - S O U A) - S O U A × S O V B + S O U B × S O V A) /
(S O U V × (S O U D - S O U C) - S O U C × S O V D + S O U D × S O V C).
Proof.
intros.
rewrite (free_points_ratio_elimination_6 U O V A B C D) by auto with Geom.
assert (S U O C × S U V D - S U V C × S U O D ≠ 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).
rewrite (free_points_area_elimination O U V U V A) in × by assumption.
rewrite (free_points_area_elimination O U V U V B) in × by assumption.
rewrite (free_points_area_elimination O U V U V C) in × by assumption.
rewrite (free_points_area_elimination O U V U V D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
replace (S O V U) with (- S O U V) in × by auto with Geom.
replace (S U O A) with (- S O U A) in × by auto with Geom.
replace (S U O B) with (- S O U B) in × by auto with Geom.
replace (S U O C) with (- S O U C) in × by auto with Geom.
replace (S U O D) with (- S O U D) in × by auto with Geom.
basic_simpl.
set (xc := S O U C) in ×.
set (xa := S O U A) in ×.
set (xb := S O U B) in ×.
set (xd := S O U D) in ×.
set (yc := S O V C) in ×.
set (ya := S O V A) in ×.
set (yb := S O V B) in ×.
set (yd := S O V D) in ×.
set (X := S O U V) in ×.
field.
repeat split;auto.
replace ((0 - - (X × X) - X × xd + X × yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X × X) - X × xc + X × yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc × (X - xd + yd)) - - ((X - xc + yc) × xd))
with (X × (xd - xc) - xc × yd + xd × yc) in H4 by ring.
auto.
replace (- (xc × ((0 - - (X × X) - X × xd + X × yd) / X)) -
- ((0 - - (X × X) - X × xc + X × yc) / X × xd))
with ((- (xc × (- - (X × X) - X × xd + X × yd)) -
- ((- - (X × X) - X × xc + X × yc) × xd)) / X) in H4
by (field;auto).
intro Hx; rewrite Hx in ×.
replace (0 / X) with 0 in × by (field;auto).
intuition.
Qed.
Lemma free_points_ratio_elimination_7_non_zero_denom :
∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col U A C →
Col A C D →
(S O U V × (S O U D - S O U C) - S O U C × S O V D + S O U D × S O V C) ≠ 0.
Proof.
intros.
assert (S U O C × S U V D - S U V C × S U O D ≠ 0)
by (apply (free_points_ratio_elimination_6_non_zero_denom U O V A B C D);auto with Geom).
rewrite (free_points_area_elimination O U V U V C) in × by assumption.
rewrite (free_points_area_elimination O U V U V D) in × by assumption.
unfold Det3 in ×.
basic_simpl.
replace (S O V U) with (- S O U V) in × by auto with Geom.
replace (S U O A) with (- S O U A) in × by auto with Geom.
replace (S U O B) with (- S O U B) in × by auto with Geom.
replace (S U O C) with (- S O U C) in × by auto with Geom.
replace (S U O D) with (- S O U D) in × by auto with Geom.
basic_simpl.
set (xc := S O U C) in ×.
set (xa := S O U A) in ×.
set (xb := S O U B) in ×.
set (xd := S O U D) in ×.
set (yc := S O V C) in ×.
set (ya := S O V A) in ×.
set (yb := S O V B) in ×.
set (yd := S O V D) in ×.
set (X := S O U V) in ×.
replace ((0 - - (X × X) - X × xd + X × yd) / X)
with (X -xd +yd) in H4 by (field;auto).
replace ((0 - - (X × X) - X × xc + X × yc) / X)
with (X - xc + yc) in H4 by (field;auto).
replace (-(xc × (X - xd + yd)) - - ((X - xc + yc) × xd))
with (X × (xd - xc) - xc × yd + xd × yc) in H4 by ring.
auto.
Qed.
Lemma free_points_ratio_elimination_8 : ∀ O U V A B C D: Point,
parallel A B C D →
C≠D →
¬ Col O U V →
¬ Col V A C →
Col A C D →
A**B / C**D =
( S O U V × (S O V B - S O V A) + S O V A × S O U B - S O V B × S O U A) /
( S O U V × (S O V D - S O V C) + S O V C × S O U D - S O V D × S O U C).
Proof.
intros.
rewrite (free_points_ratio_elimination_7 O V U A B C D) by auto with Geom.
replace (S O V U) with (- S O U V) by auto with Geom.
field.
replace (- S O U V) with (S O V U) by auto with Geom.
split.
replace (S O U V) with (- S O V U) by auto with Geom.
replace (- S O V U × (S O V D - S O V C) + S O V C × S O U D - S O V D × S O U C)
with (- (S O V U × (S O V D - S O V C) - S O V C × S O U D + S O V D × S O U C))
by ring.
Lemma aux: ∀ x, x≠0 → -x≠0.
Proof.
auto with field_hints.
Qed.
apply aux.
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
apply (free_points_ratio_elimination_7_non_zero_denom O V U A B C D); auto with Geom.
Qed.