Library GeoCoq.Meta_theory.Models.tarski_to_euclid
Require Import GeoCoq.Tarski_dev.Ch12_parallel.
Require Import GeoCoq.Axioms.euclidean_axioms.
Require Export GeoCoq.Axioms.continuity_axioms.
Require Export GeoCoq.Meta_theory.Continuity.elementary_continuity_props.
Require Export GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.
Section Tarski_neutral_to_Euclid_neutral.
Context `{TE:Tarski_neutral_dimensionless_with_decidable_point_equality}.
Definition Tcircle : Type := Tpoint×Tpoint×Tpoint %type.
Definition OnCirc P (C:Tcircle) :=
match C with
(X,A,B) ⇒ tarski_axioms.Cong X P A B
end.
Definition CI (J:Tcircle) A C D := J=(A,C,D).
Definition InCirc P (J:Tcircle) :=
match J with
(C,A,B) ⇒
∃ X Y, Definitions.BetS X C Y ∧ tarski_axioms.Cong C Y A B ∧
tarski_axioms.Cong C X A B ∧ Definitions.BetS X P Y
end.
Definition OutCirc P (J:Tcircle) :=
match J with
(C,A,B) ⇒
∃ X, Definitions.BetS C X P ∧ tarski_axioms.Cong C X A B
end.
Lemma on :
∀ A B C D J, CI J A C D ∧ OnCirc B J ↔
CI J A C D ∧ tarski_axioms.Cong A B C D.
Proof.
intros.
unfold CI,OnCirc.
destruct J.
destruct p.
split;intros;spliter;
split;congruence.
Qed.
Lemma inside : ∀ A B C J P,
CI J C A B ∧ InCirc P J ↔
∃ X Y, CI J C A B ∧
Definitions.BetS X C Y ∧
tarski_axioms.Cong C Y A B ∧
tarski_axioms.Cong C X A B ∧
Definitions.BetS X P Y.
Proof.
intros.
unfold InCirc, CI.
destruct J;destruct p.
split.
intros;spliter.
decompose [ex and] H0;clear H0.
∃ x. ∃ x0.
inversion H; subst; auto.
intros.
decompose [ex and] H;clear H.
inversion H0; subst;split; auto.
∃ x; ∃ x0;auto.
Qed.
Lemma outside : ∀ A B C J P,
CI J C A B ∧ OutCirc P J ↔
∃ X, CI J C A B ∧ Definitions.BetS C X P ∧
tarski_axioms.Cong C X A B.
Proof.
intros.
unfold OutCirc, CI.
destruct J;destruct p.
split.
intros;spliter.
decompose [ex and] H0;clear H0.
∃ x.
inversion H; subst; auto.
intros.
decompose [ex and] H;clear H.
inversion H1; subst;split; auto.
∃ x;auto.
Qed.
End Tarski_neutral_to_Euclid_neutral.
Section circle_continuity.
Context `{T2D : Tarski_2D_euclidean}.
Lemma bet_cases : ∀ B C D1 D2,
C≠B →
Definitions.BetS D1 B D2 →
Definitions.BetS D1 C D2 →
Definitions.BetS D1 B C ∨ Definitions.BetS C B D2.
Proof.
intros.
assert (T:Bet D1 C B ∨ Bet D1 B C).
apply (l5_3 D1 C B D2);unfold Definitions.BetS in *;spliter;finish.
destruct T.
right.
unfold Definitions.BetS in *;spliter.
assert (Bet C B D2)
by (eBetween).
unfold Definitions.BetS.
repeat split;auto.
left.
unfold Definitions.BetS.
unfold Definitions.BetS in *;spliter;repeat split;auto.
Qed.
Lemma circle_line :
circle_circle →
∀ A B C K P Q,
CI K C P Q → InCirc B K → A ≠ B →
∃ X Y, Definitions.Col A B X ∧ Definitions.Col A B Y ∧
OnCirc X K ∧ OnCirc Y K ∧ Definitions.BetS X B Y.
Proof.
intros.
apply circle_circle__circle_circle_bis in H.
apply circle_circle_bis__one_point_line_circle in H.
apply one_point_line_circle__two_points_line_circle in H.
unfold CI in ×.
destruct K.
destruct p.
injection H0.
intros;subst.
unfold InCirc in ×.
unfold two_points_line_circle in H.
destruct H1 as [D1 [D2 [HBetS [HCongA [HCongB HBetSB]]]]].
destruct (eq_dec_points B C).
subst.
assert (HColD: Definitions.Col A C C)
by (unfold Definitions.Col;Between).
assert (HBet: Bet C C D2) by Between.
destruct (H C D2 A C C HColD H2 HBet) as [Z1 [Z2 HZ]].
spliter.
∃ Z1. ∃ Z2.
repeat split;try assumption.
unfold OnCircle, OnCirc in *;eCong.
unfold OnCircle, OnCirc in *;eCong.
assert (C≠D2)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
unfold OnCircle in ×.
intro;treat_equalities;intuition.
unfold OnCircle in ×.
intro;treat_equalities.
unfold Definitions.BetS in *;intuition.
assert (TwoCases:Definitions.BetS D1 B C ∨ Definitions.BetS C B D2)
by (apply bet_cases;auto).
destruct TwoCases.
- assert (HColD: Definitions.Col A B B)
by (unfold Definitions.Col;Between).
assert (HBet:Bet C B D1)
by (unfold Definitions.BetS in *;spliter;finish).
destruct (H C D1 A B B HColD H2 HBet)
as [Z1 [Z2 HZ]].
∃ Z1.
∃ Z2.
spliter.
assert (B≠D1)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
assert (Z1≠B).
{
intro. subst.
unfold OnCircle in ×.
assert (B=D1) by (apply between_cong with C;finish).
subst. intuition.
}
assert_diffs.
assert (B≠Z2).
{
intro. subst.
assert (Bet C Z2 D1)
by (unfold BetS in *;spliter;finish).
unfold OnCircle in ×.
assert (Z2=D1)
by (apply between_cong with C;finish).
intuition.
}
assert (Definitions.BetS Z1 B Z2)
by (unfold Definitions.BetS;auto).
unfold OnCirc;simpl.
unfold OnCircle in ×.
repeat split; eCong.
- assert (HColD: Definitions.Col A B B)
by (unfold Definitions.Col;Between).
assert (HBet:Bet C B D2)
by (unfold Definitions.BetS in *;spliter;finish).
destruct (H C D2 A B B HColD H2 HBet)
as [Z1 [Z2 HZ]].
∃ Z1.
∃ Z2.
spliter.
assert (B≠D2)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
assert (Z1≠B).
{
intro. subst.
unfold OnCircle in ×.
assert (B=D2) by (apply between_cong with C;finish).
subst. intuition.
}
assert_diffs.
assert (B≠Z2).
{
intro. subst.
assert (Bet C Z2 D2)
by (unfold BetS in *;spliter;finish).
unfold OnCircle in ×.
assert (Z2=D2)
by (apply between_cong with C;finish).
intuition.
}
assert (Definitions.BetS Z1 B Z2)
by (unfold Definitions.BetS;auto).
unfold OnCirc;simpl.
unfold OnCircle in ×.
repeat split; eCong.
Qed.
Lemma circle_circle:
circle_circle →
∀ C D F G J K P Q R S,
CI J C R S → InCirc P J →
OutCirc Q J → CI K D F G →
OnCirc P K → OnCirc Q K →
∃ X, OnCirc X J ∧ OnCirc X K.
Proof.
intros.
unfold circle_circle in H.
destruct J.
destruct p.
destruct K.
destruct p.
unfold CI in ×.
injection H0;intros;subst.
injection H3;intros;subst.
clear H0 H3.
unfold OnCirc in ×.
unfold InCirc in ×.
destruct H1 as [D1 [D2 HD]].
spliter.
unfold OutCirc in ×.
destruct H2 as [X HX].
spliter.
assert (OnCircle P D Q)
by (unfold OnCircle;eCong).
assert (OnCircle Q D Q)
by (unfold OnCircle;eCong).
assert (InCircle P C D1).
{
unfold InCircle.
destruct (eq_dec_points C P).
subst. apply le_trivial.
assert (TwoCases:Definitions.BetS D1 P C ∨ Definitions.BetS C P D2)
by (apply bet_cases;auto).
destruct TwoCases.
∃ P.
split; unfold Definitions.BetS in *;spliter; finish.
apply l5_6 with C P C D2.
∃ P.
split; unfold Definitions.BetS in *;spliter; finish.
finish.
eCong.
}
assert (OutCircle Q C D1).
{
unfold OutCircle.
∃ X.
split; unfold Definitions.BetS in *;spliter; eCong.
}
assert (Hex: ∃ Z : Tpoint, OnCircle Z C D1 ∧ OnCircle Z D Q) by eauto.
destruct Hex as [Z HZ].
∃ Z.
unfold OnCircle in *;spliter;split;eCong.
Qed.
End circle_continuity.
Section Neutral.
Context `{TE:Tarski_neutral_dimensionless_with_decidable_point_equality}.
Instance Euclid_neutral_follows_from_Tarski_neutral : euclidean_neutral.
Proof.
eapply (Build_euclidean_neutral Tpoint Tcircle tarski_axioms.Cong Tarski_dev.Definitions.BetS InCirc OnCirc OutCirc tarski_axioms.PA tarski_axioms.PB tarski_axioms.PC CI).
- intros;congruence.
- intros;apply cong_transitivity with P Q;finish.
- intro;reflexivity.
- intro;finish.
- intro;finish.
- intros. elim (eq_dec_points A B);intuition.
- intros;subst;assumption.
- intros;∃ (C,A,B);reflexivity.
- intros; apply inside.
- intros; apply outside.
- intros. apply on.
- assert (T:=lower_dim).
split.
intro H;rewrite H in *;apply T;Between.
split.
intro H;rewrite H in *;apply T;Between.
split.
intro H;rewrite H in *;apply T;Between.
split.
unfold Definitions.BetS in *;intuition.
unfold Definitions.BetS in *;intuition.
- intros; unfold Definitions.BetS;
intro;spliter;treat_equalities;intuition.
- intros;unfold Definitions.BetS in *;
intros;spliter;finish.
- intros;unfold Definitions.BetS in *;
intros;spliter;try assumption;eBetween.
- intros;unfold Definitions.BetS in *;
intros;spliter .
assert (Bet A B C ∨ Bet A C B) by (apply l5_3 with D;auto).
assert (¬ (Bet A C B ∧ A ≠ C ∧ B ≠ C)) by intuition.
assert (T3:=eq_dec_points A B).
assert (T4:=eq_dec_points A C).
assert (T5:=eq_dec_points B C).
tauto.
- intros;treat_equalities;finish.
- intros;finish.
- intros.
assert (tarski_axioms.Cong C D c d)
by (apply (five_segment A a B b C c D d);
unfold Definitions.BetS in *;spliter;auto).
finish.
- intros.
destruct (segment_construction A B C D) as [X [HXa HXb]].
∃ X; split;unfold Definitions.BetS;assert_diffs;auto.
- intros.
destruct (segment_construction A B C D) as [X [HXa HXb]].
∃ X;unfold Definitions.BetS;intuition.
- intros;unfold Definitions.BetS in *;spliter.
destruct (inner_pasch A B C P Q H H0) as [X [HXa HXb]].
∃ X.
assert_diffs.
assert (¬ Bet A C B) by tauto.
assert (B≠C) by auto.
assert (¬ Bet A B C) by tauto.
assert (C≠A) by auto.
assert (¬ Bet C A B) by tauto.
assert (¬ Bet B C A) by Between.
repeat split;Between.
all:intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A B C) by ColR;
unfold Definitions.Col in HCol;
tauto.
- intros;unfold Definitions.BetS in *;spliter.
assert (¬ Bet B Q A) by tauto.
assert (A≠Q) by auto.
assert (¬ Bet B A Q) by tauto.
assert (B≠A) by auto.
assert (Q≠B) by auto.
assert (¬ Bet Q B A) by tauto.
assert (¬ Bet A Q B) by finish.
assert (Bet Q C B) by finish.
destruct (outer_pasch Q A C B P H18 H) as [X [HXa HXb]].
∃ X.
assert_diffs.
repeat split;Between.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col B A Q) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col B A X) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A Q B) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A Q B) by ColR;
unfold Definitions.Col in HCol;tauto.
Defined.
End Neutral.
Section RulerAndCompass.
Context `{T2D : Tarski_2D_euclidean}.
Instance En :euclidean_neutral.
Proof.
apply Euclid_neutral_follows_from_Tarski_neutral.
Defined.
Lemma BetS_BetS : ∀ A B C,
Definitions.BetS A B C ↔ BetS A B C.
Proof.
intros.
unfold BetS;simpl.
intuition.
Qed.
Lemma Col_Col : ∀ A B C,
Definitions.Col A B C ↔ Col A B C.
Proof.
intros.
unfold Definitions.Col, Col, BetS.
simpl.
unfold Definitions.BetS,eq.
split.
intros.
destruct (eq_dec_points A B).
left;auto.
destruct (eq_dec_points A C).
right;left;auto.
destruct (eq_dec_points B C).
right;right;left;auto.
decompose [or] H.
right;right;right;right;left;auto.
right;right;right;right;right;finish.
right;right;right;left;finish.
intros.
decompose [or] H;subst;spliter;finish.
Qed.
Lemma nCol_not_Col : ∀ A B C,
nCol A B C → ¬ Col A B C.
Proof.
unfold nCol.
unfold Col.
intuition.
Qed.
Lemma Euclid5 :
∀ a p q r s t,
BetS r t s → BetS p t q → BetS r a q →
Cong p t q t → Cong t r t s → nCol p q s →
∃ X, BetS p a X ∧ BetS s q X.
Proof.
intros.
assert (T:tarski_s_parallel_postulate →
euclid_5).
{
assert (T:=equivalent_postulates_without_decidability_of_intersection_of_lines_bis).
unfold all_equiv.all_equiv in ×.
apply T;simpl;auto 10.
}
assert (T2:euclid_5).
apply T.
unfold tarski_s_parallel_postulate.
apply euclid.
unfold euclid_5 in ×.
assert (T3:∃ I : Tpoint, Definitions.BetS s q I ∧ Definitions.BetS p a I).
apply (T2 p q r s t a);
auto using BetS_BetS.
unfold BetS in *;simpl in *;
unfold Definitions.BetS in *;spliter;finish.
intro HnCol.
apply Col_Col in HnCol.
apply nCol_not_Col in H4;intuition.
finish.
destruct T3 as [X HX].
∃ X;spliter;auto.
Qed.
Lemma Euclid_neutral_ruler_compass_follows_from_Tarski_2D :
continuity_axioms.circle_circle →
(euclidean_neutral_ruler_compass En).
Proof.
intros.
split.
-simpl.
intros.
destruct (circle_line H A B C K P Q H0 H1 H2)
as [X [Y HXY]].
spliter.
∃ X.
∃ Y.
split.
apply (Col_Col A B X);auto.
split.
apply (Col_Col A B Y);auto.
auto.
- simpl.
eauto using circle_circle.
Qed.
Lemma Euclid_follows_from_Tarski_2D :
∀ (H:continuity_axioms.circle_circle),
euclidean_euclidean (Euclid_neutral_ruler_compass_follows_from_Tarski_2D H) .
Proof.
intros.
split.
apply Euclid5.
Qed.
End RulerAndCompass.
Require Import GeoCoq.Axioms.euclidean_axioms.
Require Export GeoCoq.Axioms.continuity_axioms.
Require Export GeoCoq.Meta_theory.Continuity.elementary_continuity_props.
Require Export GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.
Section Tarski_neutral_to_Euclid_neutral.
Context `{TE:Tarski_neutral_dimensionless_with_decidable_point_equality}.
Definition Tcircle : Type := Tpoint×Tpoint×Tpoint %type.
Definition OnCirc P (C:Tcircle) :=
match C with
(X,A,B) ⇒ tarski_axioms.Cong X P A B
end.
Definition CI (J:Tcircle) A C D := J=(A,C,D).
Definition InCirc P (J:Tcircle) :=
match J with
(C,A,B) ⇒
∃ X Y, Definitions.BetS X C Y ∧ tarski_axioms.Cong C Y A B ∧
tarski_axioms.Cong C X A B ∧ Definitions.BetS X P Y
end.
Definition OutCirc P (J:Tcircle) :=
match J with
(C,A,B) ⇒
∃ X, Definitions.BetS C X P ∧ tarski_axioms.Cong C X A B
end.
Lemma on :
∀ A B C D J, CI J A C D ∧ OnCirc B J ↔
CI J A C D ∧ tarski_axioms.Cong A B C D.
Proof.
intros.
unfold CI,OnCirc.
destruct J.
destruct p.
split;intros;spliter;
split;congruence.
Qed.
Lemma inside : ∀ A B C J P,
CI J C A B ∧ InCirc P J ↔
∃ X Y, CI J C A B ∧
Definitions.BetS X C Y ∧
tarski_axioms.Cong C Y A B ∧
tarski_axioms.Cong C X A B ∧
Definitions.BetS X P Y.
Proof.
intros.
unfold InCirc, CI.
destruct J;destruct p.
split.
intros;spliter.
decompose [ex and] H0;clear H0.
∃ x. ∃ x0.
inversion H; subst; auto.
intros.
decompose [ex and] H;clear H.
inversion H0; subst;split; auto.
∃ x; ∃ x0;auto.
Qed.
Lemma outside : ∀ A B C J P,
CI J C A B ∧ OutCirc P J ↔
∃ X, CI J C A B ∧ Definitions.BetS C X P ∧
tarski_axioms.Cong C X A B.
Proof.
intros.
unfold OutCirc, CI.
destruct J;destruct p.
split.
intros;spliter.
decompose [ex and] H0;clear H0.
∃ x.
inversion H; subst; auto.
intros.
decompose [ex and] H;clear H.
inversion H1; subst;split; auto.
∃ x;auto.
Qed.
End Tarski_neutral_to_Euclid_neutral.
Section circle_continuity.
Context `{T2D : Tarski_2D_euclidean}.
Lemma bet_cases : ∀ B C D1 D2,
C≠B →
Definitions.BetS D1 B D2 →
Definitions.BetS D1 C D2 →
Definitions.BetS D1 B C ∨ Definitions.BetS C B D2.
Proof.
intros.
assert (T:Bet D1 C B ∨ Bet D1 B C).
apply (l5_3 D1 C B D2);unfold Definitions.BetS in *;spliter;finish.
destruct T.
right.
unfold Definitions.BetS in *;spliter.
assert (Bet C B D2)
by (eBetween).
unfold Definitions.BetS.
repeat split;auto.
left.
unfold Definitions.BetS.
unfold Definitions.BetS in *;spliter;repeat split;auto.
Qed.
Lemma circle_line :
circle_circle →
∀ A B C K P Q,
CI K C P Q → InCirc B K → A ≠ B →
∃ X Y, Definitions.Col A B X ∧ Definitions.Col A B Y ∧
OnCirc X K ∧ OnCirc Y K ∧ Definitions.BetS X B Y.
Proof.
intros.
apply circle_circle__circle_circle_bis in H.
apply circle_circle_bis__one_point_line_circle in H.
apply one_point_line_circle__two_points_line_circle in H.
unfold CI in ×.
destruct K.
destruct p.
injection H0.
intros;subst.
unfold InCirc in ×.
unfold two_points_line_circle in H.
destruct H1 as [D1 [D2 [HBetS [HCongA [HCongB HBetSB]]]]].
destruct (eq_dec_points B C).
subst.
assert (HColD: Definitions.Col A C C)
by (unfold Definitions.Col;Between).
assert (HBet: Bet C C D2) by Between.
destruct (H C D2 A C C HColD H2 HBet) as [Z1 [Z2 HZ]].
spliter.
∃ Z1. ∃ Z2.
repeat split;try assumption.
unfold OnCircle, OnCirc in *;eCong.
unfold OnCircle, OnCirc in *;eCong.
assert (C≠D2)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
unfold OnCircle in ×.
intro;treat_equalities;intuition.
unfold OnCircle in ×.
intro;treat_equalities.
unfold Definitions.BetS in *;intuition.
assert (TwoCases:Definitions.BetS D1 B C ∨ Definitions.BetS C B D2)
by (apply bet_cases;auto).
destruct TwoCases.
- assert (HColD: Definitions.Col A B B)
by (unfold Definitions.Col;Between).
assert (HBet:Bet C B D1)
by (unfold Definitions.BetS in *;spliter;finish).
destruct (H C D1 A B B HColD H2 HBet)
as [Z1 [Z2 HZ]].
∃ Z1.
∃ Z2.
spliter.
assert (B≠D1)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
assert (Z1≠B).
{
intro. subst.
unfold OnCircle in ×.
assert (B=D1) by (apply between_cong with C;finish).
subst. intuition.
}
assert_diffs.
assert (B≠Z2).
{
intro. subst.
assert (Bet C Z2 D1)
by (unfold BetS in *;spliter;finish).
unfold OnCircle in ×.
assert (Z2=D1)
by (apply between_cong with C;finish).
intuition.
}
assert (Definitions.BetS Z1 B Z2)
by (unfold Definitions.BetS;auto).
unfold OnCirc;simpl.
unfold OnCircle in ×.
repeat split; eCong.
- assert (HColD: Definitions.Col A B B)
by (unfold Definitions.Col;Between).
assert (HBet:Bet C B D2)
by (unfold Definitions.BetS in *;spliter;finish).
destruct (H C D2 A B B HColD H2 HBet)
as [Z1 [Z2 HZ]].
∃ Z1.
∃ Z2.
spliter.
assert (B≠D2)
by (unfold Definitions.BetS in *;spliter;auto).
assert (Z1≠Z2) by auto.
assert (Z1≠B).
{
intro. subst.
unfold OnCircle in ×.
assert (B=D2) by (apply between_cong with C;finish).
subst. intuition.
}
assert_diffs.
assert (B≠Z2).
{
intro. subst.
assert (Bet C Z2 D2)
by (unfold BetS in *;spliter;finish).
unfold OnCircle in ×.
assert (Z2=D2)
by (apply between_cong with C;finish).
intuition.
}
assert (Definitions.BetS Z1 B Z2)
by (unfold Definitions.BetS;auto).
unfold OnCirc;simpl.
unfold OnCircle in ×.
repeat split; eCong.
Qed.
Lemma circle_circle:
circle_circle →
∀ C D F G J K P Q R S,
CI J C R S → InCirc P J →
OutCirc Q J → CI K D F G →
OnCirc P K → OnCirc Q K →
∃ X, OnCirc X J ∧ OnCirc X K.
Proof.
intros.
unfold circle_circle in H.
destruct J.
destruct p.
destruct K.
destruct p.
unfold CI in ×.
injection H0;intros;subst.
injection H3;intros;subst.
clear H0 H3.
unfold OnCirc in ×.
unfold InCirc in ×.
destruct H1 as [D1 [D2 HD]].
spliter.
unfold OutCirc in ×.
destruct H2 as [X HX].
spliter.
assert (OnCircle P D Q)
by (unfold OnCircle;eCong).
assert (OnCircle Q D Q)
by (unfold OnCircle;eCong).
assert (InCircle P C D1).
{
unfold InCircle.
destruct (eq_dec_points C P).
subst. apply le_trivial.
assert (TwoCases:Definitions.BetS D1 P C ∨ Definitions.BetS C P D2)
by (apply bet_cases;auto).
destruct TwoCases.
∃ P.
split; unfold Definitions.BetS in *;spliter; finish.
apply l5_6 with C P C D2.
∃ P.
split; unfold Definitions.BetS in *;spliter; finish.
finish.
eCong.
}
assert (OutCircle Q C D1).
{
unfold OutCircle.
∃ X.
split; unfold Definitions.BetS in *;spliter; eCong.
}
assert (Hex: ∃ Z : Tpoint, OnCircle Z C D1 ∧ OnCircle Z D Q) by eauto.
destruct Hex as [Z HZ].
∃ Z.
unfold OnCircle in *;spliter;split;eCong.
Qed.
End circle_continuity.
Section Neutral.
Context `{TE:Tarski_neutral_dimensionless_with_decidable_point_equality}.
Instance Euclid_neutral_follows_from_Tarski_neutral : euclidean_neutral.
Proof.
eapply (Build_euclidean_neutral Tpoint Tcircle tarski_axioms.Cong Tarski_dev.Definitions.BetS InCirc OnCirc OutCirc tarski_axioms.PA tarski_axioms.PB tarski_axioms.PC CI).
- intros;congruence.
- intros;apply cong_transitivity with P Q;finish.
- intro;reflexivity.
- intro;finish.
- intro;finish.
- intros. elim (eq_dec_points A B);intuition.
- intros;subst;assumption.
- intros;∃ (C,A,B);reflexivity.
- intros; apply inside.
- intros; apply outside.
- intros. apply on.
- assert (T:=lower_dim).
split.
intro H;rewrite H in *;apply T;Between.
split.
intro H;rewrite H in *;apply T;Between.
split.
intro H;rewrite H in *;apply T;Between.
split.
unfold Definitions.BetS in *;intuition.
unfold Definitions.BetS in *;intuition.
- intros; unfold Definitions.BetS;
intro;spliter;treat_equalities;intuition.
- intros;unfold Definitions.BetS in *;
intros;spliter;finish.
- intros;unfold Definitions.BetS in *;
intros;spliter;try assumption;eBetween.
- intros;unfold Definitions.BetS in *;
intros;spliter .
assert (Bet A B C ∨ Bet A C B) by (apply l5_3 with D;auto).
assert (¬ (Bet A C B ∧ A ≠ C ∧ B ≠ C)) by intuition.
assert (T3:=eq_dec_points A B).
assert (T4:=eq_dec_points A C).
assert (T5:=eq_dec_points B C).
tauto.
- intros;treat_equalities;finish.
- intros;finish.
- intros.
assert (tarski_axioms.Cong C D c d)
by (apply (five_segment A a B b C c D d);
unfold Definitions.BetS in *;spliter;auto).
finish.
- intros.
destruct (segment_construction A B C D) as [X [HXa HXb]].
∃ X; split;unfold Definitions.BetS;assert_diffs;auto.
- intros.
destruct (segment_construction A B C D) as [X [HXa HXb]].
∃ X;unfold Definitions.BetS;intuition.
- intros;unfold Definitions.BetS in *;spliter.
destruct (inner_pasch A B C P Q H H0) as [X [HXa HXb]].
∃ X.
assert_diffs.
assert (¬ Bet A C B) by tauto.
assert (B≠C) by auto.
assert (¬ Bet A B C) by tauto.
assert (C≠A) by auto.
assert (¬ Bet C A B) by tauto.
assert (¬ Bet B C A) by Between.
repeat split;Between.
all:intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A B C) by ColR;
unfold Definitions.Col in HCol;
tauto.
- intros;unfold Definitions.BetS in *;spliter.
assert (¬ Bet B Q A) by tauto.
assert (A≠Q) by auto.
assert (¬ Bet B A Q) by tauto.
assert (B≠A) by auto.
assert (Q≠B) by auto.
assert (¬ Bet Q B A) by tauto.
assert (¬ Bet A Q B) by finish.
assert (Bet Q C B) by finish.
destruct (outer_pasch Q A C B P H18 H) as [X [HXa HXb]].
∃ X.
assert_diffs.
repeat split;Between.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col B A Q) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col B A X) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A Q B) by ColR;
unfold Definitions.Col in HCol;tauto.
intro;treat_equalities;assert_cols;
assert (HCol:Definitions.Col A Q B) by ColR;
unfold Definitions.Col in HCol;tauto.
Defined.
End Neutral.
Section RulerAndCompass.
Context `{T2D : Tarski_2D_euclidean}.
Instance En :euclidean_neutral.
Proof.
apply Euclid_neutral_follows_from_Tarski_neutral.
Defined.
Lemma BetS_BetS : ∀ A B C,
Definitions.BetS A B C ↔ BetS A B C.
Proof.
intros.
unfold BetS;simpl.
intuition.
Qed.
Lemma Col_Col : ∀ A B C,
Definitions.Col A B C ↔ Col A B C.
Proof.
intros.
unfold Definitions.Col, Col, BetS.
simpl.
unfold Definitions.BetS,eq.
split.
intros.
destruct (eq_dec_points A B).
left;auto.
destruct (eq_dec_points A C).
right;left;auto.
destruct (eq_dec_points B C).
right;right;left;auto.
decompose [or] H.
right;right;right;right;left;auto.
right;right;right;right;right;finish.
right;right;right;left;finish.
intros.
decompose [or] H;subst;spliter;finish.
Qed.
Lemma nCol_not_Col : ∀ A B C,
nCol A B C → ¬ Col A B C.
Proof.
unfold nCol.
unfold Col.
intuition.
Qed.
Lemma Euclid5 :
∀ a p q r s t,
BetS r t s → BetS p t q → BetS r a q →
Cong p t q t → Cong t r t s → nCol p q s →
∃ X, BetS p a X ∧ BetS s q X.
Proof.
intros.
assert (T:tarski_s_parallel_postulate →
euclid_5).
{
assert (T:=equivalent_postulates_without_decidability_of_intersection_of_lines_bis).
unfold all_equiv.all_equiv in ×.
apply T;simpl;auto 10.
}
assert (T2:euclid_5).
apply T.
unfold tarski_s_parallel_postulate.
apply euclid.
unfold euclid_5 in ×.
assert (T3:∃ I : Tpoint, Definitions.BetS s q I ∧ Definitions.BetS p a I).
apply (T2 p q r s t a);
auto using BetS_BetS.
unfold BetS in *;simpl in *;
unfold Definitions.BetS in *;spliter;finish.
intro HnCol.
apply Col_Col in HnCol.
apply nCol_not_Col in H4;intuition.
finish.
destruct T3 as [X HX].
∃ X;spliter;auto.
Qed.
Lemma Euclid_neutral_ruler_compass_follows_from_Tarski_2D :
continuity_axioms.circle_circle →
(euclidean_neutral_ruler_compass En).
Proof.
intros.
split.
-simpl.
intros.
destruct (circle_line H A B C K P Q H0 H1 H2)
as [X [Y HXY]].
spliter.
∃ X.
∃ Y.
split.
apply (Col_Col A B X);auto.
split.
apply (Col_Col A B Y);auto.
auto.
- simpl.
eauto using circle_circle.
Qed.
Lemma Euclid_follows_from_Tarski_2D :
∀ (H:continuity_axioms.circle_circle),
euclidean_euclidean (Euclid_neutral_ruler_compass_follows_from_Tarski_2D H) .
Proof.
intros.
split.
apply Euclid5.
Qed.
End RulerAndCompass.