Require Import GeoCoq.Axioms.tarski_axioms.
Require Import GeoCoq.Axioms.gupta_inspired_variant_axioms.
Require Import GeoCoq.Tarski_dev.Ch05_bet_le.

Section Tarski_neutral_dimensionless_to_Gupta_inspired_variant_of_Tarski_neutral_dimensionless.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma cong_inner_transitivity' : forall A B C D E F, Cong A B E F -> Cong C D E F -> Cong A B C D.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @Cong Tn A B E F) (_ : @Cong Tn C D E F), @Cong Tn A B C D *)
  intros A B C D E F H1 H2; apply (cong_inner_transitivity E F); apply cong_symmetry; assumption.
Qed.

Lemma inner_pasch' : forall A B C P Q,
  Bet A P C -> Bet B Q C -> A <> P -> P <> C -> B <> Q -> Q <> C ->
  ~ (Bet A B C \/ Bet B C A \/ Bet C A B) ->
  exists x : Tpoint, Bet P x B /\ Bet Q x A.
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : @Bet Tn A P C) (_ : @Bet Tn B Q C) (_ : not (@eq (@Tpoint Tn) A P)) (_ : not (@eq (@Tpoint Tn) P C)) (_ : not (@eq (@Tpoint Tn) B Q)) (_ : not (@eq (@Tpoint Tn) Q C)) (_ : not (or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)))), @ex (@Tpoint Tn) (fun x : @Tpoint Tn => and (@Bet Tn P x B) (@Bet Tn Q x A)) *)
  intros A B C P Q; intros; apply inner_pasch with C; assumption.
Qed.

Instance T_to_TG : Gupta_inspired_variant_of_Tarski_neutral_dimensionless_with_decidable_point_equality.
Proof.
exact (Build_Gupta_inspired_variant_of_Tarski_neutral_dimensionless_with_decidable_point_equality
  Tpoint Bet Cong eq_dec_points
  cong_pseudo_reflexivity cong_inner_transitivity' cong_identity
  segment_construction five_segment between_symmetry between_inner_transitivity inner_pasch'
  PA PB PC lower_dim).
Defined.

End Tarski_neutral_dimensionless_to_Gupta_inspired_variant_of_Tarski_neutral_dimensionless.

Section Tarski_2D_to_Gupta_inspired_variant_of_Tarski_2D.

Context `{T2D:Tarski_2D}.

Instance T2D_to_TG2D : Gupta_inspired_variant_of_Tarski_2D T_to_TG.
Proof.
(* Goal: Gupta_inspired_variant_of_Tarski_2D (@T_to_TG Tn TnEQD) *)
  split; intros A B C P Q HPQ HAB HAC HBC; apply upper_dim, HPQ.
Defined.

End Tarski_2D_to_Gupta_inspired_variant_of_Tarski_2D.

Section Tarski_euclidean_to_Gupta_inspired_variant_of_Tarski_euclidean.

Context `{TE:Tarski_euclidean}.

Instance T_euclidean_to_TG_euclidean : Gupta_inspired_variant_of_Tarski_euclidean T_to_TG.
Proof.
(* Goal: Gupta_inspired_variant_of_Tarski_euclidean (@T_to_TG Tn TnEQD) *)
  split; intros A B C D T H1 H2 HBD HDC HNCol.
(* Goal: @ex (@TpointG (@T_to_TG Tn TnEQD)) (fun x : @TpointG (@T_to_TG Tn TnEQD) => @ex (@TpointG (@T_to_TG Tn TnEQD)) (fun y : @TpointG (@T_to_TG Tn TnEQD) => and (@BetG (@T_to_TG Tn TnEQD) A B x) (and (@BetG (@T_to_TG Tn TnEQD) A C y) (@BetG (@T_to_TG Tn TnEQD) x T y)))) *)
  assert (A <> D) by (intro; subst; apply HNCol; right; right; apply between_symmetry, H2).
(* Goal: @ex (@TpointG (@T_to_TG Tn TnEQD)) (fun x : @TpointG (@T_to_TG Tn TnEQD) => @ex (@TpointG (@T_to_TG Tn TnEQD)) (fun y : @TpointG (@T_to_TG Tn TnEQD) => and (@BetG (@T_to_TG Tn TnEQD) A B x) (and (@BetG (@T_to_TG Tn TnEQD) A C y) (@BetG (@T_to_TG Tn TnEQD) x T y)))) *)
  apply euclid with D; assumption.
Defined.

End Tarski_euclidean_to_Gupta_inspired_variant_of_Tarski_euclidean.