Library GeoCoq.Meta_theory.Models.independent_tarski_to_tarski
Require Import GeoCoq.Axioms.tarski_axioms.
Require Import GeoCoq.Axioms.independent_tarski_axioms.
Require Import GeoCoq.Tarski_dev.Ch05_bet_le.
Section Independent_Tarski_neutral_dimensionless_to_Tarski_neutral_dimensionless.
Context `{ITnEQD:independent_Tarski_neutral_dimensionless_with_decidable_point_equality}.
Lemma g2_1 : ∀ A B, CongG A B A B.
Proof.
intros A B.
apply cong_inner_transitivityG with B A;
apply cong_pseudo_reflexivityG; auto.
Qed.
Lemma g2_2 : ∀ A B C D,
CongG A B C D → CongG C D A B.
Proof.
intros A B C D HCong.
apply cong_inner_transitivityG with C D; auto; apply g2_1.
Qed.
Lemma cong_inner_transitivityT : ∀ A B C D E F,
CongG A B C D → CongG A B E F → CongG C D E F.
Proof.
intros A B C D E F HCong1 HCong2.
apply cong_inner_transitivityG with A B; apply g2_2; auto.
Qed.
Lemma g2_3 : ∀ A B C D,
CongG A B C D → CongG B A C D.
Proof.
Proof.
intros A B C D HCong.
apply cong_inner_transitivityT with A B; auto.
apply cong_pseudo_reflexivityG.
Qed.
Lemma g2_4 : ∀ A B C D,
CongG A B C D → CongG A B D C.
Proof. intros A B C D HCong; apply g2_2; apply g2_3; apply g2_2; auto. Qed.
Lemma g2_5 : ∀ A B C D,
CongG A B C D → (A = B ↔ C = D).
Proof.
intros A B C D HCong.
split; intro H; rewrite H in HCong;
[apply g2_2 in HCong|]; apply cong_identityG in HCong; auto.
Qed.
Lemma g2_6 : ∀ A B,
BetG A B B ∧ CongG B B A A.
Proof.
intros A B; destruct (segment_constructionG A B A A) as [C [HBet HCong]].
assert (B = C) by (apply g2_5 with A A; auto).
rewrite H in *; auto.
Qed.
Lemma g2_7 : ∀ A B C A' B' C',
CongG A B A' B' → CongG B C B' C' →
BetG A B C → BetG A' B' C' →
CongG A C A' C'.
Proof.
intros A B C A' B' C' HCong1 HCong2 HBet1 HBet2.
elim (point_equality_decidabilityG A B); intro HDiff1; [rewrite HDiff1 in *; clear HDiff1|].
{
assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto).
rewrite HEq; auto.
}
{
elim (g2_6 A' A); intro HBet3; intro HCong3.
apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto.
apply g2_3; apply g2_4; auto.
}
Qed.
Lemma g2_8 : ∀ A B C D,
BetG A B C → BetG A B D → CongG B C B D → A ≠ B → C = D.
Proof.
intros A B C D HBet1 HBet2 HCong HDiff.
assert (HEq : CongG C C C D).
{
apply five_segmentG with A A B B; auto; try apply g2_1.
apply g2_7 with B B; auto; apply g2_1.
}
apply g2_5 with C C; auto; apply g2_2; auto.
Qed.
Lemma g2_9 : ∀ A B C, BetG A B A → BetG C A B.
Proof.
intros A B C HBet.
apply bet_inner_transitivityG with A; auto; apply g2_6.
Qed.
Lemma g2_10 : ∀ A B C, BetG A B A → BetG C B A.
Proof. intros A B C HBet; do 2 apply g2_9; auto. Qed.
Lemma g2_11 : ∀ A B C,
BetG A B A → A ≠ B →
∃ D, BetG C D C ∧ BetG D C D ∧ C ≠ D.
Proof.
intros A B C HBet1 HDiff1.
destruct (segment_constructionG C C A B) as [D [HBet2 HCong1]].
assert (HDiff2 : C ≠ D)
by (intro; apply g2_5 in HCong1; apply HDiff1; apply HCong1; auto).
destruct (segment_constructionG C D B A) as [E [HBet3 HCong2]].
assert (HCong3 : CongG C E A A) by (apply g2_7 with D B; auto).
assert (HEq : C = E) by (apply g2_5 in HCong3; apply HCong3; auto).
rewrite HEq in *; clear HEq; ∃ D; do 2 (split; auto); apply g2_9; auto.
Qed.
Lemma g2_12 : ∀ A B C, BetG A B A → BetG A B C.
Proof. intros A B C HBet; apply bet_symmetryG; apply g2_10; auto. Qed.
Lemma g2_13 : ∀ A B C, BetG A B A → A ≠ B → BetG C B C.
Proof.
intros A B C HBet1 HDiff.
destruct (segment_constructionG C B B C) as [D [HBet2 HCong1]].
assert (HEq : C = D) by (apply g2_8 with A B; try apply g2_2; try apply g2_12; auto).
rewrite HEq in *; auto.
Qed.
Lemma g2_14 : ∀ A B C D, BetG A B A → A ≠ B → BetG C D C ∧ BetG D C D.
Proof.
intros A B C D HBet1 HDiff1.
split.
{
destruct (g2_11 A B D) as [E [HBet2 [HBet3 HDiff2]]]; auto.
apply g2_13 with E; auto.
}
{
destruct (g2_11 A B C) as [E [HBet2 [HBet3 HDiff2]]]; auto.
apply g2_13 with E; auto.
}
Qed.
Lemma g2_15 : ∀ A B C D E, BetG A B A → A ≠ B → BetG C D E.
Proof.
intros A B C D E HBet HDiff.
apply g2_9. destruct (g2_14 A B D E) as [HBet1 HBet2]; auto.
Qed.
Lemma g2_16 : ∀ A B C D E, ¬ BetG C D E → BetG A B A → A = B.
Proof.
intros A B C D E HNBet HBet.
elim (point_equality_decidabilityG A B); intro HDiff; auto.
exfalso; apply HNBet; apply g2_15 with A B; auto.
Qed.
Lemma between_identityT : ∀ A B, BetG A B A → A = B.
Proof.
intros A B; apply g2_16 with GPA GPB GPC; intro HNBet; apply lower_dimG; left; auto.
Qed.
Lemma cong_trivial_identityT : ∀ A B, CongG A A B B.
Proof. intros A B; destruct (g2_6 B A); auto. Qed.
Lemma l2_11T : ∀ A B C A' B' C',
BetG A B C → BetG A' B' C' →
CongG A B A' B' → CongG B C B' C' →
CongG A C A' C'.
Proof.
intros A B C A' B' C' HBet1 HBet2 HCong1 HCong2.
elim (point_equality_decidabilityG A B); intro HDiff; [rewrite HDiff in *; clear HDiff|].
{
assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto).
rewrite HEq in *; auto.
}
{
apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto;
try apply cong_trivial_identityT; apply g2_3; apply g2_4; auto.
}
Qed.
Lemma construction_uniquenessT : ∀ Q A B C X Y,
Q ≠ A → BetG Q A X → CongG A X B C → BetG Q A Y → CongG A Y B C → X = Y.
Proof.
intros Q A B C X Y HDiff HBet1 HCong1 HBet2 HCong2.
assert (HCong3 : CongG A X A Y) by (apply cong_inner_transitivityG with B C; auto).
assert (HCong4 : CongG Q X Q Y) by (apply l2_11T with A A; auto; apply g2_1).
assert (HCong5 : CongG X X X Y)
by (apply five_segmentG with Q Q A A; auto; apply g2_1).
apply g2_5 with X X; try apply g2_2; auto.
Qed.
Lemma between_trivialT : ∀ A B, BetG A B B.
Proof. intros A B; destruct (g2_6 A B); auto. Qed.
Lemma bet_decG : ∀ A B C, BetG A B C ∨ ¬ BetG A B C.
Proof.
intros A B C.
destruct (segment_constructionG A B B C) as [D [HBet1 HCong]].
elim (point_equality_decidabilityG C D); intro HDiff1; [rewrite HDiff1 in *; auto|].
elim (point_equality_decidabilityG A B); intro HDiff2;
[rewrite HDiff2 in *; left; apply bet_symmetryG; apply between_trivialT|].
right; intro HBet2; apply HDiff1; apply construction_uniquenessT with A B B C;
auto; apply g2_1.
Qed.
Definition ColG A B C := BetG A B C ∨ BetG B C A ∨ BetG C A B.
Lemma Col_decG : ∀ A B C, ColG A B C ∨ ¬ ColG A B C.
Proof.
intros A B C; unfold ColG; induction (bet_decG A B C); induction (bet_decG B C A);
induction (bet_decG C A B); tauto.
Qed.
Lemma inner_paschT : ∀ A B C P Q,
BetG A P C → BetG B Q C →
∃ x, BetG P x B ∧ BetG Q x A.
Proof.
intros A B C P Q HBet1 HBet2.
elim (point_equality_decidabilityG A P); intro HDiff1;
[rewrite HDiff1 in *; ∃ P; split;
[apply bet_symmetryG|]; apply between_trivialT|].
elim (point_equality_decidabilityG P C); intro HDiff2;
[rewrite HDiff2 in *; ∃ Q; split; apply bet_symmetryG;
try apply between_trivialT; auto|].
elim (point_equality_decidabilityG B Q); intro HDiff3;
[rewrite HDiff3 in *; ∃ Q; split;
[|apply bet_symmetryG]; apply between_trivialT|].
elim (point_equality_decidabilityG Q C); intro HDiff4;
[rewrite HDiff4 in *; ∃ P; split; apply bet_symmetryG;
try apply between_trivialT; auto|].
elim (Col_decG A B C); intro HCol; [|apply inner_paschG with C; auto].
do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3.
{
∃ B; split; [apply between_trivialT|].
apply bet_symmetryG; apply bet_inner_transitivityG with C; auto.
}
{
∃ C; split.
{
apply bet_symmetryG; apply bet_inner_transitivityG with A;
auto; apply bet_symmetryG; auto.
}
{
apply bet_symmetryG; apply bet_inner_transitivityG with B;
apply bet_symmetryG; auto.
}
}
{
∃ A; split; [|apply between_trivialT].
apply bet_symmetryG; apply bet_inner_transitivityG with C;
auto; apply bet_symmetryG; auto.
}
Qed.
Global Instance TG_to_T : Tarski_neutral_dimensionless.
Proof.
exact
(Build_Tarski_neutral_dimensionless TpointG BetG CongG
cong_pseudo_reflexivityG cong_inner_transitivityT cong_identityG
segment_constructionG five_segmentG
between_identityT inner_paschT
GPA GPB GPC
lower_dimG).
Defined.
Global Instance TG_to_TID :
Tarski_neutral_dimensionless_with_decidable_point_equality TG_to_T.
Proof. split; exact point_equality_decidabilityG. Defined.
End Independent_Tarski_neutral_dimensionless_to_Tarski_neutral_dimensionless.
Section Independent_Tarski_2D_to_Tarski_2D.
Context `{IT2D:independent_Tarski_2D}.
Lemma upper_dimT : ∀ A B C P Q,
P ≠ Q → CongG A P A Q → CongG B P B Q → CongG C P C Q →
(BetG A B C ∨ BetG B C A ∨ BetG C A B).
Proof.
intros A B C P Q HPQ HCong1 HCong2 HCong3.
elim (point_equality_decidabilityG A B); intro HAB; try (rewrite HAB in *; clear HAB);
elim (point_equality_decidabilityG A C); intro HAC; try (rewrite HAC in *; clear HAC);
elim (point_equality_decidabilityG B C); intro HBC; try (rewrite HBC in *; clear HBC).
{
left; apply between_trivialT.
}
{
right; right; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
right; right; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
right; left; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
apply upper_dimG with P Q; auto.
}
Qed.
Global Instance TG2D_to_T2D : Tarski_2D TG_to_TID.
Proof. split; exact upper_dimT. Defined.
End Independent_Tarski_2D_to_Tarski_2D.
Section Independent_Tarski_2D_euclidean_to_Tarski_2D_euclidean.
Context `{ITE:independent_Tarski_2D_euclidean}.
Global Instance TG2D_euclidean_to_T2D_euclidean :
Tarski_2D_euclidean TG2D_to_T2D.
Proof.
assert (H := TG_to_TID).
split; intros A B C D T HBet1 HBet2 HDiff1.
elim (eq_dec_points B D); intro HDiff2;
[treat_equalities; ∃ T, C; Between|].
elim (eq_dec_points D C); intro HDiff3;
[treat_equalities; ∃ B, T; Between|].
elim (Col_dec A B C); intro HCol; [|apply euclidG with D; auto].
clear HDiff2; clear HDiff3.
do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3.
{
elim (eq_dec_points A B); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
elim (l5_2 A B C T); eBetween; intro HBet4.
{
elim (eq_dec_points B C); intro HDiff3;
[treat_equalities; ∃ T; ∃ T; Between|].
∃ B; ∃ T; do 2 (split; Between); eBetween.
}
{
elim (eq_dec_points B T); intro HDiff3;
[treat_equalities; ∃ B; ∃ C; Between|].
∃ B; ∃ C; Between.
}
}
{
elim (eq_dec_points A C); intro HDiff2;
[treat_equalities; ∃ B; ∃ T; Between|].
elim (l5_2 A C B T); eBetween; intro HBet4.
{
elim (eq_dec_points B C); intro HDiff3;
[treat_equalities; ∃ T; ∃ T; Between|].
∃ T; ∃ C; repeat (split; Between); eBetween.
}
{
∃ B; ∃ C; Between.
}
}
{
elim (l5_3 B A D C); Between; intro HBet4.
{
elim (eq_dec_points A B); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
elim (l5_2 B A C T); eBetween; intro HBet5.
{
∃ B; ∃ T; Between.
}
{
∃ B; ∃ C; do 2 (split; Between).
apply outer_transitivity_between2 with A; eBetween.
intro; treat_equalities; intuition.
}
}
{
elim (l5_2 A D B T); Between; intro HBet5.
{
elim (eq_dec_points B D); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
∃ T; ∃ C; do 2 (try split; Between); eBetween.
}
{
∃ B; ∃ C; do 2 (split; Between).
apply outer_transitivity_between with A; eBetween;
try (intro; treat_equalities; intuition).
}
}
}
Defined.
End Independent_Tarski_2D_euclidean_to_Tarski_2D_euclidean.
Require Import GeoCoq.Axioms.independent_tarski_axioms.
Require Import GeoCoq.Tarski_dev.Ch05_bet_le.
Section Independent_Tarski_neutral_dimensionless_to_Tarski_neutral_dimensionless.
Context `{ITnEQD:independent_Tarski_neutral_dimensionless_with_decidable_point_equality}.
Lemma g2_1 : ∀ A B, CongG A B A B.
Proof.
intros A B.
apply cong_inner_transitivityG with B A;
apply cong_pseudo_reflexivityG; auto.
Qed.
Lemma g2_2 : ∀ A B C D,
CongG A B C D → CongG C D A B.
Proof.
intros A B C D HCong.
apply cong_inner_transitivityG with C D; auto; apply g2_1.
Qed.
Lemma cong_inner_transitivityT : ∀ A B C D E F,
CongG A B C D → CongG A B E F → CongG C D E F.
Proof.
intros A B C D E F HCong1 HCong2.
apply cong_inner_transitivityG with A B; apply g2_2; auto.
Qed.
Lemma g2_3 : ∀ A B C D,
CongG A B C D → CongG B A C D.
Proof.
Proof.
intros A B C D HCong.
apply cong_inner_transitivityT with A B; auto.
apply cong_pseudo_reflexivityG.
Qed.
Lemma g2_4 : ∀ A B C D,
CongG A B C D → CongG A B D C.
Proof. intros A B C D HCong; apply g2_2; apply g2_3; apply g2_2; auto. Qed.
Lemma g2_5 : ∀ A B C D,
CongG A B C D → (A = B ↔ C = D).
Proof.
intros A B C D HCong.
split; intro H; rewrite H in HCong;
[apply g2_2 in HCong|]; apply cong_identityG in HCong; auto.
Qed.
Lemma g2_6 : ∀ A B,
BetG A B B ∧ CongG B B A A.
Proof.
intros A B; destruct (segment_constructionG A B A A) as [C [HBet HCong]].
assert (B = C) by (apply g2_5 with A A; auto).
rewrite H in *; auto.
Qed.
Lemma g2_7 : ∀ A B C A' B' C',
CongG A B A' B' → CongG B C B' C' →
BetG A B C → BetG A' B' C' →
CongG A C A' C'.
Proof.
intros A B C A' B' C' HCong1 HCong2 HBet1 HBet2.
elim (point_equality_decidabilityG A B); intro HDiff1; [rewrite HDiff1 in *; clear HDiff1|].
{
assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto).
rewrite HEq; auto.
}
{
elim (g2_6 A' A); intro HBet3; intro HCong3.
apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto.
apply g2_3; apply g2_4; auto.
}
Qed.
Lemma g2_8 : ∀ A B C D,
BetG A B C → BetG A B D → CongG B C B D → A ≠ B → C = D.
Proof.
intros A B C D HBet1 HBet2 HCong HDiff.
assert (HEq : CongG C C C D).
{
apply five_segmentG with A A B B; auto; try apply g2_1.
apply g2_7 with B B; auto; apply g2_1.
}
apply g2_5 with C C; auto; apply g2_2; auto.
Qed.
Lemma g2_9 : ∀ A B C, BetG A B A → BetG C A B.
Proof.
intros A B C HBet.
apply bet_inner_transitivityG with A; auto; apply g2_6.
Qed.
Lemma g2_10 : ∀ A B C, BetG A B A → BetG C B A.
Proof. intros A B C HBet; do 2 apply g2_9; auto. Qed.
Lemma g2_11 : ∀ A B C,
BetG A B A → A ≠ B →
∃ D, BetG C D C ∧ BetG D C D ∧ C ≠ D.
Proof.
intros A B C HBet1 HDiff1.
destruct (segment_constructionG C C A B) as [D [HBet2 HCong1]].
assert (HDiff2 : C ≠ D)
by (intro; apply g2_5 in HCong1; apply HDiff1; apply HCong1; auto).
destruct (segment_constructionG C D B A) as [E [HBet3 HCong2]].
assert (HCong3 : CongG C E A A) by (apply g2_7 with D B; auto).
assert (HEq : C = E) by (apply g2_5 in HCong3; apply HCong3; auto).
rewrite HEq in *; clear HEq; ∃ D; do 2 (split; auto); apply g2_9; auto.
Qed.
Lemma g2_12 : ∀ A B C, BetG A B A → BetG A B C.
Proof. intros A B C HBet; apply bet_symmetryG; apply g2_10; auto. Qed.
Lemma g2_13 : ∀ A B C, BetG A B A → A ≠ B → BetG C B C.
Proof.
intros A B C HBet1 HDiff.
destruct (segment_constructionG C B B C) as [D [HBet2 HCong1]].
assert (HEq : C = D) by (apply g2_8 with A B; try apply g2_2; try apply g2_12; auto).
rewrite HEq in *; auto.
Qed.
Lemma g2_14 : ∀ A B C D, BetG A B A → A ≠ B → BetG C D C ∧ BetG D C D.
Proof.
intros A B C D HBet1 HDiff1.
split.
{
destruct (g2_11 A B D) as [E [HBet2 [HBet3 HDiff2]]]; auto.
apply g2_13 with E; auto.
}
{
destruct (g2_11 A B C) as [E [HBet2 [HBet3 HDiff2]]]; auto.
apply g2_13 with E; auto.
}
Qed.
Lemma g2_15 : ∀ A B C D E, BetG A B A → A ≠ B → BetG C D E.
Proof.
intros A B C D E HBet HDiff.
apply g2_9. destruct (g2_14 A B D E) as [HBet1 HBet2]; auto.
Qed.
Lemma g2_16 : ∀ A B C D E, ¬ BetG C D E → BetG A B A → A = B.
Proof.
intros A B C D E HNBet HBet.
elim (point_equality_decidabilityG A B); intro HDiff; auto.
exfalso; apply HNBet; apply g2_15 with A B; auto.
Qed.
Lemma between_identityT : ∀ A B, BetG A B A → A = B.
Proof.
intros A B; apply g2_16 with GPA GPB GPC; intro HNBet; apply lower_dimG; left; auto.
Qed.
Lemma cong_trivial_identityT : ∀ A B, CongG A A B B.
Proof. intros A B; destruct (g2_6 B A); auto. Qed.
Lemma l2_11T : ∀ A B C A' B' C',
BetG A B C → BetG A' B' C' →
CongG A B A' B' → CongG B C B' C' →
CongG A C A' C'.
Proof.
intros A B C A' B' C' HBet1 HBet2 HCong1 HCong2.
elim (point_equality_decidabilityG A B); intro HDiff; [rewrite HDiff in *; clear HDiff|].
{
assert (HEq : A' = B') by (apply g2_5 with B B; try apply g2_2; auto).
rewrite HEq in *; auto.
}
{
apply g2_3; apply g2_4; apply five_segmentG with A A' B B'; auto;
try apply cong_trivial_identityT; apply g2_3; apply g2_4; auto.
}
Qed.
Lemma construction_uniquenessT : ∀ Q A B C X Y,
Q ≠ A → BetG Q A X → CongG A X B C → BetG Q A Y → CongG A Y B C → X = Y.
Proof.
intros Q A B C X Y HDiff HBet1 HCong1 HBet2 HCong2.
assert (HCong3 : CongG A X A Y) by (apply cong_inner_transitivityG with B C; auto).
assert (HCong4 : CongG Q X Q Y) by (apply l2_11T with A A; auto; apply g2_1).
assert (HCong5 : CongG X X X Y)
by (apply five_segmentG with Q Q A A; auto; apply g2_1).
apply g2_5 with X X; try apply g2_2; auto.
Qed.
Lemma between_trivialT : ∀ A B, BetG A B B.
Proof. intros A B; destruct (g2_6 A B); auto. Qed.
Lemma bet_decG : ∀ A B C, BetG A B C ∨ ¬ BetG A B C.
Proof.
intros A B C.
destruct (segment_constructionG A B B C) as [D [HBet1 HCong]].
elim (point_equality_decidabilityG C D); intro HDiff1; [rewrite HDiff1 in *; auto|].
elim (point_equality_decidabilityG A B); intro HDiff2;
[rewrite HDiff2 in *; left; apply bet_symmetryG; apply between_trivialT|].
right; intro HBet2; apply HDiff1; apply construction_uniquenessT with A B B C;
auto; apply g2_1.
Qed.
Definition ColG A B C := BetG A B C ∨ BetG B C A ∨ BetG C A B.
Lemma Col_decG : ∀ A B C, ColG A B C ∨ ¬ ColG A B C.
Proof.
intros A B C; unfold ColG; induction (bet_decG A B C); induction (bet_decG B C A);
induction (bet_decG C A B); tauto.
Qed.
Lemma inner_paschT : ∀ A B C P Q,
BetG A P C → BetG B Q C →
∃ x, BetG P x B ∧ BetG Q x A.
Proof.
intros A B C P Q HBet1 HBet2.
elim (point_equality_decidabilityG A P); intro HDiff1;
[rewrite HDiff1 in *; ∃ P; split;
[apply bet_symmetryG|]; apply between_trivialT|].
elim (point_equality_decidabilityG P C); intro HDiff2;
[rewrite HDiff2 in *; ∃ Q; split; apply bet_symmetryG;
try apply between_trivialT; auto|].
elim (point_equality_decidabilityG B Q); intro HDiff3;
[rewrite HDiff3 in *; ∃ Q; split;
[|apply bet_symmetryG]; apply between_trivialT|].
elim (point_equality_decidabilityG Q C); intro HDiff4;
[rewrite HDiff4 in *; ∃ P; split; apply bet_symmetryG;
try apply between_trivialT; auto|].
elim (Col_decG A B C); intro HCol; [|apply inner_paschG with C; auto].
do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3.
{
∃ B; split; [apply between_trivialT|].
apply bet_symmetryG; apply bet_inner_transitivityG with C; auto.
}
{
∃ C; split.
{
apply bet_symmetryG; apply bet_inner_transitivityG with A;
auto; apply bet_symmetryG; auto.
}
{
apply bet_symmetryG; apply bet_inner_transitivityG with B;
apply bet_symmetryG; auto.
}
}
{
∃ A; split; [|apply between_trivialT].
apply bet_symmetryG; apply bet_inner_transitivityG with C;
auto; apply bet_symmetryG; auto.
}
Qed.
Global Instance TG_to_T : Tarski_neutral_dimensionless.
Proof.
exact
(Build_Tarski_neutral_dimensionless TpointG BetG CongG
cong_pseudo_reflexivityG cong_inner_transitivityT cong_identityG
segment_constructionG five_segmentG
between_identityT inner_paschT
GPA GPB GPC
lower_dimG).
Defined.
Global Instance TG_to_TID :
Tarski_neutral_dimensionless_with_decidable_point_equality TG_to_T.
Proof. split; exact point_equality_decidabilityG. Defined.
End Independent_Tarski_neutral_dimensionless_to_Tarski_neutral_dimensionless.
Section Independent_Tarski_2D_to_Tarski_2D.
Context `{IT2D:independent_Tarski_2D}.
Lemma upper_dimT : ∀ A B C P Q,
P ≠ Q → CongG A P A Q → CongG B P B Q → CongG C P C Q →
(BetG A B C ∨ BetG B C A ∨ BetG C A B).
Proof.
intros A B C P Q HPQ HCong1 HCong2 HCong3.
elim (point_equality_decidabilityG A B); intro HAB; try (rewrite HAB in *; clear HAB);
elim (point_equality_decidabilityG A C); intro HAC; try (rewrite HAC in *; clear HAC);
elim (point_equality_decidabilityG B C); intro HBC; try (rewrite HBC in *; clear HBC).
{
left; apply between_trivialT.
}
{
right; right; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
right; right; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
right; left; apply between_trivialT.
}
{
left; apply between_trivialT.
}
{
apply upper_dimG with P Q; auto.
}
Qed.
Global Instance TG2D_to_T2D : Tarski_2D TG_to_TID.
Proof. split; exact upper_dimT. Defined.
End Independent_Tarski_2D_to_Tarski_2D.
Section Independent_Tarski_2D_euclidean_to_Tarski_2D_euclidean.
Context `{ITE:independent_Tarski_2D_euclidean}.
Global Instance TG2D_euclidean_to_T2D_euclidean :
Tarski_2D_euclidean TG2D_to_T2D.
Proof.
assert (H := TG_to_TID).
split; intros A B C D T HBet1 HBet2 HDiff1.
elim (eq_dec_points B D); intro HDiff2;
[treat_equalities; ∃ T, C; Between|].
elim (eq_dec_points D C); intro HDiff3;
[treat_equalities; ∃ B, T; Between|].
elim (Col_dec A B C); intro HCol; [|apply euclidG with D; auto].
clear HDiff2; clear HDiff3.
do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3.
{
elim (eq_dec_points A B); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
elim (l5_2 A B C T); eBetween; intro HBet4.
{
elim (eq_dec_points B C); intro HDiff3;
[treat_equalities; ∃ T; ∃ T; Between|].
∃ B; ∃ T; do 2 (split; Between); eBetween.
}
{
elim (eq_dec_points B T); intro HDiff3;
[treat_equalities; ∃ B; ∃ C; Between|].
∃ B; ∃ C; Between.
}
}
{
elim (eq_dec_points A C); intro HDiff2;
[treat_equalities; ∃ B; ∃ T; Between|].
elim (l5_2 A C B T); eBetween; intro HBet4.
{
elim (eq_dec_points B C); intro HDiff3;
[treat_equalities; ∃ T; ∃ T; Between|].
∃ T; ∃ C; repeat (split; Between); eBetween.
}
{
∃ B; ∃ C; Between.
}
}
{
elim (l5_3 B A D C); Between; intro HBet4.
{
elim (eq_dec_points A B); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
elim (l5_2 B A C T); eBetween; intro HBet5.
{
∃ B; ∃ T; Between.
}
{
∃ B; ∃ C; do 2 (split; Between).
apply outer_transitivity_between2 with A; eBetween.
intro; treat_equalities; intuition.
}
}
{
elim (l5_2 A D B T); Between; intro HBet5.
{
elim (eq_dec_points B D); intro HDiff2;
[treat_equalities; ∃ T; ∃ C; Between|].
∃ T; ∃ C; do 2 (try split; Between); eBetween.
}
{
∃ B; ∃ C; do 2 (split; Between).
apply outer_transitivity_between with A; eBetween;
try (intro; treat_equalities; intuition).
}
}
}
Defined.
End Independent_Tarski_2D_euclidean_to_Tarski_2D_euclidean.