Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section rah_posidonius.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma rah__posidonius_aux : postulate_of_right_saccheri_quadrilaterals ->
  forall A1 A2 A3 B1 B2 B3,
  Per A2 A1 B1 -> Per A1 A2 B2 -> Cong A1 B1 A2 B2 -> OS A1 A2 B1 B2 ->
  Col A1 A2 A3 -> Col B1 B2 B3 -> Perp A1 A2 A3 B3 ->
  Cong A3 B3 A1 B1.
Proof.
(* Goal: forall (_ : @postulate_of_right_saccheri_quadrilaterals Tn) (A1 A2 A3 B1 B2 B3 : @Tpoint Tn) (_ : @Per Tn A2 A1 B1) (_ : @Per Tn A1 A2 B2) (_ : @Cong Tn A1 B1 A2 B2) (_ : @OS Tn A1 A2 B1 B2) (_ : @Col Tn A1 A2 A3) (_ : @Col Tn B1 B2 B3) (_ : @Perp Tn A1 A2 A3 B3), @Cong Tn A3 B3 A1 B1 *)
  intros rah A1 A2 A3 B1 B2 B3 HPer1 HPer2 HCong HOS HA HB HPerp.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  assert (HSac : Saccheri A1 B1 B2 A2) by repeat (split; finish).
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  assert(Hdiff := sac_distincts A1 B1 B2 A2 HSac).
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  spliter.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  assert_diffs.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  elim(eq_dec_points A1 A3).
(* Goal: @Per Tn A1 A3 B'3 *)
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  { intro.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
    subst A3.
(* Goal: @Cong Tn A1 B3 A1 B1 *)
    assert(B1 = B3); [|subst; Cong].
(* Goal: @eq (@Tpoint Tn) B1 B3 *)
    apply (l6_21 B1 B2 A1 B1); Col.
(* Goal: not (@Col Tn B1 B2 A1) *)
(* Goal: @Col Tn A1 B1 B3 *)
      apply not_col_permutation_1; apply (sac__ncol123 _ _ _ A2); assumption.
(* Goal: @Col Tn A1 B1 B3 *)
      unfold Saccheri in HSac; spliter; apply (cop_perp2__col _ _ _ A1 A2); Perp.
(* Goal: @Coplanar Tn A1 A2 B1 B3 *)
      apply col_cop__cop with B2; Cop.
  }
(* Goal: not (@eq (@Tpoint Tn) B1 B3) *)
  intro.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  destruct(segment_construction_3 A3 B3 A1 B1) as [B'3 []]; auto.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  assert_diffs.
(* Goal: @Cong Tn A3 B3 A1 B1 *)
  assert(B3 = B'3); [|subst; assumption].
(* Goal: @eq (@Tpoint Tn) B3 B'3 *)
  assert(Par_strict B1 B2 A1 A3).
(* Goal: @Per Tn A1 A3 B'3 *)
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  { apply (par_strict_col_par_strict _ _ _ A2); auto.
(* Goal: @Par_strict Tn B1 B2 A1 A2 *)
    apply par_strict_symmetry.
(* Goal: @Par_strict Tn A1 A2 B1 B2 *)
    apply sac__par_strict1423; assumption.
  }
(* Goal: @eq (@Tpoint Tn) B3 B'3 *)
  apply (l6_21 B1 B2 A3 B3); Col.
(* Goal: not (@Col Tn B1 B2 A3) *)
(* Goal: @Col Tn B1 B2 B'3 *)
    apply (par_strict_not_col_4 _ _ A1); auto.
(* Goal: @Col Tn B1 B2 B'3 *)
  apply col_permutation_2.
(* Goal: @Col Tn B2 B'3 B1 *)
  assert (Coplanar A1 B2 B'3 B1).
(* Goal: @Per Tn A1 A3 B'3 *)
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  { apply coplanar_perm_15, coplanar_trans_1 with A3.
(* Goal: not (@Col Tn A3 B1 B2) *)
(* Goal: @Coplanar Tn A3 B1 B2 A1 *)
(* Goal: @Coplanar Tn A3 B1 B2 B'3 *)
      apply not_col_permutation_2, par_strict_not_col_4 with A1; assumption.
(* Goal: @Coplanar Tn A3 B1 B2 A1 *)
(* Goal: @Coplanar Tn A3 B1 B2 B'3 *)
      apply coplanar_perm_18, pars__coplanar; assumption.
(* Goal: @Coplanar Tn A3 B1 B2 B'3 *)
    exists B3; right; right; split; Col.
  }
(* Goal: @Col Tn B2 B'3 B1 *)
  apply cop_per2__col with A1; auto; apply l8_2.
(* Goal: @Per Tn A1 B1 B2 *)
(* Goal: @Per Tn A1 B1 B'3 *)
    apply (rah _ _ _ A2); auto.
(* Goal: @Per Tn A1 B1 B'3 *)
  apply (rah _ _ _ A3).
(* Goal: @Saccheri Tn A1 B1 B'3 A3 *)
  unfold Saccheri in *.
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  spliter.
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  assert(B1 <> B3).
(* Goal: @Per Tn A1 A3 B'3 *)
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  { intro.
(* Goal: False *)
    subst B3.
(* Goal: False *)
    assert(A1 = A3); auto.
(* Goal: @eq (@Tpoint Tn) A1 A3 *)
    apply (l8_18_uniqueness A1 A2 B1); Col; Perp.
(* Goal: not (@Col Tn A1 A2 B1) *)
    apply not_col_permutation_1; apply per_not_col; auto.
  }
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  assert(Per A1 A3 B'3).
(* Goal: @Per Tn A1 A3 B'3 *)
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  { apply perp_per_1; auto.
(* Goal: @Perp Tn A3 A1 B'3 A3 *)
    apply perp_comm; apply (perp_col _ A2); Col.
(* Goal: @Perp Tn A1 A2 A3 B'3 *)
    apply (perp_col1 _ _ _ B3); Col.
  }
(* Goal: and (@Per Tn B1 A1 A3) (and (@Per Tn A1 A3 B'3) (and (@Cong Tn A1 B1 B'3 A3) (@OS Tn A1 A3 B1 B'3))) *)
  repeat split; Cong.
(* Goal: @Per Tn B1 A1 A3 *)
(* Goal: @OS Tn A1 A3 B1 B'3 *)
    apply (per_col _ _ A2); auto.
(* Goal: @OS Tn A1 A3 B1 B'3 *)
  apply (one_side_transitivity _ _ _ B3).
(* Goal: @OS Tn A1 A3 B1 B3 *)
(* Goal: @OS Tn A1 A3 B3 B'3 *)
    apply l12_6; auto; apply (par_strict_col_par_strict _ _ _ B2); Col; Par.
(* Goal: @OS Tn A1 A3 B3 B'3 *)
    apply invert_one_side; apply out_one_side; auto; right; apply not_col_permutation_4; apply per_not_col; auto.
Qed.

Lemma rah__posidonius :
  postulate_of_right_saccheri_quadrilaterals -> posidonius_postulate.
Proof.
(* Goal: forall _ : @postulate_of_right_saccheri_quadrilaterals Tn, @posidonius_postulate Tn *)
intro HP.
(* Goal: @posidonius_postulate Tn *)
destruct ex_saccheri as [A1 [B1 [B2 [A2 [HPer1 [HPer2 [HCong HOS]]]]]]].
(* Goal: @posidonius_postulate Tn *)
exists A1; exists A2; exists B1; exists B2.
(* Goal: and (not (@Col Tn A1 A2 B1)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (forall (A3 A4 B3 B4 : @Tpoint Tn) (_ : @Col Tn A1 A2 A3) (_ : @Col Tn B1 B2 B3) (_ : @Perp Tn A1 A2 A3 B3) (_ : @Col Tn A1 A2 A4) (_ : @Col Tn B1 B2 B4) (_ : @Perp Tn A1 A2 A4 B4), @Cong Tn A3 B3 A4 B4))) *)
assert (HNE : A1 <> A2) by (destruct HOS as [X [[H ?] ?]]; intro; subst A2; Col).
(* Goal: and (not (@Col Tn A1 A2 B1)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (forall (A3 A4 B3 B4 : @Tpoint Tn) (_ : @Col Tn A1 A2 A3) (_ : @Col Tn B1 B2 B3) (_ : @Perp Tn A1 A2 A3 B3) (_ : @Col Tn A1 A2 A4) (_ : @Col Tn B1 B2 B4) (_ : @Perp Tn A1 A2 A4 B4), @Cong Tn A3 B3 A4 B4))) *)
split; [destruct HOS; unfold TS in *; spliter; Col|].
(* Goal: and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (forall (A3 A4 B3 B4 : @Tpoint Tn) (_ : @Col Tn A1 A2 A3) (_ : @Col Tn B1 B2 B3) (_ : @Perp Tn A1 A2 A3 B3) (_ : @Col Tn A1 A2 A4) (_ : @Col Tn B1 B2 B4) (_ : @Perp Tn A1 A2 A4 B4), @Cong Tn A3 B3 A4 B4)) *)
split; [intro; treat_equalities; apply l8_7 in HPer1; intuition|split; [Cop|]].
(* Goal: forall (A3 A4 B3 B4 : @Tpoint Tn) (_ : @Col Tn A1 A2 A3) (_ : @Col Tn B1 B2 B3) (_ : @Perp Tn A1 A2 A3 B3) (_ : @Col Tn A1 A2 A4) (_ : @Col Tn B1 B2 B4) (_ : @Perp Tn A1 A2 A4 B4), @Cong Tn A3 B3 A4 B4 *)
intros A3 A4 B3 B4 HC1 HC2 HPerp1 HC3 HC4 HPerp2.
(* Goal: @Cong Tn A3 B3 A4 B4 *)
assert (HCong1 := rah__posidonius_aux HP A1 A2 A3 B1 B2 B3).
(* Goal: @Cong Tn A3 B3 A4 B4 *)
assert (HCong2 := rah__posidonius_aux HP A1 A2 A4 B1 B2 B4).
apply cong_inner_transitivity with A1 B1; apply cong_symmetry;
[apply HCong1|apply HCong2]; Cong; apply l8_2; auto.
Qed.

End rah_posidonius.