(***************************************************************************)
(* 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 B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
Require  Import area_method.

Lemma l3_44: forall O A X P Q U R G r N,
 on_line_d P O A r ->
 inversion Q P O A ->
 is_midpoint U P O ->
 inter_lc R O X U N ->
 inversion G R O A -> 
 perp G Q O A.
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

Theorem example6_9 : forall L M N A B C SS:Point,
 parallel A M M C -> 
 parallel A N N B -> 
 parallel A SS SS L ->
 M<>C -> 
 N<>B -> 
 SS<>L -> 
 inter_ll L B C A SS ->
 inter_ll N B A C SS ->
 inter_ll M A C B SS ->
 A**M/M**C+A**N/N**B = A**SS/SS**L.
Proof.
(* Goal: forall (L M N A B C SS : Point) (_ : parallel A M M C) (_ : parallel A N N B) (_ : parallel A SS SS L) (_ : not (@eq Point M C)) (_ : not (@eq Point N B)) (_ : not (@eq Point SS L)) (_ : inter_ll L B C A SS) (_ : inter_ll N B A C SS) (_ : inter_ll M A C B SS), @eq F (Fplus (Fdiv (DSeg A M) (DSeg M C)) (Fdiv (DSeg A N) (DSeg N B))) (Fdiv (DSeg A SS) (DSeg SS L)) *)
am_before_field.
(* Goal: @eq F (Fminus (Fopp (Fmult (S A B SS) (Finv (S C B SS)))) (Fmult (S A C SS) (Finv (Fopp (S C B SS))))) (Finv (Fopp (Fmult (S C B SS) (Finv (Fminus (S A B SS) (S A C SS)))))) *)
(* Goal: @eq F (Fminus (Fopp (Fmult (S A B SS) (Finv (S C B SS)))) (Fmult (S A C SS) (Finv (Fopp (S C B SS))))) F1 *)
field_and_conclude.
(* Goal: @eq F (Fminus (Fopp (Fmult (S A B SS) (Finv (S C B SS)))) (Fmult (S A C SS) (Finv (Fopp (S C B SS))))) (Finv (Fopp (Fmult (S C B SS) (Finv (Fminus (S A B SS) (S A C SS)))))) *)
(* Goal: @eq F (Fminus (Fopp (Fmult (S A B SS) (Finv (S C B SS)))) (Fmult (S A C SS) (Finv (Fopp (S C B SS))))) F1 *)
field_and_conclude.
(* Goal: @eq F (Fminus (Fopp (Fmult (S A B SS) (Finv (S C B SS)))) (Fmult (S A C SS) (Finv (Fopp (S C B SS))))) F1 *)
intuition.
Qed.

Theorem th6_41_b : forall A B C M N L P K X1 X2:Point,
 is_midpoint M A B ->
 is_midpoint N A C ->
 is_midpoint K B C ->
 on_parallel X1 A C M ->
 on_parallel X2 K B N ->
 inter_ll P X1 A X2 K ->
 is_midpoint L A K ->
 B<>C -> 
 parallel L P B C -> 
 2+2<>0 ->
 L<>P ->
 L**P / B**C = (1+2)/(2+2).
Proof.
(* Goal: forall (A B C M N L P K : Point) (_ : is_midpoint M A B) (_ : is_midpoint N A C) (_ : is_midpoint K B C) (_ : is_midpoint L A K) (_ : on_inter_parallel_parallel P A C M K B N) (_ : not (@eq Point B C)) (_ : not (@eq Point P L)) (_ : not (@eq Point P A)) (_ : not (@eq Point P K)) (_ : parallel L P B C) (_ : not (@eq F (S A B C) F0)) (_ : not (@eq F (Fplus (Fplus F1 F1) (Fplus F1 F1)) F0)), @eq F (Fdiv (DSeg L P) (DSeg B C)) (Fdiv (Fplus F1 (Fplus F1 F1)) (Fplus (Fplus F1 F1) (Fplus F1 F1))) *)
geoInit.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
eliminate P;area_method.
Qed.

Lemma th6_232 : forall A B C D P Q,
  on_parallel_d D A B C 1 ->
  is_midpoint P B D ->
  is_midpoint Q A C ->
  parallel P Q A B.
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

Lemma th6_234_1 : forall A B C D O E F,
  on_parallel D A B C ->
  inter_ll O A C B D ->
  on_inter_line_parallel E O B C A B ->
  on_inter_line_parallel F O A D A B ->
  Col O E F.
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

Lemma th6_239 : forall A B C D P Q R A1 D1 J,
 is_midpoint Q B C ->
 is_midpoint P B A ->
 is_midpoint R C D ->
 inter_ll A1 D Q B R ->
 inter_ll D1 A Q C P ->
 inter_ll J A A1 D D1 ->
 parallel A J A1 J ->
 A<>J ->
 A1<>J ->
  A**J/A1**J=- (2+1).
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

Theorem th6_258 : forall A B C D E F M N P Q:Point,
  on_parallel_d D B E A 1 ->
  on_line C A E ->
  on_line F B D ->
  inter_ll M D C A F ->
  inter_ll N E F B C ->
  inter_ll P M N A D ->
  inter_ll Q M N E B ->
  D<>P -> E<>Q ->
  parallel A P D P ->
  parallel B Q E Q ->
 A**P/D**P=B**Q/E**Q.
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.


Lemma exercice2_38_3 : forall Y P Q U V A B,
  inter_ll Y P Q U V -> 
  on_line A U V -> 
  S4 U P V Q <>0 ->
  ~Col U V Q ->
  S A B Y = (S U B V) * (S A P Q) / S4 U P V Q.
Proof.
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

Theorem th6_41 : forall A B C M N L P K:Point,
  is_midpoint M A B ->
  is_midpoint N A C ->
  is_midpoint K B C ->
  is_midpoint L A K ->
  on_inter_parallel_parallel P A C M K B N -> 
  B<>C -> 
  P<>L ->
  P<>A ->
  P<>K ->
  parallel L P B C -> 
  S A B C <> 0 -> 
  2+2 <> 0 ->
  L**P / B**C = (1+2)/(2+2).
Proof.
(* Goal: forall (A B C M N L P K : Point) (_ : is_midpoint M A B) (_ : is_midpoint N A C) (_ : is_midpoint K B C) (_ : is_midpoint L A K) (_ : on_inter_parallel_parallel P A C M K B N) (_ : not (@eq Point B C)) (_ : not (@eq Point P L)) (_ : not (@eq Point P A)) (_ : not (@eq Point P K)) (_ : parallel L P B C) (_ : not (@eq F (S A B C) F0)) (_ : not (@eq F (Fplus (Fplus F1 F1) (Fplus F1 F1)) F0)), @eq F (Fdiv (DSeg L P) (DSeg B C)) (Fdiv (Fplus F1 (Fplus F1 F1)) (Fplus (Fplus F1 F1) (Fplus F1 F1))) *)
geoInit.
(* we force the elimination of P first *)
eliminate P;
(* Goal: forall (Y P Q U V A B : Point) (_ : inter_ll Y P Q U V) (_ : on_line A U V) (_ : not (@eq F (S4 U P V Q) F0)) (_ : not (Col U V Q)), @eq F (S A B Y) (Fdiv (Fmult (S U B V) (S A P Q)) (S4 U P V Q)) *)
area_method.
Qed.

