Require Export GeoCoq.Axioms.tarski_axioms.

Section segment_construction_independent.

Inductive Point :=
 P0.

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

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

Lemma between_identity : forall A B, Bet A B A -> A=B.
Proof.
(* Goal: not (or (Bet P0 P0 P0) (or (Bet P0 P0 P0) (Bet P0 P0 P0))) *)
unfold Bet; tauto.
Qed.


Lemma cong_pseudo_reflexivity : forall A B, Cong A B B A.
Proof.
(* Goal: and (Cong A P0 B P0) (Cong A P0 C P0) *)
unfold Cong; tauto.
Qed.

Lemma cong_identity : forall A B C, Cong A B C C -> A = B.
Proof.
(* Goal: forall (A B C : Point) (_ : Cong A B C C), @eq Point A B *)
destruct A; destruct B; reflexivity.
Qed.

Lemma cong_inner_transitivity : forall A B C D E F,
  Cong A B C D -> Cong A B E F -> Cong C D E F.
Proof.
(* Goal: and (Cong A P0 B P0) (Cong A P0 C P0) *)
unfold Cong; tauto.
Qed.

Lemma inner_pasch : forall A B C P Q,
  Bet A P C -> Bet B Q C ->
  exists x, Bet P x B /\ Bet Q x A.
Proof.
(* Goal: not (or (Bet P0 P0 P0) (or (Bet P0 P0 P0) (Bet P0 P0 P0))) *)
unfold Bet; tauto.
Qed.

Lemma five_segment : forall A A' B B' C C' D D',
  Cong A B A' B' ->
  Cong B C B' C' ->
  Cong A D A' D' ->
  Cong B D B' D' ->
  Bet A B C -> Bet A' B' C' -> A <> B -> Cong C D C' D'.
Proof.
(* Goal: forall (A A' B B' C C' D D' : Point) (_ : Cong A B A' B') (_ : Cong B C B' C') (_ : Cong A D A' D') (_ : Cong B D B' D') (_ : Bet A B C) (_ : Bet A' B' C') (_ : not (@eq Point A B)), Cong C D C' D' *)
unfold Bet, Cong; tauto.
Qed.

Lemma not_segment_construction : ~ (forall A B C D,
  exists E, Bet A B E /\ Cong B E C D).
Proof.
(* Goal: not (forall A B C D : Point, @ex Point (fun E : Point => and (Bet A B E) (Cong B E C D))) *)
intro.
(* Goal: False *)
unfold Bet in *.
(* Goal: False *)
assert (T:= H P0 P0 P0 P0).
(* Goal: False *)
destruct T.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
tauto.
Qed.

Lemma lower_dim : exists A, exists B, exists C, ~ (Bet A B C \/ Bet B C A \/ Bet C A B).
Proof.
(* Goal: @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
exists P0.
(* Goal: @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
exists P0.
(* Goal: @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
exists P0.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
unfold Bet;tauto.
Qed.

Lemma upper_dim : forall A B C P Q ,
  P <> Q -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q ->
  (Bet A B C \/ Bet B C A \/ Bet C A B).
Proof.
(* Goal: forall (A B C : Point) (_ : not (or (Bet A B C) (or (Bet B C A) (Bet C A B)))), @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
intros.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
destruct P.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
destruct Q.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
tauto.
Qed.

Lemma euclid : forall A B C,
  ~ (Bet A B C \/ Bet B C A \/ Bet C A B) -> exists CC, Cong A CC B CC /\ Cong A CC C CC.
Proof.
(* Goal: forall (A B C : Point) (_ : not (or (Bet A B C) (or (Bet B C A) (Bet C A B)))), @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
intros.
(* Goal: @ex Point (fun CC : Point => and (Cong A CC B CC) (Cong A CC C CC)) *)
exists P0.
(* Goal: or (Bet A B C) (or (Bet B C A) (Bet C A B)) *)
unfold Cong;tauto.
Qed.

End segment_construction_independent.
