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

(****************************************************************************)
(*                       orthogonality.v                                    *)
(****************************************************************************)

Require Import basis.
Require Import part1.
Require Import part2.
Require Import part3.
Require Import affinity.

Parameter Unort : Line -> Line -> Prop.

Axiom O1 : forall l m : Line, ConLn l m \/ Unort l m.

Axiom O2 : Separating Line (fun l m : Line => ConLn l m /\ Unort l m).

Definition Ort := Negation Line Unort.

Axiom
  constructed_orthogonal :
    forall (l : Line) (a : Point), {l' : Line | Ort l' l /\ Incident a l'}.

Definition ort : Line -> Point -> Line.
Proof.
(* Goal: forall (_ : Line) (_ : Point), Line *)
intros l a; elim (constructed_orthogonal l a).
(* Goal: forall (x : Line) (_ : and (Ort x l) (Incident a x)), Line *)
intros x H'; exact x.
Defined.

Axiom
  constructive_uniqueness_for_orthogonals :
    forall (l m n : Line) (a : Point),
    DiLn l m -> (Apart a l \/ Apart a m) \/ Unort l n \/ Unort m n.

Theorem O3_i : forall (l : Line) (a : Point), Ort (ort l a) l.
Proof.
(* Goal: forall (l : Line) (a : Point), Incident a (ort l a) *)
intros l a.
(* Goal: Incident a (ort l a) *)
unfold ort at 1 in |- *.
(* Goal: Incident a (@sig_rec Line (fun l' : Line => and (Ort l' l) (Incident a l')) (fun _ : @sig Line (fun l' : Line => and (Ort l' l) (Incident a l')) => Line) (fun (x : Line) (_ : and (Ort x l) (Incident a x)) => x) (constructed_orthogonal l a)) *)
elim (constructed_orthogonal l a).
(* Goal: forall (x : Line) (p : and (Ort x l) (Incident a x)), Incident a (@sig_rec Line (fun l' : Line => and (Ort l' l) (Incident a l')) (fun _ : @sig Line (fun l' : Line => and (Ort l' l) (Incident a l')) => Line) (fun (x0 : Line) (_ : and (Ort x0 l) (Incident a x0)) => x0) (@exist Line (fun l' : Line => and (Ort l' l) (Incident a l')) x p)) *)
simpl in |- *; tauto.
Qed.

Theorem O3_ii : forall (l : Line) (a : Point), Incident a (ort l a).
Proof.
(* Goal: forall (l : Line) (a : Point), Incident a (ort l a) *)
intros l a.
(* Goal: Incident a (ort l a) *)
unfold ort at 1 in |- *.
(* Goal: Incident a (@sig_rec Line (fun l' : Line => and (Ort l' l) (Incident a l')) (fun _ : @sig Line (fun l' : Line => and (Ort l' l) (Incident a l')) => Line) (fun (x : Line) (_ : and (Ort x l) (Incident a x)) => x) (constructed_orthogonal l a)) *)
elim (constructed_orthogonal l a).
(* Goal: forall (x : Line) (p : and (Ort x l) (Incident a x)), Incident a (@sig_rec Line (fun l' : Line => and (Ort l' l) (Incident a l')) (fun _ : @sig Line (fun l' : Line => and (Ort l' l) (Incident a l')) => Line) (fun (x0 : Line) (_ : and (Ort x0 l) (Incident a x0)) => x0) (@exist Line (fun l' : Line => and (Ort l' l) (Incident a l')) x p)) *)
simpl in |- *; tauto.
Qed.
Hint Resolve O3_i O3_ii.

Theorem O4' :
 forall (l m n : Line) (a : Point),
 (Incident a l /\ Incident a m) /\ Ort l n /\ Ort m n -> EqLn l m.
Proof.
(* Goal: forall (l m n : Line) (a : Point) (_ : and (and (Incident a l) (Incident a m)) (and (Ort l n) (Ort m n))), EqLn l m *)
unfold Incident, Ort, EqLn, Negation in |- *.
(* Goal: forall (l m n : Line) (a : Point) (_ : and (and (not (Apart a l)) (not (Apart a m))) (and (not (Unort l n)) (not (Unort m n)))), not (DiLn l m) *)
intros l m n a.
(* Goal: forall _ : and (and (not (Apart a l)) (not (Apart a m))) (and (not (Unort l n)) (not (Unort m n))), not (DiLn l m) *)
generalize (constructive_uniqueness_for_orthogonals l m n a).
(* Goal: forall (_ : forall _ : DiLn l m, or (or (Apart a l) (Apart a m)) (or (Unort l n) (Unort m n))) (_ : and (and (not (Apart a l)) (not (Apart a m))) (and (not (Unort l n)) (not (Unort m n)))), not (DiLn l m) *)
tauto.
Qed.

Theorem Uniqueness_of_orthogonality :
 forall (l m : Line) (a : Point), Incident a l /\ Ort l m -> EqLn l (ort m a).
Proof.
(* Goal: forall (l m : Line) (a : Point) (_ : and (Incident a l) (Ort l m)), EqLn l (ort m a) *)
intros l m a H'; elim H'; intros H'0 H'1; clear H'.
(* Goal: EqLn l (ort m a) *)
apply O4' with (n := m) (a := a); auto.
Qed.

Theorem Unort_reflexive : Reflexive Line Unort.
Proof.
(* Goal: Reflexive Line Unort *)
red in |- *.
(* Goal: forall x : Line, Unort x x *)
intro l.
(* Goal: Unort l l *)
generalize (O1 l l); intro H'.
(* Goal: Unort l l *)
elim H'; [ intro H'0; clear H' | trivial ].
(* Goal: False *)
(* Goal: Separating Line Oblique *)
elim apart_con.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), Unort l l *)
intro H'; elim (H' l); auto.
Qed.

Theorem cmp_unort_con :
 forall l m n : Line, Unort l m -> ConLn l n \/ Unort m n.
Proof.
(* Goal: forall (l m n : Line) (_ : ConLn l m), or (Unort l n) (Unort m n) *)
intros l m n H'.
(* Goal: or (ConLn l n) (Unort m n) *)
generalize (O1 m n); intro H'1.
(* Goal: or (ConLn l n) (Unort m n) *)
elim H'1; [ intro H'0; clear H'1 | auto ].
(* Goal: False *)
(* Goal: Separating Line Oblique *)
elim apart_con.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), or (ConLn l n) (Unort m n) *)
intros H'1 H'2; red in H'2.
(* Goal: or (ConLn l n) (Unort m n) *)
lapply (H'2 m n l); [ intro H'6 | assumption ].
(* Goal: or (ConLn l n) (Unort m n) *)
elim H'6; [ intro H'3; clear H'6 | auto ].
(* Goal: or (ConLn l n) (Unort m n) *)
generalize O2.
(* Goal: forall _ : Separating Line (fun l m : Line => and (ConLn l m) (Unort l m)), or (ConLn l n) (Unort m n) *)
intro H'4; red in H'4.
(* Goal: or (ConLn l n) (Unort m n) *)
lapply (H'4 l m n); intuition.
Qed.

Theorem cmp_unort_diln :
 forall l m n : Line, Unort l m -> DiLn l n \/ Unort m n.
Proof.
(* Goal: forall (l m n : Line) (_ : ConLn l m), or (Unort l n) (Unort m n) *)
intros l m n H'.
(* Goal: or (DiLn l n) (Unort m n) *)
lapply (cmp_unort_con l m n); [ intro H'3 | assumption ]; auto.
(* Goal: or (DiLn l n) (Unort m n) *)
intuition.
Qed.

Theorem Unort_symmetric : Symmetric Line Unort.
Proof.
(* Goal: Symmetric Line Unort *)
unfold Symmetric at 1 in |- *.
(* Goal: forall (x y : Line) (_ : Unort x y), Unort y x *)
intros l m H'.
lapply (cmp_unort_con l m l);
 [ intro H'3; elim H'3; [ intro H'4; clear H'3 | trivial ] | idtac ];
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
 auto.
(* Goal: Unort m l *)
cut (Irreflexive Line ConLn); auto.
(* Goal: forall _ : Irreflexive Line ConLn, Unort m l *)
(* Goal: Irreflexive Line ConLn *)
intro H'0; red in H'0.
(* Goal: Unort m l *)
(* Goal: Irreflexive Line ConLn *)
elim (H'0 l); auto.
(* Goal: Irreflexive Line ConLn *)
elim apart_con; auto.
Qed.

Theorem thm8_6 : forall l m n : Line, ConLn l m -> Unort l n \/ Unort m n.
Proof.
(* Goal: forall (l m n : Line) (_ : ConLn l m), or (Unort l n) (Unort m n) *)
intros l m n H'.
(* Goal: or (Unort l n) (Unort m n) *)
lapply (Convergent_imp_distinct l m); [ intro H'2 | assumption ].
lapply (constructive_uniqueness_for_orthogonals l m n (pt (Twol l m H')));
 [ intro H'5 | assumption ].
(* Goal: or (Unort l n) (Unort m n) *)
elim H'5; [ intro H'0; clear H'5 | trivial ].
(* Goal: or (Unort l n) (Unort m n) *)
generalize (inc_pt1 (Twol l m H')); generalize (inc_pt2 (Twol l m H')).
(* Goal: forall (_ : forall _ : DiLn l m, or (or (Apart a l) (Apart a m)) (or (Unort l n) (Unort m n))) (_ : and (and (not (Apart a l)) (not (Apart a m))) (and (not (Unort l n)) (not (Unort m n)))), not (DiLn l m) *)
simpl in |- *; unfold Incident, Negation in |- *; tauto.
Qed.

Definition Oblique : Relation Line :=
  fun l m : Line => ConLn l m /\ Unort l m.

Theorem apart_obl : Apartness Line Oblique.
Proof.
(* Goal: Apartness Line Oblique *)
apply Definition_of_apartness.
(* Goal: Irreflexive Line Oblique *)
(* Goal: Separating Line Oblique *)
unfold Irreflexive, Negation, Oblique in |- *.
(* Goal: forall x : Line, not (and (ConLn x x) (Unort x x)) *)
(* Goal: Separating Line Oblique *)
intro l; red in |- *; intro H'; elim H'; intros H'0 H'1; clear H'.
(* Goal: False *)
(* Goal: Separating Line Oblique *)
elim apart_con.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), False *)
(* Goal: Separating Line Oblique *)
intros H' H'2; apply (H' l); assumption.
(* Goal: Separating Line Oblique *)
unfold Oblique in |- *; exact O2.
Qed.

Theorem ort_ort_like_par_i :
 forall (l : Line) (a : Point), Incident a (ort (ort l a) a).
Proof.
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
auto.
Qed.

Theorem thm8_8 :
 forall (l : Line) (a b : Point),
 Incident b (ort l a) -> EqLn (ort l a) (ort l b).
Proof.
(* Goal: forall (l : Line) (a b : Point) (_ : Incident b (ort l a)), EqLn (ort l a) (ort l b) *)
intros l a b H'.
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
apply O4' with (n := l) (a := b); auto.
Qed.

Section delicate.
Variable a : Point.
Variable l : Line.
Variable H : ConLn l (ort (ort l a) a).

Let t : Twolines := Twol l (ort (ort l a) a) H.

Let b : Point := pt t.

Theorem thm8_9_aux : False.
Proof.
(* Goal: False *)
generalize (inc_pt1 t); intro H'0; simpl in H'0.
(* Goal: False *)
generalize (inc_pt2 t); intro H'1; simpl in H'1.
lapply (Convergent_imp_distinct l (ort (ort l a) a));
 [ intro H'4 | assumption ].
(* Goal: False *)
lapply (thm8_8 (ort l a) a b); [ intro H'6 | assumption ].
lapply (cong_eqln_diln l (ort (ort l a) a) (ort (ort l a) b));
 [ intro H'7; lapply H'7; [ intro H'8; clear H'7 | clear H'7 ] | idtac ];
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
 auto.
lapply
 (constructive_uniqueness_for_orthogonals l (ort (ort l a) b) (ort l a) b);
 [ intro H'9 | assumption ].
elim H'9;
 [ intro H'2; elim H'2;
    [ intro H'3; clear H'2 H'9 | intro H'3; clear H'2 H'9 ]
 | intro H'2; clear H'9 ].
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
unfold b at 1 in H'3; elim H'0; auto.
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
elim (O3_ii (ort l a) b); auto.
(* Goal: False *)
generalize Unort_symmetric.
(* Goal: forall _ : Symmetric Line Unort, False *)
intro H'; red in H'.
(* Goal: False *)
elim H'2; (intro H'3; clear H'2).
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
elim (O3_i l a); auto.
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
elim (O3_i (ort l a) b); auto.
Qed.

End delicate.

Theorem thm8_9 : forall (l : Line) (a : Point), Par l (ort (ort l a) a).
Proof.
(* Goal: forall (l : Line) (a : Point), Par l (ort (ort l a) a) *)
intros l a; unfold Par, Negation in |- *.
(* Goal: not (ConLn l (ort (ort l a) a)) *)
red in |- *; intro H'; apply (thm8_9_aux a l); trivial.
Qed.
Hint Resolve thm8_9.

Theorem thm8_10 :
 forall (l : Line) (a : Point), EqLn (par l a) (ort (ort l a) a).
Proof.
(* Goal: forall (l : Line) (a : Point), Incident a (ort (ort l a) a) *)
intros l a; apply sym_EqLn; auto.
Qed.


