Library Ch03_bet

Require Export Ch02_cong.

Section T2_1.

Context `{M:Tarski_neutral_dimensionless}.

Definition Col (A B C : Tpoint) : Prop := Bet A B C ∨ Bet B C A ∨ Bet C A B.

Lemma bet_col : ∀ A B C, Bet A B C → Col A B C.
Proof.
intros;unfold Col;auto.
Qed.

Lemma between_trivial : ∀ A B : Tpoint, Bet A B B.
Proof.
intros.
prolong A B x B B.
assert (x = B) by (apply cong_reverse_identity with B; Cong).
subst;assumption.
Qed.

Lemma bet_dec_eq_dec :
  (∀ A B C, Bet A B C ∨ ¬ Bet A B C) →
  (∀ A B:Tpoint, A=B ∨ A≠B).
Proof.
intros.
induction (H A B A).

  left; apply between_identity; assumption.

  right; intro; subst; apply H0; apply between_trivial.
Qed.

Lemma between_symmetry : ∀ A B C : Tpoint, Bet A B C → Bet C B A.
Proof.
intros.
assert (Bet B C C) by (apply between_trivial).
assert(∃ x, Bet B x B ∧ Bet C x A)
  by (eapply inner_pasch;eauto).
ex_and H1 x.
apply between_identity in H1; subst; assumption.
Qed.

Lemma Bet_cases :
 ∀ A B C,
 Bet A B C ∨ Bet C B A →
 Bet A B C.
Proof.
intros.
decompose [or] H; auto using between_symmetry.
Qed.

Lemma Bet_perm :
  ∀ A B C,
 Bet A B C →
 Bet A B C ∧ Bet C B A.
Proof.
intros.
auto using between_symmetry.
Qed.

Lemma between_trivial2 : ∀ A B : Tpoint, Bet A A B.
Proof.
intros.
apply between_symmetry.
apply between_trivial.
Qed.

Lemma between_egality : ∀ A B C : Tpoint, Bet A B C → Bet B A C → A = B.
Proof.
intros.
assert (∃ x, Bet B x B ∧ Bet A x A)
  by (apply (inner_pasch A B C);assumption).
ex_and H1 x.
apply between_identity in H1.
apply between_identity in H2.
congruence.
Qed.

End T2_1.


Ltac assert_cols :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _ ⇒
     not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ ⇒ clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ ⇒ clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ ⇒ clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _ ⇒ clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _ ⇒ clear H
   | H:(Col ?X1 ?X1 ?X2) |- _ ⇒ clear H
   | H:(Col ?X2 ?X1 ?X1) |- _ ⇒ clear H
   | H:(Col ?X1 ?X2 ?X1) |- _ ⇒ clear H
end.

Ltac clean_reap_hyps :=
  repeat
  match goal with
 
   | H:(¬Col ?A ?B ?C), H2 : ¬Col ?A ?B ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ ⇒ clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ ⇒ clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ ⇒ clear H2
   | H:(?A<>?B), H2 : (?B<>?A) |- _ ⇒ clear H2
   | H:(?A<>?B), H2 : (?A<>?B) |- _ ⇒ clear H2
end.

Ltac clean := clean_trivial_hyps;clean_duplicated_hyps;clean_reap_hyps.

Ltac smart_subst X := subst X;clean.

Ltac treat_equalities_aux :=
  repeat
  match goal with
   | H:(?X1 = ?X2) |- _ ⇒ smart_subst X2
end.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ ⇒
      apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ ⇒
      apply cong_identity in H;smart_subst X2
   | H:(Bet ?X1 ?X2 ?X1) |- _ ⇒ apply between_identity in H;smart_subst X2
end.

Ltac show_distinct X Y := assert (X≠Y);[unfold not;intro;treat_equalities|idtac].

Hint Resolve between_symmetry bet_col : between.
Hint Resolve between_trivial between_trivial2 : between_no_eauto.

Ltac eBetween := treat_equalities;eauto with between.
Ltac Between := treat_equalities;auto with between between_no_eauto.

Section T2_2.

Context `{M:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Lemma between_inner_transitivity : ∀ A B C D, Bet A B D → Bet B C D → Bet A B C.
Proof.
intros.
assert (∃ x, Bet B x B ∧ Bet C x A)
  by (eapply inner_pasch;eauto).
ex_and H1 x.
Between.
Qed.

Lemma between_exchange3 : ∀ A B C D, Bet A B C → Bet A C D → Bet B C D.
Proof.
intros.
assert (∃ x, Bet C x C ∧ Bet B x D)
 by (eapply inner_pasch;eBetween).
ex_and H1 x.
Between.
Qed.

Lemma outer_transitivity_between2 : ∀ A B C D, Bet A B C → Bet B C D → B≠C → Bet A C D.
Proof.
intros.
prolong A C x C D.
assert (x = D)
  by (apply (construction_unicity B C C D); try apply (between_exchange3 A B C x); Cong).
subst x;assumption.
Qed.

End T2_2.

Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 : between.

Section T2_3.

Context `{M:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Lemma between_exchange2 : ∀ A B C D, Bet A B D → Bet B C D → Bet A C D.
Proof.
intros.
induction (eq_dec_points B C);eBetween.
Qed.

Lemma outer_transitivity_between : ∀ A B C D, Bet A B C → Bet B C D → B≠C → Bet A B D.
Proof.
intros.
eBetween.
Qed.

End T2_3.

Hint Resolve between_exchange2 : between.

Section T2_4.

Context `{M:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Lemma between_exchange4 : ∀ A B C D, Bet A B C → Bet A C D → Bet A B D.
Proof.
intros.
eBetween.
Qed.

End T2_4.

Hint Resolve outer_transitivity_between between_exchange4 : between.

Section T2_5.

Context `{M:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Definition Bet_4 := fun A1 A2 A3 A4 ⇒
   Bet A1 A2 A3 ∧ Bet A2 A3 A4 ∧ Bet A1 A3 A4 ∧ Bet A1 A2 A4.

Lemma l_3_9_4 : ∀ A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 → Bet_4 A4 A3 A2 A1.
Proof.
unfold Bet_4.
intros;spliter;Between.
Qed.

Lemma l3_17 : ∀ A B C A' B' P,
  Bet A B C → Bet A' B' C → Bet A P A' → ∃ Q, Bet P Q C ∧ Bet B Q B'.
Proof.
intros.
assert (∃ Q', Bet B' Q' A ∧ Bet P Q' C)
 by (eapply inner_pasch;eBetween).
ex_and H2 x.
assert (∃ y, Bet x y C ∧ Bet B y B')
 by (eapply inner_pasch;eBetween).
ex_and H4 y.
∃ y;eBetween.
Qed.

Lemma two_distinct_points : ∃ X, ∃ Y: Tpoint, X ≠ Y.
Proof.
assert (ld:=lower_dim).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
induction (eq_dec_points A B).

  subst A; ∃ B; ∃ C; Between.

  ∃ A; ∃ B; assumption.
Qed.

Lemma point_construction_different : ∀ A B, ∃ C, Bet A B C ∧ B ≠ C.
Proof.
intros.
assert (tdp := two_distinct_points).
ex_elim tdp x.
ex_elim H y.
prolong A B F x y.
∃ F.
show_distinct B F.
  intuition.
intuition.
Qed.

Lemma another_point : ∀ A: Tpoint, ∃ B, A≠B.
Proof.
intros.
assert (pcd := point_construction_different A A).
ex_and pcd B.
∃ B;assumption.
Qed.

End T2_5.

Section Beeson_1.

Context `{M:Tarski_neutral_dimensionless}.

Variable Cong_stability : ∀ A B C D, ¬ ¬ Cong A B C D → Cong A B C D.

Lemma l2_11_b : ∀ A B C A' B' C',
 Bet A B C → Bet A' B' C' → Cong A B A' B' → Cong B C B' C' → Cong A C A' C'.
Proof.
intros.
apply Cong_stability; intro.
assert (A≠B).
  intro; subst.
  assert (A'=B') by (apply (cong_identity A' B' B); Cong).
  subst; tauto.

assert (Cong C A C' A')
 by (apply (five_segments _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity).
apply H3; Cong.
Qed.

Lemma cong_dec_eq_dec_b :
 (∀ A B:Tpoint, ¬ A ≠ B → A = B).
Proof.
intros A B HAB.
apply cong_identity with A.
apply Cong_stability.
intro HNCong.
apply HAB.
intro HEq.
subst.
apply HNCong.
apply cong_pseudo_reflexivity.
Qed.

End Beeson_1.

Section Beeson_2.

Context `{M:Tarski_neutral_dimensionless}.

Variable Bet_stability : ∀ A B C, ¬ ¬ Bet A B C → Bet A B C.

Lemma bet_dec_eq_dec_b :
 (∀ A B:Tpoint, ¬ A ≠ B → A = B).
Proof.
intros A B HAB.
apply between_identity.
apply Bet_stability.
intro HNBet.
apply HAB.
intro HEq.
subst.
apply HNBet.
apply between_trivial.
Qed.

End Beeson_2.