(***************************************************************************)
(* 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 (A B C A' B' C' P Q R T : Point) (_ : on_line C A B) (_ : on_line C' A' B') (_ : inter_ll P A' B A B') (_ : inter_ll Q A C' A' C) (_ : inter_ll R B' C B C') (_ : inter_ll T B' C P Q) (_ : not (@eq Point C R)) (_ : not (@eq Point C T)) (_ : parallel B' R C R) (_ : parallel B' T C T), @eq F (Fdiv (DSeg B' R) (DSeg C R)) (Fdiv (DSeg B' T) (DSeg C T)) *)
Require  Import area_method.

(** The Pappus line theorem *)

Theorem Pappus : forall A B C A' B' C' P Q R :Point,
  on_line C A B ->
  on_line C' A' B' ->
  inter_ll P A' B A B' ->
  inter_ll Q A C' A' C ->
  inter_ll R B' C B C' ->
  Col P Q R.
Proof.
(* Goal: forall (A B C A' B' C' P Q R T : Point) (_ : on_line C A B) (_ : on_line C' A' B') (_ : inter_ll P A' B A B') (_ : inter_ll Q A C' A' C) (_ : inter_ll R B' C B C') (_ : inter_ll T B' C P Q) (_ : not (@eq Point C R)) (_ : not (@eq Point C T)) (_ : parallel B' R C R) (_ : parallel B' T C T), @eq F (Fdiv (DSeg B' R) (DSeg C R)) (Fdiv (DSeg B' T) (DSeg C T)) *)
area_method.
Qed.

(** This version uses an extra point *)

Theorem Pappus_2 : forall A B C A' B' C' P Q R T:Point,
  on_line C A B ->
  on_line C' A' B' ->
  inter_ll P A' B A B' ->
  inter_ll Q A C' A' C ->
  inter_ll R B' C B C' ->
  inter_ll T B' C P Q ->
  C<>R -> C<>T ->
  parallel B' R C R ->
  parallel B' T C T ->
  B'**R / C**R = B'**T / C**T.
Proof.
(* Goal: forall (A B C A' B' C' P Q R T : Point) (_ : on_line C A B) (_ : on_line C' A' B') (_ : inter_ll P A' B A B') (_ : inter_ll Q A C' A' C) (_ : inter_ll R B' C B C') (_ : inter_ll T B' C P Q) (_ : not (@eq Point C R)) (_ : not (@eq Point C T)) (_ : parallel B' R C R) (_ : parallel B' T C T), @eq F (Fdiv (DSeg B' R) (DSeg C R)) (Fdiv (DSeg B' T) (DSeg C T)) *)
area_method.
Qed.
