Library GeoCoq.Tarski_dev.Ch03_bet
Require Export GeoCoq.Tarski_dev.Ch02_cong.
Section T2_1.
Context `{Tn:Tarski_neutral_dimensionless}.
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 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 (apply inner_pasch with C;auto).
ex_and H1 x.
apply between_identity in H1; subst; assumption.
Qed.
Section T2_1.
Context `{Tn:Tarski_neutral_dimensionless}.
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 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 (apply inner_pasch with C;auto).
ex_and H1 x.
apply between_identity in H1; subst; assumption.
Qed.
This lemma is used by tactics for trying several permutations.
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_equality : ∀ 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.
Lemma between_equality_2 : ∀ A B C : Tpoint, Bet A B C → Bet A C B → B = C.
Proof.
intros.
apply between_equality with A; auto using between_symmetry.
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 (apply inner_pasch with A; apply between_symmetry; auto).
ex_and H1 x.
assert (C = x) by (apply between_identity; auto); subst; auto.
Qed.
Lemma bet_neq12__neq : ∀ A B C, Bet A B C → A ≠ B → A ≠ C.
Proof.
intros A B C HBet HAB Heq.
subst C; apply HAB, between_identity; trivial.
Qed.
Lemma bet_neq21__neq : ∀ A B C, Bet A B C → B ≠ A → A ≠ C.
Proof.
intros A B C HBet HAB.
apply bet_neq12__neq with B; auto.
Qed.
Lemma bet_neq23__neq : ∀ A B C, Bet A B C → B ≠ C → A ≠ C.
Proof.
intros A B C HBet HBC Heq.
subst C; apply HBC; symmetry.
apply between_identity; trivial.
Qed.
Lemma bet_neq32__neq : ∀ A B C, Bet A B C → C ≠ B → A ≠ C.
Proof.
intros A B C HBet HAB.
apply bet_neq23__neq with B; auto.
Qed.
Lemma not_bet_distincts : ∀ A B C, ¬ Bet A B C → A ≠ B ∧ B ≠ C.
Proof.
intros A B C HNBet.
repeat split; intro; subst B; apply HNBet.
apply between_trivial2.
apply between_trivial.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 (apply inner_pasch with D;auto).
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_uniqueness 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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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; auto with 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.
∀ 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_equality : ∀ 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.
Lemma between_equality_2 : ∀ A B C : Tpoint, Bet A B C → Bet A C B → B = C.
Proof.
intros.
apply between_equality with A; auto using between_symmetry.
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 (apply inner_pasch with A; apply between_symmetry; auto).
ex_and H1 x.
assert (C = x) by (apply between_identity; auto); subst; auto.
Qed.
Lemma bet_neq12__neq : ∀ A B C, Bet A B C → A ≠ B → A ≠ C.
Proof.
intros A B C HBet HAB Heq.
subst C; apply HAB, between_identity; trivial.
Qed.
Lemma bet_neq21__neq : ∀ A B C, Bet A B C → B ≠ A → A ≠ C.
Proof.
intros A B C HBet HAB.
apply bet_neq12__neq with B; auto.
Qed.
Lemma bet_neq23__neq : ∀ A B C, Bet A B C → B ≠ C → A ≠ C.
Proof.
intros A B C HBet HBC Heq.
subst C; apply HBC; symmetry.
apply between_identity; trivial.
Qed.
Lemma bet_neq32__neq : ∀ A B C, Bet A B C → C ≠ B → A ≠ C.
Proof.
intros A B C HBet HAB.
apply bet_neq23__neq with B; auto.
Qed.
Lemma not_bet_distincts : ∀ A B C, ¬ Bet A B C → A ≠ B ∧ B ≠ C.
Proof.
intros A B C HNBet.
repeat split; intro; subst B; apply HNBet.
apply between_trivial2.
apply between_trivial.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 (apply inner_pasch with D;auto).
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_uniqueness 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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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 `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.
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; auto with 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.
The prove the former version of lower dimension axiom for compatibility.
Lemma lower_dim_ex : ∃ A B C,
¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B).
Proof.
∃ PA.
∃ PB.
∃ PC.
apply lower_dim.
Qed.
Lemma two_distinct_points : ∃ X, ∃ Y: Tpoint, X ≠ Y.
Proof.
assert (ld:=lower_dim_ex).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
induction (eq_dec_points A B).
subst A; ∃ B; ∃ C; auto with between between_no_eauto.
∃ 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 `{Tn: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_segment _ _ _ _ _ _ _ _ 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 `{Tn: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.
Lemma BetSEq : ∀ A B C, BetS A B C ↔ Bet A B C ∧ A ≠ B ∧ A ≠ C ∧ B ≠ C.
Proof.
intros; unfold BetS; split; intro; spliter;
repeat split; auto; intro; treat_equalities; auto.
Qed.
End Beeson_2.