Library GeoCoq.Axioms.hilbert_axioms

Require Export Setoid.
Require Export GeoCoq.Utils.triples.

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;

 

 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;

 

 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;

 

 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;

 outH :=
   fun P A B ⇒ BetH P A B ∨ BetH P B A ∨ (P ≠ A ∧ A = B);

 cong_existence :
   ∀ A B A' P l,
     A ≠ B → A' ≠ P →
     Incid A' l → Incid P l →
     ∃ B', Incid B' l ∧ outH A' P B' ∧ CongH A' 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;

 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
}.