Library HilbertDegeneratedModel

Require Import hilbert_axioms.

Module CounterExample : Hilbert.

Module HilbertL <: HilbertLanguage.

Inductive SinglePoint : Set := MyPoint.

Definition Point := SinglePoint.

Inductive Empty : Set :=.

Definition Line := Empty.

Definition Incid (A:Point) (l:Line) := True.

Definition EqP (A B : Point) := True.
Definition EqL (A B : Line) := True.

Lemma EqP_transitivity : forall l m n, EqP l m -> EqP m n -> EqP l n.
Proof.
tauto.
Qed.

Lemma EqP_reflexivity : forall l, EqP l l.
Proof.
unfold EqP.
tauto.
Qed.

Lemma EqP_symmetry : forall l m, EqP l m -> EqP m l.
Proof.
tauto.
Qed.

Lemma EqL_transitivity : forall l m n, EqL l m -> EqL m n -> EqL l n.
Proof.
tauto.
Qed.

Lemma EqL_reflexivity : forall l, EqL l l.
Proof.
unfold EqL.
tauto.
Qed.

Lemma EqL_symmetry : forall l m, EqL l m -> EqL m l.
Proof.
tauto.
Qed.

Lemma EqL_compat_incid : forall A l m, EqL l m -> Incid A l -> Incid A m.
Proof.
tauto.
Qed.

Lemma EqP_compat_incid : forall A B l, EqP A B -> Incid A l -> Incid B l.
Proof.
tauto.
Qed.

Definition Bet (A B C:Point) := False.

Definition Col (A B C:Point) := exists l : Line, Incid A l /\ Incid B l /\ Incid C l.

Lemma not_two_points : forall A B:Point, A<>B -> False.
Proof.
intros.
unfold Point in *.
induction A.
induction B.
auto.
Qed.

Lemma not_one_line : forall l:Line, False.
Proof.
intros.
induction l.
Qed.

End HilbertL.

Import HilbertL.

Hint Resolve not_two_points not_one_line.

Lemma line_existence : forall A B, A<>B -> exists l, Incid A l /\ Incid B l.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Lemma line_unicity : forall A B l m, A <> B ->
 Incid A l -> Incid B l -> Incid A m -> Incid B m -> EqL l m.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Lemma two_points_on_line : forall l,
  exists A, exists B, Incid B l /\ Incid A l /\ A <> B.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Lemma plan : exists A, exists B, exists C, ~ Col A B C.
Proof.
exists MyPoint.
exists MyPoint.
exists MyPoint.
unfold Col.
unfold not;intro.
elim H.
intro l.
assert False.
eauto.
intuition.
Qed.

Lemma between_col : forall A B C : Point, Bet A B C -> Col A B C.
Proof.
unfold Bet.
tauto.
Qed.

Lemma between_comm : forall A B C : Point, Bet A B C -> Bet C B A.
Proof.
unfold Bet.
tauto.
Qed.

Lemma between_out :
 forall A B : Point, A <> B -> exists C : Point, Bet A B C.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Lemma between_only_one :
 forall A B C : Point, Bet A B C -> ~ Bet B C A /\ ~ Bet B A C.
Proof.
unfold Bet.
tauto.
Qed.

Lemma between_one : forall A B C,
 A<>B -> A<>C -> B<>C -> Col A B C ->
 Bet A B C \/ Bet B C A \/ Bet B A C.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Definition go_through := fun l A B => exists C, Incid C l /\ Bet A C B.

Lemma Pasch : forall A B C l,
 ~Col A B C -> ~ Incid A l -> ~ Incid B l -> ~ Incid C l ->
 go_through l A B ->
 (go_through l A C /\ ~go_through l B C) \/
 (go_through l B C /\ ~ go_through l A C).
Proof.
unfold Incid.
tauto.
Qed.

Definition Cong (A B C D : Point) := True.

Lemma cong_pseudo_transitivity : forall A B C D E F,
   Cong A B C D -> Cong A B E F -> Cong C D E F.
Proof.
unfold Cong.
tauto.
Qed.

Lemma cong_reflexivity : forall A B, Cong A B A B.
Proof.
unfold Cong.
tauto.
Qed.

Lemma addition : forall A B C D E F,
  Bet A B C -> Bet D E F ->
  Cong A B D E -> Cong B C E F -> Cong A C D F.
Proof.
unfold Bet.
tauto.
Qed.

Lemma point_construction_existence : forall A B C D,
C<>D -> exists X, (Bet C X D \/ Bet C D X) /\ Cong C X A B.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

Lemma point_construction_unicity : forall A B C D X1 X2,
C<>D ->
Bet C X1 D \/ Bet C D X1 -> Cong C X1 A B ->
Bet C X2 D \/ Bet C D X2 -> Cong C X2 A B ->
EqP X1 X2.
Proof.
intros.
assert False.
eauto.
intuition.
Qed.

End CounterExample.