(***************************************************************************)
(* Formalization of the Chou, Gao and Zhang's decision procedure.          *)
(* Julien Narboux (Julien@narboux.fr)                                      *)
(* LIX/INRIA FUTURS 2004-2006                                              *)
(* University of Strasbourg 2008                                           *)
(***************************************************************************)

Require Export advanced_parallel_lemmas.
Require Export geometry_tools.

(*********************************************************************)
(*  Elimination Theorems                                               *)
(*********************************************************************)

(* Area elimination *)

Theorem non_zero_denom_on_line_area : forall A B C : Point, on_line A B C -> B <> C.
(* Goal: forall (A B C : Point) (_ : on_line A B C), not (@eq Point B C) *)
unfold on_line in |- *.
Proof.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.
Qed.

Theorem non_zero_denom_inter_ll_area :
 forall A B C D E : Point, inter_ll A B C D E -> S4 B D C E <> 0.
Proof.
(* Goal: forall (A B C D E : Point) (_ : inter_ll A B C D E), not (@eq F (S4 B D C E) F0) *)
unfold inter_ll in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (parallel A B E G) (not (parallel E G C D))))), not (@eq F (S4 E C G D) F0) *)
unfold parallel in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.
Qed.

Theorem non_zero_denom_on_parallel_d_area : forall A B C D : Point, on_parallel A B C D -> C <> D.
Proof.
(* Goal: forall (A B C D : Point) (_ : on_parallel A B C D), not (@eq Point C D) *)
unfold on_parallel in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.
Qed.

Theorem non_zero_denom_on_inter_line_parallel_area :
 forall A B C D E G : Point, on_inter_line_parallel A B C D E G -> S4 E C G D <> 0.
Proof.
(* Goal: forall (A B C D E G : Point) (_ : on_inter_line_parallel A B C D E G), not (@eq F (S4 E C G D) F0) *)
unfold on_inter_line_parallel in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (parallel A B E G) (not (parallel E G C D))))), not (@eq F (S4 E C G D) F0) *)
unfold parallel in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.
Qed.

Theorem non_zero_denom_on_inter_parallel_parallel_area :
 forall A B C D E G H : Point, on_inter_parallel_parallel A B C D E G H -> S4 C G D H <> 0.
Proof with Geometry.
unfold on_inter_parallel_parallel in |- *.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (parallel A B E G) (not (parallel E G C D))))), not (@eq F (S4 E C G D) F0) *)
unfold parallel in |- *.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
assert (S4 G C H D = - S4 C G D H)...
rewrite H1 in H0.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.
Qed.


Theorem elim_area_on_line_d :
 forall (A B P Q Y : Point) (lambda : F),
 on_line_d Y P Q lambda -> S A B Y = lambda * S A B Q + (1 - lambda) * S A B P.
Proof with Geometry.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
unfold on_line_d in *.
DecompAndAll.
RewriteVar lambda H3...
clear H3.
assert (1 - P ** Y / P ** Q = Y ** Q / P ** Q)...
assert (Y ** P + P ** Q = Y ** Q)...
rewrite <- H1...
assert (P ** Y = - Y ** P)...
rewrite H3; field...
rewrite H1...
replace (S A B Y) with (S Y A B)...
replace (S A B Q) with (S Q A B)...
replace (S A B P) with (S P A B)...
apply l2_9...
Qed.

Theorem elim_area_on_line :
 forall A B P Q Y : Point,
 on_line Y P Q ->
 S A B Y = P ** Y / P ** Q * S A B Q + (1 - P ** Y / P ** Q) * S A B P.
Proof with Geometry.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
assert (on_line_d Y P Q (P ** Y / P ** Q)).
apply on_line_to_on_line_d...
apply elim_area_on_line_d...
Qed.

Theorem elim_area_inter_ll :
 forall A B P Q U V Y : Point,
 inter_ll Y P Q U V ->
 S A B Y = 1 / S4 P U Q V * (S P U V * S A B Q + S Q V U * S A B P). 
Proof with Geometry.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
unfold inter_ll in *.
DecompAndAll.
assert (P <> Q);eauto with Geom.
assert (S Y A B = P ** Y / P ** Q * S Q A B + Y ** Q / P ** Q * S P A B)...
apply l2_9...
unfold parallel in H3.
assert (P ** Y / P ** Q = S P U V / S4 P U Q V)...
assert (Q ** Y / P ** Q = S Q U V / S4 P U Q V)...
replace (Q**Y) with (- Y**Q) in H5.
2:symmetry;Geometry.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (S B A D)))) (S A B F)) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
uniformize_signed_areas.
IsoleVar (Y ** Q) H5...
rewrite H1.
rewrite H4.
rewrite H5.
field...
Qed.


Theorem elim_area_on_parallel_d :
 forall (A B P Q R Y : Point) (lambda : F),
 on_parallel_d Y R P Q lambda -> 
 S A B Y = S A B R + lambda * S4 A P B Q. 
Proof with Geometry.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
unfold on_parallel_d in H.
DecompAndAll.

cases_equality R Y.
subst R;basic_simpl.
IsoleVar lambda H3...
assert (lambda = 0).
rewrite H3.
field...
rewrite H1.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (Fopp (S A B D))))) (Fopp (S B A F))) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
ring.

assert (parallel R Y P Q)...

assert (Th := on_line_dex_spec_strong_f R Y P Q H1 H)...
DecompExAnd Th T.
assert (R <> T).
unfold not;intro;subst R;basic_simpl...

assert (S A B Y = lambda * S A B T + (1 - lambda) * S A B R).
apply elim_area_on_line_d.
rewrite <- H7 in H3.
unfold on_line_d in *...

assert (S R A B + S Q A B = S T A B + S P A B).
apply l2_11a_strong_strong_strong...
IsoleVar (S T A B) H9.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (S B A D)))) (S A B F)) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
uniformize_signed_areas.
rewrite H9 in H6.
replace (S4 A P B Q) with (S Q A B - S P A B).
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (Fopp (S A B D))))) (Fopp (S B A F))) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
rewrite H6;ring.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (Fopp (S A B D))))) (Fopp (S B A F))) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
unfold S4 in |- *;uniformize_signed_areas;ring.
Qed.

Theorem elim_area_on_parallel :
 forall A B P Q R Y : Point,
 on_parallel Y R P Q -> 
 S A B Y = S A B R + R ** Y / P ** Q * S4 A P B Q.
Proof with auto.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros. 
assert (on_parallel_d Y R P Q (R ** Y / P ** Q)).
apply on_parallel_to_on_parallel_d...
apply elim_area_on_parallel_d...
Qed.


(** We prove parallel transitivity using the elimination lemmas *)

Lemma parallel_transitivity : forall A B C D E F, 
  C<> D -> 
  parallel A B C D -> 
  parallel C D E F -> 
  parallel A B E F.
Proof.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.

(* Goal: parallel A B E F *)
cases_equality A B.

(* Goal: parallel A B E F *)
(* Goal: parallel A B E F *)
subst;Geometry.

(* Goal: parallel A B E F *)
assert (on_parallel E F C D).
(* Goal: on_parallel E F C D *)
(* Goal: parallel A B E F *)
unfold on_parallel;intuition Geometry.
(* Goal: parallel A B E F *)
assert (on_parallel_d E F C D (F ** E / C ** D)).
(* Goal: on_parallel_d E F C D (Fdiv (DSeg F E) (DSeg C D)) *)
(* Goal: parallel A B E F *)
apply on_parallel_to_on_parallel_d.
(* Goal: on_parallel_d C D A B f0 *)
assumption.
(* Goal: parallel A B E F *)
set (F ** E / C ** D).
(* Goal: parallel A B E F *)
unfold parallel,S4.
(* Goal: @eq field.F (Fplus (S A E B) (S A B F)) F0 *)
replace (S A E B) with (S B A E) by Geometry.
(* Goal: @eq field.F (Fplus (S B A E) (S A B F)) F0 *)
assert (T: S B A E = S B A F + f * S4 B C A D). 
(* Goal: @eq field.F (S B A E) (Fplus (S B A F) (Fmult f (S4 B C A D))) *)
(* Goal: @eq field.F (Fplus (S B A E) (S A B F)) F0 *)
apply (elim_area_on_parallel_d B A C D F E).
(* Goal: on_parallel_d E F C D f *)
(* Goal: @eq field.F (Fplus (S B A E) (S A B F)) F0 *)
auto.
(* Goal: @eq field.F (Fplus (S B A E) (S A B F)) F0 *)
rewrite T.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (S4 B C A D))) (S A B F)) F0 *)
unfold S4.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S B C A) (S B A D)))) (S A B F)) F0 *)
replace (S B C A) with (S A B C) by Geometry.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
assert (on_parallel_d C D A B ( D ** C / A ** B)). 
(* Goal: on_parallel_d C D A B (Fdiv (DSeg D C) (DSeg A B)) *)
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
unfold on_parallel_d.
(* Goal: and (not (@eq Point A B)) (and (parallel C D A B) (@eq field.F (DSeg D C) (Fmult (Fdiv (DSeg D C) (DSeg A B)) (DSeg A B)))) *)
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
repeat split;Geometry.
(* Goal: @eq field.F (DSeg D C) (Fmult (Fdiv (DSeg D C) (DSeg A B)) (DSeg A B)) *)
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
field;Geometry.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
set (D ** C / A ** B).
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B C) (S B A D)))) (S A B F)) F0 *)
replace (S A B C) with (S A B D + f0 * S4 A A B B).
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S B A D)))) (S A B F)) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
basic_simpl.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (S B A D)))) (S A B F)) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
uniformize_signed_areas.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (S A B D) (Fopp (S A B D))))) (Fopp (S B A F))) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
ring.
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
symmetry.
(* Goal: @eq field.F (S A B C) (Fplus (S A B D) (Fmult f0 (S4 A A B B))) *)
apply elim_area_on_parallel_d.
(* Goal: on_parallel_d C D A B f0 *)
assumption.
Qed.

Lemma elim_area_on_inter_line_parallel :
    forall P Q R U V Y A B : Point,
    on_inter_line_parallel Y R U V P Q ->
    R <>Y ->
    S A B Y = (S4 P U Q R * S A B V - S4 P V Q R * S A B U) / S4 P U Q V.
Proof with Geometry.
(* Goal: forall (A B C D E F : Point) (_ : not (@eq Point C D)) (_ : parallel A B C D) (_ : parallel C D E F), parallel A B E F *)
intros.
unfold on_inter_line_parallel in H.
DecompAndAll.
assert (P<>Q);eauto with Geom.
assert (parallel R Y P Q)...

assert (~ Col R Y Q).
eapply diff_not_col_par_not_col.
2:apply H1.
(* Goal: on_parallel_d E F C D f *)
(* Goal: @eq field.F (Fplus (S B A E) (S A B F)) F0 *)
auto.
Geometry.

assert (Th:= (on_line_dex_spec_strong R Y P Q H4 H H6)).
DecompExAnd Th T.
assert (R<>T).
unfold not;intro;subst T.
(* Goal: @eq field.F (Fplus (Fplus (S B A F) (Fmult f (Fplus (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S B A D)))) (S A B F)) F0 *)
(* Goal: @eq field.F (Fplus (S A B D) (Fmult f0 (S4 A A B B))) (S A B C) *)
basic_simpl...

assert  (~ parallel U V T R).
unfold not;intro.
unfold parallelogram in *.
DecompAndAll.
assert (parallel T R P Q)...
assert (parallel U V P Q).
eapply parallel_transitivity.
apply H7.
Geometry.
Geometry.
(* Goal: forall (A B C D E G : Point) (_ : and (not (Col B E G)) (and (Col A C D) (and (@eq F (S4 A E B G) F0) (not (@eq F (S4 E C G D) F0))))), not (@eq F (S4 E C G D) F0) *)
intuition.

assert ((S A B Y) =  1 / (S4 U T V R) * ((S U T R)*(S A B V) + (S V R T)*(S A B U))). 
apply elim_area_inter_ll...
unfold inter_ll...

assert ((S4 U R V T) = (S4 U P V Q)).
apply l2_11b...
assert ((S U R T) = (S4 U P R Q)).
apply l2_12b...
assert ((S V R T) = (S4 V P R Q)).
apply l2_12b...

rewrite H12.

replace (S4 P U Q V) with (- S4 U P V Q)...
rewrite <- H13.
replace (S4 U R V T) with (- S4 U T V R)...
replace  (S U T R) with (- S U R T)...
rewrite H14.
rewrite H15.
replace (S4 V P R Q) with (- S4 P V Q R)...
replace (S4 U P R Q) with (- S4 P U Q R)...
field.
assert (S4 U T V R<>0)...
Qed.

