Require Import GeoCoq.Axioms.continuity_axioms.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.

Section Aristotle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma aristotle__greenberg : aristotle_s_axiom -> greenberg_s_axiom.
Proof.
  intros aristotle P Q R A B C.
  intros HNColB HABCacute HQRdiff HQright.
  elim (eq_dec_points P Q); intro HPQdiff.
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
  { treat_equalities.
(* Goal: @Lt Tn P Z P Q *)
    assert_diffs.
    exists R.
    split; [|apply out_trivial; auto].
    split.
    apply lea121345; auto.
    intro.
    apply HNColB.
    apply col_permutation_4.
    apply out_col.
    apply (eq_conga_out P R); auto.
  }
  assert (HXY : (exists X Y, Out B A X /\ Out B C Y /\ Per B X Y /\ Lt P Q X Y)) by (apply aristotle; assumption).
  destruct HXY as [X [Y [PX [PY [HXright [Hle HNcong]]]]]].
(* Goal: @Lt Tn P Z P Q *)
  assert_diffs.
  assert (HXYdiff : X <> Y) by (intro; treat_equalities; auto).
  assert (HT : (exists T, Out Q T P /\ Cong Q T X Y)) by (apply l6_11_existence; auto).
  destruct HT as [T []].
  assert (HS : (exists S, Out Q S R /\ Cong Q S X B)) by (apply l6_11_existence; auto).
  destruct HS as [S []].
(* Goal: @Lt Tn P Z P Q *)
  assert_diffs.
  exists S.
  split; auto.
  assert_cols.
  assert (Per S Q P) by (apply (l8_3 R); Perp; Col).
  assert (Per T Q S) by (apply (l8_3 P); Perp; Col).
  assert (P<>S).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
  { intro; treat_equalities.
    assert (P=Q) by (apply l8_8; auto); treat_equalities; absurde.
  }
  assert (T<>S).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
  { intro; treat_equalities.
    assert (T=Q) by (apply l8_8; auto); treat_equalities; absurde.
  }
  apply conga_preserves_lta with P S Q T S Q; try (apply conga_refl; auto); [|split].
  - apply conga_trans with X B Y.
    2: apply (out_conga A B C A B C); CongA; apply out_trivial; auto.
    assert (HInter : (Cong T S Y B /\ (T <> S -> CongA Q T S X Y B /\ CongA Q S T X B Y))).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { apply (l11_49 T Q S Y X B); Cong.
      apply l11_16; Perp.
    }
    destruct HInter as [_ [_ HConga]]; auto.
    apply conga_left_comm; auto.

  - apply lea_comm.
    apply (l11_29_b Q S P Q S T).
    exists T.
    split; CongA.
    repeat split; auto.
    exists P.
    split; [|right; apply out_trivial; auto].
    apply l6_13_1.
    apply l6_6; auto.
    apply (le_transitivity Q P X Y).
    apply (le_transitivity Q P P Q); Le.
    apply (cong__le); Cong.

  - intro HConga.
    assert (HInter : Cong Q P Q T /\ Cong S P S T /\ CongA Q P S Q T S).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { apply l11_50_1; Cong.
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
      { intro.
        assert (HUn : S=Q\/P=Q) by (apply l8_9; Col).
        destruct HUn; treat_equalities; absurde.
      }
      apply l11_16; Perp.
      CongA.
    }
    destruct HInter as [HCong _].
    apply HNcong.
    apply (cong_transitivity P Q T Q); Cong.
Qed.

(** This proof is inspired by Several topics from geometry, by Franz Rothe *)

Lemma aristotle__obtuse_case_elimination :
  aristotle_s_axiom ->
  ~ hypothesis_of_obtuse_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @aristotle_s_axiom Tn, not (@hypothesis_of_obtuse_saccheri_quadrilaterals Tn) *)
  intros aristotle obtuse.
(* Goal: False *)
  destruct ex_lambert as [Q' [C' [P [Q HLam]]]].
  assert (HObtuse : Obtuse C' P Q) by (apply <- (lam_obtuse__oah Q'); trivial).
(* Goal: False *)
  assert (HPar : Par_strict Q' Q C' P) by (apply lam__par_strict1423, HLam).
(* Goal: False *)
  destruct HLam; spliter.
(* Goal: False *)
  destruct (l10_15 P Q P C') as [A' [HPerp HOS]]; Col.
(* Goal: not (@Col Tn P Q C') *)
(* Goal: False *)
    apply not_col_permutation_1.
(* Goal: not (@Col Tn C' P Q) *)
(* Goal: False *)
    apply par_strict_not_col_1 with Q'; Par.
(* Goal: @Lt Tn P Z P Q *)
  assert_diffs.
(* Goal: False *)
  assert (HLtA : LtA Q P A' C' P Q) by (apply obtuse_per__lta; Perp).
(* Goal: False *)
  destruct HLtA as [HLeA HNCongA].
(* Goal: False *)
  assert (HInAngle : InAngle A' Q P C').
(* Goal: @InAngle Tn A' Q P C' *)
(* Goal: False *)
    apply lea_in_angle; Side; apply lea_right_comm; trivial.
(* Goal: False *)
  destruct (segment_construction C' P C' P) as [C [HC1 HC2]].
(* Goal: False *)
  destruct (segment_construction A' P A' P) as [A [HA1 HA2]].
(* Goal: @Lt Tn P Z P Q *)
  assert_diffs.
(* Goal: False *)
  assert (HInAngle1 : InAngle C A P Q).
(* Goal: @InAngle Tn C A P Q *)
(* Goal: False *)
    apply in_angle_reverse with A'; auto.
(* Goal: @InAngle Tn Q A' P C *)
(* Goal: False *)
    apply l11_24, in_angle_reverse with C'; auto.
(* Goal: @InAngle Tn A' C' P Q *)
(* Goal: False *)
    apply l11_24; trivial.
(* Goal: False *)
  assert (HNCol : ~ Col P C' A').
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
  { intro Habs.
(* Goal: False *)
    apply HNCongA, conga_right_comm, out2__conga.
(* Goal: @Out Tn P Q Q *)
(* Goal: @Out Tn P C' A' *)
      apply out_trivial; auto.
(* Goal: @Out Tn P C' A' *)
    apply col_one_side_out with Q; trivial.
  }
(* Goal: False *)
  assert (HNCol1 : ~ Col P C A) by (intro; apply HNCol; ColR).
(* Goal: False *)
  assert (HNCol2 : ~ Col P Q C) by (intro; apply (par_strict_not_col_2 Q' Q C' P); ColR).
(* Goal: False *)
  assert (HPer : Per A P Q) by (apply l8_2, per_col with A'; Perp; Col).
(* Goal: False *)
  assert (HOS1 : OS A P C Q).
(* Goal: @OS Tn A P C Q *)
(* Goal: False *)
    apply in_angle_one_side; Col.
(* Goal: not (@Col Tn A P Q) *)
(* Goal: False *)
    apply per_not_col; auto.
(* Goal: False *)
  destruct (aristotle P Q A P C) as [X [Y]]; Col.
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
  { exists A, P, Q; split; Perp; split.
(* Goal: @LeA Tn A P C A P Q *)
(* Goal: not (@CongA Tn A P C A P Q) *)
      apply inangle__lea; trivial.
    intro HCongA.
(* Goal: False *)
    destruct (conga_cop__or_out_ts A P C Q); CongA; Cop.
(* Goal: False *)
(* Goal: False *)
      assert_cols; Col.
(* Goal: False *)
      apply (l9_9 A P C Q); trivial.
  }

(* Goal: False *)
  spliter.
(* Goal: False *)
  apply (not_and_lt P Q X Y).
(* Goal: and (@Lt Tn P Q X Y) (@Lt Tn X Y P Q) *)
  split; trivial.
(* Goal: @Lt Tn X Y P Q *)
  destruct (l8_18_existence P Q Y) as [Z [HZ1 HZ2]].
(* Goal: not (@Col Tn P Q Y) *)
(* Goal: @Lt Tn X Y P Q *)
    intro; assert_diffs; apply HNCol2; ColR.
(* Goal: @Lt Tn X Y P Q *)
  apply lt_transitivity with P Z.

  - assert (P <> Z).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { intro; subst Z.
(* Goal: @Lt Tn P Z P Q *)
      assert_diffs.
(* Goal: False *)
      assert (Per Q P C) by (apply per_col with Y; Col; Perp).
(* Goal: False *)
      apply HNCol1, cop_perp2__col with P Q; Perp; Cop.
    }
(* Goal: @Lt Tn X Y P Z *)
    assert (HLam : Lambert P X Y Z).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { assert_diffs.
      repeat split; auto.
(* Goal: @Per Tn X P Z *)
(* Goal: @Per Tn P Z Y *)
(* Goal: @Coplanar Tn P X Y Z *)
        apply per_col with Q; Col.
(* Goal: @Per Tn X P Q *)
(* Goal: @Per Tn P Z Y *)
(* Goal: @Coplanar Tn P X Y Z *)
        apply l8_2, per_col with A; Perp; Col.
(* Goal: @Per Tn P Z Y *)
(* Goal: @Coplanar Tn P X Y Z *)
        apply perp_per_1, perp_left_comm, perp_col with Q; auto.
(* Goal: @Coplanar Tn P X Y Z *)
        assert (InAngle Y X P Q).
(* Goal: @Out Tn P Q Q *)
(* Goal: @Out Tn P C' A' *)
          apply l11_25 with C A Q; try (apply l6_6); trivial; apply out_trivial; auto.
(* Goal: @Coplanar Tn P X Y Z *)
        apply coplanar_perm_12, col_cop__cop with Q; Col; Cop.
    }
(* Goal: @Lt Tn X Y P Z *)
    apply lam_obtuse__lt; trivial.
    apply <- (lam_obtuse__oah P); trivial.

  - assert (HOut : Out Q P Z).
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { apply col_one_side_out with Q'; Col.
(* Goal: @OS Tn P A Z Q *)
      apply one_side_transitivity with Y.
(* Goal: @OS Tn Q Q' P Y *)
(* Goal: @OS Tn Q Q' Y Z *)
        apply l12_6, par_strict_col_par_strict with C'; Par; ColR.
(* Goal: @OS Tn P A Z Y *)
      apply l12_6, par_not_col_strict with Y; Col.
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
      { apply l12_9 with P Q; Perp; [Cop..| |Cop].
(* Goal: @Coplanar Tn P Q Q' Y *)
        apply coplanar_perm_12, col_cop__cop with C; Col.
        apply  col_cop__cop with C'; Col; Cop.
      }
(* Goal: not (@Col Tn Q Q' Y) *)
      apply not_col_permutation_1, par_not_col with P C'; Par; ColR.
    }
(* Goal: @Lt Tn P Z P Q *)
    assert_diffs.
(* Goal: @Lt Tn P Z P Q *)
    apply bet__lt1213; auto.
(* Goal: @Bet Tn P Z Q *)
    apply out2__bet; trivial.
(* Goal: @Out Tn P Z Q *)
    apply col_one_side_out with A; Col.
(* Goal: @OS Tn P A Z Q *)
    apply one_side_transitivity with Y.
(* Goal: @OS Tn P A Z Y *)
(* Goal: @OS Tn P A Y Q *)
    { apply l12_6, par_not_col_strict with Y; Col.
(* Goal: @Par Tn P A Z Y *)
(* Goal: not (@Col Tn P A Y) *)
        apply l12_9 with P Q; Perp; [Cop..|].
(* Goal: @Coplanar Tn P Q A Y *)
(* Goal: not (@Col Tn P A Y) *)
        apply coplanar_perm_12, col_cop__cop with C; Col; Cop.
(* Goal: not (@Col Tn P A Y) *)
      intro; apply HNCol1; ColR.
    }
(* Goal: @OS Tn P A Y Q *)
    apply one_side_symmetry, out_out_one_side with C; Side.
Qed.

Lemma aristotle__acute_or_right :
  aristotle_s_axiom ->
  hypothesis_of_acute_saccheri_quadrilaterals \/ hypothesis_of_right_saccheri_quadrilaterals.
Proof.
(* Goal: forall _ : @aristotle_s_axiom Tn, or (@hypothesis_of_acute_saccheri_quadrilaterals Tn) (@hypothesis_of_right_saccheri_quadrilaterals Tn) *)
  intros aristotle.
(* Goal: or (@hypothesis_of_acute_saccheri_quadrilaterals Tn) (@hypothesis_of_right_saccheri_quadrilaterals Tn) *)
  destruct saccheri_s_three_hypotheses as [Ha|[Hr|Ho]]; auto.
(* Goal: or (@hypothesis_of_acute_saccheri_quadrilaterals Tn) (@hypothesis_of_right_saccheri_quadrilaterals Tn) *)
  exfalso; apply aristotle__obtuse_case_elimination in aristotle; auto.
Qed.

End Aristotle.