Library hilbert_axioms

Require Export Setoid.
Require Export aux.

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

 

 line_existence : ∀ A B, A≠B → ∃ l, Incid A l ∧ Incid B l;
 line_unicity : ∀ 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, ∃ B, Incid B l ∧ Incid A l ∧ A ≠ B;
 ColH := fun A B C ⇒ ∃ l, Incid A l ∧ Incid B l ∧ Incid C l;
 plan : ∃ A, ∃ B, ∃ C, ¬ ColH A B C;

 

 BetH : Point → Point → Point → Prop;
 between_col : ∀ A B C : Point, BetH A B C → ColH A B C;
 between_comm : ∀ A B C : Point, BetH A B C → BetH C B A;
 between_out : ∀ A B : Point, A ≠ B → ∃ C : Point, BetH A B C;
 between_only_one : ∀ A B C : Point, BetH A B C → ¬ BetH B C A ∧ ¬ BetH B A C;
 between_one : ∀ A B C, A≠B → A≠C → B≠C → ColH A B C → BetH A B C ∨ BetH B C A ∨ BetH B A C;
 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;


 

 Para := fun l m ⇒ ¬ ∃ X, Incid X l ∧ Incid X m;
 euclid_existence : ∀ l P, ¬ Incid P l → ∃ m, Para l m;
 euclid_unicity : ∀ l P m1 m2, ¬ Incid P l → Para l m1 → Incid P m1→ Para l m2 → Incid P m2 → EqL m1 m2;
 
 

 CongH : Point → Point → Point → Point → Prop;
 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_refl : ∀ A B, CongH A B A B;
 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;
 cong_unicity : ∀ A B l M A' B' A'' B'', A ≠ B → Incid M l →
  Incid A' l → Incid B' l →
  Incid A'' l → Incid B'' l →
  BetH A' M B' → CongH M A' A B →
  CongH M B' A B → BetH A'' M B'' →
  CongH M A'' A B →
  CongH M B'' A B →
  (A' = A'' ∧ B' = B'') ∨ (A' = B'' ∧ B' = A'');

 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';
 Angle := @Triple Point;
 angle := build_triple Point;
 CongaH : Angle → Angle → Prop;
 cong_5 : ∀ A B C A' B' C', ∀ H1 : (B≠A ∧ C≠A), ∀ H2: B' ≠ A' ∧ C' ≠ A',
  ∀ H3 : (A≠B ∧ C≠B), ∀ H4: A' ≠ B' ∧ C' ≠ B',
  CongH A B A' B' → CongH A C A' C' → CongaH (angle B A C H1) (angle B' A' C' H2) →
   CongaH (angle A B C H3) (angle A' B' C' H4);

 same_side := fun A B l ⇒ ∃ P, cut l A P ∧ cut l B P;

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

 InAngleH := fun a P ⇒
 (∃ M, BetH (V1 a) M (V2 a) ∧ ((outH (V a) M P) ∨ M = (V a))) ∨
                                   outH (V a) (V1 a) P ∨ outH (V a) (V2 a) P;

 Hline := @Couple Point;
 line_of_hline : Hline → Line;
 hline_construction := fun a (h: Hline) P (hc:Hline) H ⇒
 (P1 h) = (P1 hc) ∧
 CongaH a (angle (P2 h) (P1 h) (P2 hc) (conj (sym_not_equal (Cond h)) H)) ∧
  (∀ M, InAngleH (angle (P2 h) (P1 h) (P2 hc) (conj (sym_not_equal (Cond h)) H)) M →
   same_side P M (line_of_hline h));


  aux : ∀ (h h1 : Hline), P1 h = P1 h1 → P2 h1 ≠ P1 h;

  hcong_4_existence: ∀ a h P,
  ¬Incid P (line_of_hline h) → ¬ BetH (V1 a)(V a)(V2 a) →
  ∃ h1, (P1 h) = (P1 h1) ∧ (∀ CondAux : P1 h = P1 h1,
                                    CongaH a (angle (P2 h) (P1 h) (P2 h1) (conj (sym_not_equal (Cond h)) (aux h h1 CondAux)))
                                    ∧ (∀ M, ¬ Incid M (line_of_hline h) ∧ InAngleH (angle (P2 h) (P1 h) (P2 h1) (conj (sym_not_equal (Cond h)) (aux h h1 CondAux))) M
                                                    → same_side P M (line_of_hline h)));


 hEq : relation Hline := fun h1 h2 ⇒ (P1 h1) = (P1 h2) ∧
                          ((P2 h1) = (P2 h2) ∨ BetH (P1 h1) (P2 h2) (P2 h1) ∨
                                                  BetH (P1 h1) (P2 h1) (P2 h2));

 hcong_4_unicity :
  ∀ a h P h1 h2 HH1 HH2,
  ¬Incid P (line_of_hline h) → ¬ BetH (V1 a)(V a)(V2 a) →
  hline_construction a h P h1 HH1 → hline_construction a h P h2 HH2 →
  hEq h1 h2

}.