(***************************************************************************)
(* 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 pythagoras_difference.

Definition on_perp (A' B C : Point) : Prop := B <> C /\ perp A' B B C /\ S B C A' <> 0.

Definition on_perp_d (Y U V : Point)  (lambda : F) : Prop := 
     U <> V  /\ perp Y U U V /\ lambda * Py U V U = (2+2) * S U V Y /\ lambda <> 0.

Definition on_inter_line_perp (Y R U V P Q : Point) : Prop :=
  Col Y U V /\ perp Y R P Q /\ ~ perp P Q U V.

Lemma proj_ex : forall A P Q, P<>Q -> exists X, on_foot X A P Q.
Proof.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: @ex Point (fun X : Point => on_foot X A P Q) *)
unfold on_foot.
(* Goal: @ex Point (fun X : Point => and (perp X A P Q) (and (Col X P Q) (not (@eq Point P Q)))) *)
assert (T:=on_line_dex P Q (Py A P Q/Py P Q P) H).
(* Goal: @ex Point (fun X : Point => and (perp X A P Q) (and (Col X P Q) (not (@eq Point P Q)))) *)
elim T;clear T.
(* Goal: forall (x : Point) (_ : and (Col x P Q) (@eq F (DSeg P x) (Fmult (Fdiv (Py A P Q) (Py P Q P)) (DSeg P Q)))), @ex Point (fun X : Point => and (perp X A P Q) (and (Col X P Q) (not (@eq Point P Q)))) *)
intros Y HY.
(* Goal: @ex Point (fun X : Point => and (perp X A P Q) (and (Col X P Q) (not (@eq Point P Q)))) *)
use HY.
(* Goal: @ex Point (fun X : Point => and (perp X A P Q) (and (Col X P Q) (not (@eq Point P Q)))) *)
exists Y.
(* Goal: and (perp Y A P Q) (and (Col Y P Q) (not (@eq Point P Q))) *)
repeat split;auto.

(* Goal: perp Y A P Q *)
unfold perp, Py4.
(* Goal: @eq F (Fminus (Py Y P Q) (Py A P Q)) F0 *)
rewrite col_pyth by assumption.
(* Goal: @eq F (Fminus (Fmult (Fmult (Fplus F1 F1) (DSeg P Y)) (DSeg P Q)) (Py A P Q)) F0 *)
rewrite H1.
(* Goal: @eq F (Fminus (Fmult (Fmult (Fplus F1 F1) (Fmult (Fdiv (Py A P Q) (Py P Q P)) (DSeg P Q))) (DSeg P Q)) (Py A P Q)) F0 *)
unfold Py.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (DSeg B A) (Fmult r (DSeg B C)) *)
uniformize_dir_seg.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (Fminus (Fmult (Fmult (Fplus F1 F1) (Fmult (Fdiv (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg P Q) (DSeg P Q))) (Fmult (DSeg A Q) (DSeg A Q))) (Fplus (Fmult (DSeg P Q) (DSeg P Q)) (Fmult (DSeg P Q) (DSeg P Q)))) (DSeg P Q))) (DSeg P Q)) (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg P Q) (DSeg P Q))) (Fmult (DSeg A Q) (DSeg A Q)))) F0 *)
field.
(* Goal: not (@eq F (Fplus (Fmult (DSeg P Q) (DSeg P Q)) (Fmult (DSeg P Q) (DSeg P Q))) F0) *)
replace (P ** Q * P ** Q + P ** Q * P ** Q) with (2*P ** Q * P ** Q) by ring.
(* Goal: not (@eq F (Fmult (Fmult (Fplus F1 F1) (DSeg P Q)) (DSeg P Q)) F0) *)
repeat apply nonzeromult; auto with Geom.
Qed.




Lemma on_perp_to_on_perp_d : forall A B C : Point,
       on_perp A B C  -> on_perp_d A B C ((2 + 2) * S B C A / Py B C B).
Proof.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
unfold on_perp, on_perp_d in *.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
decompose [and] H; clear H.
repeat split; try assumption.
(* Goal: @eq F (Fminus (Fmult (Fmult (Fplus F1 F1) (Fmult (Fdiv (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg P Q) (DSeg P Q))) (Fmult (DSeg A Q) (DSeg A Q))) (Fplus (Fmult (DSeg P Q) (DSeg P Q)) (Fmult (DSeg P Q) (DSeg P Q)))) (DSeg P Q))) (DSeg P Q)) (Fminus (Fplus (Fmult (DSeg A P) (DSeg A P)) (Fmult (DSeg P Q) (DSeg P Q))) (Fmult (DSeg A Q) (DSeg A Q)))) F0 *)
field.
auto with Geom.
replace (2+2) with (2*2) by ring.
repeat apply nonzeromult;auto with Geom.
intro.
assert ( Py B C B * / Py B C B = 0 * Py B C B).
rewrite H.
(* Goal: @eq F (Fmult r (DSeg B C)) (Fmult (Fminus F0 r) (Fopp (DSeg B C))) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
ring.
replace (Py B C B * / Py B C B) with 1 in H1.
2: field;auto with Geom.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: iff (@eq F (Fmult (S C A D) (Py C B D)) (Fmult (S C B D) (Py C A D))) (@eq F (Fmult (S C A D) (Py C B D)) (Fmult (S C B D) (Py C A D))) *)
intuition.
Qed.

Lemma on_line_d_iff_on_parallel_d : forall A B C r,
 on_line_d A B C r <-> on_parallel_d A B C B (0-r).
Proof.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: iff (on_line_d A B C r) (on_parallel_d A B C B (Fminus F0 r)) *)
unfold on_line_d, on_parallel_d.
(* Goal: iff (and (Col A B C) (not (@eq Point B C))) (and (not (@eq Point C B)) (parallel B A C B)) *)
unfold parallel, S4, Col.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
split.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
decompose [and] H; clear H.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
repeat split.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
uniformize_signed_areas.
(* Goal: @eq F (Fopp (S A B C)) F0 *)
(* Goal: @eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
rewrite H0.
(* Goal: @eq F (Fmult r (DSeg B C)) (Fmult (Fminus F0 r) (Fopp (DSeg B C))) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
ring.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: @eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
rewrite H3.
(* Goal: @eq F (DSeg B A) (Fmult r (DSeg B C)) *)
uniformize_dir_seg.
(* Goal: @eq F (Fmult r (DSeg B C)) (Fmult (Fminus F0 r) (Fopp (DSeg B C))) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
ring.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
decompose [and] H; clear H.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
repeat split.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
uniformize_signed_areas.
(* Goal: @eq F (Fmult r (DSeg B C)) (Fmult (Fminus F0 r) (Fopp (DSeg B C))) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
rewrite H2;ring.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: @eq F (DSeg B A) (Fmult r (DSeg B C)) *)
uniformize_dir_seg.
(* Goal: @eq F (Fmult r (DSeg B C)) (Fmult (Fminus F0 r) (Fopp (DSeg B C))) *)
(* Goal: forall _ : and (not (@eq Point C B)) (and (@eq F (Fplus (S A C B) (S A B B)) F0) (@eq F (DSeg B A) (Fmult (Fminus F0 r) (DSeg C B)))), and (@eq F (S A B C) F0) (and (not (@eq Point B C)) (@eq F (DSeg B A) (Fmult r (DSeg B C)))) *)
rewrite H3;ring.
Qed.

Lemma on_line_iff_on_parallel : forall A B C,
 on_line A B C <-> on_parallel A B C B.
Proof.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: iff (on_line A B C) (on_parallel A B C B) *)
unfold on_line, on_parallel.
(* Goal: iff (and (Col A B C) (not (@eq Point B C))) (and (not (@eq Point C B)) (parallel B A C B)) *)
unfold parallel, S4, Col.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
split.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
decompose [and] H; clear H.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
split.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
uniformize_signed_areas.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
decompose [and] H; clear H.
(* Goal: and (@eq F (S A B C) F0) (not (@eq Point B C)) *)
split.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
basic_simpl.
(* Goal: @eq F (S A B C) F0 *)
(* Goal: not (@eq Point B C) *)
uniformize_signed_areas.
(* Goal: not (@eq Point B C) *)
auto.
(* Goal: not (@eq Point B C) *)
auto.
Qed.

Definition eq_distance A B C D := Py A B A = Py C D C.

Definition harmonic A B C D := A**C / C**B = D**A / D**B.

Definition eq_product A B C D P Q R S := Py A B A * Py C D C = Py P Q P * Py R S R.

Definition tangent O1 A O2 B :=
Py O1 O2 O1 * Py O1 O2 O1 / (2+2) + 
Py O1 A O1   * Py O1 A O1 / (2+2) +  
Py O1 B O1   * Py O1 B O1 / (2+2) -
Py O1 O2 O1 * Py O1 A O1 / 2 -
Py O1 O2 O1 * Py O1 B O1 / 2 -
 Py O1 A O1 * Py O1 B O1 / 2.

Definition m_ratio Y U V r := 1+r<>0 /\ on_parallel_d Y U U V (r/(1+r)).

Definition inversion P Q O A := Py O Q O <> 0 /\ on_line_d P O Q (Py O A O / Py O Q O).

Definition eq_angle A B C D E F := 
  S A B C * Py D E F = S D E F  * Py A B C.

Definition co_circle A B C D :=
  S C A D * Py C B D = S C B D * Py C A D.

Lemma check_co_circle : forall A B C D, 
 co_circle A B C D <-> eq_angle C A D C B D.
Proof.
(* Goal: forall A B C D : Point, iff (co_circle A B C D) (eq_angle C A D C B D) *)
intros.
(* Goal: iff (co_circle A B C D) (eq_angle C A D C B D) *)
unfold co_circle, eq_angle.
(* Goal: iff (@eq F (Fmult (S C A D) (Py C B D)) (Fmult (S C B D) (Py C A D))) (@eq F (Fmult (S C A D) (Py C B D)) (Fmult (S C B D) (Py C A D))) *)
intuition.
Qed.

(* TODO remove auxiliary points *)


Definition inter_lc Y U V O N := on_foot N O U V /\ on_parallel_d Y N N U 1.

Definition on_circle Y O P Q' N' :=  inter_lc Y P Q' O N'.
