Library GeoCoq.Meta_theory.Counter_models.counter_model_bet_identity

Require Export GeoCoq.Axioms.tarski_axioms.

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 : ¬ (∀ A B, Bet A B A → A=B).
Proof.
intro.
assert (T:= H P0 P1).
assert (P0=P1).
apply T.
unfold Bet;tauto.
discriminate.
Qed.

Lemma cong_pseudo_reflexivity : ∀ A B, Cong A B B A.
Proof.
unfold Cong;intros;destruct A; destruct B;try
tauto;
right;split;discriminate.
Qed.

Lemma cong_identity : ∀ A B C, Cong A B C C → A = B.
Proof.
unfold Cong.
intros.
tauto.
Qed.

Lemma cong_inner_transitivity : ∀ 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 inner_pasch : ∀ A B C P Q,
  Bet A P C → Bet B Q C →
  ∃ x, Bet P x B ∧ Bet Q x A.
Proof.
unfold Bet; intros.
intuition;subst;
try (∃ P;tauto);
try (∃ Q;tauto);
∃ C;tauto.
Qed.

Lemma five_segment : ∀ 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.
unfold Bet, Cong;intros.
intuition;repeat subst;tauto.
Qed.

Lemma point_eq_dec : ∀ A B : Point, A=B ∨ A≠B.
Proof.
intros.
destruct A; destruct B;try tauto;right;discriminate.
Qed.

Lemma segment_construction : ∀ A B C D,
  ∃ E, Bet A B E ∧ Cong B E C D.
Proof.
intros.
unfold Bet, Cong.

elim (point_eq_dec C D).
intros.
∃ B.
tauto.
intros.
elim (point_eq_dec A B).
intro;subst.
destruct B; try (∃ P0; split; try tauto; right; split; try discriminate; assumption);
∃ P1; split; try tauto; right; split; try discriminate; assumption.

intros; ∃ A; firstorder.
Qed.

Lemma lower_dim : ∃ A, ∃ B, ∃ C, ¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B).
Proof.
∃ P0.
∃ P1.
∃ P2.
unfold Bet.
intro.
intuition discriminate.
Qed.

Lemma cong_sym : ∀ A B C D, Cong A B C D → Cong C D A B.
Proof.
unfold Cong.
intros;tauto.
Qed.

Lemma cong_aux : ∀ A, Cong A P0 A P1 → A = P2 ∨ A = P3.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_2 : ∀ A, Cong A P0 A P2 → A = P1 ∨ A = P3.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_3 : ∀ A, Cong A P1 A P2 → A = P0 ∨ A = P3.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_4 : ∀ A, Cong A P0 A P3 → A = P1 ∨ A = P2.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_5 : ∀ A, Cong A P1 A P3 → A = P0 ∨ A = P2.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma cong_aux_6 : ∀ A, Cong A P2 A P3 → A = P0 ∨ A = P1.
Proof.
intros.
destruct A;unfold Cong in *;
intuition;congruence.
Qed.

Lemma upper_dim : ∀ 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.
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);
intuition; subst; unfold Bet; tauto.
Qed.

Lemma not_bet_diff : ∀ A B C,
  ¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B) → A ≠ B ∧ B ≠ C ∧ A ≠ C.
Proof.
unfold Bet; intros.
destruct A; destruct B; destruct C; intuition.
Qed.

Lemma euclid : ∀ A B C,
  ¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B) → ∃ CC, Cong A CC B CC ∧ Cong A CC C CC.
Proof.
intros.
apply not_bet_diff in H; spliter; unfold Cong.
destruct A; destruct B; destruct C; try tauto;
try (∃ P3; split; right; split; discriminate);
try (∃ P2; split; right; split; discriminate);
try (∃ P1; split; right; split; discriminate);
∃ P0; split; right; split; discriminate.
Qed.

End between_identity_independent.