Library GeoCoq.Meta_theory.Decidability.equivalence_between_decidability_properties_of_basic_relations
Require Export GeoCoq.Tarski_dev.Ch04_col.
Require Import GeoCoq.Utils.all_equiv.
Section Equivalence_between_decidability_properties_of_basic_relations.
Context `{Tn:Tarski_neutral_dimensionless}.
Lemma cong_dec_eq_dec :
(∀ A B C D, Cong A B C D ∨ ¬ Cong A B C D) →
(∀ A B:Tpoint, A=B ∨ A≠B).
Proof.
intros H A B.
elim (H A B A A); intro HCong.
left; apply cong_identity with A; assumption.
right; intro; subst; apply HCong.
apply cong_pseudo_reflexivity.
Qed.
Lemma eq_dec_implies_l2_11 :
(∀ A B:Tpoint, A=B ∨ A≠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.
intro eq_dec; intros.
induction (eq_dec A B).
subst B.
assert (A' = B') by (apply (cong_identity A' B' A); Cong).
subst; Cong.
apply cong_commutativity; apply (five_segment A A' B B' C C' A A'); Cong.
Qed.
Lemma eq_dec_implies_construction_uniqueness :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ Q A B C X Y,
Q ≠ A → Bet Q A X → Cong A X B C → Bet Q A Y → Cong A Y B C → X=Y.
Proof.
intro eq_dec; intros.
assert (Cong A X A Y) by eCong.
assert (Cong Q X Q Y) by (apply (eq_dec_implies_l2_11 eq_dec Q A X Q A Y);Cong).
assert(OFSC Q A X Y Q A X X) by (unfold OFSC;repeat split;Cong).
apply five_segment_with_def in H6; try assumption.
apply cong_identity with X; Cong.
Qed.
Lemma eq_dec_implies_outer_transitivity_between2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D, Bet A B C → Bet B C D → B≠C → Bet A C D.
Proof.
intro eq_dec; intros.
prolong A C x C D.
assert (x = D) by (apply (eq_dec_implies_construction_uniqueness eq_dec B C C D); try apply (between_exchange3 A B C x); Cong).
subst x;assumption.
Qed.
Lemma eq_dec_implies_between_exchange4 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D, Bet A B C → Bet A C D → Bet A B D.
Proof.
intro eq_dec; intros.
induction (eq_dec B C); [subst; auto|].
apply between_symmetry;
apply eq_dec_implies_outer_transitivity_between2 with C; eBetween.
Qed.
Lemma eq_dec_implies_two_distinct_points :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∃ X, ∃ Y: Tpoint, X ≠ Y.
Proof.
intro eq_dec.
assert (ld:=lower_dim_ex).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
induction (eq_dec A B).
subst A; ∃ B; ∃ C; Between.
∃ A; ∃ B; assumption.
Qed.
Lemma eq_dec_implies_point_construction_different :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B, ∃ C, Bet A B C ∧ B ≠ C.
Proof.
intro eq_dec; intros.
assert (tdp := eq_dec_implies_two_distinct_points eq_dec).
ex_elim tdp x.
ex_elim H y.
prolong A B F x y.
∃ F.
show_distinct B F.
intuition.
intuition.
Qed.
Lemma eq_dec_implies_l4_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D A' B' C' D', IFSC A B C D A' B' C' D' → Cong B D B' D'.
Proof.
unfold IFSC.
intro eq_dec; intros.
spliter.
induction (eq_dec A C).
treat_equalities;assumption.
assert (∃ E, Bet A C E ∧ C ≠ E)
by (apply eq_dec_implies_point_construction_different; auto).
ex_and H6 E.
prolong A' C' E' C E.
assert (Cong E D E' D')
by (
apply (five_segment_with_def A C E D A' C' E' D');[
unfold OFSC; repeat split;Cong|
assumption]).
apply (five_segment_with_def E C B D E' C' B' D').
unfold OFSC.
repeat split; try solve [eBetween| Cong ].
auto.
Qed.
Lemma eq_dec_implies_l4_5 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C A' C',
Bet A B C → Cong A C A' C' →
∃ B', Bet A' B' C' ∧ Cong_3 A B C A' B' C'.
Proof.
intro eq_dec; intros.
unfold Cong_3.
assert (∃ D', Bet C' A' D' ∧ A' ≠ D')
by (apply eq_dec_implies_point_construction_different; auto).
ex_and H1 x'.
prolong x' A' B' A B.
prolong x' B' C'' B C.
assert (Bet A' B' C'') by eBetween.
assert (C'' = C').
eapply (eq_dec_implies_construction_uniqueness eq_dec x' A' ).
auto.
apply eq_dec_implies_between_exchange4 with B'; auto.
apply (eq_dec_implies_l2_11 eq_dec A' B' C'' A B C);Between.
eBetween.
Cong.
subst C''.
∃ B'.
repeat split;Cong.
Qed.
Lemma eq_dec_implies_l4_6 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C A' B' C', Bet A B C → Cong_3 A B C A' B' C' → Bet A' B' C'.
Proof.
unfold Cong_3.
intro eq_dec; intros.
assert (∃ B'', Bet A' B'' C' ∧ Cong_3 A B C A' B'' C')
by (eapply eq_dec_implies_l4_5;intuition).
ex_and H1 x.
unfold Cong_3 in *;spliter.
assert (Cong_3 A' x C' A' B' C')
by (unfold Cong_3;repeat split;eCong).
unfold Cong_3 in H7;spliter.
assert (IFSC A' x C' x A' x C' B')
by (unfold IFSC;repeat split;Cong).
assert (Cong x x x B')
by (eapply eq_dec_implies_l4_2; try apply H10; auto).
Between.
Qed.
Lemma eq_dec_implies_l4_16 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D A' B' C' D',
FSC A B C D A' B' C' D' → A≠B → Cong C D C' D'.
Proof.
unfold FSC.
unfold Col.
intro eq_dec; intros.
decompose [or and] H; clear H.
assert (Bet A' B' C') by (eapply eq_dec_implies_l4_6;eauto).
unfold Cong_3 in *; spliter.
assert(OFSC A B C D A' B' C' D') by (unfold OFSC;repeat split; assumption).
eapply five_segment_with_def; eauto.
assert(Bet B' C' A') by (apply (eq_dec_implies_l4_6 eq_dec B C A B' C' A'); Cong;auto with cong3).
apply (eq_dec_implies_l4_2 eq_dec B C A D B' C' A' D').
unfold IFSC; unfold Cong_3 in *; spliter; repeat split;Between;Cong.
assert (Bet C' A' B') by (eapply (eq_dec_implies_l4_6 eq_dec C A B C' A' B'); auto with cong3).
eapply (five_segment_with_def B A C D B' A'); unfold OFSC; unfold Cong_3 in *; spliter; repeat split; Between; Cong.
Qed.
Lemma eq_dec_implies_l4_17 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C P Q,
A≠B → Col A B C → Cong A P A Q → Cong B P B Q → Cong C P C Q.
Proof.
intros.
assert (FSC A B C P A B C Q) by (unfold FSC; unfold Cong_3; repeat split;Cong).
eapply eq_dec_implies_l4_16; eauto.
Qed.
Lemma eq_dec_implies_l5_1 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D,
A≠B → Bet A B C → Bet A B D → Bet A C D ∨ Bet A D C.
Proof.
intro eq_dec; intros.
prolong A D C' C D.
prolong A C D' C D.
prolong A C' B' C B.
prolong A D' B'' D B.
assert (Cong B C' B'' C).
apply (eq_dec_implies_l2_11 eq_dec B D C' B'' D' C).
apply between_exchange3 with A; Between.
apply between_inner_transitivity with A; Between.
Cong.
apply cong_transitivity with C D; Cong.
assert (Cong B B' B'' B).
{
apply (eq_dec_implies_l2_11 eq_dec B C' B' B'' C B); Cong.
{
assert (Bet A B C'); [|eBetween].
induction (eq_dec B D); [treat_equalities; auto|].
apply between_symmetry.
apply eq_dec_implies_outer_transitivity_between2 with D; eBetween.
}
{
induction (eq_dec C D'); [treat_equalities; eBetween|].
apply eq_dec_implies_outer_transitivity_between2 with D'; eBetween.
}
}
assert(B'' = B').
apply (eq_dec_implies_construction_uniqueness eq_dec A B B B''); try Cong.
apply eq_dec_implies_between_exchange4 with D'; Between;
apply eq_dec_implies_between_exchange4 with C; Between.
apply eq_dec_implies_between_exchange4 with C'; Between;
apply eq_dec_implies_between_exchange4 with D; Between.
subst B''.
assert (FSC B C D' C' B' C' D C).
unfold FSC.
repeat split; unfold Col; try Cong.
left; apply between_exchange3 with A; Between.
apply (eq_dec_implies_l2_11 eq_dec B C D' B' C' D); Cong.
apply between_exchange3 with A; assumption.
apply between_symmetry.
apply between_exchange3 with A; assumption.
apply cong_transitivity with C D; Cong.
apply cong_transitivity with C D; Cong.
induction (eq_dec B C).
subst C; auto.
assert (Cong D' C' D C) by (eapply eq_dec_implies_l4_16; try apply H12; assumption).
assert (∃ E, Bet C E C' ∧ Bet D E D') by (apply inner_pasch with A; Between).
ex_and H15 E.
assert (IFSC D E D' C D E D' C') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (IFSC C E C' D C E C' D') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (Cong E C E C') by (eapply eq_dec_implies_l4_2; try apply H17; auto).
assert (Cong E D E D') by (eapply eq_dec_implies_l4_2; try apply H18; auto).
induction (eq_dec C C').
subst C'; right; assumption.
show_distinct C D'; intuition.
prolong C' C P C D'.
prolong D' C R C E.
prolong P R Q R P.
assert (FSC D' C R P P C E D').
unfold FSC.
unfold Cong_3.
assert_cols.
repeat split; Cong.
apply eq_dec_implies_l2_11 with C C; Cong.
apply between_inner_transitivity with C'; Between.
assert (Cong R P E D') by (eauto using eq_dec_implies_l4_16).
assert (Cong R Q E D).
eapply cong_transitivity.
apply cong_transitivity with R P; Cong.
apply cong_transitivity with E D'; Cong.
assert (FSC D' E D C P R Q C).
unfold FSC.
repeat split; Cong.
unfold Col; Between.
eapply (eq_dec_implies_l2_11 eq_dec D' E D P R Q); Between; Cong.
assert (Cong D C Q C).
induction (eq_dec D' E).
unfold FSC, IFSC, Cong_3 in *; spliter; treat_equalities; Cong.
apply eq_dec_implies_l4_16 with D' E P R; assumption.
assert (Cong C P C Q).
unfold FSC in *;unfold Cong_3 in ×.
spliter.
apply cong_transitivity with C D.
apply cong_transitivity with C D'; Cong.
Cong.
show_distinct R C.
intuition.
assert (Cong D' P D' Q) by (apply (eq_dec_implies_l4_17 eq_dec R C); unfold Col; Between; Cong).
assert (Cong B P B Q).
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; right;right.
apply between_exchange3 with A; assumption.
assert (Cong B' P B' Q).
eapply (eq_dec_implies_l4_17 eq_dec C D'); Cong.
unfold Col; left.
apply between_exchange3 with A; assumption.
assert (Cong C' P C' Q).
induction(eq_dec B B').
subst B'.
unfold IFSC,FSC, Cong_3 in ×.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; left.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with B; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
eapply eq_dec_implies_l4_17 with B B'; Cong.
unfold Col; right; left.
apply between_symmetry.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
assert (Cong P P P Q).
apply eq_dec_implies_l4_17 with C C'; try assumption.
unfold Col; right; right.
apply between_symmetry; assumption.
unfold IFSC,FSC, Cong_3 in *; spliter.
treat_equalities.
Between.
Qed.
Lemma eq_dec_implies_l5_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D,
A≠B → Bet A B C → Bet A B D → Bet B C D ∨ Bet B D C.
Proof.
intros.
assert (Bet A C D ∨ Bet A D C) by (eapply eq_dec_implies_l5_1; eauto).
induction H3.
left; eBetween.
right; eBetween.
Qed.
Lemma eq_dec_implies_segment_construction_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A Q B C, A≠Q → ∃ X, (Bet Q A X ∨ Bet Q X A) ∧ Cong Q X B C.
Proof.
intro eq_dec; intros.
prolong A Q A' A Q.
prolong A' Q X B C.
∃ X.
show_distinct A' Q.
solve [intuition].
split; try assumption.
eapply (eq_dec_implies_l5_2 eq_dec A' Q); Between.
Qed.
Lemma eq_dec_implies_between_cong :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C, Bet A C B → Cong A C A B → C=B.
Proof.
intros.
assert (Bet A B C).
eapply eq_dec_implies_l4_6 with A C B; unfold Cong_3; repeat split; Cong.
eapply between_equality; eBetween.
Qed.
Lemma eq_dec_cong_dec :
(∀ A B:Tpoint, A=B ∨ A≠B) →
(∀ A B C D, Cong A B C D ∨ ¬ Cong A B C D).
Proof.
intro eq_dec; intros.
elim (eq_dec A B); intro; subst; elim (eq_dec C D); intro; subst.
left; Cong.
right; intro; apply H; apply cong_identity with B; Cong.
right; intro; apply H; apply cong_identity with D; Cong.
elim (eq_dec_implies_segment_construction_2 eq_dec B A C D).
intros D' HD'.
spliter.
elim (eq_dec B D');intro.
subst; left; assumption.
right; intro.
assert (Cong A D' A B) by eCong.
elim H1; intro; clear H1.
assert (B = D') by (apply (eq_dec_implies_between_cong eq_dec A D' B); Cong).
subst;intuition.
assert (D'=B) by (apply (eq_dec_implies_between_cong eq_dec A B D');assumption).
subst;intuition.
intuition.
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 eq_dec_implies_between_cong_3 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B D E, A ≠ B → Bet A B D → Bet A B E → Cong B D B E → D = E.
Proof.
intro eq_dec; intros.
assert (T:=eq_dec_implies_l5_2 eq_dec A B D E H H0 H1).
elim T; intro; clear T.
apply eq_dec_implies_between_cong with B; Cong.
symmetry; apply eq_dec_implies_between_cong with B; Cong.
Qed.
Lemma eq_dec_bet_dec :
(∀ A B:Tpoint, A=B ∨ A≠B) →
(∀ A B C, Bet A B C ∨ ¬ Bet A B C).
Proof.
intro eq_dec; intros.
elim (segment_construction A B B C); intros C' HC'.
spliter.
elim (eq_dec C C'); intro.
subst; tauto.
elim (eq_dec A B);intro.
left; subst; Between.
right; intro; apply H1; apply eq_dec_implies_between_cong_3 with A B; Cong.
Qed.
Definition decidability_of_equality_of_points := ∀ A B:Tpoint, A=B ∨ A≠B.
Definition decidability_of_congruence_of_points := ∀ A B C D:Tpoint,
Cong A B C D ∨ ¬ Cong A B C D.
Definition decidability_of_betweenness_of_points := ∀ A B C:Tpoint,
Bet A B C ∨ ¬ Bet A B C.
Theorem equivalence_between_decidability_properties_of_basic_relations :
all_equiv (decidability_of_equality_of_points::
decidability_of_congruence_of_points::
decidability_of_betweenness_of_points::nil).
Proof.
unfold all_equiv.
simpl.
intros.
assert (P:=cong_dec_eq_dec).
assert (Q:=eq_dec_cong_dec).
assert (R:=bet_dec_eq_dec).
assert (S:=eq_dec_bet_dec).
decompose [or] H;clear H;decompose [or] H0;clear H0;subst; tauto.
Qed.
End Equivalence_between_decidability_properties_of_basic_relations.
Require Import GeoCoq.Utils.all_equiv.
Section Equivalence_between_decidability_properties_of_basic_relations.
Context `{Tn:Tarski_neutral_dimensionless}.
Lemma cong_dec_eq_dec :
(∀ A B C D, Cong A B C D ∨ ¬ Cong A B C D) →
(∀ A B:Tpoint, A=B ∨ A≠B).
Proof.
intros H A B.
elim (H A B A A); intro HCong.
left; apply cong_identity with A; assumption.
right; intro; subst; apply HCong.
apply cong_pseudo_reflexivity.
Qed.
Lemma eq_dec_implies_l2_11 :
(∀ A B:Tpoint, A=B ∨ A≠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.
intro eq_dec; intros.
induction (eq_dec A B).
subst B.
assert (A' = B') by (apply (cong_identity A' B' A); Cong).
subst; Cong.
apply cong_commutativity; apply (five_segment A A' B B' C C' A A'); Cong.
Qed.
Lemma eq_dec_implies_construction_uniqueness :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ Q A B C X Y,
Q ≠ A → Bet Q A X → Cong A X B C → Bet Q A Y → Cong A Y B C → X=Y.
Proof.
intro eq_dec; intros.
assert (Cong A X A Y) by eCong.
assert (Cong Q X Q Y) by (apply (eq_dec_implies_l2_11 eq_dec Q A X Q A Y);Cong).
assert(OFSC Q A X Y Q A X X) by (unfold OFSC;repeat split;Cong).
apply five_segment_with_def in H6; try assumption.
apply cong_identity with X; Cong.
Qed.
Lemma eq_dec_implies_outer_transitivity_between2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D, Bet A B C → Bet B C D → B≠C → Bet A C D.
Proof.
intro eq_dec; intros.
prolong A C x C D.
assert (x = D) by (apply (eq_dec_implies_construction_uniqueness eq_dec B C C D); try apply (between_exchange3 A B C x); Cong).
subst x;assumption.
Qed.
Lemma eq_dec_implies_between_exchange4 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D, Bet A B C → Bet A C D → Bet A B D.
Proof.
intro eq_dec; intros.
induction (eq_dec B C); [subst; auto|].
apply between_symmetry;
apply eq_dec_implies_outer_transitivity_between2 with C; eBetween.
Qed.
Lemma eq_dec_implies_two_distinct_points :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∃ X, ∃ Y: Tpoint, X ≠ Y.
Proof.
intro eq_dec.
assert (ld:=lower_dim_ex).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
induction (eq_dec A B).
subst A; ∃ B; ∃ C; Between.
∃ A; ∃ B; assumption.
Qed.
Lemma eq_dec_implies_point_construction_different :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B, ∃ C, Bet A B C ∧ B ≠ C.
Proof.
intro eq_dec; intros.
assert (tdp := eq_dec_implies_two_distinct_points eq_dec).
ex_elim tdp x.
ex_elim H y.
prolong A B F x y.
∃ F.
show_distinct B F.
intuition.
intuition.
Qed.
Lemma eq_dec_implies_l4_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D A' B' C' D', IFSC A B C D A' B' C' D' → Cong B D B' D'.
Proof.
unfold IFSC.
intro eq_dec; intros.
spliter.
induction (eq_dec A C).
treat_equalities;assumption.
assert (∃ E, Bet A C E ∧ C ≠ E)
by (apply eq_dec_implies_point_construction_different; auto).
ex_and H6 E.
prolong A' C' E' C E.
assert (Cong E D E' D')
by (
apply (five_segment_with_def A C E D A' C' E' D');[
unfold OFSC; repeat split;Cong|
assumption]).
apply (five_segment_with_def E C B D E' C' B' D').
unfold OFSC.
repeat split; try solve [eBetween| Cong ].
auto.
Qed.
Lemma eq_dec_implies_l4_5 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C A' C',
Bet A B C → Cong A C A' C' →
∃ B', Bet A' B' C' ∧ Cong_3 A B C A' B' C'.
Proof.
intro eq_dec; intros.
unfold Cong_3.
assert (∃ D', Bet C' A' D' ∧ A' ≠ D')
by (apply eq_dec_implies_point_construction_different; auto).
ex_and H1 x'.
prolong x' A' B' A B.
prolong x' B' C'' B C.
assert (Bet A' B' C'') by eBetween.
assert (C'' = C').
eapply (eq_dec_implies_construction_uniqueness eq_dec x' A' ).
auto.
apply eq_dec_implies_between_exchange4 with B'; auto.
apply (eq_dec_implies_l2_11 eq_dec A' B' C'' A B C);Between.
eBetween.
Cong.
subst C''.
∃ B'.
repeat split;Cong.
Qed.
Lemma eq_dec_implies_l4_6 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C A' B' C', Bet A B C → Cong_3 A B C A' B' C' → Bet A' B' C'.
Proof.
unfold Cong_3.
intro eq_dec; intros.
assert (∃ B'', Bet A' B'' C' ∧ Cong_3 A B C A' B'' C')
by (eapply eq_dec_implies_l4_5;intuition).
ex_and H1 x.
unfold Cong_3 in *;spliter.
assert (Cong_3 A' x C' A' B' C')
by (unfold Cong_3;repeat split;eCong).
unfold Cong_3 in H7;spliter.
assert (IFSC A' x C' x A' x C' B')
by (unfold IFSC;repeat split;Cong).
assert (Cong x x x B')
by (eapply eq_dec_implies_l4_2; try apply H10; auto).
Between.
Qed.
Lemma eq_dec_implies_l4_16 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D A' B' C' D',
FSC A B C D A' B' C' D' → A≠B → Cong C D C' D'.
Proof.
unfold FSC.
unfold Col.
intro eq_dec; intros.
decompose [or and] H; clear H.
assert (Bet A' B' C') by (eapply eq_dec_implies_l4_6;eauto).
unfold Cong_3 in *; spliter.
assert(OFSC A B C D A' B' C' D') by (unfold OFSC;repeat split; assumption).
eapply five_segment_with_def; eauto.
assert(Bet B' C' A') by (apply (eq_dec_implies_l4_6 eq_dec B C A B' C' A'); Cong;auto with cong3).
apply (eq_dec_implies_l4_2 eq_dec B C A D B' C' A' D').
unfold IFSC; unfold Cong_3 in *; spliter; repeat split;Between;Cong.
assert (Bet C' A' B') by (eapply (eq_dec_implies_l4_6 eq_dec C A B C' A' B'); auto with cong3).
eapply (five_segment_with_def B A C D B' A'); unfold OFSC; unfold Cong_3 in *; spliter; repeat split; Between; Cong.
Qed.
Lemma eq_dec_implies_l4_17 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C P Q,
A≠B → Col A B C → Cong A P A Q → Cong B P B Q → Cong C P C Q.
Proof.
intros.
assert (FSC A B C P A B C Q) by (unfold FSC; unfold Cong_3; repeat split;Cong).
eapply eq_dec_implies_l4_16; eauto.
Qed.
Lemma eq_dec_implies_l5_1 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D,
A≠B → Bet A B C → Bet A B D → Bet A C D ∨ Bet A D C.
Proof.
intro eq_dec; intros.
prolong A D C' C D.
prolong A C D' C D.
prolong A C' B' C B.
prolong A D' B'' D B.
assert (Cong B C' B'' C).
apply (eq_dec_implies_l2_11 eq_dec B D C' B'' D' C).
apply between_exchange3 with A; Between.
apply between_inner_transitivity with A; Between.
Cong.
apply cong_transitivity with C D; Cong.
assert (Cong B B' B'' B).
{
apply (eq_dec_implies_l2_11 eq_dec B C' B' B'' C B); Cong.
{
assert (Bet A B C'); [|eBetween].
induction (eq_dec B D); [treat_equalities; auto|].
apply between_symmetry.
apply eq_dec_implies_outer_transitivity_between2 with D; eBetween.
}
{
induction (eq_dec C D'); [treat_equalities; eBetween|].
apply eq_dec_implies_outer_transitivity_between2 with D'; eBetween.
}
}
assert(B'' = B').
apply (eq_dec_implies_construction_uniqueness eq_dec A B B B''); try Cong.
apply eq_dec_implies_between_exchange4 with D'; Between;
apply eq_dec_implies_between_exchange4 with C; Between.
apply eq_dec_implies_between_exchange4 with C'; Between;
apply eq_dec_implies_between_exchange4 with D; Between.
subst B''.
assert (FSC B C D' C' B' C' D C).
unfold FSC.
repeat split; unfold Col; try Cong.
left; apply between_exchange3 with A; Between.
apply (eq_dec_implies_l2_11 eq_dec B C D' B' C' D); Cong.
apply between_exchange3 with A; assumption.
apply between_symmetry.
apply between_exchange3 with A; assumption.
apply cong_transitivity with C D; Cong.
apply cong_transitivity with C D; Cong.
induction (eq_dec B C).
subst C; auto.
assert (Cong D' C' D C) by (eapply eq_dec_implies_l4_16; try apply H12; assumption).
assert (∃ E, Bet C E C' ∧ Bet D E D') by (apply inner_pasch with A; Between).
ex_and H15 E.
assert (IFSC D E D' C D E D' C') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (IFSC C E C' D C E C' D') by (unfold IFSC; repeat split; Cong; apply cong_transitivity with C D; Cong).
assert (Cong E C E C') by (eapply eq_dec_implies_l4_2; try apply H17; auto).
assert (Cong E D E D') by (eapply eq_dec_implies_l4_2; try apply H18; auto).
induction (eq_dec C C').
subst C'; right; assumption.
show_distinct C D'; intuition.
prolong C' C P C D'.
prolong D' C R C E.
prolong P R Q R P.
assert (FSC D' C R P P C E D').
unfold FSC.
unfold Cong_3.
assert_cols.
repeat split; Cong.
apply eq_dec_implies_l2_11 with C C; Cong.
apply between_inner_transitivity with C'; Between.
assert (Cong R P E D') by (eauto using eq_dec_implies_l4_16).
assert (Cong R Q E D).
eapply cong_transitivity.
apply cong_transitivity with R P; Cong.
apply cong_transitivity with E D'; Cong.
assert (FSC D' E D C P R Q C).
unfold FSC.
repeat split; Cong.
unfold Col; Between.
eapply (eq_dec_implies_l2_11 eq_dec D' E D P R Q); Between; Cong.
assert (Cong D C Q C).
induction (eq_dec D' E).
unfold FSC, IFSC, Cong_3 in *; spliter; treat_equalities; Cong.
apply eq_dec_implies_l4_16 with D' E P R; assumption.
assert (Cong C P C Q).
unfold FSC in *;unfold Cong_3 in ×.
spliter.
apply cong_transitivity with C D.
apply cong_transitivity with C D'; Cong.
Cong.
show_distinct R C.
intuition.
assert (Cong D' P D' Q) by (apply (eq_dec_implies_l4_17 eq_dec R C); unfold Col; Between; Cong).
assert (Cong B P B Q).
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; right;right.
apply between_exchange3 with A; assumption.
assert (Cong B' P B' Q).
eapply (eq_dec_implies_l4_17 eq_dec C D'); Cong.
unfold Col; left.
apply between_exchange3 with A; assumption.
assert (Cong C' P C' Q).
induction(eq_dec B B').
subst B'.
unfold IFSC,FSC, Cong_3 in ×.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.
apply eq_dec_implies_l4_17 with C D'; try assumption.
unfold Col; left.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with B; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
eapply eq_dec_implies_l4_17 with B B'; Cong.
unfold Col; right; left.
apply between_symmetry.
apply between_exchange3 with A; try assumption.
apply eq_dec_implies_between_exchange4 with D; assumption.
assert (Cong P P P Q).
apply eq_dec_implies_l4_17 with C C'; try assumption.
unfold Col; right; right.
apply between_symmetry; assumption.
unfold IFSC,FSC, Cong_3 in *; spliter.
treat_equalities.
Between.
Qed.
Lemma eq_dec_implies_l5_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C D,
A≠B → Bet A B C → Bet A B D → Bet B C D ∨ Bet B D C.
Proof.
intros.
assert (Bet A C D ∨ Bet A D C) by (eapply eq_dec_implies_l5_1; eauto).
induction H3.
left; eBetween.
right; eBetween.
Qed.
Lemma eq_dec_implies_segment_construction_2 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A Q B C, A≠Q → ∃ X, (Bet Q A X ∨ Bet Q X A) ∧ Cong Q X B C.
Proof.
intro eq_dec; intros.
prolong A Q A' A Q.
prolong A' Q X B C.
∃ X.
show_distinct A' Q.
solve [intuition].
split; try assumption.
eapply (eq_dec_implies_l5_2 eq_dec A' Q); Between.
Qed.
Lemma eq_dec_implies_between_cong :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B C, Bet A C B → Cong A C A B → C=B.
Proof.
intros.
assert (Bet A B C).
eapply eq_dec_implies_l4_6 with A C B; unfold Cong_3; repeat split; Cong.
eapply between_equality; eBetween.
Qed.
Lemma eq_dec_cong_dec :
(∀ A B:Tpoint, A=B ∨ A≠B) →
(∀ A B C D, Cong A B C D ∨ ¬ Cong A B C D).
Proof.
intro eq_dec; intros.
elim (eq_dec A B); intro; subst; elim (eq_dec C D); intro; subst.
left; Cong.
right; intro; apply H; apply cong_identity with B; Cong.
right; intro; apply H; apply cong_identity with D; Cong.
elim (eq_dec_implies_segment_construction_2 eq_dec B A C D).
intros D' HD'.
spliter.
elim (eq_dec B D');intro.
subst; left; assumption.
right; intro.
assert (Cong A D' A B) by eCong.
elim H1; intro; clear H1.
assert (B = D') by (apply (eq_dec_implies_between_cong eq_dec A D' B); Cong).
subst;intuition.
assert (D'=B) by (apply (eq_dec_implies_between_cong eq_dec A B D');assumption).
subst;intuition.
intuition.
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 eq_dec_implies_between_cong_3 :
(∀ A B:Tpoint, A=B ∨ A≠B) →
∀ A B D E, A ≠ B → Bet A B D → Bet A B E → Cong B D B E → D = E.
Proof.
intro eq_dec; intros.
assert (T:=eq_dec_implies_l5_2 eq_dec A B D E H H0 H1).
elim T; intro; clear T.
apply eq_dec_implies_between_cong with B; Cong.
symmetry; apply eq_dec_implies_between_cong with B; Cong.
Qed.
Lemma eq_dec_bet_dec :
(∀ A B:Tpoint, A=B ∨ A≠B) →
(∀ A B C, Bet A B C ∨ ¬ Bet A B C).
Proof.
intro eq_dec; intros.
elim (segment_construction A B B C); intros C' HC'.
spliter.
elim (eq_dec C C'); intro.
subst; tauto.
elim (eq_dec A B);intro.
left; subst; Between.
right; intro; apply H1; apply eq_dec_implies_between_cong_3 with A B; Cong.
Qed.
Definition decidability_of_equality_of_points := ∀ A B:Tpoint, A=B ∨ A≠B.
Definition decidability_of_congruence_of_points := ∀ A B C D:Tpoint,
Cong A B C D ∨ ¬ Cong A B C D.
Definition decidability_of_betweenness_of_points := ∀ A B C:Tpoint,
Bet A B C ∨ ¬ Bet A B C.
Theorem equivalence_between_decidability_properties_of_basic_relations :
all_equiv (decidability_of_equality_of_points::
decidability_of_congruence_of_points::
decidability_of_betweenness_of_points::nil).
Proof.
unfold all_equiv.
simpl.
intros.
assert (P:=cong_dec_eq_dec).
assert (Q:=eq_dec_cong_dec).
assert (R:=bet_dec_eq_dec).
assert (S:=eq_dec_bet_dec).
decompose [or] H;clear H;decompose [or] H0;clear H0;subst; tauto.
Qed.
End Equivalence_between_decidability_properties_of_basic_relations.