Library GeoCoq.Axioms.hilbert_axioms

Require Export Setoid.
Require Export GeoCoq.Utils.aux.

Class Hilbert_neutral_2D :=
{
 Point : Type;
 Line : Type;
 EqL : Line Line Prop;
 EqL_Equiv : Equivalence EqL;
 Incid : Point Line Prop;

 Incid_morphism :
    P l m, Incid P l EqL l m Incid P m;
 Incid_dec : P l, Incid P l ¬ Incid P l;
 eq_dec_pointsH : A B : Point, A=B ¬ A=B;

 
Group I Incidence
 line_existence :
    A B, A B l, Incid A l Incid B l;
 line_uniqueness :
    A B l m,
     A B
     Incid A l Incid B l Incid A m Incid B m
     EqL l m;
 two_points_on_line :
    l,
     { A : Point & { B | Incid B l Incid A l A B}};
 ColH :=
   fun A B C l, Incid A l Incid B l Incid C l;
 l0 : Line;
 P0 : Point;
 plan : ¬ Incid P0 l0;

 
Group II Order
 BetH : Point Point Point Prop;
 between_col : A B C, BetH A B C ColH A B C;
 between_diff : A B C, BetH A B C A C;
 between_comm : A B C, BetH A B C BetH C B A;
 between_out : A B, A B C, BetH A B C;
 between_only_one : A B C, BetH A B C ¬ BetH B C A;
 cut :=
   fun l A B¬ Incid A l ¬ Incid B l
                 I, Incid I l BetH A I B;
 pasch :
    A B C l,
     ¬ ColH A B C ¬ Incid C l cut l A B
     cut l A C cut l B C;

 
Group III Congruence
 CongH : Point Point Point Point Prop;
 cong_permr : A B C D, CongH A B C D CongH A B D C;
 cong_pseudo_transitivity :
    A B C D E F,
     CongH A B C D CongH A B E F CongH C D E F;
 cong_existence :
    A B l M,
     A B Incid M l
      A', B', Incid A' l Incid B' l
                           BetH A' M B'
                           CongH M A' A B CongH M B' A B;
 disjoint := fun A B C D¬ P, BetH A P B BetH C P D;
 addition :
    A B C A' B' C',
     ColH A B C ColH A' B' C'
     disjoint A B B C disjoint A' B' B' C'
     CongH A B A' B' CongH B C B' C'
     CongH A C A' C';

 CongaH :
   Point Point Point Point Point Point Prop;
 conga_refl : A B C, ¬ ColH A B C CongaH A B C A B C;
 conga_comm : A B C, ¬ ColH A B C CongaH A B C C B A;
 congaH_permlr :
    A B C D E F, CongaH A B C D E F CongaH C B A F E D;
 cong_5 :
    A B C A' B' C',
     ¬ ColH A B C ¬ ColH A' B' C'
     CongH A B A' B' CongH A C A' C'
     CongaH B A C B' A' C'
     CongaH A B C A' B' C';

 same_side := fun A B l P, cut l A P cut l B P;
 same_side' :=
   fun A B X Y
     X Y
      l, Incid X l Incid Y l same_side A B l;

 outH :=
   fun P A BBetH P A B BetH P B A (P A A = B);
 congaH_outH_congaH :
    A B C D E F A' C' D' F',
    CongaH A B C D E F
    outH B A A' outH B C C' outH E D D' outH E F F'
    CongaH A' B C' D' E F';
 hcong_4_existence :
    A B C O X P,
     ¬ ColH P O X ¬ ColH A B C
      Y, CongaH A B C X O Y same_side' P Y O X;
 hcong_4_uniqueness :
    A B C O P X Y Y',
     ¬ ColH P O X ¬ ColH A B C
     CongaH A B C X O Y CongaH A B C X O Y'
     same_side' P Y O X same_side' P Y' O X
     outH O Y Y'
}.

Class Hilbert_euclidean_2D `(Hilbert2 : Hilbert_neutral_2D) :=
{
 Para := fun l m¬ X, Incid X l Incid X m;
 euclid_uniqueness :
    l P m1 m2,
     ¬ Incid P l
     Para l m1 Incid P m1 Para l m2 Incid P m2
     EqL m1 m2
}.