Library out_lines
Require Export bet_le.
Section T6.
Context `{M:Tarski}.
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 smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
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 : Between.
Hint Resolve 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.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition IFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A C A' C' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong C D C' D'.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Definition out := fun P A B => A<>P /\ B<>P /\ (Bet P A B \/ Bet P B A).
Lemma out_diff1 : forall A B C, out A B C -> B <> A.
Proof.
intros.
unfold out in H.
spliter.
assumption.
Qed.
Lemma out_diff2 : forall A B C, out A B C -> C <> A.
Proof.
intros.
unfold out in H.
spliter.
assumption.
Qed.
Lemma out_col : forall 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 : forall A B C P, A<>P -> B<>P -> C<>P -> Bet A P C -> (Bet B P C <-> out P A B).
Proof.
intros.
unfold out.
split.
intros.
repeat split.
assumption.
assumption.
eapply l5_2;eBetween.
intro.
spliter;induction H5;eBetween.
Qed.
Lemma l6_3_1 : forall A B P, out P A B -> (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C).
Proof.
unfold out.
intros.
spliter.
repeat split.
assumption.
assumption.
induction H1.
assert(exists C, Bet A P C /\ P <> C)
by (apply point_construction_different).
ex_and H2 C.
exists C.
repeat split.
intro.
treat_equalities;intuition.
assumption.
eBetween.
assert(exists C, Bet B P C /\ P <> C)
by (apply point_construction_different).
ex_and H2 C.
exists C.
repeat split;eBetween.
Qed.
Lemma l6_3_2 : forall A B P,
(A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C) -> out P A B.
Proof.
intros.
spliter.
ex_and H1 C.
unfold out.
repeat split.
assumption.
assumption.
eapply l5_2;eBetween.
Qed.
Lemma l6_4_1 : forall 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_egality;eauto.
right;left.
assumption.
intro.
apply H0.
eapply between_egality;eBetween.
Qed.
Lemma l6_4_2 : forall A B P, Col A P B /\ ~ Bet A P B -> out P A B.
Proof.
unfold Col.
intros.
spliter.
unfold out.
induction H.
contradiction.
induction (eq_dec_points A P).
subst P.
intuition.
induction (eq_dec_points B P).
subst P.
intuition.
induction H;repeat split;Between.
Qed.
Section T6.
Context `{M:Tarski}.
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 smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.
Ltac treat_equalities_aux :=
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 : Between.
Hint Resolve 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.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition IFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A C A' C' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong C D C' D'.
Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
cong_left_commutativity cong_right_commutativity
cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Ltac Col := auto with Col.
Ltac eCol := eauto with Col.
Definition out := fun P A B => A<>P /\ B<>P /\ (Bet P A B \/ Bet P B A).
Lemma out_diff1 : forall A B C, out A B C -> B <> A.
Proof.
intros.
unfold out in H.
spliter.
assumption.
Qed.
Lemma out_diff2 : forall A B C, out A B C -> C <> A.
Proof.
intros.
unfold out in H.
spliter.
assumption.
Qed.
Lemma out_col : forall 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 : forall A B C P, A<>P -> B<>P -> C<>P -> Bet A P C -> (Bet B P C <-> out P A B).
Proof.
intros.
unfold out.
split.
intros.
repeat split.
assumption.
assumption.
eapply l5_2;eBetween.
intro.
spliter;induction H5;eBetween.
Qed.
Lemma l6_3_1 : forall A B P, out P A B -> (A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C).
Proof.
unfold out.
intros.
spliter.
repeat split.
assumption.
assumption.
induction H1.
assert(exists C, Bet A P C /\ P <> C)
by (apply point_construction_different).
ex_and H2 C.
exists C.
repeat split.
intro.
treat_equalities;intuition.
assumption.
eBetween.
assert(exists C, Bet B P C /\ P <> C)
by (apply point_construction_different).
ex_and H2 C.
exists C.
repeat split;eBetween.
Qed.
Lemma l6_3_2 : forall A B P,
(A<>P /\ B<>P /\ exists C, C<>P /\ Bet A P C /\ Bet B P C) -> out P A B.
Proof.
intros.
spliter.
ex_and H1 C.
unfold out.
repeat split.
assumption.
assumption.
eapply l5_2;eBetween.
Qed.
Lemma l6_4_1 : forall 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_egality;eauto.
right;left.
assumption.
intro.
apply H0.
eapply between_egality;eBetween.
Qed.
Lemma l6_4_2 : forall A B P, Col A P B /\ ~ Bet A P B -> out P A B.
Proof.
unfold Col.
intros.
spliter.
unfold out.
induction H.
contradiction.
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 : forall P A, A<>P -> out P A A.
Proof.
intros.
unfold out.
repeat split;Between.
Qed.
out symmetry.
out transitivity.
Lemma l6_7 : forall P A B C, out P A B -> out P B C -> out P A C.
Proof.
unfold out.
intros.
spliter.
repeat split.
assumption.
assumption.
induction H4.
induction H2.
left.
eapply between_exchange4;eauto.
eapply l5_3;eauto.
induction H2.
eapply (l5_1 P B);auto.
right;eBetween.
Qed.
Hint Resolve out_trivial l6_6 l6_7 : Out.
Lemma bet_out_out_bet : forall A B C A' C', Bet A B C -> out B A A' -> out B C C' -> Bet A' B C'.
intros.
unfold out in *.
spliter.
induction H5; induction H3.
assert(Bet A' B C).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H5.
assumption.
assumption.
eapply outer_transitivity_between.
apply H6.
assumption.
auto.
assert(Bet A' B C).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H5.
assumption.
assumption.
eapply between_inner_transitivity.
apply H6.
assumption.
assert(Bet A' B C).
eapply between_exchange3.
apply between_symmetry.
apply H5.
assumption.
eapply outer_transitivity_between.
apply H6.
assumption.
auto.
assert(Bet A' B C).
eapply between_exchange3.
apply between_symmetry.
apply H5.
assumption.
eapply between_inner_transitivity.
apply H6.
assumption.
Qed.
Lemma out2_bet_out : forall 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.
intros.
unfold out in *.
spliter.
induction H5; induction H3.
repeat split; try assumption.
left.
eapply between_exchange4.
eapply between_inner_transitivity.
apply H5.
apply H1.
assumption.
eapply l5_1.
3: apply H3.
auto.
eapply between_exchange2.
apply H5.
assumption.
repeat split; try assumption.
eapply l5_3.
2:apply H3.
eapply between_inner_transitivity.
apply H5.
assumption.
right.
eapply between_exchange4.
apply H3.
eapply between_exchange2.
apply H5.
assumption.
repeat split; try assumption.
eapply l5_1.
3: apply H3.
auto.
eapply between_exchange2.
apply H5.
apply between_symmetry.
assumption.
left.
eapply between_exchange4.
2:apply H3.
eapply between_inner_transitivity.
apply H5.
apply between_symmetry.
assumption.
repeat split; try assumption.
right.
eapply between_exchange4.
apply H3.
eapply between_exchange2.
apply H5.
apply between_symmetry.
assumption.
eapply l5_3.
2: apply H3.
eapply between_inner_transitivity.
apply H5.
apply between_symmetry.
assumption.
Qed.
Lemma l6_11_unicity : forall A B C R X Y,
R<>A -> B<>C -> 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).
eapply cong_transitivity.
apply H2.
apply cong_symmetry.
assumption.
induction H8;
induction H6.
eapply l4_19.
apply H8.
assumption.
eapply l4_3.
apply between_symmetry.
apply H8.
apply between_symmetry.
apply H6.
apply cong_reflexivity.
apply cong_commutativity.
assumption.
assert (Bet A X Y) by eBetween.
eapply between_cong;eauto.
assert (Bet A Y X) by eBetween.
apply sym_equal.
eapply between_cong.
apply H10.
Cong.
assert (Bet A X Y \/ Bet A Y X).
eapply l5_1;eauto.
induction H10.
eapply between_cong.
apply H10.
assumption.
apply sym_equal.
eapply between_cong.
apply H10.
apply cong_symmetry.
assumption.
Qed.
Lemma l6_11_existence : forall A B C R,
R<>A -> B<>C -> exists X, out A X R /\ Cong A X B C.
Proof.
intros.
assert (exists 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.
exists X.
unfold out;repeat split;
try intro;treat_equalities;intuition.
Qed.
Lemma l6_13_1 : forall P A B, out P A B -> le P A P B -> Bet P A B.
Proof.
unfold out.
intros.
spliter.
induction H2.
assumption.
unfold le in H0.
ex_and H0 Y.
assert(Y = A).
eapply l6_11_unicity.
4: apply cong_symmetry.
4:apply H3.
apply H1.
intro.
apply H.
rewrite H4.
reflexivity.
unfold out.
repeat split.
intro.
treat_equalities;auto.
auto.
auto.
unfold out.
repeat split;auto.
Cong.
subst Y;assumption.
Qed.
Lemma l6_13_2 : forall P A B, out P A B -> Bet P A B -> le P A P B.
Proof.
intros.
unfold le.
exists A.
split;eCong.
Qed.
Lemma l6_16_1 : forall P Q S X, P<>Q -> S<>P -> 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)).
intro.
induction H3.
Between.
Between.
unfold Col.
induction H1;induction H2.
right.
apply H3.
eapply (l5_2 Q P);eBetween.
induction H2.
left;eBetween.
left;eBetween.
induction H1.
left;eBetween.
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.
Definition Inter := fun X P Q R S =>
P<>Q /\ R <> S /\ Col X P Q /\ Col X R S /\
((exists X, Col X P Q /\ ~ Col X R S) \/ (exists X, ~ Col X P Q /\ Col X R S)).
Lemma col_transitivity_1 : forall P Q A B,
P<>Q -> 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).
assert (Col B P A).
apply (l6_16_1 P Q A B);Col.
Col.
Qed.
Lemma col_transitivity_2 : forall P Q A B,
P<>Q -> Col P Q A -> Col P Q B -> Col Q A B.
Proof.
intros.
apply (col_transitivity_1 Q P A B);Col.
Qed.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.
Unicity of intersection
Theorem l6_21 : forall A B C D P Q,
~ Col A B C -> C<>D -> Col A B P -> Col A B Q -> Col C D P -> Col C D Q -> P=Q.
Proof.
intros.
apply NNPP.
intro.
assert (Col D P Q) by eCol.
show_distinct A B.
intuition.
assert (Col A P Q) by eCol.
assert (Col C P Q) by eCol.
assert (Col Q A C) by eCol.
assert (Col Q B C).
induction (eq_dec_points Q A).
subst Q.
eapply col_transitivity_2;eCol.
eCol.
assert (Col A B C).
induction (eq_dec_points Q A).
subst Q;assumption.
eCol.
contradiction.
Qed.
Lemma l6_25 : forall A B,
A<>B -> exists C, ~ Col A B C.
Proof.
intros.
assert (T:=lower_dim).
induction T.
induction H0.
induction H0.
induction(classic(Col A B x)).
2:firstorder.
induction(classic(Col A B x0)).
2:firstorder.
induction(classic(Col A B x1)).
2:firstorder.
induction (eq_dec_points A x).
assert (~(Col x x0 x1)).
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.
contradiction.
Qed.
Theorem t2_8 : forall A B C D E : Tpoint,
Bet A B C -> Bet D B E -> Cong A B D B -> Cong B C B E -> Cong A E C D.
Proof.
intros.
induction (eq_dec_points A B).
treat_equalities;Cong.
assert
(Cong A B D B ->
Cong B C B E ->
Cong A D D A ->
Cong B D B A -> Bet A B C -> Bet D B E -> A <> B -> Cong C D E A).
apply five_segments.
apply cong_symmetry.
apply cong_right_commutativity.
apply H4;Cong;Between.
Qed.
Lemma col3 : forall X Y A B C, X <> Y -> Col X Y A -> Col X Y B -> Col X Y C -> Col A B C.
intros.
assert (Col X A B).
eapply col_transitivity_1.
apply H.
assumption.
assumption.
induction(eq_dec_points C X).
subst X.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H4.
eapply col_permutation_2.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
eapply col_permutation_2.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
Qed.
End T6.