Library GeoCoq.Meta_theory.Models.tarski_to_beeson

Require Import GeoCoq.Axioms.beeson_s_axioms.
Require Export GeoCoq.Tarski_dev.Ch08_orthogonality.

Section Tarski_to_intuitionistic_Tarski.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma cong_stability : ∀ A B C D, ¬ ¬ Cong A B C D → Cong A B C D.
Proof.
intros.
elim (Cong_dec A B C D); intro HCong.

  apply HCong.

  contradiction.
Qed.

Definition BetH A B C : Prop := Bet A B C ∧ A ≠ B ∧ B ≠ C.

Lemma bet_stability : ∀ A B C, ¬ ¬ BetH A B C → BetH A B C.
Proof.
intros A B C HNNBet.
unfold BetH in ×.
elim (bet_dec A B C); intro HBet; elim (eq_dec_points A B); intro HAB; elim (eq_dec_points B C); intro HBC.

  subst.
  exfalso.
  apply HNNBet.
  intro.
  spliter.
  intuition.

  subst.
  exfalso.
  apply HNNBet.
  intro.
  spliter.
  intuition.

  subst.
  exfalso.
  apply HNNBet.
  intro.
  spliter.
  intuition.

  repeat split; assumption.

  exfalso.
  apply HNNBet.
  intro.
  spliter.
  contradiction.

  exfalso.
  apply HNNBet.
  intro.
  spliter.
  contradiction.

  exfalso.
  apply HNNBet.
  intro.
  spliter.
  contradiction.

  exfalso.
  apply HNNBet.
  intro.
  spliter.
  contradiction.
Qed.

Definition T A B C : Prop := ¬ (A≠B ∧ B≠C ∧ ¬ BetH A B C).

Definition ColB A B C := ¬ (~ T C A B ∧ ¬ T A C B ∧ ¬ T A B C).

Lemma between_identity_B : ∀ A B, ¬ BetH A B A.
Proof.
intros A B HNBet.
unfold BetH in ×.
destruct HNBet as [HBet [HAB HBA]].
apply between_identity in HBet.
subst.
intuition.
Qed.

Lemma Bet_T : ∀ A B C, Bet A B C → T A B C.
Proof.
intros A B C HBet.
unfold T.
intro HT.
destruct HT as [HAB [HBC HNBet]].
apply HNBet.
unfold BetH.
intuition.
Qed.

Lemma BetH_Bet : ∀ A B C, BetH A B C → Bet A B C.
Proof.
unfold BetH.
intuition.
Qed.

Lemma T_Bet : ∀ A B C, T A B C → Bet A B C.
Proof.
intros A B C HT.
unfold T in HT.
elim (bet_dec A B C); intro HBet.

  assumption.

  exfalso.
  apply HT.
  split.

    intro; subst; apply HBet; apply between_trivial2.

    split.

      intro; subst; apply HBet; apply between_trivial.

      intro HBetH; apply HBet; apply BetH_Bet in HBetH; assumption.
Qed.

Lemma NT_NBet : ∀ A B C, ¬ T A B C → ¬ Bet A B C.
Proof.
intros A B C HNT.
intro HNBet.
apply HNT.
apply Bet_T.
assumption.
Qed.

Lemma T_dec : ∀ A B C, T A B C ∨ ¬ T A B C.
Proof.
intros A B C.
elim (bet_dec A B C); intro HBet.

  left; apply Bet_T; assumption.

  right; intro HT; apply HBet; apply T_Bet in HT; assumption.
Qed.

Lemma between_inner_transitivity_B : ∀ A B C D : Tpoint, BetH A B D → BetH B C D → BetH A B C.
Proof.
intros A B C D HBet1 HBet2.
unfold BetH.
repeat split.

  apply BetH_Bet in HBet1.
  apply BetH_Bet in HBet2.
  apply between_inner_transitivity with D; assumption.

  unfold BetH in HBet1.
  spliter; assumption.

  unfold BetH in HBet2.
  spliter; assumption.
Qed.

Lemma ColB_Col : ∀ A B C, ColB A B C → Col A B C.
Proof.
intros A B C HCol.
unfold ColB in HCol.
unfold Col.
elim (T_dec A B C); intro HT1;
elim (T_dec A C B); intro HT2;
elim (T_dec C A B); intro HT3.

  apply T_Bet in HT1; intuition.

  apply T_Bet in HT1; intuition.

  apply T_Bet in HT1; intuition.

  apply T_Bet in HT1; intuition.

  apply T_Bet in HT2; intuition.

  apply T_Bet in HT2; intuition.

  apply T_Bet in HT3; intuition.

  exfalso; apply HCol; intuition.
Qed.

Lemma Diff_Col_ColB : ∀ A B C, Col A B C → ColB A B C.
Proof.
intros A B C H.
unfold Col in H.
unfold ColB.
intro HColB.
destruct HColB as [HNT1 [HNT2 HNT3]].
apply NT_NBet in HNT1.
apply NT_NBet in HNT2.
apply NT_NBet in HNT3.
elim H.

  intro HBet; contradiction.

  intro HColAux; elim HColAux; intro HBet; clear HColAux.

    apply between_symmetry in HBet.
    contradiction.

    contradiction.
Qed.

Lemma NColB_NDiffCol : ∀ A B C, ¬ ColB A B C → ¬ Col A B C.
Proof.
intros A B C HNCB.
intro HNC.
apply HNCB.
apply Diff_Col_ColB.
assumption.
Qed.

Lemma NColB_NColOrEq : ∀ A B C, ¬ ColB A B C → ¬ Col A B C.
Proof.
intros A B C HNCB.
apply NColB_NDiffCol in HNCB.
assumption.
Qed.

Lemma inner_pasch_B : ∀ A B C P Q,
  BetH A P C → BetH B Q C → ¬ ColB A B C →
  ∃ x, BetH P x B ∧ BetH Q x A.
Proof.
intros A B C P Q HBetH1 HBetH2 HNC.
unfold BetH in HBetH1.
destruct HBetH1 as [HBet1 [HAP HPC]].
unfold BetH in HBetH2.
destruct HBetH2 as [HBet2 [HBQ HQC]].
apply NColB_NColOrEq in HNC.
assert (HIP := inner_pasch A B C P Q HBet1 HBet2).
destruct HIP as [x [HBet3 HBet4]].
∃ x.
split.

  split; try assumption.
  split.

    intro.
    subst.
    apply HNC.
    assert_cols.
    ColR.

    intro.
    subst.
    apply HNC.
    assert_cols.
    ColR.

  split; try assumption.
  split.

    intro.
    subst.
    apply HNC.
    assert_cols.
    ColR.

    intro.
    subst.
    apply HNC.
    assert_cols.
    ColR.
Qed.

Lemma between_symmetry_B : ∀ A B C, BetH A B C → BetH C B A.
Proof.
unfold BetH.
intros A B C HBet.
repeat split; intuition.
Qed.

Lemma five_segment_B : ∀ A A' B B' C C' D D' : Tpoint,
    Cong A B A' B' →
    Cong B C B' C' →
    Cong A D A' D' →
    Cong B D B' D' →
    ¬ (A ≠ B ∧ B ≠ C ∧ ¬ BetH A B C) →
    ¬ (A' ≠ B' ∧ B' ≠ C' ∧ ¬ BetH A' B' C') →
    A ≠ B → Cong C D C' D'.
Proof.
intros.
assert (HBet1 : T A B C) by (unfold T; assumption).
assert (HBet2 : T A' B' C') by (unfold T; assumption).
apply T_Bet in H3.
apply T_Bet in H4.
apply five_segment with A A' B B'; assumption.
Qed.

Lemma segment_construction_B : ∀ A B C D, A≠B → ∃ E, T A B E ∧ Cong B E C D.
Proof.
intros A B C D HDiff.
assert (T := segment_construction A B C D).
destruct T as [E [HBet HCong]].
apply Bet_T in HBet.
∃ E; intuition.
Qed.

Lemma lower_dim_B : ¬ T PC PA PB ∧ ¬ T PA PC PB ∧ ¬ T PA PB PC.
Proof.
assert (HNBet := lower_dim).
elim (T_dec PC PA PB); intro HT1; elim (T_dec PA PC PB); intro HT2; elim (T_dec PA PB PC); intro HT3.

  exfalso; apply HNBet; left; apply T_Bet; assumption.

  exfalso; apply HNBet; right; right; apply T_Bet; assumption.

  exfalso; apply HNBet; left; apply T_Bet; assumption.

  exfalso; apply HNBet; right; right; apply T_Bet; assumption.

  exfalso; apply HNBet; left; apply T_Bet; assumption.

  exfalso; apply HNBet; right; left; apply between_symmetry; apply T_Bet; assumption.

  exfalso; apply HNBet; left; apply T_Bet; assumption.

  tauto.
Qed.

Instance Beeson_follows_from_Tarski : intuitionistic_Tarski_neutral_dimensionless.
Proof.
exact (Build_intuitionistic_Tarski_neutral_dimensionless
 Tpoint BetH Cong
 cong_stability
 bet_stability
 cong_identity
 cong_inner_transitivity
 cong_pseudo_reflexivity
 segment_construction_B
 five_segment_B
 between_identity_B
 between_symmetry_B
 between_inner_transitivity_B
 inner_pasch_B
 PA PB PC
 lower_dim_B).
Qed.

End Tarski_to_intuitionistic_Tarski.

Section Proof_of_eq_stability_in_IT.

Context `{BTn:intuitionistic_Tarski_neutral_dimensionless}.

Lemma cong_stability_eq_stability : ∀ A B : ITpoint, ¬ A ≠ B → A = B.
Proof.
intros A B HAB.
apply Icong_identity with A.
apply Cong_stability.
intro HNCong.
apply HAB.
intro HEq.
subst.
apply HNCong.
apply Icong_pseudo_reflexivity.
Qed.

End Proof_of_eq_stability_in_IT.

Require Import Classical.

Section Intuitionistic_Tarski_to_Tarski.

Context `{BTn:intuitionistic_Tarski_neutral_dimensionless}.

Lemma Col_dec : ∀ A B C, ICol A B C ∨ ¬ ICol A B C.
Proof.
intros.
tauto.
Qed.

Lemma eq_dec : ∀ A B :ITpoint, A=B ∨ A≠B.
Proof.
intros.
tauto.
Qed.

Definition BetT A B C := IBet A B C ∨ A=B ∨ B=C.

Lemma bet_id : ∀ A B : ITpoint, BetT A B A → A = B.
Proof.
intros.
unfold BetT in H.
decompose [or] H.
apply Ibetween_identity in H0.
elim H0.
assumption.
intuition.
Qed.

Lemma IT_chara : ∀ A B C,
 IT A B C ↔ A=B ∨ B=C ∨ IBet A B C.
Proof.
intros.
unfold IT.
tauto. Qed.

Lemma BetT_symmetry : ∀ A B C, BetT A B C → BetT C B A.
Proof.
intros.
unfold BetT in ×.
intuition.
left.
apply Ibetween_symmetry.
assumption.
Qed.

Lemma BetT_id : ∀ A B, BetT A B A → A=B.
Proof.
intros.
unfold BetT in ×.
intuition.
apply Ibetween_identity in H0.
elim H0.
Qed.


Lemma pasch_col_case : ∀ A B C P Q : ITpoint,
        BetT A P C →
        BetT B Q C → ICol A B C → ∃ x : ITpoint, BetT P x B ∧ BetT Q x A.
Proof.
intros.
elim (eq_dec A B);intro.
 subst.
 ∃ B.
 unfold BetT;auto.
elim (eq_dec A C);intro.
 subst.
 apply BetT_id in H.
 subst.
 ∃ P.
 unfold BetT;auto.
elim (eq_dec B C);intro.
 subst.
 apply BetT_id in H0.
 subst.
 ∃ Q.
 unfold BetT;auto.
elim (eq_dec B Q);intro.
 subst.
 ∃ Q.
 unfold BetT;auto.
elim (eq_dec C Q);intro.
 subst.
 ∃ P.
 split.
 unfold BetT;auto.
 apply BetT_symmetry.
 auto.
elim (eq_dec A P);intro.
 subst.
 ∃ P.
 unfold BetT;auto.
elim (eq_dec C P);intro.
 subst.
 ∃ Q.
 split.
 apply BetT_symmetry.
 auto.
 unfold BetT;auto.

unfold ICol in H1.
spliter.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
unfold IT in ×.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply NNPP in H1.
∃ A.
split.
apply Ibetween_symmetry in H1.
induction H.
assert (T:=Ibetween_inner_transitivity B A P C H1 H).
unfold BetT.
left.
apply Ibetween_symmetry;auto.
induction H;subst.
unfold BetT;auto.
left.
apply Ibetween_symmetry;auto.
unfold BetT;auto.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
unfold IT in H1.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply NNPP in H1.

∃ C.

unfold BetT in H.
induction H;induction H0.
split.
apply BetT_symmetry.
left.

apply Ibetween_inner_transitivity with A.
apply Ibetween_symmetry;auto.
apply Ibetween_symmetry;auto.
apply BetT_symmetry.
left.
apply Ibetween_inner_transitivity with B.
assumption.
apply Ibetween_symmetry;auto.
induction H0;subst;intuition.
induction H;subst;intuition.
induction H;subst;intuition.

apply NNPP in H1.
induction H;induction H0.

∃ B.
split.
unfold BetT;auto.

left.
apply Ibetween_symmetry.
apply Ibetween_inner_transitivity with C.
unfold IT in H1.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply not_and_or in H1.
induction H1.
apply NNPP in H1.
subst.
intuition.
apply NNPP in H1.
assumption.
assumption.

induction H0;subst;intuition.
induction H;subst;intuition.
induction H;subst;intuition.
Qed.

Lemma pasch : ∀ A B C P Q : ITpoint,
        BetT A P C →
        BetT B Q C → ∃ x : ITpoint, BetT P x B ∧ BetT Q x A.
Proof.
intros.
induction (Col_dec A B C).
eapply pasch_col_case;eauto.

unfold BetT in ×.
decompose [or] H;clear H.
decompose [or] H0;clear H0.

elim (Iinner_pasch A B C P Q H2 H H1).
intros.
spliter.
∃ x.
split.
tauto.
tauto.

subst.
∃ Q;auto.
subst.
∃ P.
split.
auto.
left.
apply Ibetween_symmetry.
auto.
subst.
∃ P;auto.
subst.
decompose [or] H0;clear H0.
∃ Q.
split.
left.
apply Ibetween_symmetry.
auto.
auto.
subst.
∃ Q;auto.
subst.
∃ C;auto.
Qed.

Lemma five_segment:
 ∀ A A' B B' C C' D D' : ITpoint,
        ICong A B A' B' →
        ICong B C B' C' →
        ICong A D A' D' →
        ICong B D B' D' →
        BetT A B C → BetT A' B' C' → A ≠ B → ICong C D C' D'.
Proof.
intros.
apply Ifive_segment with A A' B B' ;try assumption.
unfold IT.
intro.
spliter.
unfold BetT in ×.
intuition.
unfold BetT in ×.
unfold IT.
intro.
intuition.
Qed.

Lemma IT_trivial : ∀ A B, IT A A B.
Proof.
intros.
unfold IT.
intro.
spliter.
intuition.
Qed.

Lemma IT_trivial2 : ∀ A B, IT A B B.
Proof.
intros.
unfold IT.
intro.
spliter.
intuition.
Qed.

Lemma another_point : ∀ A, ∃ B:ITpoint, A≠B.
Proof.
intros.
assert (T:=Ilower_dim).
elim (eq_dec A beeson_s_axioms.PA);intro.
subst.
elim (eq_dec beeson_s_axioms.PA beeson_s_axioms.PB);intro.
rewrite <- H in ×.
exfalso.
apply T.
apply IT_trivial.
∃ beeson_s_axioms.PB.
assumption.
∃ beeson_s_axioms.PA.
assumption.
Qed.

Lemma segment_construction :
 ∀ A B C D : ITpoint,
        ∃ E : ITpoint, BetT A B E ∧ ICong B E C D.
Proof.
intros.
induction (eq_dec A B).
subst.
elim (another_point B);intros.
elim (Isegment_construction x B C D);intros.
∃ x0.
split.
unfold BetT.
intuition.
intuition.
intuition.
elim (Isegment_construction A B C D H).
intros.
∃ x.
spliter.
split;try assumption.
unfold IT in ×.
unfold BetT.
tauto.
Qed.

Lemma lower_dim :
  ¬ (BetT beeson_s_axioms.PA beeson_s_axioms.PB beeson_s_axioms.PC ∨
     BetT beeson_s_axioms.PB beeson_s_axioms.PC beeson_s_axioms.PA ∨
     BetT beeson_s_axioms.PC beeson_s_axioms.PA beeson_s_axioms.PB).
Proof.
assert (T:=Ilower_dim).
unfold BetT in ×.
unfold ICol in ×.
unfold IT in ×.
firstorder using Ibetween_symmetry.
Qed.

Lemma eq_dec_points_from_classic : ∀ A B : ITpoint, A = B ∨ A ≠ B.
Proof.
intros.
apply classic.
Qed.

Instance IT_to_T : Tarski_neutral_dimensionless.
exact
(Build_Tarski_neutral_dimensionless
   ITpoint BetT ICong
   Icong_pseudo_reflexivity Icong_inner_transitivity Icong_identity
   segment_construction five_segment
   bet_id pasch beeson_s_axioms.PA beeson_s_axioms.PB beeson_s_axioms.PC lower_dim).
Defined.

Instance IT_to_TID :
  Tarski_neutral_dimensionless_with_decidable_point_equality IT_to_T.
Proof. split; apply eq_dec_points_from_classic. Defined.

End Intuitionistic_Tarski_to_Tarski.