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


(****************************************************************************)
(*                               part1.v                                    *)
(*                                                                          *)
(* Congruence lemmas near the end slightly more explicit than in von Plato  *)
(****************************************************************************)
Require Import basis.

Theorem Uniqueness_of_constructed_lines :
 forall (x : Segment) (l : Line),
 Incident (origin x) l -> Incident (extremity x) l -> EqLn l (ln x).
Proof.
(* Goal: forall (x : Segment) (l : Line) (_ : Incident (origin x) l) (_ : Incident (extremity x) l), EqLn l (ln x) *)
intros x l.
(* Goal: forall (_ : Incident (origin x) l) (_ : Incident (extremity x) l), EqLn l (ln x) *)
generalize (inc_ln2 x); generalize (inc_ln1 x).
(* Goal: forall (_ : Incident (origin x) (ln x)) (_ : Incident (extremity x) (ln x)) (_ : Incident (origin x) l) (_ : Incident (extremity x) l), EqLn l (ln x) *)
unfold Incident, EqLn, Negation in |- *.
(* Goal: forall (_ : not (Apart (origin x) (ln x))) (_ : not (Apart (extremity x) (ln x))) (_ : not (Apart (origin x) l)) (_ : not (Apart (extremity x) l)), not (DiLn l (ln x)) *)
intros H' H'0 H'1 H'2; red in |- *; intro H'3.
(* Goal: False *)
lapply (el_ax x l (ln x)); trivial.
(* Goal: forall _ : or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x))), False *)
(* Goal: DiLn (line1 x) (line2 x) *)
tauto.
Qed.

Theorem Convergent_imp_distinct : forall l m : Line, ConLn l m -> DiLn l m.
Proof.
(* Goal: forall (l m : Line) (_ : ConLn l m), DiLn l m *)
intros l m H'.
(* Goal: DiLn l m *)
lapply (cmp_con_diln l m l); trivial.
(* Goal: forall _ : or (DiLn m l) (ConLn l l), DiLn l m *)
intro H'0; elim H'0; auto.
(* Goal: forall _ : ConLn l l, DiLn l m *)
intro H'1; elim apart_con.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), DiLn l m *)
intro H'2; elim (H'2 l); trivial.
Qed.
Hint Resolve Convergent_imp_distinct.

Theorem Uniqueness_of_constructed_points :
 forall (x : Twolines) (a : Point),
 Incident a (line1 x) -> Incident a (line2 x) -> EqPt a (pt x).
Proof.
(* Goal: forall (x : Twolines) (a : Point) (_ : Incident a (line1 x)) (_ : Incident a (line2 x)), EqPt a (pt x) *)
intro x.
(* Goal: forall (a : Point) (_ : Incident a (line1 x)) (_ : Incident a (line2 x)), EqPt a (pt x) *)
generalize (inc_pt2 x); generalize (inc_pt1 x).
(* Goal: forall (_ : Incident (pt x) (line1 x)) (_ : Incident (pt x) (line2 x)) (a : Point) (_ : Incident a (line1 x)) (_ : Incident a (line2 x)), EqPt a (pt x) *)
unfold Incident, EqPt, Negation in |- *.
(* Goal: forall (_ : not (Apart (pt x) (line1 x))) (_ : not (Apart (pt x) (line2 x))) (a : Point) (_ : not (Apart a (line1 x))) (_ : not (Apart a (line2 x))), not (DiPt a (pt x)) *)
intros H' H'0 a H'1 H'2; red in |- *; intro H'3.
(* Goal: False *)
lapply (el_ax (Seg a (pt x) H'3) (line1 x) (line2 x)); simpl in |- *.
(* Goal: forall _ : or (or (Apart a (line1 x)) (Apart (pt x) (line1 x))) (or (Apart a (line2 x)) (Apart (pt x) (line2 x))), False *)
(* Goal: DiLn (line1 x) (line2 x) *)
tauto.
(* Goal: DiLn (line1 x) (line2 x) *)
elim x; auto.
Qed.

Theorem cong_eqpt_apt :
 forall (a b : Point) (l : Line), Apart a l -> EqPt a b -> Apart b l.
Proof.
(* Goal: forall (a b : Point) (l : Line) (_ : Apart a l) (_ : EqPt a b), Apart b l *)
intros a b l H' H'0.
(* Goal: Apart b l *)
elim (cmp_apt_dipt a b l); auto.
(* Goal: forall _ : DiLn m n, ConLn l n *)
intro H'1; elim H'0; trivial.
Qed.

Theorem cong_eqln_apt :
 forall (a : Point) (l m : Line), Apart a l -> EqLn l m -> Apart a m.
Proof.
(* Goal: forall (a : Point) (l m : Line) (_ : Apart a l) (_ : EqLn l m), Apart a m *)
intros a l m H' H'0.
(* Goal: Apart a m *)
elim (cmp_apt_diln a l m); auto.
(* Goal: forall _ : DiLn m n, ConLn l n *)
intro H'1; elim H'0; trivial.
Qed.

Theorem cong_eqpt_inc :
 forall (a b : Point) (l : Line), Incident a l -> EqPt a b -> Incident b l.
Proof.
(* Goal: forall (a : Point) (l m : Line) (_ : Incident a l) (_ : EqLn l m), Incident a m *)
unfold Incident in |- *.
(* Goal: forall (a b : Point) (l : Line) (_ : not (Apart a l)) (_ : EqPt a b), not (Apart b l) *)
intros a b l H' H'0; red in |- *; intro H'1; apply H'.
(* Goal: Apart a l *)
apply cong_eqpt_apt with (a := b); auto.
Qed.

Theorem cong_eqln_inc :
 forall (a : Point) (l m : Line), Incident a l -> EqLn l m -> Incident a m.
Proof.
(* Goal: forall (a : Point) (l m : Line) (_ : Incident a l) (_ : EqLn l m), Incident a m *)
unfold Incident in |- *.
(* Goal: forall (a : Point) (l m : Line) (_ : not (Apart a l)) (_ : EqLn l m), not (Apart a m) *)
intros a l m H' H'0; red in |- *; intro H'1; apply H'.
(* Goal: Apart a l *)
apply cong_eqln_apt with (l := m); auto.
Qed.

Theorem cong_eqln_con :
 forall l m n : Line, ConLn l m -> EqLn m n -> ConLn l n.
Proof.
(* Goal: forall (l m n : Line) (_ : ConLn l m) (_ : Par m n), ConLn l n *)
intros l m n H' H'0.
(* Goal: ConLn l n *)
elim (cmp_con_diln l m n); auto.
(* Goal: forall _ : DiLn m n, ConLn l n *)
intro H'1; elim H'0; trivial.
Qed.

Theorem cong_eqln_par : forall l m n : Line, Par l m -> EqLn m n -> Par l n.
Proof.
(* Goal: forall (l m n : Line) (_ : Par l m) (_ : EqLn m n), Par l n *)
unfold Par, Negation in |- *.
(* Goal: forall (l m n : Line) (_ : not (ConLn l m)) (_ : EqLn m n), not (ConLn l n) *)
intros l m n H' H'0; red in |- *; intro H'1; apply H'.
(* Goal: ConLn l m *)
apply cong_eqln_con with (m := n); auto.
Qed.

Theorem cong_eqpt_dipt :
 forall a b c : Point, DiPt a b -> EqPt b c -> DiPt a c.
Proof.
(* Goal: forall (a b c : Point) (_ : DiPt a b) (_ : EqPt b c), DiPt a c *)
intros a b c H' H'0; elim apart_dipt.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), ConLn l n *)
unfold Separating at 1 in |- *.
(* Goal: forall (_ : Irreflexive Point DiPt) (_ : forall (x y z : Point) (_ : DiPt x y), or (DiPt x z) (DiPt y z)), DiPt a c *)
intros H'1 H'2; elim (H'2 a b c); trivial.
(* Goal: forall _ : ConLn m n, ConLn l n *)
intro H'3; elim H'0; trivial.
Qed.

Theorem cong_eqln_diln :
 forall l m n : Line, DiLn l m -> EqLn m n -> DiLn l n.
Proof.
(* Goal: forall (l m n : Line) (_ : DiLn l m) (_ : EqLn m n), DiLn l n *)
intros l m n H' H'0; elim apart_diln.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), ConLn l n *)
unfold Separating at 1 in |- *.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : forall (x y z : Line) (_ : ConLn x y), or (ConLn x z) (ConLn y z)), ConLn l n *)
intros H'1 H'2; elim (H'2 l m n); trivial.
(* Goal: forall _ : ConLn m n, ConLn l n *)
intro H'3; elim H'0; trivial.
Qed.

Theorem eqln_imp_par : forall l m : Line, EqLn l m -> Par l m.
Proof.
(* Goal: forall (l m : Line) (_ : EqLn l m), Par l m *)
unfold Par, EqLn, Negation in |- *; red in |- *; auto.
Qed.

Theorem cong_par_con : forall l m n : Line, ConLn l m -> Par m n -> ConLn l n.
Proof.
(* Goal: forall (l m n : Line) (_ : ConLn l m) (_ : Par m n), ConLn l n *)
intros l m n H' H'0.
(* Goal: ConLn l n *)
elim apart_con.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : Separating Line ConLn), ConLn l n *)
unfold Separating at 1 in |- *.
(* Goal: forall (_ : Irreflexive Line ConLn) (_ : forall (x y z : Line) (_ : ConLn x y), or (ConLn x z) (ConLn y z)), ConLn l n *)
intros H'1 H'2; elim (H'2 l m n); trivial.
(* Goal: forall _ : ConLn m n, ConLn l n *)
intro H'3; elim H'0; trivial.
Qed.

Theorem sym_SPar : forall x y : Line, SPar x y -> SPar y x.
Proof.
(* Goal: forall (l m n : Line) (_ : SPar l m) (_ : EqLn m n), SPar l n *)
unfold SPar in |- *.
(* Goal: forall (x y : Line) (_ : and (Par x y) (DiLn x y)), and (Par y x) (DiLn y x) *)
intuition.
Qed.
Hint Resolve sym_SPar.

Theorem cong_eqln_spar :
 forall l m n : Line, SPar l m -> EqLn m n -> SPar l n.
Proof.
(* Goal: forall (l m n : Line) (_ : SPar l m) (_ : EqLn m n), SPar l n *)
unfold SPar in |- *.
(* Goal: forall (l m n : Line) (_ : and (Par l m) (DiLn l m)) (_ : EqLn m n), and (Par l n) (DiLn l n) *)
intros l m n H'; elim H'; intros H'0 H'1; try exact H'0; clear H'.
(* Goal: forall _ : EqLn m n, and (Par l n) (DiLn l n) *)
intro H'; split.
(* Goal: Par l n *)
(* Goal: DiLn l n *)
apply cong_eqln_par with (m := m); trivial.
(* Goal: DiLn l n *)
apply cong_eqln_diln with (m := m); trivial.
Qed.

Definition reverse : Segment -> Segment.
Proof.
(* Goal: forall _ : Equivalence Line EqLn, Equivalence Segment colinear *)
intro H'; elim H'.
(* Goal: forall (origin extremity : Point) (_ : DiPt origin extremity), Segment *)
intros a b H'0.
(* Goal: Segment *)
apply (Seg b a); auto.
Defined.

Theorem orig_rev : forall x : Segment, origin x = extremity (reverse x).
Proof.
(* Goal: forall x : Twolines, @eq Line (line2 x) (line1 (flip x)) *)
intro x; elim x; simpl in |- *; auto.
Qed.

Theorem ext_rev : forall x : Segment, extremity x = origin (reverse x).
Proof.
(* Goal: forall x : Twolines, @eq Line (line2 x) (line1 (flip x)) *)
intro x; elim x; simpl in |- *; auto.
Qed.

Theorem rev_defines_sameln : forall x : Segment, EqLn (ln x) (ln (reverse x)).
Proof.
(* Goal: forall x : Segment, EqLn (ln x) (ln (reverse x)) *)
intro x; apply Uniqueness_of_constructed_lines.
(* Goal: Incident (origin (reverse x)) (ln x) *)
(* Goal: Incident (extremity (reverse x)) (ln x) *)
rewrite <- (ext_rev x); auto.
(* Goal: Incident (extremity (reverse x)) (ln x) *)
rewrite <- (orig_rev x); auto.
Qed.
Hint Resolve rev_defines_sameln.

Definition flip : Twolines -> Twolines.
Proof.
(* Goal: forall _ : Equivalence Line EqLn, Equivalence Segment colinear *)
intro H'; elim H'.
(* Goal: forall (line1 line2 : Line) (_ : ConLn line1 line2), Twolines *)
intros l m H'0.
(* Goal: Twolines *)
apply (Twol m l); auto.
Defined.

Theorem line1_flip : forall x : Twolines, line1 x = line2 (flip x).
Proof.
(* Goal: forall x : Twolines, @eq Line (line2 x) (line1 (flip x)) *)
intro x; elim x; simpl in |- *; auto.
Qed.

Theorem line2_flip : forall x : Twolines, line2 x = line1 (flip x).
Proof.
(* Goal: forall x : Twolines, @eq Line (line2 x) (line1 (flip x)) *)
intro x; elim x; simpl in |- *; auto.
Qed.

Theorem flip_defines_samept : forall x : Twolines, EqPt (pt x) (pt (flip x)).
Proof.
(* Goal: forall x : Twolines, EqPt (pt x) (pt (flip x)) *)
intro x; apply Uniqueness_of_constructed_points.
(* Goal: Incident (pt x) (line1 (flip x)) *)
(* Goal: Incident (pt x) (line2 (flip x)) *)
rewrite <- (line2_flip x); auto.
(* Goal: Incident (pt x) (line2 (flip x)) *)
rewrite <- (line1_flip x); auto.
Qed.
Hint Resolve rev_defines_sameln flip_defines_samept.

Definition colinear (x y : Segment) : Prop := EqLn (ln x) (ln y).

Theorem Colinearity_is_equivalence : Equivalence Segment colinear.
Proof.
(* Goal: Equivalence Segment colinear *)
cut (Equivalence Line EqLn); auto.
(* Goal: forall _ : Equivalence Line EqLn, Equivalence Segment colinear *)
intro H'; elim H'.
intros H'0 H'1 H'2; apply Definition_of_equivalence; unfold colinear in |- *;
 auto.
(* Goal: Transitive Segment (fun x y : Segment => EqLn (ln x) (ln y)) *)
red in |- *.
(* Goal: forall (x y z : Segment) (_ : EqLn (ln x) (ln y)) (_ : EqLn (ln y) (ln z)), EqLn (ln x) (ln z) *)
intros x y z H'3 H'4.
(* Goal: EqLn (ln x) (ln z) *)
red in H'2.
(* Goal: EqLn (ln x) (ln z) *)
apply H'2 with (y := ln y); auto.
Qed.


