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

Definition Py A B C := A**B * A**B + B**C * B**C - A**C * A**C.
Definition Py4 A B C D := Py A B D - Py C B D.
Definition per A B C := Py A B C = 0.
Definition perp A B C D := Py4 A C B D = 0.
Definition on_foot (Y P U V : Point) := perp Y P U V /\ Col Y U V /\ U<>V.

(* We introduce three additionnal axioms *)

Axiom perp_perp_para : forall A B C D E F,
 C<>D ->
 perp A B C D -> perp E F C D -> parallel A B E F.

Axiom perp_para_perp : forall A B C D E F, 
  A<>B ->
  perp A B C D -> parallel A B E F -> perp E F C D.

(* We use the square to get rid of sign issues *)

Axiom on_foot_area : forall A B C F, 
  on_foot F A B C ->
  2 * 2 * S A B C * S A B C = A**F * A**F * B**C * B**C.

Lemma on_foot_area_paper : forall A B C F, 
  perp F A B C -> Col F B C ->
  2 * 2 * S A B C * S A B C = A**F * A**F * B**C * B**C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq field.F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A F) (DSeg A F)) (DSeg B C)) (DSeg B C)) *)
cases_equality B C.
(* Goal: @eq field.F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A F) (DSeg A F)) (DSeg B C)) (DSeg B C)) *)
(* Goal: @eq field.F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A F) (DSeg A F)) (DSeg B C)) (DSeg B C)) *)
subst.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq field.F F0 F0 *)
(* Goal: @eq field.F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A F) (DSeg A F)) (DSeg B C)) (DSeg B C)) *)
trivial.
(* Goal: @eq field.F (Fmult (Fmult (Fmult (Fplus F1 F1) (Fplus F1 F1)) (S A B C)) (S A B C)) (Fmult (Fmult (Fmult (DSeg A F) (DSeg A F)) (DSeg B C)) (DSeg B C)) *)
apply on_foot_area.
(* Goal: on_foot F A B C *)
unfold on_foot;auto.
Qed.


Lemma pyth_simpl_1 : forall A B, Py A A B = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq F F0 F0 *)
reflexivity.
Qed.

Lemma pyth_simpl_2 : forall A B, Py A B B = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq F F0 F0 *)
reflexivity.
Qed.

Hint Rewrite pyth_simpl_1  pyth_simpl_2 : seg_simplifications.
Hint Resolve pyth_simpl_1 pyth_simpl_2 : Geom.

Lemma test_basic_simpl : forall A B, Py A A B = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq F F0 F0 *)
reflexivity.
Qed.

Lemma pyth_sym : forall A B C, Py A B C = Py C B A.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Hint Resolve pyth_sym : Geom.

Lemma pyth_simpl_3 : forall A B, Py A B A = 2 * A**B * A**B.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma pyth_simpl_4 : forall A B, Py A B A = Py B A B.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Hint Immediate pyth_simpl_4 : Geom.

Ltac uniformize_pys :=
  repeat (rewrite pyth_simpl_1);
  repeat (rewrite pyth_simpl_2);
  repeat
   match goal with
   |  |- context [(Py ?A ?B ?C)] =>
    (match goal with
       |  |- context [(Py C B A)] => rewrite (pyth_sym A B C) in *   
       end)
   |  |- context [(Py ?A ?B ?A)] =>
    (match goal with
       |  |- context [(Py B A B)] => rewrite (pyth_simpl_4 A B) in *   
       end)
   end.

Lemma test_uniformize_pys : forall A B C, 
 Py A B C - Py C B A + Py A A C + Py A C C + Py A B A - Py B A B = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Fminus (Fplus (Fplus (Fplus (Fminus (Py A B C) (Py C B A)) (Py A A C)) (Py A C C)) (Py A B A)) (Py B A B)) F0 *)
uniformize_pys.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma square_to_py : forall A B, A**B * A**B = Py A B A / 2.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Fmult (DSeg A B) (DSeg A B)) (Fdiv (Py A B A) (Fplus F1 F1)) *)
rewrite pyth_simpl_3.
(* Goal: @eq F (Fmult (DSeg A B) (DSeg A B)) (Fdiv (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fplus F1 F1)) *)
field.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
auto with Geom.
Qed.

Lemma col_pyth : forall A B C, Col A B C -> Py A B C = 2 * B**A * B**C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq F (Fminus (Fplus (Fmult (DSeg A B) (DSeg A B)) (Fmult (DSeg B C) (DSeg B C))) (Fmult (DSeg A C) (DSeg A C))) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
replace (A**C) with (A**B + B**C) by (apply chasles;auto).
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.


Lemma py4_1 : forall A B C D, Py4 A B C D = - Py4 A D C B.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_2 : forall A B C D, Py4 A B C D = Py4 B A D C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_3 : forall A B C D, Py4 A B C D = - Py4 B C D A.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_4 : forall A B C D, Py4 A B C D = Py4 C D A B.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_5 : forall A B C D, Py4 A B C D = - Py4 C B A D.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_6 : forall A B C D, Py4 A B C D = Py4 D C B A.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_7 : forall A B C D, Py4 A B C D = - Py4 D A B C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C D) (Fopp (Py4 D A B C)) *)
unfold Py4, Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Hint Resolve py4_1 py4_2 py4_3 py4_4 py4_5 py4_6 py4_7 : Geom.

Lemma py4_simpl_1 : forall A B C, Py4 A A B C = - Py B A C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 B A C A) F0 *)
unfold Py4.
(* Goal: @eq F (Fminus (Py B A C) (Py A A C)) (Py B A C) *)
rewrite pyth_simpl_1.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_simpl_2 : forall A B C, Py4 B A A C = Py B A C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 B A C A) F0 *)
unfold Py4.
(* Goal: @eq F (Fminus (Py B A C) (Py A A C)) (Py B A C) *)
rewrite pyth_simpl_1.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_simpl_3 : forall A B C, Py4 A B A C = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 B A C A) F0 *)
unfold Py4.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_simpl_4 : forall A B C, Py4 B A C A = 0.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 B A C A) F0 *)
unfold Py4.
(* Goal: @eq F (Fminus (Py B A A) (Py C A A)) F0 *)
repeat (rewrite pyth_simpl_2).
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_simpl_5 : forall A B C, Py4 B C A A = - Py B A C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 B C A A) (Fopp (Py B A C)) *)
rewrite py4_6.
(* Goal: @eq F (Py4 A A C B) (Fopp (Py B A C)) *)
rewrite py4_simpl_1.
(* Goal: @eq F (Fopp (Fopp (Py C A B))) (Py B A C) *)
rewrite pyth_sym.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma py4_simpl_6 : forall A B C, Py4 A B C A = Py B A C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py4 A B C A) (Py B A C) *)
rewrite py4_5.
(* Goal: @eq F (Fopp (Py4 C B A A)) (Py B A C) *)
rewrite py4_simpl_5.
(* Goal: @eq F (Fopp (Fopp (Py C A B))) (Py B A C) *)
rewrite pyth_sym.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Hint Resolve 
py4_simpl_1 
py4_simpl_2 
py4_simpl_3 
py4_simpl_4 
py4_simpl_5 
py4_simpl_6 : Geom.

Hint Rewrite
pyth_simpl_1
pyth_simpl_2
py4_simpl_1 
py4_simpl_2 
py4_simpl_3 
py4_simpl_4 
py4_simpl_5 
py4_simpl_6 : py_simplifications.

Ltac py_simpl := autorewrite with py_simplifications in *.

Lemma test_py_simpl : forall A B C, Py A A B = 0 -> Py A A B + Py B A A + Py4 B A C A = 0.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Fplus (Fplus (Py A A B) (Py B A A)) (Py4 B A C A)) F0 *)
py_simpl.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_1 : forall A B C D,
perp A B C D -> perp A B D C.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 A D B C) with (- Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_2 : forall A B C D,
perp A B C D -> perp B A C D.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 B C A D) with (- Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_3 : forall A B C D,
perp A B C D -> perp B A D C.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 B D A C) with (Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_4 : forall A B C D,
perp A B C D -> perp C D A B.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 C A D B) with (Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_5 : forall A B C D,
perp A B C D -> perp C D B A.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 C B D A) with (- Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_6 : forall A B C D,
perp A B C D -> perp D C A B.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 D A C B) with (- Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_7 : forall A B C D,
perp A B C D -> perp D C B A.
Proof.
(* Goal: forall (A B C D : Point) (_ : perp A B C D), perp D C B A *)
unfold perp.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
replace (Py4 D B C A) with ( Py4 A C B D) by auto with Geom.
(* Goal: @eq F (Py4 A C B D) F0 *)
rewrite H.
(* Goal: @eq F F0 F0 *)
ring.
Qed.

Lemma perp_8 : forall A B C,
perp A B B C -> per A B C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: perp A B B C *)
unfold perp, Py4 in *.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq Point A B *)
(* Goal: @eq Point A B *)
auto.
Qed.

Lemma perp_9 : forall A B C,
per A B C -> perp A B B C.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: perp A B B C *)
unfold perp, Py4 in *.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq Point A B *)
(* Goal: @eq Point A B *)
auto.
Qed.


Hint Resolve 
perp_1
perp_2
perp_3
perp_4
perp_5
perp_6
perp_7 : Geom.

Hint Immediate perp_8 perp_9 : Geom.

Lemma not_eq_py_not_zero : forall A B, A<>B -> Py A B A <> 0.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
Proof with auto with Geom.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq F (Py A B C) (Fmult (Fmult (Fplus F1 F1) (DSeg B A)) (DSeg B C)) *)
unfold Py.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq Point A B *)
basic_simpl.
unfold not;intro.
apply H.
(* Goal: @eq F F0 F0 *)
replace (A ** B * A ** B + A ** B * A ** B) with (2* A ** B * A ** B) in H0 by ring.
IsoleVar (A ** B ) H0...
replace (0 / A ** B / 2) with 0 in H0 ...
(* Goal: @eq F (Fmult (DSeg A B) (DSeg A B)) (Fdiv (Fmult (Fmult (Fplus F1 F1) (DSeg A B)) (DSeg A B)) (Fplus F1 F1)) *)
field...
Qed.

Hint Resolve not_eq_py_not_zero : Geom.

Lemma py_zero_eq : forall A B, Py A B A = 0 -> A = B.
Proof.
(* Goal: forall (A B : Point) (_ : @eq F (Py A B A) F0), @eq Point A B *)
intros.
(* Goal: @eq Point A B *)
cases_equality A B.
(* Goal: @eq Point A B *)
(* Goal: @eq Point A B *)
auto.
(* Goal: @eq Point A B *)
unfold Py in H.
(* Goal: @eq Point A B *)
uniformize_dir_seg.
(* Goal: @eq Point A B *)
basic_simpl.
(* Goal: @eq Point A B *)
ring_simplify in H.
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
assert (A**B<>0) by auto with Geom.
(* Goal: @eq Point A B *)
assert (2 * A ** B * A ** B <>0).
(* Goal: not (@eq F (Fplus F1 F1) F0) *)
repeat apply nonzeromult;auto with Geom.
(* Goal: @eq Point A B *)
intuition.
Qed.

Hint Resolve py_zero_eq : Geom.
