Library GeoCoq.Tarski_dev.Ch06_out_lines

Require Export GeoCoq.Tarski_dev.Ch05_bet_le.

Ltac eCol := eauto with col.

Section T6_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma bet_out : A B C, B A Bet A B C Out A B C.
Proof.
intros.
unfold Out.
repeat split; auto.
intro; treat_equalities; auto.
Qed.

Lemma out_dec : P A B, Out P A B ¬ Out P A B.
Proof.
intros.
unfold Out.
elim (bet_dec P A B);intro; elim (bet_dec P B A);intro; elim (eq_dec_points A P);intro; elim (eq_dec_points B P);intro; tauto.
Qed.

Lemma out_diff1 : A B C, Out A B C B A.
Proof.
intros.
unfold Out in H.
spliter.
assumption.
Qed.

Lemma out_diff2 : A B C, Out A B C C A.
Proof.
intros.
unfold Out in H.
spliter.
assumption.
Qed.

Lemma out_distinct : A B C, Out A B C B A C A.
Proof.
intros.
split.
eapply out_diff1;eauto.
eapply out_diff2;eauto.
Qed.

Lemma out_col : A B C, Out A B C Col A B C.
Proof.
intros.
unfold Col.
unfold Out in H.
spliter.
induction H1;Between.
Qed.

Lemma l6_2 : A B C P, AP BP CP Bet A P C (Bet B P C Out P A B).
Proof.
intros.
unfold Out.
split.
intros.
repeat split; try assumption; eapply l5_2;eBetween.
intro; spliter; induction H5; eBetween.
Qed.

Lemma bet_out__bet : A B C P, Bet A P C Out P A B Bet B P C.
Proof.
intros A B C P HBet HOut.
destruct (eq_dec_points C P).
subst; Between.
apply (l6_2 A); trivial; destruct HOut as [HPA [HPB]]; auto.
Qed.

Lemma l6_3_1 : A B P, Out P A B (AP BP C, CP Bet A P C Bet B P C).
Proof.
unfold Out.
intros.
spliter.
repeat split; try assumption.
induction H1.
assert( C, Bet A P C P C) by (apply point_construction_different).
ex_and H2 C.
C.
repeat split; eBetween.
assert( C, Bet B P C P C) by (apply point_construction_different).
ex_and H2 C.
C.
repeat split;eBetween.
Qed.

Lemma l6_3_2 : A B P,
(AP BP C, CP Bet A P C Bet B P C) Out P A B.
Proof.
intros.
spliter.
ex_and H1 C.
unfold Out.
repeat split; try assumption; eapply l5_2; eBetween.
Qed.

Lemma l6_4_1 : A B P, Out P A B Col A P B ¬ Bet A P B.
Proof.
unfold Out.
intros.
spliter.
unfold Col.
induction H1; split.
Between.
intro; apply H; eapply between_equality;eauto.
right; left; assumption.
intro; apply H0; eapply between_equality; eBetween.
Qed.

Lemma l6_4_2 : A B P, Col A P B ¬ Bet A P B Out P A B.
Proof.
unfold Col.
intros.
spliter.
unfold Out.
induction H.
induction (eq_dec_points A P).
subst P; intuition.
induction (eq_dec_points B P).
subst P; intuition.
induction H; repeat split; Between.
Qed.

out reflexivity. l6_5

Lemma out_trivial : P A, AP Out P A A.
Proof.
intros.
unfold Out.
repeat split; Between.
Qed.

out symmetry.

Lemma l6_6 : P A B, Out P A B Out P B A.
Proof.
unfold Out.
intuition.
Qed.

out transitivity.

Lemma l6_7 : P A B C, Out P A B Out P B C Out P A C.
Proof.
unfold Out.
intros.
spliter.
repeat split; try assumption.
induction H4; induction H2.
left; eapply between_exchange4; eauto.
eapply l5_3; eauto.
eapply (l5_1 P B); auto.
right; eBetween.
Qed.

Lemma bet_out_out_bet : A B C A' C',
Bet A B C Out B A A' Out B C C' Bet A' B C'.
Proof.
intros.
unfold Out in ×.
spliter.
induction H5; induction H3.
assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
apply outer_transitivity_between with C; auto.
assert(Bet A' B C) by (apply outer_transitivity_between2 with A; Between).
apply between_inner_transitivity with C; assumption.
assert(Bet A' B C) by (apply between_exchange3 with A; Between).
apply outer_transitivity_between with C; auto.
assert(Bet A' B C) by (apply between_exchange3 with A; Between).
eapply between_inner_transitivity with C; assumption.
Qed.

Lemma out2_bet_out : A B C X P,
Out B A C Out B X P Bet A X C Out B A P Out B C P.
Proof.
intros.
unfold Out in ×.
spliter.
induction H5; induction H3.
repeat split; try assumption.
left; eapply between_exchange4 with X; try assumption.
apply between_inner_transitivity with C; assumption.
apply l5_1 with X; try auto.
apply between_exchange2 with A; assumption.
repeat split; try assumption.
apply l5_3 with X; try assumption.
apply between_inner_transitivity with C; assumption.
right; apply between_exchange4 with X; try assumption.
apply between_exchange2 with A; assumption.
repeat split; try assumption.
apply l5_1 with X; try auto.
apply between_exchange2 with C; Between.
left; apply between_exchange4 with X; try assumption.
apply between_inner_transitivity with A; Between.
repeat split; try assumption.
right; apply between_exchange4 with X; try assumption.
apply between_exchange2 with C; Between.
apply l5_3 with X; try assumption.
apply between_inner_transitivity with A; Between.
Qed.

Lemma l6_11_uniqueness : A B C R X Y,
RA BC
Out A X R Cong A X B C
Out A Y R Cong A Y B C
X=Y.
Proof.
unfold Out.
intros.
spliter.
assert (Cong A X A Y) by eCong.
induction H8; induction H6.
apply l4_19 with A R; try assumption.
apply l4_3 with A A; Between; Cong.
assert (Bet A X Y) by eBetween.
eapply between_cong; eauto.
assert (Bet A Y X) by eBetween.
apply sym_equal; apply between_cong with A; Cong.
assert (Bet A X Y Bet A Y X) by (eapply l5_1; eauto).
induction H10.
apply between_cong with A; assumption.
apply sym_equal; apply between_cong with A; Cong.
Qed.

Lemma l6_11_existence : A B C R,
RA BC X, Out A X R Cong A X B C.
Proof.
intros.
assert ( X : Tpoint, (Bet A R X Bet A X R) Cong A X B C) by (apply (segment_construction_2);assumption).
ex_and H1 X.
X.
unfold Out;repeat split; try intro;treat_equalities;intuition.
Qed.

Lemma segment_construction_3 : A B X Y, A B X Y C, Out A B C Cong A C X Y.
Proof.
intros.
destruct (l6_11_existence A X Y B) as [C [HC1 HC2]]; auto.
apply l6_6 in HC1.
C; auto.
Qed.

Lemma l6_13_1 : P A B, Out P A B Le
P A P B Bet P A B.
Proof.
unfold Out.
intros.
spliter.
induction H2; try assumption.
unfold Le
in H0.
ex_and H0 Y.
assert(Y = A).
apply (l6_11_uniqueness P P A B); Between; Cong.
unfold Out; repeat split; auto.
intro; treat_equalities; auto.
unfold Out; repeat split; auto.
subst Y; assumption.
Qed.

Lemma l6_13_2 : P A B, Out P A B Bet P A B Le
P A P B.
Proof.
intros.
unfold Le.
A.
split; Cong.
Qed.

Lemma l6_16_1 : P Q S X, PQ SP Col S P Q Col X P Q Col X P S.
Proof.
intros.
assert((Bet P S X Bet P X S) (Bet P S X Bet S X P)) by (intro; induction H3; Between).
unfold Col.
induction H1;induction H2.
right; apply H3; eapply (l5_2 Q P); Between.
induction H2; left; eBetween.
induction H1; left; eBetween.
induction H1; induction H2.
right; apply H3; eapply l5_1; eauto.
right; right; eBetween.
right; left; eBetween.
right; apply H3; eapply l5_3; eBetween.
Qed.

Lemma col_transitivity_1 : P Q A B,
PQ Col P Q A Col P Q B Col P A B.
Proof.
intros.
induction (eq_dec_points A P).
subst; unfold Col; Between.
assert (T:=l6_16_1 P Q A B).
apply col_permutation_1; apply T; Col.
Qed.

Lemma col_transitivity_2 : P Q A B,
PQ Col P Q A Col P Q B Col Q A B.
Proof.
intros.
apply (col_transitivity_1 Q P A B);Col.
Qed.

Unicity of intersection

Lemma l6_21 : A B C D P Q,
¬ Col A B C CD Col A B P Col A B Q Col C D P Col C D Q P=Q.
Proof.
intros.
elim (eq_dec_points P Q); intro; try assumption.
cut False.
intro; intuition.
apply not_col_distincts in H.
spliter.
assert (Col C P Q) by (apply col_transitivity_1 with D; Col).
assert (Col Q B C).
induction (eq_dec_points Q A).
subst; apply col_transitivity_1 with P; Col.
apply col_transitivity_1 with P; try Col; apply col_permutation_1; apply col_transitivity_1 with A; Col.
assert (Col A B C).
induction (eq_dec_points Q A).
subst Q; assumption.
induction (eq_dec_points Q B).
subst; apply col_permutation_2; apply col_transitivity_1 with P; try Col.
apply col_permutation_2; apply col_transitivity_1 with Q; try Col.
Qed.

End T6_1.

Hint Resolve col_transitivity_1 col_transitivity_2 out_col : col.

Section T6_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma not_col_exists : A B,
AB C, ¬ Col A B C.
Proof.
intros.
assert (T:=lower_dim_ex).
induction T.
induction H0.
induction H0.
induction (Col_dec A B x).
induction(Col_dec A B x0).
induction(Col_dec A B x1).
induction (eq_dec_points A x).
assert (~(Col x x0 x1)) by (unfold Col; auto).
treat_equalities; eCol.
assert (Col A x x0) by eCol.
assert (Col A x x1) by eCol.
assert (Col A x0 x1) by eCol.
assert (Col x x0 x1) by eCol.
x1; assumption.
x0; assumption.
x; assumption.
Qed.

Lemma col3 : X Y A B C,
X Y
Col X Y A Col X Y B Col X Y C
Col A B C.
Proof.
intros.
assert (Col X A B) by (apply col_transitivity_1 with Y; assumption).
induction(eq_dec_points C X).
subst X; apply col_permutation_1; assumption.
apply col_permutation_1.
apply col_transitivity_1 with X; try assumption.
apply col_permutation_2.
apply col_transitivity_1 with Y; assumption.
apply col_permutation_2.
apply col_transitivity_1 with Y; assumption.
Qed.

Lemma out2__bet : A B C, Out A B C Out C A B Bet A B C.
Proof.
intros A B C Hout1 Hout2.
apply l6_4_1 in Hout2.
destruct Hout2 as [_ Hout2].
destruct Hout1 as [_ [_ [|]]].
assumption.
exfalso.
apply Hout2.
assumption.
Qed.

Lemma bet2_le2__le1346 : A B C A' B' C', Bet A B C Bet A' B' C' Le
A B A' B' Le
B C B' C'
Le
A C A' C'.
Proof.
intros A B C A' B' C' HBet HBet' HleAB HleBC.

elim(eq_dec_points A B).
{ intro.
subst B.
apply (le_transitivity _ _ B' C'); auto.
apply le_comm.
B'.
split; Between; Cong.
}
intro.
elim(eq_dec_points B C).
{ intro.
subst C.
apply (le_transitivity _ _ A' B'); auto.
B'; Cong.
}
intro.

assert(A' B') by (intro; subst B'; assert(A = B); auto; apply (le_zero _ _ A'); auto).
assert(B' C') by (intro; subst C'; assert(B = C); auto; apply (le_zero _ _ B'); auto).
destruct HleAB as [B0 []].
assert(A' B0) by (intro; subst B0; assert(A = B); auto; apply (cong_reverse_identity A'); Cong).
assert(HC0 := segment_construction A' B0 B C).
destruct HC0 as [C0 []].
assert(B0 C0) by (intro; subst C0; assert(B = C); auto; apply (cong_reverse_identity B0); auto).
C0.
split.
2: apply (l2_11 _ B _ _ B0); Cong.
apply (outer_transitivity_between2 _ B0); auto.
assert(Bet B0 B' C') by (apply between_symmetry; apply (between_inner_transitivity _ _ _ A'); Between).
apply l6_13_1.
- elim(eq_dec_points B0 B').
{ intro.
subst.
apply (l6_2 _ _ A'); Between.
}
intro.
apply (l6_7 _ _ B').
apply (l6_2 _ _ A'); Between.
apply bet_out; auto.
- apply (le_transitivity _ _ B' C').
apply (l5_6 B C B' C'); Cong.
apply le_comm.
B'.
split; Between; Cong.
Qed.

Lemma bet2_le2__le2356 : A B C A' B' C', Bet A B C Bet A' B' C'
Le A B A' B' Le A' C' A C Le B' C' B C.
Proof.
intros A B C A' B' C' HBet HBet' HLe1 HLe2.
elim(eq_dec_points A B).
{ intro; treat_equalities.
apply (le_transitivity _ _ A' C'); auto.
destruct (l5_12_a A' B' C'); auto.
}
intro.
assert (AC) by (intro; treat_equalities; auto).
destruct (l5_5_1 A B A' B' HLe1) as [B0 [HBet1 HCong1]].
assert (AB0) by (intro; treat_equalities; auto).
destruct HLe2 as [C0 [HBet2 HCong2]].
assert (AC0) by (intro; treat_equalities; auto).
assert (Bet A B0 C0).
{ apply l6_13_1.
apply (l6_7 _ _ B); [|apply (l6_7 _ _ C)]; [apply l6_6| |apply l6_6]; apply bet_out; auto.
apply (l5_6 A' B' A' C'); Cong.
destruct (l5_12_a A' B' C'); auto.
}
apply (l5_6 B0 C0 B C); Cong; [apply (le_transitivity _ _ B C0)|].
destruct (l5_12_a B B0 C0); eBetween.
destruct (l5_12_a B C0 C); eBetween.
apply cong_commutativity; apply (l4_3 _ _ A _ _ A'); Between; Cong.
Qed.

Lemma bet2_le2__le1245 : A B C A' B' C', Bet A B C Bet A' B' C'
Le B C B' C' Le A' C' A C Le A' B' A B.
Proof.
intros A B C A' B' C'; intros.
apply le_comm.
apply (bet2_le2__le2356 C _ _ C'); Le; Between.
Qed.

Lemma cong_preserves_bet : B A' A0 E D' D0,
Bet B A' A0 Cong B A' E D' Cong B A0 E D0 Out E D' D0
Bet E D' D0.
Proof.
intros.
unfold Out in H2.
spliter.
induction H4.
assumption.
assert (Le
E D0 E D').
eapply l5_5_2.
D'.
split.
assumption.
Cong.
assert(Le
E D' E D0).
eapply l5_6.
repeat split.
2:apply H0.
2:apply H1.
eapply l5_5_2.
A0.
split.
assumption.
Cong.
assert(Cong E D' E D0).
apply le_anti_symmetry.
assumption.
assumption.
assert(D0 = D').
eapply between_cong.
apply H4.
Cong.
subst D'.
Between.
Qed.

Lemma out_cong_cong : B A A0 E D D0,
Out B A A0 Out E D D0
Cong B A E D Cong B A0 E D0
Cong A A0 D D0.
Proof.
intros.
unfold Out in H.
spliter.
induction H4.
assert (Bet E D D0).
eapply cong_preserves_bet.
2:apply H1.
2:apply H2.
assumption.
assumption.
apply cong_commutativity.
eapply l4_3.
apply between_symmetry.
apply H4.
apply between_symmetry.
apply H5.
Cong.
Cong.
assert (Bet E D0 D).
eapply cong_preserves_bet.
2:apply H2.
2:apply H1.
assumption.
apply l6_6.
assumption.
eapply l4_3;eBetween;Cong.
Qed.

Lemma not_out_bet : A B C, Col A B C ¬ Out B A C Bet A B C.
Proof.
intros.
unfold Out in H0.
induction (eq_dec_points A B).
subst.
Between.
induction (eq_dec_points B C).
subst.
Between.
unfold Col in ×.
decompose [or] H;clear H.
assumption.
exfalso.
apply H0.
intuition.
exfalso.
apply H0.
intuition.
Qed.

Lemma or_bet_out : A B C, Bet A B C Out B A C ¬Col A B C.
Proof.
intros.
destruct (Col_dec A B C); auto.
destruct (out_dec B A C); auto.
left; apply not_out_bet; trivial.
Qed.

Lemma not_bet_out : A B C,
Col A B C ¬Bet A B C Out B A C.
Proof.
intros.
destruct (or_bet_out A B C) as [HBet|[HOut|HNCol]]; trivial; contradiction.
Qed.

Lemma not_bet_and_out :
A B C,
¬ (Bet A B C Out B A C).
Proof.
intros.
intro.
spliter.
unfold Out in H0.
spliter.
induction H2.
assert ( A = B).
eapply between_equality.
apply H.
assumption.
assert(C = B).
eapply between_equality.
apply between_symmetry.
apply H.
assumption.
Qed.

Lemma out_to_bet :
A B C A' B' C',
Col A' B' C'
(Out B A C Out B' A' C')
Bet A B C
Bet A' B' C'.
Proof.
intros.
induction(out_dec B A C).
unfold Out in H2.
spliter.
induction H4.
assert( A = B).
eapply between_equality.
apply H1.
assumption.
assert(C = B).
apply(between_symmetry) in H4.
eapply between_equality.
apply between_symmetry.
apply H1.
apply between_symmetry.
assumption.
destruct H0.
assert (¬Out B' A' C').
intro.
apply H2.
apply H3.
assumption.
apply not_out_bet.
assumption.
assumption.
Qed.

Lemma col_out2_col : A B C AA CC, Col A B C Out B A AA Out B C CC Col AA B CC.
Proof.
intros.
induction H.
assert (Bet AA B CC).
eapply bet_out_out_bet.
apply H.
assumption.
assumption.
unfold Col.
left.
assumption.
induction H.
assert(Out B AA CC).
eapply l6_7.
eapply l6_6.
apply H0.
apply l6_6.
eapply l6_7.
apply l6_6.
apply H1.
apply bet_out.
unfold Out in ×.
spliter.
assumption.
unfold Out in ×.
spliter.
assumption.
apply col_permutation_4.
apply out_col.
assumption.
assert(Out B AA CC).
eapply l6_6.
eapply l6_7.
eapply l6_6.
apply H1.
eapply l6_6.
eapply l6_7.
eapply l6_6.
apply H0.
apply bet_out.
unfold Out in ×.
spliter.
assumption.
unfold Out in ×.
spliter.
apply between_symmetry.
assumption.
apply col_permutation_4.
apply out_col.
assumption.
Qed.

Lemma bet2_out_out : A B C B' C', B A B' A Out A C C' Bet A B C Bet A B' C' Out A B B'.
Proof.
intros.
induction(eq_dec_points B' C').
subst C'.
unfold Out in ×.
spliter.
repeat split; try assumption.
induction H5.
left.
eapply between_exchange4.
apply H2.
assumption.
eapply l5_3.
apply H2.
assumption.
unfold Out in ×.
spliter.
repeat split.
assumption.
assumption.
induction H6.
assert(Bet A B C').
eapply between_exchange4.
apply H2.
assumption.
eapply l5_3.
apply H7.
assumption.
assert(Bet B' C' C).
eapply between_exchange3.
apply H3.
assumption.
assert(Bet A B' C).
eapply outer_transitivity_between.
apply H3.
assumption.
assumption.
eapply l5_3.
apply H2.
assumption.
Qed.

Lemma out2_out_1 : B C D X,
Out B X C Out B X D Out B C D.
Proof.
intros.
unfold Out in ×.
spliter.
repeat split.
assumption.
assumption.
induction H2; induction H4.
eapply l5_1.
2: apply H4.
auto.
assumption.
left.
eapply between_exchange4.
apply H4.
assumption.
right.
eapply between_exchange4.
apply H2.
assumption.
eapply l5_3.
apply H4.
apply H2.
Qed.

Lemma out2_out_2 : B C D X,
Out B C X Out B D X Out B C D.
Proof.
intros.
eapply out2_out_1.
apply l6_6.
apply H.
apply l6_6.
assumption.
Qed.

Lemma out_bet_out_1 : A B C P,
Out P A C Bet A B C Out P A B.
Proof.
intros.
induction (eq_dec_points B P).
subst P.
apply False_ind.
apply (not_bet_and_out A B C).
split; assumption.
unfold Out in ×.
spliter.
repeat split.
assumption.
assumption.
induction H3.
left.
eapply between_inner_transitivity.
apply H3.
assumption.
right.
eapply between_exchange2.
apply H3.
apply between_symmetry.
assumption.
Qed.

Lemma out_bet_out_2 : A B C P,
Out P A C Bet A B C Out P B C.
Proof.
intros.
apply l6_6.
eapply out_bet_out_1.
apply l6_6.
apply H.
apply between_symmetry.
assumption.
Qed.

Lemma out_bet__out : A B P Q,
Bet P Q A Out Q A B Out P A B.
Proof.
intros A B P Q HBet Hout.
destruct Hout as [HAQ [HBQ [HQAB|HQBA]]]; [|apply l6_6];
apply bet_out; eBetween; intro; treat_equalities; auto.
apply HBQ; apply (between_equality _ _ A); Between.
Qed.

End T6_2.

Hint Resolve bet_out out_trivial l6_6 : out.