Library GeoCoq.Meta_theory.Models.tarski_to_hilbert

Require Import GeoCoq.Tarski_dev.Ch12_parallel_inter_dec.
Require Import Morphisms.
Require Import GeoCoq.Axioms.hilbert_axioms.

Section T.

Context `{TE:Tarski_2D_euclidean}.

We need a notion of line.

Definition Line := @Couple Tpoint.
Definition Lin := build_couple Tpoint.

Definition Incident (A : Tpoint) (l : Line) := Col A (P1 l) (P2 l).

Group I Combination

For every pair of distinct points there is a line containing them.

Lemma axiom_line_existence : A B, AB l, Incident A l Incident B l.
Proof.
intros.
(Lin A B H).
unfold Incident.
intuition.
Qed.

We need a notion of equality over lines.

Definition Eq : relation Line := fun l m X, Incident X l Incident X m.

Infix "=l=" := Eq (at level 70):type_scope.

Lemma incident_eq : A B l, H : AB,
 Incident A l Incident B l
 (Lin A B H) =l= l.
Proof.
intros.
unfold Eq.
intros.
unfold Incident in ×.
replace (P1 (Lin A B H)) with A.
replace (P2 (Lin A B H)) with B.
2:auto.
2:auto.
split;intro.
assert (T:=Cond l).
elim (eq_dec_points X B); intro.
subst X.
auto.
assert (Col (P1 l) A B).
eapply col_transitivity_1;try apply T;Col.
assert (Col (P2 l) A B) by eCol.
assert (Col B (P2 l) X).
eCol.
assert (Col B (P1 l) X).
eCol.
eapply col_transitivity_2.
assert (BX) by auto.
apply H8.
Col.
Col.

assert (U:=Cond l).
elim (eq_dec_points X (P1 l)); intro.
smart_subst X.
eCol.

assert (Col (P1 l) X A).
eCol.
assert (Col (P1 l) X B).
eCol.
eapply col_transitivity_1.
apply H3.
Col.
Col.
Qed.

Our equality is an equivalence relation.

Lemma eq_transitivity : l m n, l =l= m m =l= n l =l= n.
Proof.
unfold Eq,Incident.
intros.
assert (T:=H X).
assert (V:= H0 X).
split;intro;intuition.
Qed.

Lemma eq_reflexivity : l, l =l= l.
Proof.
intros.
unfold Eq.
intuition.
Qed.

Lemma eq_symmetry : l m, l =l= m m =l= l.
unfold Eq.
intros.
assert (T:=H X).
intuition.
Qed.

Instance Eq_Equiv : Equivalence Eq.
Proof.
split.
unfold Reflexive.
apply eq_reflexivity.
unfold Symmetric.
apply eq_symmetry.
unfold Transitive.
apply eq_transitivity.
Qed.

The equality is compatible with Incident

Lemma eq_incident : A l m, l =l= m
 (Incident A l Incident A m).
Proof.
intros.
split;intros;
unfold Eq in *;
assert (T:= H A);
intuition.
Qed.

Instance incident_Proper (A:Tpoint) :
Proper (Eq ==>iff) (Incident A).
intros a b H .
apply eq_incident.
assumption.
Qed.

Lemma axiom_Incid_morphism :
  P l m, Incident P l Eq l m Incident P m.
Proof.
intros.
destruct (eq_incident P l m H0).
intuition.
Qed.

Lemma axiom_Incid_dec : P l, Incident P l ¬Incident P l.
Proof.
intros.
unfold Incident.
apply Col_dec.
Qed.

There is only one line going through two points.
Lemma axiom_line_uniqueness : A B l m, A B
 (Incident A l) (Incident B l) (Incident A m) (Incident B m)
 l =l= m.
Proof.
intros.
assert ((Lin A B H) =l= l).
eapply incident_eq;assumption.
assert ((Lin A B H) =l= m).
eapply incident_eq;assumption.
rewrite <- H4.
assumption.
Qed.

Every line contains at least two points.

Lemma axiom_two_points_on_line : l,
  { A : Tpoint & { B | Incident B l Incident A l A B}}.
Proof.
intros.
(P1 l).
(P2 l).
unfold Incident.
repeat split;Col.
exact (Cond l).
Qed.

Definition of the collinearity predicate. We say that three points are collinear if they belongs to the same line.

Definition Col_H := fun A B C
   l, Incident A l Incident B l Incident C l.

We show that the notion of collinearity we just defined is equivalent to the notion of collinearity of Tarski.

Lemma cols_coincide_1 : A B C, Col_H A B C Col A B C.
Proof.
intros.
unfold Col_H in H.
DecompExAnd H l.
unfold Incident in ×.
assert (T:=Cond l).
assert (Col (P1 l) A B).
eapply col_transitivity_1;try apply T;Col.
assert (Col (P1 l) A C).
eapply col_transitivity_1;try apply T;Col.
elim (eq_dec_points (P1 l) A); intro.
smart_subst A.
eapply col_transitivity_1;try apply T;Col.
eapply col_transitivity_2;try apply H2;Col.
Qed.

Lemma cols_coincide_2 : A B C, Col A B C Col_H A B C.
Proof.
intros.
unfold Col_H.
elim (eq_dec_points A B); intro.
subst B.
elim (eq_dec_points A C); intro.
subst C.
assert ( B, AB).
eapply another_point.
DecompEx H0 B.
(Lin A B H1).
unfold Incident;intuition.
(Lin A C H0).
unfold Incident;intuition.
(Lin A B H0).
unfold Incident;intuition.
Qed.

Lemma cols_coincide : A B C, Col A B C Col_H A B C.
Proof.
intros.
split.
apply cols_coincide_2.
apply cols_coincide_1.
Qed.

There exists three non collinear points.

Lemma axiom_plan : l, P, ¬ Incident P l.
Proof.
assert (T:=lower_dim_ex).
DecompEx T A.
DecompEx H B.
DecompEx H0 C.
assert (¬ Col A B C) by auto.
assert_diffs.
(Lin A B H4).
C.
unfold Incident.
simpl.
Col.
Qed.

Lemma axiom_plan' :
  A , B, C, ¬ Col_H A B C.
Proof.
assert (T:=lower_dim_ex).
DecompEx T A.
DecompEx H B.
DecompEx H0 C.
assert (¬ Col_H A B C).
unfold not;intro.
assert (Col A B C).
apply cols_coincide_1.
auto.
intuition.

A.
B.
C.
auto.
Qed.

Group II Order

Definition of the Between predicate of Hilbert. Note that it is different from the Between of Tarski. The Between of Hilbert is strict.

Definition Between_H A B C :=
  Bet A B C A B B C A C.

Lemma axiom_between_col :
  A B C, Between_H A B C Col_H A B C.
Proof.
intros.
unfold Col_H, Between_H in ×.
DecompAndAll.
(Lin A B H2).
unfold Incident.
intuition.
Qed.

Lemma axiom_between_diff :
  A B C, Between_H A B C AC.
Proof.
intros.
unfold Between_H in ×.
intuition.
Qed.

If B is between A and C, it is also between C and A.

Lemma axiom_between_comm : A B C, Between_H A B C Between_H C B A.
Proof.
unfold Between_H in |- ×.
intros.
intuition.
Qed.

Lemma axiom_between_out :
  A B, A B C, Between_H A B C.
Proof.
intros.
prolong A B C A B.
C.
unfold Between_H.
repeat split;
auto;
intro;
treat_equalities;
tauto.
Qed.

Lemma axiom_between_only_one :
  A B C,
 Between_H A B C ¬ Between_H B C A.
Proof.
unfold Between_H in |- ×.
intros.
intro;
spliter.
assert (B=C) by
 (apply (between_equality B C A);Between).
solve [intuition].
Qed.

Lemma between_one : A B C,
 AB AC BC Col A B C
 Between_H A B C Between_H B C A Between_H B A C.
Proof.
intros.
unfold Col, Between_H in ×.
intuition.
Qed.

Lemma axiom_between_one : A B C,
 AB AC BC Col_H A B C
 Between_H A B C Between_H B C A Between_H B A C.
Proof.
intros.
apply between_one;try assumption.
apply cols_coincide_1.
assumption.
Qed.

Axiom of Pasch, (Hilbert version).
First we define a predicate which means that the line l intersects the segment AB.

Definition cut := fun l A B¬Incident A l ¬Incident B l I, Incident I l Between_H A I B.

We show that this definition is equivalent to the predicate TS of Tarski.

Lemma cut_two_sides : l A B, cut l A B TS (P1 l) (P2 l) A B.
Proof.
intros.
unfold cut.
unfold TS.
split.
intros.
spliter.
repeat split; intuition.
ex_and H1 T.
T.
unfold Incident in H1.
unfold Between_H in ×.
intuition.

intros.
spliter.
ex_and H1 T.
unfold Incident.
repeat split; try assumption.
T.
split.
assumption.
unfold Between_H.
repeat split.
assumption.
intro.
subst.
contradiction.
intro.
subst.
contradiction.
intro.
treat_equalities.
contradiction.
Qed.

Lemma axiom_pasch : A B C l,
 ¬ Col_H A B C ¬ Incident C l
 cut l A B cut l A C cut l B C.
Proof.
intros.
apply cut_two_sides in H1.
assert(¬Col A B C).
intro.
apply H.
apply cols_coincide_2.
assumption.

assert(HH:=H1).
unfold TS in HH.
spliter.

unfold Incident in H0.

assert(HH:= one_or_two_sides (P1 l)(P2 l) A C H3 H0 ).

induction HH.
left.
apply <-cut_two_sides.
assumption.
right.
apply <-cut_two_sides.
apply l9_2.
eapply l9_8_2.
apply H1.
assumption.
Qed.

Lemma Incid_line :
  P A B l, AB
 Incident A l Incident B l Col P A B Incident P l.
Proof.
intros.
unfold Incident in ×.
destruct l as [C D HCD].
simpl in ×.
assert (Col D A B) by eCol.
assert (Col C A B) by eCol.
assert (Col A D P) by eCol.
assert (Col A D C) by eCol.
elim (eq_dec_points A D); intro.
subst.
clear H3 H5 H6.
eCol.
eCol.
Qed.

Goup IV Congruence

The cong predicate of Hilbert is the same as the one of Tarski:

Definition Hcong:=Cong.

Definition outH := fun P A BBetween_H P A B Between_H P B A (P A A = B).

Lemma out_outH : P A B, Out P A B outH P A B.
unfold Out.
unfold outH.
intros.
spliter.
induction H1.

induction (eq_dec_points A B).
right; right.
split; auto.
left.
unfold Between_H.
repeat split; auto.

induction (eq_dec_points A B).
right; right.
split; auto.
right; left.
unfold Between_H.
repeat split; auto.
Qed.

Lemma axiom_hcong_1_existence : A B A' P l,
  A B A' P
  Incident A' l Incident P l
   B', Incident B' l outH A' P B' Hcong A' B' A B.
Proof.
intros; destruct (l6_11_existence A' A B P) as [B' [HOut HCong]]; auto.
B'; repeat split; try apply out_outH, l6_6; auto; unfold Incident in ×.
assert_cols; destruct l; simpl in *; ColR.
Qed.

Lemma axiom_hcong_1_uniqueness :
  A B l M A' B' A'' B'', A B Incident M l
  Incident A' l Incident B' l
  Incident A'' l Incident B'' l
  Between_H A' M B' Hcong M A' A B
  Hcong M B' A B Between_H A'' M B''
  Hcong M A'' A B Hcong M B'' A B
  (A' = A'' B' = B'') (A' = B'' B' = A'').
Proof.
unfold Hcong.
unfold Between_H.
unfold Incident.
intros.
spliter.

assert(A' M A'' M B' M B'' M A' B' A'' B'').
repeat split; intro; treat_equalities; tauto.
spliter.

induction(out_dec M A' A'').
left.
assert(A' = A'').
eapply (l6_11_uniqueness M A B A''); try assumption.
apply out_trivial.
assumption.

split.
assumption.
subst A''.

eapply (l6_11_uniqueness M A B B''); try assumption.

unfold Out.
repeat split; try assumption.
eapply l5_2.
apply H18.
assumption.
assumption.
apply out_trivial.
assumption.

right.
apply not_out_bet in H23.

assert(A' = B'').
eapply (l6_11_uniqueness M A B A'); try assumption.
apply out_trivial.
assumption.

unfold Out.
repeat split; try assumption.

eapply l5_2.
apply H18.
assumption.
apply between_symmetry.
assumption.

split.
assumption.

subst B''.
eapply (l6_11_uniqueness M A B B'); try assumption.
apply out_trivial.
assumption.
unfold Out.
repeat split; try assumption.
eapply l5_2.
apply H20.
apply between_symmetry.
assumption.
assumption.
eapply col3.
apply (Cond l).
Col.
Col.
Col.
Qed.

As a remark we also prove another version of this axiom as formalized in Isabelle by Phil Scott.

Definition same_side_scott E A B := E A E B Col_H E A B ¬ Between_H A E B.

Remark axiom_hcong_scott:
  P Q A C, A C P Q
   B, same_side_scott A B C Hcong P Q A B.
Proof.
intros.
unfold same_side_scott.
assert ( X : Tpoint, Out A X C Cong A X P Q).
apply l6_11_existence;auto.
decompose [ex and] H1;clear H1.
x.
repeat split.
unfold Out in H3.
intuition.
unfold Out in H3.
intuition.
apply cols_coincide_2.
apply out_col;assumption.

unfold Out in H3.
unfold Between_H.
intro.
decompose [and] H3;clear H3.
decompose [and] H1;clear H1.
clear H8.
destruct H7.
assert (A = x).
eapply between_equality;eauto.
intuition.
assert (A = C).
eapply between_equality;eauto.
apply between_symmetry.
auto.
intuition.
unfold Hcong.
Cong.
Qed.

Transivity of congruence.

Lemma axiom_hcong_trans : A B C D E F, Hcong A B C D Hcong A B E F Hcong C D E F.
Proof.
unfold Hcong.
intros.
apply cong_symmetry.
apply cong_symmetry in H0.
eapply cong_transitivity;eauto.
Qed.

Reflexivity of congruence.

Lemma axiom_hcong_refl : A B , Hcong A B A B.
Proof.
unfold Hcong.
intros.
Cong.
Qed.

We define when two segments do not intersect.

Definition disjoint := fun A B C D¬ P, Between_H A P B Between_H C P D.

Note that two disjoint segments may share one of their extremities.

Lemma col_disjoint_bet : A B C, Col_H A B C disjoint A B B C Bet A B C.
Proof.
intros.
apply cols_coincide_1 in H.
unfold disjoint in H0.

induction (eq_dec_points A B).
subst B.
apply between_trivial2.
induction (eq_dec_points B C).
subst C.
apply between_trivial.

unfold Col in H.
induction H.
assumption.

induction H.
apply False_ind.
apply H0.
assert( M, Midpoint M B C) by(apply midpoint_existence).
ex_and H3 M.
M.
unfold Midpoint in H4.
spliter.
split.
unfold Between_H.
repeat split.
apply between_symmetry.
eapply between_exchange4.
apply H3.
assumption.
intro.
treat_equalities.
tauto.
intro.
treat_equalities.
tauto.
assumption.
unfold Between_H.
repeat split.
assumption.
intro.
treat_equalities.
tauto.
intro.
treat_equalities.
tauto.
assumption.

apply False_ind.
apply H0.
assert( M, Midpoint M A B) by(apply midpoint_existence).
ex_and H3 M.
M.
unfold Midpoint in H4.
spliter.
split.
unfold Between_H.
repeat split.
assumption.
intro.
treat_equalities.
tauto.
intro.
treat_equalities.
tauto.
assumption.

unfold Between_H.
repeat split.

eapply between_exchange4.
apply between_symmetry.
apply H3.
apply between_symmetry.
assumption.
intro.
treat_equalities.
tauto.
intro.
treat_equalities.
intuition.
assumption.
Qed.

Lemma axiom_hcong_3 : A B C A' B' C',
   Col_H A B C Col_H A' B' C'
  disjoint A B B C disjoint A' B' B' C'
  Hcong A B A' B' Hcong B C B' C' Hcong A C A' C'.
Proof.
unfold Hcong.
intros.
assert(Bet A B C).
eapply col_disjoint_bet.
assumption.
assumption.

assert(Bet A' B' C').
eapply col_disjoint_bet.
assumption.
assumption.
eapply l2_11;eauto.
Qed.

Lemma exists_not_incident : A B : Tpoint, HH : A B , C, ¬ Incident C (Lin A B HH).
Proof.
intros.
unfold Incident.
assert(HC:=not_col_exists A B HH).
ex_and HC C.
C.
intro.
apply H.
simpl in H0.
Col.
Qed.

Definition same_side := fun A B l P, cut l A P cut l B P.

Same side predicate corresponds to OS of Tarski.

Lemma same_side_one_side : A B l, same_side A B l OS (P1 l) (P2 l) A B.
Proof.
unfold same_side.
intros.
ex_and H P.
apply cut_two_sides in H.
apply cut_two_sides in H0.
eapply l9_8_1.
apply H.
apply H0.
Qed.

Lemma one_side_same_side : A B l, OS (P1 l) (P2 l) A B same_side A B l.
Proof.
intros.
unfold same_side.
unfold OS in H.
ex_and H P.
P.
unfold cut.
unfold Incident.
unfold TS in H.
unfold TS in H0.
spliter.
repeat split; auto.
ex_and H4 T.
T.
unfold Between_H.
repeat split; auto.
intro.
subst T.
contradiction.
intro.
subst T.
contradiction.
intro.
subst P.
apply between_identity in H5.
subst T.
contradiction.
ex_and H2 T.
T.
unfold Between_H.
repeat split; auto.
intro.
subst T.
contradiction.
intro.
subst T.
contradiction.
intro.
subst P.
apply between_identity in H5.
subst T.
contradiction.
Qed.

Definition same_side' := fun A B X YXY l, Incident X l Incident Y l same_side A B l.

Lemma OS_distinct : P Q A B,
  OS P Q A B PQ.
Proof.
intros.
apply one_side_not_col123 in H.
assert_diffs;assumption.
Qed.

Lemma OS_same_side' :
  P Q A B, OS P Q A B same_side' A B P Q.
Proof.
intros.
unfold same_side'.
intros.
split.
apply OS_distinct with A B;assumption.
intros.

apply one_side_same_side.
destruct l.
unfold Incident in ×.
simpl in ×.
apply col2_os__os with P Q;try assumption;ColR.
Qed.

Lemma same_side_OS :
  P Q A B, same_side' P Q A B OS A B P Q.
Proof.
intros.
unfold same_side' in ×.
destruct H.
destruct (axiom_line_existence A B H).
destruct H1.
assert (T:=H0 x H1 H2).
assert (U:=same_side_one_side P Q x T).
destruct x.
unfold Incident in ×.
simpl in ×.
apply col2_os__os with P1 P2;Col.
Qed.

This is equivalent to the out predicate of Tarski.

Lemma outH_out : P A B, outH P A B Out P A B.
Proof.
unfold outH.
unfold Out.
intros.
induction H.
unfold Between_H in H.
spliter.
repeat split; auto.
induction H.
unfold Between_H in H.
spliter.
repeat split; auto.
spliter.
repeat split.
auto.
subst B.
auto.
subst B.
left.
apply between_trivial.
Qed.

The 2D version of the fourth congruence axiom

Lemma incident_col : M l, Incident M l Col M (P1 l)(P2 l).
Proof.
unfold Incident.
intros.
assumption.
Qed.

Lemma col_incident : M l, Col M (P1 l)(P2 l) Incident M l.
Proof.
unfold Incident.
intros.
assumption.
Qed.

Lemma Bet_Between_H : A B C,
 Bet A B C AB BC Between_H A B C.
Proof.
intros.
unfold Between_H.
repeat split;try assumption.
intro.
subst.
treat_equalities.
intuition.
Qed.

Lemma axiom_cong_5' : A B C A' B' C', ¬ Col_H A B C ¬ Col_H A' B' C'
           Hcong A B A' B' Hcong A C A' C' CongA B A C B' A' C' CongA A B C A' B' C'.
Proof.
intros A B C A' B' C'.
intros.
unfold Hcong in ×.
assert (T:=l11_49 B A C B' A' C').
assert (¬ Col A B C).
intro.
apply cols_coincide_2 in H4.
intuition.
assert_diffs.
intuition.
Qed.

Lemma axiom_hcong_4_existence : A B C O X P,
   ¬ Col_H P O X ¬ Col_H A B C
   Y, CongA A B C X O Y same_side' P Y O X.
Proof.
intros.
rewrite <- cols_coincide in H.
rewrite <- cols_coincide in H0.

assert(¬Col X O P).
intro.
apply H.
Col.
assert(HH:=angle_construction_1 A B C X O P H0 H1).

ex_and HH Y.

Y.
split.
assumption.
apply OS_same_side'.
apply invert_one_side.
apply one_side_symmetry.
assumption.
Qed.

Lemma same_side_trans :
  A B C l,
  same_side A B l same_side B C l same_side A C l.
Proof.
intros.
apply one_side_same_side.
apply same_side_one_side in H.
apply same_side_one_side in H0.
eapply one_side_transitivity.
apply H.
assumption.
Qed.

Lemma same_side_sym :
  A B l,
  same_side A B l same_side B A l.
Proof.
intros.
apply one_side_same_side.
apply same_side_one_side in H.
apply one_side_symmetry.
assumption.
Qed.

Lemma axiom_hcong_4_uniqueness :
   A B C O P X Y Y', ¬ Col_H P O X ¬ Col_H A B C CongA A B C X O Y CongA A B C X O Y'
  same_side' P Y O X same_side' P Y' O X outH O Y Y'.
Proof.
intros.
rewrite <- cols_coincide in H.
rewrite <- cols_coincide in H0.
assert (T:CongA X O Y X O Y').
eapply conga_trans.
apply conga_sym.
apply H1.
assumption.

apply conga__or_out_ts in T.
induction T.
apply out_outH.
assumption.

apply same_side_OS in H3.
apply same_side_OS in H4.
exfalso.
assert (OS O X Y Y').
apply one_side_transitivity with P.
apply one_side_symmetry.
assumption.
assumption.
apply invert_one_side in H6.
apply l9_9 in H5.
intuition.
Qed.

Lemma axiom_conga_comm : A B C,
 ¬ Col_H A B C CongA A B C C B A.
Proof.
intros.
rewrite <- cols_coincide in H.
assert_diffs.
apply conga_pseudo_refl;auto.
Qed.

Lemma axiom_cong_permr : A B C D, Hcong A B C D Hcong A B D C.
Proof.
intros;unfold Hcong.
Cong.
Qed.

Lemma axiom_congaH_outH_congaH :
  A B C D E F A' C' D' F' : Tpoint,
  CongA A B C D E F
  Between_H B A A' Between_H B A' A B A A = A'
  Between_H B C C' Between_H B C' C B C C = C'
  Between_H E D D' Between_H E D' D E D D = D'
  Between_H E F F' Between_H E F' F E F F = F'
  CongA A' B C' D' E F'.
Proof.
intros.
apply out_conga with A C D F;auto using outH_out.
Qed.

Lemma axiom_conga_permlr:
A B C D E F : Tpoint, CongA A B C D E F CongA C B A F E D.
Proof.
intros.
auto using conga_right_comm, conga_left_comm.
Qed.

Lemma axiom_inter_dec : l m,
  ( P, Incident P l Incident P m) ¬ ( P, Incident P l Incident P m).
Proof.
intros l m;
elim (Ch12_parallel_inter_dec.inter_dec (P1 l) (P2 l) (P1 m) (P2 m));
intro; [left|right]; auto.
Qed.

Lemma axiom_conga_refl : A B C, ¬ Col_H A B C CongA A B C A B C.
Proof.
intros A B C H. apply Ch11_angles.conga_refl;
intro; subst; apply H; apply cols_coincide; Col.
Qed.

End T.

Section Hilbert_neutral_to_Tarski_neutral.

Context `{TE:Tarski_2D_euclidean}.

Lemma PAneqPB : PA PB.
Proof.
assert (T:= lower_dim).
intro.
rewrite H in ×.
apply T.
left.
Between.
Qed.

Definition l0 := Lin PA PB PAneqPB.

Lemma plan : ¬ Incident PC l0.
Proof.
unfold Incident.
unfold Col.
assert (T:= lower_dim).
unfold l0;simpl.
intro;apply T.
intuition.
Qed.

Instance Hilbert_neutral_follows_from_Tarski_neutral : Hilbert_neutral_2D.
Proof.
 exact (Build_Hilbert_neutral_2D Tpoint Line Eq Eq_Equiv Incident
       axiom_Incid_morphism axiom_Incid_dec eq_dec_points axiom_line_existence axiom_line_uniqueness axiom_two_points_on_line l0 PC plan
       Between_H axiom_between_col axiom_between_diff axiom_between_comm axiom_between_out
       axiom_between_only_one axiom_pasch
       Hcong axiom_cong_permr axiom_hcong_trans axiom_hcong_1_existence
       axiom_hcong_3 CongA axiom_conga_refl axiom_conga_comm axiom_conga_permlr axiom_cong_5' axiom_congaH_outH_congaH axiom_hcong_4_existence axiom_hcong_4_uniqueness).
Defined.

End Hilbert_neutral_to_Tarski_neutral.

Section Hilbert_Euclidean_to_Tarski_Euclidean.

Context `{TE:Tarski_2D_euclidean}.

Group Parallels

We use a definition of parallel which is valid only in 2D:

Definition Para l m := ¬ X, Incident X l Incident X m.

Lemma Para_Par : A B C D, HAB: AB, HCD: CD,
 Para (Lin A B HAB) (Lin C D HCD) Par A B C D.
Proof.
intros.
unfold Para in H.
unfold Incident in *;simpl in ×.
unfold Par.
left.
unfold Par_strict.
repeat split;auto;try apply all_coplanar.
Qed.

Lemma axiom_euclid_uniqueness :
   l P m1 m2,
  ¬ Incident P l
   Para l m1 Incident P m1
   Para l m2 Incident P m2
   Eq m1 m2.
Proof.
intros.
destruct l as [A B HAB].
destruct m1 as [C D HCD].
destruct m2 as [C' D' HCD'].
unfold Incident in *;simpl in ×.
apply Para_Par in H0.
apply Para_Par in H2.
elim (parallel_uniqueness A B C D C' D' P H0 H1 H2 H3);intros.
apply axiom_line_uniqueness with C' D';
unfold Incident;simpl;Col.
Qed.

Instance Hilbert_euclidean_follows_from_Tarski_euclidean : Hilbert_euclidean_2D Hilbert_neutral_follows_from_Tarski_neutral.
Proof.
split.
apply axiom_euclid_uniqueness.
Qed.

End Hilbert_Euclidean_to_Tarski_Euclidean.