Require Export GeoCoq.Axioms.tarski_axioms.

(** This proves that between_identity is independent from other axioms of neutral geometry. *)

Section between_identity_independent.

Inductive Point :=
  P0 | P1 | P2 | P3.

Definition Bet (A B C : Point) :=
  A = B \/ B = C \/ A = C.

Definition Cong (A B C D : Point) :=
  (A = B /\ C = D) \/ (A <> B /\ C <> D).

Lemma not_between_identity : ~ (forall A B, Bet A B A -> A=B).
Proof.
(* Goal: not (or (or (@eq Point P0 P1) (or (@eq Point P1 P2) (@eq Point P0 P2))) (or (or (@eq Point P1 P2) (or (@eq Point P2 P0) (@eq Point P1 P0))) (or (@eq Point P2 P0) (or (@eq Point P0 P1) (@eq Point P2 P1))))) *)
intro.
(* Goal: False *)
assert (T:= H P0 P1).
(* Goal: False *)
assert (P0=P1).
(* Goal: @eq Point P0 P1 *)
(* Goal: False *)
apply T.
(* Goal: Bet P0 P1 P0 *)
(* Goal: False *)
unfold Bet;tauto.
(* Goal: False *)
discriminate.
Qed.

Lemma cong_pseudo_reflexivity : forall A B, Cong A B B A.
Proof.
unfold Cong;intros;destruct A; destruct B;try
tauto;
(* Goal: False *)
right;split;discriminate.
Qed.

Lemma cong_identity : forall A B C, Cong A B C C -> A = B.
Proof.
(* Goal: forall (A B C D : Point) (_ : Cong A B C D), Cong C D A B *)
unfold Cong.
(* 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: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
tauto.
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 (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
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: 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)) *)
unfold Bet; intros.
intuition;subst;
try (exists P;tauto);
try (exists Q;tauto);
(* Goal: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
exists C;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 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)) *)
unfold Bet, Cong;intros.
(* Goal: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
intuition;repeat subst;tauto.
Qed.

Lemma point_eq_dec : forall A B : Point, A=B \/ 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: False *)
destruct A; destruct B;try tauto;right;discriminate.
Qed.

Lemma segment_construction : forall A B C D,
  exists E, Bet A B E /\ Cong B E C D.
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 E : Point => and (Bet A B E) (Cong B E C D)) *)
unfold Bet, Cong.

(* Goal: @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
elim (point_eq_dec C D).
(* 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 E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
exists B.
(* Goal: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
tauto.
(* 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 E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
elim (point_eq_dec A B).
(* Goal: forall _ : @eq Point A B, @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
(* Goal: forall _ : not (@eq Point A B), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
intro;subst.
destruct B; try (exists P0; split; try tauto; right; split; try discriminate; assumption);
exists P1; split; try tauto; right; split; try discriminate; assumption.

(* Goal: forall _ : not (@eq Point A B), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
intros; exists A; firstorder.
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 A : Point => @ex Point (fun B : Point => @ex Point (fun C : Point => not (or (Bet A B C) (or (Bet B C A) (Bet C A B)))))) *)
exists P0.
(* Goal: @ex Point (fun B : Point => @ex Point (fun C : Point => not (or (Bet P0 B C) (or (Bet B C P0) (Bet C P0 B))))) *)
exists P1.
(* Goal: @ex Point (fun C : Point => not (or (Bet P0 P1 C) (or (Bet P1 C P0) (Bet C P0 P1)))) *)
exists P2.
(* Goal: not (or (Bet P0 P1 P2) (or (Bet P1 P2 P0) (Bet P2 P0 P1))) *)
unfold Bet.
(* Goal: not (or (or (@eq Point P0 P1) (or (@eq Point P1 P2) (@eq Point P0 P2))) (or (or (@eq Point P1 P2) (or (@eq Point P2 P0) (@eq Point P1 P0))) (or (@eq Point P2 P0) (or (@eq Point P0 P1) (@eq Point P2 P1))))) *)
intro.
(* Goal: False *)
intuition discriminate.
Qed.

Lemma cong_sym : forall A B C D, Cong A B C D -> Cong C D A B.
Proof.
(* Goal: forall (A B C D : Point) (_ : Cong A B C D), Cong C D A B *)
unfold Cong.
(* Goal: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
intros;tauto.
Qed.

Lemma cong_aux : forall A, Cong A P0 A P1 -> A = P2 \/ A = P3.
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.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_2 : forall A, Cong A P0 A P2 -> A = P1 \/ A = P3.
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.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_3 : forall A, Cong A P1 A P2 -> A = P0 \/ A = P3.
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.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_4 : forall A, Cong A P0 A P3 -> A = P1 \/ A = P2.
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.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_5 : forall A, Cong A P1 A P3 -> A = P0 \/ A = P2.
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.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_6 : forall A, Cong A P2 A P3 -> A = P0 \/ A = P1.
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.
destruct A;unfold Cong in *;
intuition;congruence.
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.
destruct P; destruct Q; try solve [intuition];
try (apply cong_aux in H0; apply cong_aux in H1; apply cong_aux in H2);
try (apply cong_aux_2 in H0; apply cong_aux_2 in H1; apply cong_aux_2 in H2);
try (apply cong_aux_3 in H0; apply cong_aux_3 in H1; apply cong_aux_3 in H2);
try (apply cong_aux_4 in H0; apply cong_aux_4 in H1; apply cong_aux_4 in H2);
try (apply cong_aux_5 in H0; apply cong_aux_5 in H1; apply cong_aux_5 in H2);
try (apply cong_aux_6 in H0; apply cong_aux_6 in H1; apply cong_aux_6 in H2);
try (apply cong_sym in H0; apply cong_sym in H1; apply cong_sym in H2);
try (apply cong_aux in H0; apply cong_aux in H1; apply cong_aux in H2);
try (apply cong_aux_2 in H0; apply cong_aux_2 in H1; apply cong_aux_2 in H2);
try (apply cong_aux_3 in H0; apply cong_aux_3 in H1; apply cong_aux_3 in H2);
try (apply cong_aux_4 in H0; apply cong_aux_4 in H1; apply cong_aux_4 in H2);
try (apply cong_aux_5 in H0; apply cong_aux_5 in H1; apply cong_aux_5 in H2);
try (apply cong_aux_6 in H0; apply cong_aux_6 in H1; apply cong_aux_6 in H2);
(* Goal: and (or (@eq Point A B) (or (@eq Point B B) (@eq Point A B))) (or (and (@eq Point B B) (@eq Point C D)) (and (not (@eq Point B B)) (not (@eq Point C D)))) *)
(* Goal: forall _ : not (@eq Point C D), @ex Point (fun E : Point => and (or (@eq Point A B) (or (@eq Point B E) (@eq Point A E))) (or (and (@eq Point B E) (@eq Point C D)) (and (not (@eq Point B E)) (not (@eq Point C D))))) *)
intuition; subst; unfold Bet; tauto.
Qed.

Lemma not_bet_diff : forall A B C,
  ~ (Bet A B C \/ Bet B C A \/ Bet C A B) -> A <> B /\ B <> C /\ A <> C.
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)) *)
unfold Bet; intros.
(* Goal: and (not (@eq Point A B)) (and (not (@eq Point B C)) (not (@eq Point A C))) *)
destruct A; destruct B; destruct C; intuition.
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: forall (A B C D : Point) (_ : Cong A B C D), Cong C D A B *)
apply not_bet_diff in H; spliter; unfold Cong.
destruct A; destruct B; destruct C; try tauto;
try (exists P3; split; right; split; discriminate);
try (exists P2; split; right; split; discriminate);
try (exists P1; split; right; split; discriminate);
(* Goal: False *)
exists P0; split; right; split; discriminate.
Qed.

End between_identity_independent.
