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

(* Goal: forall (Y P Q U V A C D : Point) (_ : inter_ll Y P Q U V) (_ : not (@eq Point C D)) (_ : parallel A Y C D) (_ : parallel Y A C D) (_ : not (@eq Point A Y)) (_ : not (@eq Point Y A)), @eq F (Fplus (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg Y A) (DSeg C D))) F0 *)
Require  Import area_method.

(***********************)
(* Ratios elimination *)
(***********************)

Lemma test_on_line_4 : forall I X Y A B C , 
  on_line I X Y -> B<>C -> parallel A I B C ->
  False ->
  A**I/B**C = 1.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg A I) (DSeg B C)) F1 *)
eliminate I.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
Qed.

(** Test on_line_d in a ratio *)

Lemma test_on_line_d_11 : forall Y P Q A C D lambda,
  on_line_d Y P Q lambda ->  C<>D -> parallel A Y C D ->
  False -> A**Y/C**D =  1.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
Qed.

Lemma test_on_line_d_12 : forall Y P Q A C D lambda,
  on_line_d Y P Q lambda ->  C<>D -> parallel Y A C D ->
  False ->
  Y**A/C**D = 1.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (lambda : F) (_ : on_parallel_d Y R P Q lambda) (_ : not (@eq Point C D)) (_ : parallel A Y C D), @eq F (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg A Y) (DSeg C D)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
Qed.

(*
Lemma test_on_line_d_13 : forall Y P Q A C D lambda,
  on_line_d Y P Q lambda ->  Y<>A -> parallel C D Y A ->
  False ->
  C**D/Y**A = C**D.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
Qed.
*)

(** Test inter_ll in a ratio *)

(** Test cases where Y occurs both in denominator and numerator *)

Lemma test_inter_ll_1 :  forall Y P Q U V,
  inter_ll Y P Q U V ->  V<>Y -> parallel U Y V Y ->
  U**Y/V**Y = S U P Q / S V P Q.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_2 :  forall Y P Q U V,
  inter_ll Y P Q U V ->  U<>Y -> parallel V Y U Y ->
  V**Y/U**Y = S V P Q / S U P Q.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_3 :  forall Y P Q U V,
  inter_ll Y P Q U V ->  Q<>Y -> parallel P Y Q Y ->
  P**Y/Q**Y =S P U V / S Q U V.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_4 :  forall Y P Q U V,
  inter_ll Y P Q U V ->  P<>Y -> parallel Q Y P Y ->
  Q**Y/P**Y =S Q U V / S P U V.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.


Lemma test_inter_ll : forall T P Q A B C D,
 inter_ll T A B C D-> 
 parallel T P T Q ->
 T<>Q ->
 P<>T ->
 T ** P / T ** Q = T ** P / T ** Q + 1 - 1.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg T P) (DSeg T Q)) (Fminus (Fplus (Fdiv (DSeg T P) (DSeg T Q)) F1) F1) *)
eliminate T;ring.
Qed.

Lemma test_inter_ll_1b :  forall Y P Q U V,
  inter_ll Y P Q U V ->  Y<>V -> parallel Y U Y V ->
  Y**U/Y**V = S U P Q / S V P Q.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_2b :  forall Y P Q U V,
  inter_ll Y P Q U V ->  Y<>U -> parallel V Y Y U ->
  V**Y/Y**U = - (S V P Q / S U P Q).
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_3b :  forall Y P Q U V,
  inter_ll Y P Q U V ->  Q<>Y -> parallel Y P Q Y ->
  Y**P/Q**Y = - (S P U V / S Q U V).
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_inter_ll_4b :  forall Y P Q U V,
  inter_ll Y P Q U V ->  P<>Y -> parallel Q Y P Y ->
  Q**Y/P**Y =S Q U V / S P U V.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.


Lemma test_inter_ll_5 :  forall Y P Q U V A C,
  inter_ll Y P Q U V ->  C<>Y -> parallel A Y C Y ->
  A**Y/C**Y = A**Y/C**Y.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (lambda : F) (_ : on_parallel_d Y R P Q lambda) (_ : not (@eq Point C D)) (_ : parallel A Y C D), @eq F (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg A Y) (DSeg C D)) *)
intros.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
elimi_inter_ll P Q U V A Y C Y H; reflexivity.
(* TODO debug *)
Qed.

Lemma test_inter_ll_gen_1 :  forall Y P Q U V A C D,
  inter_ll Y P Q U V ->  C<>D -> parallel A Y C D ->
  False ->
  A**Y/C**D = 1.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
(* Goal: @eq F (Fdiv (S A U V) (Fplus (S C U D) (S C D V))) F1 *)
intuition.
Qed.

Lemma test_inter_ll_gen_2 :  forall Y P Q U V A C D,
  inter_ll Y P Q U V ->  C<>D -> parallel A Y C D -> parallel Y A C D -> A<>Y -> Y<>A ->
  A**Y/C**D + Y**A/C**D=0.
Proof.
(* Goal: forall (Y P Q U V A C D : Point) (_ : inter_ll Y P Q U V) (_ : not (@eq Point C D)) (_ : parallel A Y C D) (_ : parallel Y A C D) (_ : not (@eq Point A Y)) (_ : not (@eq Point Y A)), @eq F (Fplus (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg Y A) (DSeg C D))) F0 *)
area_method.
Qed.

Lemma test_inter_ll_gen_3 :  forall Y P Q U V A C D,
  inter_ll Y P Q U V ->  A<>Y -> C<>D -> parallel C D A Y ->
  C**D/A**Y = C**D/A**Y.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (lambda : F) (_ : on_parallel_d Y R P Q lambda) (_ : not (@eq Point C D)) (_ : parallel A Y C D), @eq F (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg A Y) (DSeg C D)) *)
intros.
(* Goal: @eq F (Fdiv (DSeg C D) (DSeg A Y)) (Fdiv (DSeg C D) (DSeg A Y)) *)
eliminate Y.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
reflexivity.
Qed.

Lemma test_on_parallel_d_1 : forall A C D Y R P Q lambda,
  on_parallel_d Y R P Q lambda ->
  C<>D ->
  parallel A Y C D ->
  A**Y/C**D = A**Y/C**D.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (lambda : F) (_ : on_parallel_d Y R P Q lambda) (_ : not (@eq Point C D)) (_ : parallel A Y C D), @eq F (Fdiv (DSeg A Y) (DSeg C D)) (Fdiv (DSeg A Y) (DSeg C D)) *)
intros.
(* Goal: @eq F (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) (Fdiv F1 (Fdiv (S A U V) (Fplus (S C U D) (S C D V)))) *)
eliminate Y; reflexivity.
Qed.

Lemma test_on_foot_1 : forall A C D Y R P Q,
  on_foot Y R P Q ->
  C<>D ->
  parallel A Y C D ->
  A**Y/C**D = 1-1+ A**Y/C**D.
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
eliminate Y;
field;assumption.
Qed.

Lemma test_on_foot_2 : forall A C D Y R P Q,
	on_foot Y R P Q ->
        False ->
        C <> D ->
        parallel Y A C D ->
        Y**A/C**D = - - (Y**A/C**D).
Proof.
(* Goal: forall (A C D Y R P Q : Point) (_ : on_foot Y R P Q) (_ : False) (_ : not (@eq Point C D)) (_ : parallel Y A C D), @eq F (Fdiv (DSeg Y A) (DSeg C D)) (Fopp (Fopp (Fdiv (DSeg Y A) (DSeg C D)))) *)
geoInit.
eliminate Y;
field;auto.
Qed.

