(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                                                                          *)
(*                          Constructive Geometry                           *)
(*                             according to                                 *)
(*                            Jan von Plato                                 *)
(*                                                                          *)
(*                               Coq V5.10                                  *)
(*									    *)
(*			        Gilles Kahn 				    *)
(*				   INRIA                                    *)
(*		              Sophia-Antipolis		 	            *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work started in Turin in May 95 with Yves Bertot.  *)
(* Thanks to the Newton Institute for providing an exceptional work         *)
(* environment in Summer 1995 so that I could complete this.                *)
(****************************************************************************)

(****************************************************************************)
(*                                part2.v                                   *)
(****************************************************************************)
Require Import basis.
Require Import part1.

Theorem thm4_1a :
 forall (x : Segment) (l : Line),
 DiLn l (ln x) -> Apart (origin x) l \/ Apart (extremity x) l.
Proof.
(* Goal: forall (x : Segment) (l : Line) (_ : or (Apart (origin x) l) (Apart (extremity x) l)), DiLn l (ln x) *)
intros x l.
(* Goal: forall _ : or (Apart (origin x) l) (Apart (extremity x) l), DiLn l (ln x) *)
generalize (inc_ln2 x); generalize (inc_ln1 x).
(* Goal: forall (_ : Incident (pt x) (line1 x)) (_ : Incident (pt x) (line2 x)) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
unfold Incident in |- *.
(* Goal: forall (_ : not (Apart (origin x) (ln x))) (_ : not (Apart (extremity x) (ln x))) (_ : DiLn l (ln x)), or (Apart (origin x) l) (Apart (extremity x) l) *)
generalize (el_ax x l (ln x)).
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
tauto.
Qed.

Theorem thm4_1b :
 forall (x : Segment) (l : Line),
 Apart (origin x) l \/ Apart (extremity x) l -> DiLn l (ln x).
Proof.
(* Goal: forall (x : Segment) (l : Line) (_ : or (Apart (origin x) l) (Apart (extremity x) l)), DiLn l (ln x) *)
intros x l.
(* Goal: forall _ : or (Apart (origin x) l) (Apart (extremity x) l), DiLn l (ln x) *)
generalize (inc_ln2 x); generalize (inc_ln1 x).
(* Goal: forall (_ : Incident (pt x) (line1 x)) (_ : Incident (pt x) (line2 x)) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
unfold Incident in |- *.
(* Goal: forall (_ : not (Apart (pt x) (line1 x))) (_ : not (Apart (pt x) (line2 x))) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
intros H' H'0 H'1; elim H'1; intro H'2; clear H'1.
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
elim (cmp_apt_diln (origin x) l (ln x)); tauto.
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
elim (cmp_apt_diln (extremity x) l (ln x)); tauto.
Qed.
Hint Resolve thm4_1a thm4_1b.

Theorem thm4_1c :
 forall (x : Twolines) (a : Point),
 DiPt a (pt x) -> Apart a (line1 x) \/ Apart a (line2 x).
Proof.
(* Goal: forall (x : Twolines) (a : Point) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
intros x a.
(* Goal: forall _ : or (Apart a (line1 x)) (Apart a (line2 x)), DiPt a (pt x) *)
generalize (inc_pt2 x); generalize (inc_pt1 x).
(* Goal: forall (_ : Incident (pt x) (line1 x)) (_ : Incident (pt x) (line2 x)) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
unfold Incident in |- *.
(* Goal: forall (_ : not (Apart (pt x) (line1 x))) (_ : not (Apart (pt x) (line2 x))) (_ : DiPt a (pt x)), or (Apart a (line1 x)) (Apart a (line2 x)) *)
intros H' H'0 H'1.
(* Goal: or (Apart a (line1 x)) (Apart a (line2 x)) *)
generalize (el_ax (Seg a (pt x) H'1) (line1 x) (line2 x)); simpl in |- *.
(* Goal: forall _ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
cut (DiLn (line1 x) (line2 x)).
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
tauto.
(* Goal: DiLn (line1 x) (line2 x) *)
elim x; auto.
Qed.

Theorem thm4_1d :
 forall (x : Twolines) (a : Point),
 Apart a (line1 x) \/ Apart a (line2 x) -> DiPt a (pt x).
Proof.
(* Goal: forall (x : Twolines) (a : Point) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
intros x a.
(* Goal: forall _ : or (Apart a (line1 x)) (Apart a (line2 x)), DiPt a (pt x) *)
generalize (inc_pt2 x); generalize (inc_pt1 x).
(* Goal: forall (_ : Incident (pt x) (line1 x)) (_ : Incident (pt x) (line2 x)) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
unfold Incident in |- *.
(* Goal: forall (_ : not (Apart (pt x) (line1 x))) (_ : not (Apart (pt x) (line2 x))) (_ : or (Apart a (line1 x)) (Apart a (line2 x))), DiPt a (pt x) *)
intros H' H'0 H'1; elim H'1; intro H'2; clear H'1.
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
generalize (cmp_apt_dipt a (pt x) (line1 x)); tauto.
(* Goal: forall (_ : DiLn (line1 x) (line2 x)) (_ : forall _ : DiLn (line1 x) (line2 x), or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x)))), or (Apart a (line1 x)) (Apart a (line2 x)) *)
(* Goal: DiLn (line1 x) (line2 x) *)
generalize (cmp_apt_dipt a (pt x) (line2 x)); tauto.
Qed.

Theorem Symmetry_of_Apart :
 forall x y : Segment,
 Apart (origin x) (ln y) \/ Apart (extremity x) (ln y) ->
 Apart (origin y) (ln x) \/ Apart (extremity y) (ln x).
(* Goal: forall (x y : Segment) (_ : or (Apart (origin x) (ln y)) (Apart (extremity x) (ln y))), or (Apart (origin y) (ln x)) (Apart (extremity y) (ln x)) *)
intros x y H'.
(* Goal: or (Apart (origin y) (ln x)) (Apart (extremity y) (ln x)) *)
apply thm4_1a.
(* Goal: DiLn (ln x) (ln y) *)
apply sym_DiLn; auto.
Qed.

Theorem thm4_3a :
 forall (x : Segment) (c : Point), Apart c (ln x) -> DiPt c (origin x).
Proof.
(* Goal: forall (x : Segment) (c : Point) (_ : Apart c (ln x)), DiPt c (extremity x) *)
intros x c H'.
(* Goal: DiPt c (origin x) *)
elim (cmp_apt_dipt c (origin x) (ln x)); trivial.
(* Goal: forall _ : Apart (origin x) (ln x), DiPt c (origin x) *)
intro H0; elim (inc_ln1 x); trivial.
Qed.

Theorem thm4_3b :
 forall (x : Segment) (c : Point), Apart c (ln x) -> DiPt c (extremity x).
Proof.
(* Goal: forall (x : Segment) (c : Point) (_ : Apart c (ln x)), DiPt c (extremity x) *)
intros x c H'.
(* Goal: DiPt c (extremity x) *)
elim (cmp_apt_dipt c (extremity x) (ln x)); trivial.
(* Goal: forall _ : Apart (extremity x) (ln x), DiPt c (extremity x) *)
intro H0; elim (inc_ln2 x); trivial.
Qed.

Definition Side1 : Triangle -> Segment.
Proof.
(* Goal: forall t : Triangle, DiLn (ln (base t)) (ln (Side2 t)) *)
intro H'; elim H'; clear H'.
(* Goal: forall (summit : Point) (base : Segment) (_ : Apart summit (ln base)), Segment *)
intros summit base H'.
(* Goal: Segment *)
apply (Seg summit (origin base)).
(* Goal: DiPt summit (origin base) *)
apply thm4_3a; trivial.
Defined.

Definition Side2 : Triangle -> Segment.
Proof.
(* Goal: forall t : Triangle, DiLn (ln (base t)) (ln (Side2 t)) *)
intro H'; elim H'; clear H'.
(* Goal: forall (summit : Point) (base : Segment) (_ : Apart summit (ln base)), Segment *)
intros summit base H'.
(* Goal: Segment *)
apply (Seg summit (extremity base)).
(* Goal: DiPt summit (extremity base) *)
apply thm4_3b; trivial.
Defined.

Theorem auxs1 : forall t : Triangle, origin (base t) = extremity (Side1 t).
Proof.
(* Goal: forall t : Triangle, @eq Point (summit t) (origin (Side2 t)) *)
intro t; elim t; auto.
Qed.

Theorem auxs2 : forall t : Triangle, extremity (base t) = extremity (Side2 t).
Proof.
(* Goal: forall t : Triangle, @eq Point (summit t) (origin (Side2 t)) *)
intro t; elim t; auto.
Qed.

Theorem auxs3 : forall t : Triangle, summit t = origin (Side1 t).
Proof.
(* Goal: forall t : Triangle, @eq Point (summit t) (origin (Side2 t)) *)
intro t; elim t; auto.
Qed.

Theorem auxs4 : forall t : Triangle, summit t = origin (Side2 t).
Proof.
(* Goal: forall t : Triangle, @eq Point (summit t) (origin (Side2 t)) *)
intro t; elim t; auto.
Qed.

Theorem thm4_3c : forall t : Triangle, DiLn (ln (base t)) (ln (Side1 t)).
Proof.
(* Goal: forall t : Triangle, DiLn (ln (base t)) (ln (Side2 t)) *)
intro H'; elim H'; clear H'.
(* Goal: forall (summit : Point) (base0 : Segment) (Tri_cond : Apart summit (ln base0)), DiLn (ln (base (Tri summit base0 Tri_cond))) (ln (Side2 (Tri summit base0 Tri_cond))) *)
intros summit base Tri_cond.
elim (cmp_apt_diln summit (ln base) (ln (Side1 (Tri summit base Tri_cond))));
 auto.
Qed.

Theorem thm4_3d : forall t : Triangle, DiLn (ln (base t)) (ln (Side2 t)).
Proof.
(* Goal: forall t : Triangle, DiLn (ln (base t)) (ln (Side2 t)) *)
intro H'; elim H'; clear H'.
(* Goal: forall (summit : Point) (base0 : Segment) (Tri_cond : Apart summit (ln base0)), DiLn (ln (base (Tri summit base0 Tri_cond))) (ln (Side2 (Tri summit base0 Tri_cond))) *)
intros summit base Tri_cond.
elim (cmp_apt_diln summit (ln base) (ln (Side2 (Tri summit base Tri_cond))));
 auto.
Qed.

Hint Resolve thm4_3c thm4_3d.


