Library midpoint
Require Export out_lines.
Section T7.
Context `{MT: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.
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 is_midpoint := fun M A B => Bet A M B /\ Cong A M M B.
Lemma l7_2 : forall M A B, is_midpoint M A B -> is_midpoint M B A.
Proof.
unfold is_midpoint.
intuition.
Qed.
Lemma l7_3 : forall M A, is_midpoint M A A -> M=A.
Proof.
unfold is_midpoint.
intros;spliter;repeat split;Between;Cong.
Qed.
Lemma l7_3_2 : forall A, is_midpoint A A A.
Proof.
unfold is_midpoint.
intros;repeat split;Between;Cong.
Qed.
Lemma symmetric_point_construction : forall A P, exists P', is_midpoint P A P'.
Proof.
unfold is_midpoint.
intros.
prolong A P E A P.
exists E.
split;Cong;Between.
Qed.
Lemma symmetric_point_unicity : forall A P P1 P2, is_midpoint P A P1 -> is_midpoint P A P2 -> P1=P2.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points A P).
treat_equalities;auto.
apply (construction_unicity A P A P);Cong.
Qed.
Lemma l7_9 : forall P Q A X, is_midpoint A P X -> is_midpoint A Q X -> P=Q.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points A X).
treat_equalities;reflexivity.
apply (construction_unicity X A X A);Cong;Between.
Qed.
Lemma diff_bet : forall A B C, A <> B -> Bet A B C -> A <> C.
Proof.
intros.
intro.
treat_equalities.
auto.
Qed.
Lemma l7_13 : forall A P Q P' Q', is_midpoint A P' P -> is_midpoint A Q' Q -> Cong P Q P' Q'.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points P A).
treat_equalities;Cong.
prolong P' P X Q A.
prolong X P' X' Q A.
prolong Q' Q Y P A.
prolong Y Q' Y' P A.
assert (Bet Y A Q') by eBetween.
assert (Bet P' A X) by eBetween.
assert (Bet A P X) by eBetween.
assert(Bet Y Q A) by eBetween.
assert (Bet A Q' Y') by eBetween.
assert (Bet X' P' A) by eBetween.
assert(Bet X A X') by eBetween.
assert(Bet Y A Y') by eBetween.
assert (Cong A X Y A) by (eapply l2_l1;eCong).
assert (Cong A Y' X' A) by (eapply l2_l1;eCong).
assert (Cong A Y A Y')
by (apply (l2_l1 A Q Y _ Q' Y');Between;eCong).
assert (FSC X A X' Y' Y' A Y X).
unfold FSC;repeat split.
apply bet_col;auto.
eCong.
eapply (l2_l1 X A X' Y' A Y);Between;eCong.
eCong.
eCong.
eCong.
assert (A <> X).
eapply diff_bet.
intro.
apply H3.
apply sym_equal.
apply H24.
assumption.
assert (Cong X' Y' Y X) by eauto using l4_16.
assert (IFSC Y Q A X Y' Q' A X') by
(unfold IFSC, FSC in *;spliter;repeat split;Between;eCong).
assert (Cong Q X Q' X') by eauto using l4_2.
assert (IFSC X P A Q X' P' A Q') by
(unfold IFSC;repeat split;Between;eCong).
eauto using l4_2.
Qed.
Lemma l7_15 : forall P Q R P' Q' R' A,
is_midpoint A P P' -> is_midpoint A Q Q' -> is_midpoint A R R' -> Bet P Q R -> Bet P' Q' R'.
Proof.
intros.
spliter.
eapply l4_6.
apply H2.
unfold Cong_3.
repeat split.
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
assumption.
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
assumption.
eapply l7_13.
apply l7_2.
apply H0.
apply l7_2.
assumption.
Qed.
Lemma l7_16 : forall P Q R S P' Q' R' S' A,
is_midpoint A P P' -> is_midpoint A Q Q' -> is_midpoint A R R' -> is_midpoint A S S' -> Cong P Q R S -> Cong P' Q' R' S'.
Proof.
intros.
assert (Cong P Q P' Q').
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
apply H0.
assert (Cong R S R' S').
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
apply H2.
eCong.
Qed.
Lemma symmetry_preserves_midpoint :
forall A B C D E F Z,
is_midpoint Z A D -> is_midpoint Z B E -> is_midpoint Z C F -> is_midpoint B A C -> is_midpoint E D F.
Proof.
intros.
unfold is_midpoint.
unfold is_midpoint in H2.
spliter.
split.
eapply l7_15;eauto.
eapply l7_16;eauto.
Qed.
Hint Resolve l7_2 : Midpoint.
Hint Resolve l7_13 : Cong.
Lemma l7_17 : forall P P' A B, is_midpoint A P P' -> is_midpoint B P P' -> A=B.
Proof.
intros.
assert (Cong P B P' B).
unfold is_midpoint in *.
spliter.
Cong.
assert (exists B', is_midpoint A B B') by
(apply symmetric_point_construction).
induction H2.
assert (Cong P' B P x) by
eauto with Midpoint Cong.
assert (Cong P B P x) by eCong.
assert (Cong P B P' x) by
eauto with Midpoint Cong.
assert (Cong P' B P' x) by eCong.
assert (Bet P B P') by (unfold is_midpoint in *;spliter;assumption).
assert (B=x) by (apply (l4_19 P P' B x);Between).
subst x.
apply l7_3.
assumption.
Qed.
Lemma l7_20 : forall M A B,
Col A M B -> Cong M A M B -> A=B \/ is_midpoint M A B.
Proof.
unfold Col.
intros.
induction H.
right.
unfold is_midpoint.
split.
assumption.
Cong.
induction H.
assert (Cong A B B B)
by (apply (l4_3 A B M B B M);Between;Cong).
treat_equalities;auto.
assert (Cong B A A A)
by (apply (l4_3 B A M A A M);Cong;Between).
treat_equalities;auto.
Qed.
Lemma l7_21 : forall A B C D P,
~ Col A B C -> B<>D -> Cong A B C D -> Cong B C D A ->
Col A P C -> Col B P D -> is_midpoint P A C /\ is_midpoint P B D.
intros.
assert (exists P', Cong_3 B D P D B P').
eapply l4_14.
Col.
Cong.
induction H5.
assert (Col D B x).
eapply l4_13.
2:apply H5.
Col.
assert (FSC B D P A D B x C).
unfold FSC.
unfold Cong_3 in H5.
spliter.
repeat split; try Cong.
Col.
assert (FSC B D P C D B x A).
unfold FSC.
unfold Cong_3 in H5.
spliter.
repeat split; try assumption.
Col.
Cong.
assert (Cong P A x C).
eapply l4_16.
apply H7.
assumption.
assert (Cong P C x A).
eapply l4_16.
apply H8.
assumption.
assert (Cong_3 A P C C x A).
unfold Cong_3.
repeat split; try Cong.
assert (Col C x A).
eapply l4_13.
2:apply H11.
assumption.
assert (P=x).
unfold FSC in *.
spliter.
eapply (l6_21 A C B D); Col.
subst x.
assert (C = A \/ is_midpoint P C A).
eapply l7_20.
assumption.
assumption.
assert (B = D \/ is_midpoint P B D).
eapply l7_20.
assumption.
unfold FSC, Cong_3 in *.
spliter.
Cong.
unfold is_midpoint,FSC,Cong_3 in *.
spliter.
induction H14.
contradiction.
spliter.
induction H13.
subst C.
apply False_ind.
apply H.
apply col_trivial_3.
repeat split; try Cong.
apply between_symmetry.
spliter.
assumption.
Qed.
Hint Resolve l7_2 l7_3 l7_3_2 : Midpoint.
Hint Resolve symmetric_point_construction : Midpoint.
Hint Resolve symmetry_preserves_midpoint : Midpoint.
Lemma l7_22_aux : forall A1 A2 B1 B2 C M1 M2,
Bet A1 C A2 -> Bet B1 C B2 -> Cong C A1 C B1 -> Cong C A2 C B2 ->
is_midpoint M1 A1 B1 -> is_midpoint M2 A2 B2 -> le C A1 C A2 ->
Bet M1 C M2.
intros.
induction (eq_dec_points A2 C).
subst C.
apply le_zero in H5.
subst A2.
apply cong_reverse_identity in H1.
subst B1.
apply cong_reverse_identity in H2.
subst B2.
apply l7_3 in H4.
subst A1.
apply between_trivial.
assert (exists A, is_midpoint C A2 A).
apply symmetric_point_construction.
induction H7.
assert (exists B, is_midpoint C B2 B).
apply symmetric_point_construction.
induction H8.
assert (exists M, is_midpoint C M2 M).
apply symmetric_point_construction.
induction H9.
assert(is_midpoint x1 x x0).
unfold is_midpoint.
split.
eapply l7_15.
apply H7.
apply H9.
apply H8.
unfold is_midpoint in H4.
spliter.
assumption.
eapply l7_16.
apply H7.
apply H9.
apply H9.
apply H8.
unfold is_midpoint in H4.
spliter.
assumption.
assert (le C A1 C x).
eapply l5_6.
repeat split.
apply H5.
apply cong_reflexivity.
unfold is_midpoint in H7.
spliter.
apply cong_left_commutativity.
assumption.
assert (Bet C A1 x).
induction (eq_dec_points A1 C).
subst A1.
apply between_trivial2.
eapply l6_13_1.
unfold out.
2:assumption.
repeat split.
assumption.
intro.
subst x.
apply le_zero in H11.
apply H12.
subst A1.
reflexivity.
eapply l5_2.
apply H6.
apply between_symmetry.
assumption;
intro.
unfold is_midpoint in H7.
spliter.
assumption.
assert (le C B1 C x0).
eapply l5_6.
split.
apply H11.
split.
assumption.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H16.
eapply cong_transitivity.
2:apply H15.
apply cong_commutativity.
assumption.
assert (Bet C B1 x0).
induction (eq_dec_points B1 C).
subst B1.
apply cong_symmetry in H1.
apply cong_reverse_identity in H1.
subst A1.
apply between_trivial2.
induction (eq_dec_points x0 C).
subst x0.
apply le_zero in H13.
subst B1.
apply between_trivial.
induction (eq_dec_points B2 C).
subst B2.
apply cong_symmetry in H2.
eapply cong_reverse_identity in H2.
subst A2.
apply le_zero in H5.
subst A1.
apply cong_reverse_identity in H1.
subst B1.
apply False_ind.
apply H14.
reflexivity.
eapply l6_13_1.
unfold out.
repeat split.
assumption.
assumption.
eapply l5_2.
2:apply between_symmetry.
2:apply H0.
assumption.
2:assumption.
unfold is_midpoint in H8.
spliter.
assumption.
assert (exists Q, Bet x1 Q C /\ Bet A1 Q B1).
eapply l3_17.
apply between_symmetry.
apply H12.
apply between_symmetry.
apply H14.
unfold is_midpoint in H10.
spliter.
assumption.
ex_and H15 Q.
assert (IFSC x A1 C x1 x0 B1 C x1).
unfold IFSC.
unfold is_midpoint in *.
spliter.
repeat split.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply cong_symmetry.
apply H20.
eapply cong_transitivity.
apply H2.
apply cong_commutativity.
assumption.
apply cong_commutativity.
assumption.
apply cong_right_commutativity.
assumption.
apply cong_reflexivity.
assert (Cong A1 x1 B1 x1).
eapply l4_2.
apply H17.
assert (Cong Q A1 Q B1).
induction(eq_dec_points C x1).
subst x1.
apply between_identity in H15.
subst Q.
apply cong_commutativity.
assumption.
eapply l4_17.
apply H19.
unfold Col.
right; left.
assumption.
assumption.
apply cong_commutativity.
assumption.
assert (is_midpoint Q A1 B1).
unfold is_midpoint.
split.
assumption.
apply cong_left_commutativity.
assumption.
assert (Q=M1).
eapply l7_17.
apply H20.
assumption.
subst Q.
eapply between_exchange3.
apply H15.
unfold is_midpoint in H9.
spliter.
apply between_symmetry.
assumption.
Qed.
Lemma l7_22 : forall A1 A2 B1 B2 C M1 M2,
Bet A1 C A2 -> Bet B1 C B2 ->
Cong C A1 C B1 -> Cong C A2 C B2 ->
is_midpoint M1 A1 B1 -> is_midpoint M2 A2 B2 ->
Bet M1 C M2.
intros.
assert (le C A1 C A2 \/ le C A2 C A1).
eapply le_cases.
induction H5.
eapply l7_22_aux.
apply H.
apply H0.
apply H1.
apply H2.
assumption.
assumption.
assumption.
apply between_symmetry.
eapply l7_22_aux.
7:apply H5.
apply between_symmetry.
apply H.
5:apply H3.
4:apply H4.
apply between_symmetry.
apply H0.
assumption.
assumption.
Qed.
Lemma bet_col1 : forall A B C D, Bet A B D -> Bet A C D -> Col A B C.
intros.
assert(Bet A B C \/ Bet A C B).
eapply l5_3.
apply H.
assumption.
unfold Col.
induction H1.
left.
assumption.
right; left.
apply between_symmetry.
assumption.
Qed.
Lemma bet_col2 : forall A B C D, A <> B -> Bet A B C -> Bet A B D -> Col A C D.
intros.
assert(Bet A D C \/ Bet A C D).
eapply l5_1.
apply H.
assumption.
assumption.
unfold Col.
induction H2.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
Qed.
Lemma mid_diff : forall A B M : Tpoint, A <> B -> is_midpoint M A B -> M <> A /\ M <> B.
unfold is_midpoint.
intros.
induction H0.
split;
intro;
subst M;
[apply cong_symmetry in H1|idtac];
apply cong_identity in H1;
apply H;
assumption.
Qed.
Lemma l7_25 : forall A B C, Cong C A C B -> exists X, is_midpoint X A B.
intros.
induction(classic(Col A B C)).
assert(A = B \/ is_midpoint C A B).
apply l7_20.
unfold Col in *.
intuition.
assumption.
induction H1.
subst B.
exists A.
apply l7_3_2.
exists C.
assumption.
assert (exists P, Bet C A P /\ A<>P).
apply point_construction_different.
ex_and H1 P.
prolong C B Q A P.
assert (exists R, Bet A R Q /\ Bet B R P).
eapply inner_pasch.
apply between_symmetry.
apply H1.
apply between_symmetry.
assumption.
ex_and H5 R.
assert (exists X, Bet A X B /\ Bet R X C).
eapply inner_pasch.
apply H1.
assumption.
ex_and H7 X.
exists X.
unfold is_midpoint.
split.
assumption.
apply cong_left_commutativity.
cut(Cong R A R B).
intros.
induction(eq_dec_points R C).
subst R.
assert (C = X).
apply between_identity.
assumption.
subst X.
assumption.
eapply l4_17.
apply H10.
unfold Col.
right; left.
apply between_symmetry.
assumption.
assumption.
assumption.
assert (OFSC C A P B C B Q A).
unfold OFSC.
repeat split.
assumption.
assumption.
assumption.
apply cong_symmetry.
assumption.
apply cong_symmetry.
assumption.
apply cong_pseudo_reflexivity.
assert (Cong P B Q A).
eapply five_segments_with_def.
eapply H9.
unfold Col in H0.
intuition.
apply H0.
subst A.
apply between_trivial.
assert (exists R', Bet A R' Q /\ Cong_3 B R P A R' Q).
eapply l4_5.
assumption.
apply cong_commutativity.
assumption.
ex_and H11 R'.
assert (IFSC B R P A A R' Q B).
unfold IFSC.
repeat split.
assumption.
assumption.
apply cong_commutativity.
assumption.
unfold Cong_3 in H12.
spliter.
assumption.
apply cong_pseudo_reflexivity.
apply cong_commutativity.
apply cong_symmetry.
assumption.
assert (IFSC B R P Q A R' Q P).
unfold IFSC.
repeat split;try assumption.
apply cong_commutativity.
assumption.
unfold Cong_3 in H12.
spliter.
assumption.
apply cong_pseudo_reflexivity.
assert (Cong R A R' B).
eapply l4_2.
apply H13.
assert (Cong R Q R' P).
eapply l4_2.
apply H14.
assert (Cong_3 A R Q B R' P).
unfold Cong_3.
repeat split.
apply cong_commutativity.
assumption.
apply cong_commutativity.
apply cong_symmetry.
assumption.
assumption.
assert (Col B R' P).
eapply l4_13.
2:apply H17.
unfold Col.
left.
assumption.
cut(R=R').
intro.
subst R'.
assumption.
assert (B <> P).
unfold IFSC, OFSC, Cong_3 in *.
spliter.
intro.
subst P.
apply between_identity in H14.
subst R.
apply cong_reverse_identity in H12.
subst R'.
apply cong_reverse_identity in H32.
subst Q.
apply between_identity in H5.
apply H2.
assumption.
assert (A <> Q).
unfold IFSC, OFSC, Cong_3 in *.
spliter.
intro.
subst Q.
apply cong_reverse_identity in H20.
subst P.
apply H19.
reflexivity.
assert(B <> Q).
intro.
subst Q.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst P.
apply H2.
reflexivity.
assert (B <> R).
intro.
unfold Cong_3, IFSC, OFSC in *.
spliter.
subst R.
clean_duplicated_hyps.
assert (Col B A C).
eapply bet_col2.
2:apply between_symmetry.
2:apply H7.
2:assumption.
intro.
apply cong_symmetry in H12.
apply cong_identity in H12.
subst R'.
subst X.
clean_duplicated_hyps.
assert (Bet B A C \/ Bet B C A).
eapply l5_2.
2:apply between_symmetry.
2:apply H5.
intro.
apply H21.
rewrite H9.
reflexivity.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
induction H9.
right;right.
apply between_symmetry.
assumption.
right; left.
assumption.
apply H0.
apply col_permutation_4.
assumption.
eapply (l6_21 A Q B P R R' ).
intro.
unfold Col in H23.
induction H23.
assert(Bet A B C).
eapply outer_transitivity_between2.
apply H23.
apply between_symmetry.
assumption.
intro.
apply H21.
rewrite H24.
reflexivity.
apply H0.
unfold Col.
left.
assumption.
induction H23.
assert(Bet B A C \/ Bet B C A).
eapply l5_2.
2:apply H23.
intro.
apply H21.
rewrite H24.
reflexivity.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
induction H24.
right;right.
apply between_symmetry.
assumption.
right; left.
assumption.
assert(Bet A B C).
eapply between_exchange3.
apply between_symmetry.
apply H23.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
left.
assumption.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
unfold Col in H18.
induction H18.
right; left.
apply between_symmetry.
assumption.
induction H18.
left.
apply between_symmetry.
assumption.
right;right.
apply between_symmetry.
assumption.
Qed.
End T7.
Section T7.
Context `{MT: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.
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 is_midpoint := fun M A B => Bet A M B /\ Cong A M M B.
Lemma l7_2 : forall M A B, is_midpoint M A B -> is_midpoint M B A.
Proof.
unfold is_midpoint.
intuition.
Qed.
Lemma l7_3 : forall M A, is_midpoint M A A -> M=A.
Proof.
unfold is_midpoint.
intros;spliter;repeat split;Between;Cong.
Qed.
Lemma l7_3_2 : forall A, is_midpoint A A A.
Proof.
unfold is_midpoint.
intros;repeat split;Between;Cong.
Qed.
Lemma symmetric_point_construction : forall A P, exists P', is_midpoint P A P'.
Proof.
unfold is_midpoint.
intros.
prolong A P E A P.
exists E.
split;Cong;Between.
Qed.
Lemma symmetric_point_unicity : forall A P P1 P2, is_midpoint P A P1 -> is_midpoint P A P2 -> P1=P2.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points A P).
treat_equalities;auto.
apply (construction_unicity A P A P);Cong.
Qed.
Lemma l7_9 : forall P Q A X, is_midpoint A P X -> is_midpoint A Q X -> P=Q.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points A X).
treat_equalities;reflexivity.
apply (construction_unicity X A X A);Cong;Between.
Qed.
Lemma diff_bet : forall A B C, A <> B -> Bet A B C -> A <> C.
Proof.
intros.
intro.
treat_equalities.
auto.
Qed.
Lemma l7_13 : forall A P Q P' Q', is_midpoint A P' P -> is_midpoint A Q' Q -> Cong P Q P' Q'.
Proof.
unfold is_midpoint.
intros.
spliter.
induction (eq_dec_points P A).
treat_equalities;Cong.
prolong P' P X Q A.
prolong X P' X' Q A.
prolong Q' Q Y P A.
prolong Y Q' Y' P A.
assert (Bet Y A Q') by eBetween.
assert (Bet P' A X) by eBetween.
assert (Bet A P X) by eBetween.
assert(Bet Y Q A) by eBetween.
assert (Bet A Q' Y') by eBetween.
assert (Bet X' P' A) by eBetween.
assert(Bet X A X') by eBetween.
assert(Bet Y A Y') by eBetween.
assert (Cong A X Y A) by (eapply l2_l1;eCong).
assert (Cong A Y' X' A) by (eapply l2_l1;eCong).
assert (Cong A Y A Y')
by (apply (l2_l1 A Q Y _ Q' Y');Between;eCong).
assert (FSC X A X' Y' Y' A Y X).
unfold FSC;repeat split.
apply bet_col;auto.
eCong.
eapply (l2_l1 X A X' Y' A Y);Between;eCong.
eCong.
eCong.
eCong.
assert (A <> X).
eapply diff_bet.
intro.
apply H3.
apply sym_equal.
apply H24.
assumption.
assert (Cong X' Y' Y X) by eauto using l4_16.
assert (IFSC Y Q A X Y' Q' A X') by
(unfold IFSC, FSC in *;spliter;repeat split;Between;eCong).
assert (Cong Q X Q' X') by eauto using l4_2.
assert (IFSC X P A Q X' P' A Q') by
(unfold IFSC;repeat split;Between;eCong).
eauto using l4_2.
Qed.
Lemma l7_15 : forall P Q R P' Q' R' A,
is_midpoint A P P' -> is_midpoint A Q Q' -> is_midpoint A R R' -> Bet P Q R -> Bet P' Q' R'.
Proof.
intros.
spliter.
eapply l4_6.
apply H2.
unfold Cong_3.
repeat split.
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
assumption.
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
assumption.
eapply l7_13.
apply l7_2.
apply H0.
apply l7_2.
assumption.
Qed.
Lemma l7_16 : forall P Q R S P' Q' R' S' A,
is_midpoint A P P' -> is_midpoint A Q Q' -> is_midpoint A R R' -> is_midpoint A S S' -> Cong P Q R S -> Cong P' Q' R' S'.
Proof.
intros.
assert (Cong P Q P' Q').
eapply l7_13.
apply l7_2.
apply H.
apply l7_2.
apply H0.
assert (Cong R S R' S').
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
apply H2.
eCong.
Qed.
Lemma symmetry_preserves_midpoint :
forall A B C D E F Z,
is_midpoint Z A D -> is_midpoint Z B E -> is_midpoint Z C F -> is_midpoint B A C -> is_midpoint E D F.
Proof.
intros.
unfold is_midpoint.
unfold is_midpoint in H2.
spliter.
split.
eapply l7_15;eauto.
eapply l7_16;eauto.
Qed.
Hint Resolve l7_2 : Midpoint.
Hint Resolve l7_13 : Cong.
Lemma l7_17 : forall P P' A B, is_midpoint A P P' -> is_midpoint B P P' -> A=B.
Proof.
intros.
assert (Cong P B P' B).
unfold is_midpoint in *.
spliter.
Cong.
assert (exists B', is_midpoint A B B') by
(apply symmetric_point_construction).
induction H2.
assert (Cong P' B P x) by
eauto with Midpoint Cong.
assert (Cong P B P x) by eCong.
assert (Cong P B P' x) by
eauto with Midpoint Cong.
assert (Cong P' B P' x) by eCong.
assert (Bet P B P') by (unfold is_midpoint in *;spliter;assumption).
assert (B=x) by (apply (l4_19 P P' B x);Between).
subst x.
apply l7_3.
assumption.
Qed.
Lemma l7_20 : forall M A B,
Col A M B -> Cong M A M B -> A=B \/ is_midpoint M A B.
Proof.
unfold Col.
intros.
induction H.
right.
unfold is_midpoint.
split.
assumption.
Cong.
induction H.
assert (Cong A B B B)
by (apply (l4_3 A B M B B M);Between;Cong).
treat_equalities;auto.
assert (Cong B A A A)
by (apply (l4_3 B A M A A M);Cong;Between).
treat_equalities;auto.
Qed.
Lemma l7_21 : forall A B C D P,
~ Col A B C -> B<>D -> Cong A B C D -> Cong B C D A ->
Col A P C -> Col B P D -> is_midpoint P A C /\ is_midpoint P B D.
intros.
assert (exists P', Cong_3 B D P D B P').
eapply l4_14.
Col.
Cong.
induction H5.
assert (Col D B x).
eapply l4_13.
2:apply H5.
Col.
assert (FSC B D P A D B x C).
unfold FSC.
unfold Cong_3 in H5.
spliter.
repeat split; try Cong.
Col.
assert (FSC B D P C D B x A).
unfold FSC.
unfold Cong_3 in H5.
spliter.
repeat split; try assumption.
Col.
Cong.
assert (Cong P A x C).
eapply l4_16.
apply H7.
assumption.
assert (Cong P C x A).
eapply l4_16.
apply H8.
assumption.
assert (Cong_3 A P C C x A).
unfold Cong_3.
repeat split; try Cong.
assert (Col C x A).
eapply l4_13.
2:apply H11.
assumption.
assert (P=x).
unfold FSC in *.
spliter.
eapply (l6_21 A C B D); Col.
subst x.
assert (C = A \/ is_midpoint P C A).
eapply l7_20.
assumption.
assumption.
assert (B = D \/ is_midpoint P B D).
eapply l7_20.
assumption.
unfold FSC, Cong_3 in *.
spliter.
Cong.
unfold is_midpoint,FSC,Cong_3 in *.
spliter.
induction H14.
contradiction.
spliter.
induction H13.
subst C.
apply False_ind.
apply H.
apply col_trivial_3.
repeat split; try Cong.
apply between_symmetry.
spliter.
assumption.
Qed.
Hint Resolve l7_2 l7_3 l7_3_2 : Midpoint.
Hint Resolve symmetric_point_construction : Midpoint.
Hint Resolve symmetry_preserves_midpoint : Midpoint.
Lemma l7_22_aux : forall A1 A2 B1 B2 C M1 M2,
Bet A1 C A2 -> Bet B1 C B2 -> Cong C A1 C B1 -> Cong C A2 C B2 ->
is_midpoint M1 A1 B1 -> is_midpoint M2 A2 B2 -> le C A1 C A2 ->
Bet M1 C M2.
intros.
induction (eq_dec_points A2 C).
subst C.
apply le_zero in H5.
subst A2.
apply cong_reverse_identity in H1.
subst B1.
apply cong_reverse_identity in H2.
subst B2.
apply l7_3 in H4.
subst A1.
apply between_trivial.
assert (exists A, is_midpoint C A2 A).
apply symmetric_point_construction.
induction H7.
assert (exists B, is_midpoint C B2 B).
apply symmetric_point_construction.
induction H8.
assert (exists M, is_midpoint C M2 M).
apply symmetric_point_construction.
induction H9.
assert(is_midpoint x1 x x0).
unfold is_midpoint.
split.
eapply l7_15.
apply H7.
apply H9.
apply H8.
unfold is_midpoint in H4.
spliter.
assumption.
eapply l7_16.
apply H7.
apply H9.
apply H9.
apply H8.
unfold is_midpoint in H4.
spliter.
assumption.
assert (le C A1 C x).
eapply l5_6.
repeat split.
apply H5.
apply cong_reflexivity.
unfold is_midpoint in H7.
spliter.
apply cong_left_commutativity.
assumption.
assert (Bet C A1 x).
induction (eq_dec_points A1 C).
subst A1.
apply between_trivial2.
eapply l6_13_1.
unfold out.
2:assumption.
repeat split.
assumption.
intro.
subst x.
apply le_zero in H11.
apply H12.
subst A1.
reflexivity.
eapply l5_2.
apply H6.
apply between_symmetry.
assumption;
intro.
unfold is_midpoint in H7.
spliter.
assumption.
assert (le C B1 C x0).
eapply l5_6.
split.
apply H11.
split.
assumption.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H16.
eapply cong_transitivity.
2:apply H15.
apply cong_commutativity.
assumption.
assert (Bet C B1 x0).
induction (eq_dec_points B1 C).
subst B1.
apply cong_symmetry in H1.
apply cong_reverse_identity in H1.
subst A1.
apply between_trivial2.
induction (eq_dec_points x0 C).
subst x0.
apply le_zero in H13.
subst B1.
apply between_trivial.
induction (eq_dec_points B2 C).
subst B2.
apply cong_symmetry in H2.
eapply cong_reverse_identity in H2.
subst A2.
apply le_zero in H5.
subst A1.
apply cong_reverse_identity in H1.
subst B1.
apply False_ind.
apply H14.
reflexivity.
eapply l6_13_1.
unfold out.
repeat split.
assumption.
assumption.
eapply l5_2.
2:apply between_symmetry.
2:apply H0.
assumption.
2:assumption.
unfold is_midpoint in H8.
spliter.
assumption.
assert (exists Q, Bet x1 Q C /\ Bet A1 Q B1).
eapply l3_17.
apply between_symmetry.
apply H12.
apply between_symmetry.
apply H14.
unfold is_midpoint in H10.
spliter.
assumption.
ex_and H15 Q.
assert (IFSC x A1 C x1 x0 B1 C x1).
unfold IFSC.
unfold is_midpoint in *.
spliter.
repeat split.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply cong_symmetry.
apply H20.
eapply cong_transitivity.
apply H2.
apply cong_commutativity.
assumption.
apply cong_commutativity.
assumption.
apply cong_right_commutativity.
assumption.
apply cong_reflexivity.
assert (Cong A1 x1 B1 x1).
eapply l4_2.
apply H17.
assert (Cong Q A1 Q B1).
induction(eq_dec_points C x1).
subst x1.
apply between_identity in H15.
subst Q.
apply cong_commutativity.
assumption.
eapply l4_17.
apply H19.
unfold Col.
right; left.
assumption.
assumption.
apply cong_commutativity.
assumption.
assert (is_midpoint Q A1 B1).
unfold is_midpoint.
split.
assumption.
apply cong_left_commutativity.
assumption.
assert (Q=M1).
eapply l7_17.
apply H20.
assumption.
subst Q.
eapply between_exchange3.
apply H15.
unfold is_midpoint in H9.
spliter.
apply between_symmetry.
assumption.
Qed.
Lemma l7_22 : forall A1 A2 B1 B2 C M1 M2,
Bet A1 C A2 -> Bet B1 C B2 ->
Cong C A1 C B1 -> Cong C A2 C B2 ->
is_midpoint M1 A1 B1 -> is_midpoint M2 A2 B2 ->
Bet M1 C M2.
intros.
assert (le C A1 C A2 \/ le C A2 C A1).
eapply le_cases.
induction H5.
eapply l7_22_aux.
apply H.
apply H0.
apply H1.
apply H2.
assumption.
assumption.
assumption.
apply between_symmetry.
eapply l7_22_aux.
7:apply H5.
apply between_symmetry.
apply H.
5:apply H3.
4:apply H4.
apply between_symmetry.
apply H0.
assumption.
assumption.
Qed.
Lemma bet_col1 : forall A B C D, Bet A B D -> Bet A C D -> Col A B C.
intros.
assert(Bet A B C \/ Bet A C B).
eapply l5_3.
apply H.
assumption.
unfold Col.
induction H1.
left.
assumption.
right; left.
apply between_symmetry.
assumption.
Qed.
Lemma bet_col2 : forall A B C D, A <> B -> Bet A B C -> Bet A B D -> Col A C D.
intros.
assert(Bet A D C \/ Bet A C D).
eapply l5_1.
apply H.
assumption.
assumption.
unfold Col.
induction H2.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
Qed.
Lemma mid_diff : forall A B M : Tpoint, A <> B -> is_midpoint M A B -> M <> A /\ M <> B.
unfold is_midpoint.
intros.
induction H0.
split;
intro;
subst M;
[apply cong_symmetry in H1|idtac];
apply cong_identity in H1;
apply H;
assumption.
Qed.
Lemma l7_25 : forall A B C, Cong C A C B -> exists X, is_midpoint X A B.
intros.
induction(classic(Col A B C)).
assert(A = B \/ is_midpoint C A B).
apply l7_20.
unfold Col in *.
intuition.
assumption.
induction H1.
subst B.
exists A.
apply l7_3_2.
exists C.
assumption.
assert (exists P, Bet C A P /\ A<>P).
apply point_construction_different.
ex_and H1 P.
prolong C B Q A P.
assert (exists R, Bet A R Q /\ Bet B R P).
eapply inner_pasch.
apply between_symmetry.
apply H1.
apply between_symmetry.
assumption.
ex_and H5 R.
assert (exists X, Bet A X B /\ Bet R X C).
eapply inner_pasch.
apply H1.
assumption.
ex_and H7 X.
exists X.
unfold is_midpoint.
split.
assumption.
apply cong_left_commutativity.
cut(Cong R A R B).
intros.
induction(eq_dec_points R C).
subst R.
assert (C = X).
apply between_identity.
assumption.
subst X.
assumption.
eapply l4_17.
apply H10.
unfold Col.
right; left.
apply between_symmetry.
assumption.
assumption.
assumption.
assert (OFSC C A P B C B Q A).
unfold OFSC.
repeat split.
assumption.
assumption.
assumption.
apply cong_symmetry.
assumption.
apply cong_symmetry.
assumption.
apply cong_pseudo_reflexivity.
assert (Cong P B Q A).
eapply five_segments_with_def.
eapply H9.
unfold Col in H0.
intuition.
apply H0.
subst A.
apply between_trivial.
assert (exists R', Bet A R' Q /\ Cong_3 B R P A R' Q).
eapply l4_5.
assumption.
apply cong_commutativity.
assumption.
ex_and H11 R'.
assert (IFSC B R P A A R' Q B).
unfold IFSC.
repeat split.
assumption.
assumption.
apply cong_commutativity.
assumption.
unfold Cong_3 in H12.
spliter.
assumption.
apply cong_pseudo_reflexivity.
apply cong_commutativity.
apply cong_symmetry.
assumption.
assert (IFSC B R P Q A R' Q P).
unfold IFSC.
repeat split;try assumption.
apply cong_commutativity.
assumption.
unfold Cong_3 in H12.
spliter.
assumption.
apply cong_pseudo_reflexivity.
assert (Cong R A R' B).
eapply l4_2.
apply H13.
assert (Cong R Q R' P).
eapply l4_2.
apply H14.
assert (Cong_3 A R Q B R' P).
unfold Cong_3.
repeat split.
apply cong_commutativity.
assumption.
apply cong_commutativity.
apply cong_symmetry.
assumption.
assumption.
assert (Col B R' P).
eapply l4_13.
2:apply H17.
unfold Col.
left.
assumption.
cut(R=R').
intro.
subst R'.
assumption.
assert (B <> P).
unfold IFSC, OFSC, Cong_3 in *.
spliter.
intro.
subst P.
apply between_identity in H14.
subst R.
apply cong_reverse_identity in H12.
subst R'.
apply cong_reverse_identity in H32.
subst Q.
apply between_identity in H5.
apply H2.
assumption.
assert (A <> Q).
unfold IFSC, OFSC, Cong_3 in *.
spliter.
intro.
subst Q.
apply cong_reverse_identity in H20.
subst P.
apply H19.
reflexivity.
assert(B <> Q).
intro.
subst Q.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst P.
apply H2.
reflexivity.
assert (B <> R).
intro.
unfold Cong_3, IFSC, OFSC in *.
spliter.
subst R.
clean_duplicated_hyps.
assert (Col B A C).
eapply bet_col2.
2:apply between_symmetry.
2:apply H7.
2:assumption.
intro.
apply cong_symmetry in H12.
apply cong_identity in H12.
subst R'.
subst X.
clean_duplicated_hyps.
assert (Bet B A C \/ Bet B C A).
eapply l5_2.
2:apply between_symmetry.
2:apply H5.
intro.
apply H21.
rewrite H9.
reflexivity.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
induction H9.
right;right.
apply between_symmetry.
assumption.
right; left.
assumption.
apply H0.
apply col_permutation_4.
assumption.
eapply (l6_21 A Q B P R R' ).
intro.
unfold Col in H23.
induction H23.
assert(Bet A B C).
eapply outer_transitivity_between2.
apply H23.
apply between_symmetry.
assumption.
intro.
apply H21.
rewrite H24.
reflexivity.
apply H0.
unfold Col.
left.
assumption.
induction H23.
assert(Bet B A C \/ Bet B C A).
eapply l5_2.
2:apply H23.
intro.
apply H21.
rewrite H24.
reflexivity.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
induction H24.
right;right.
apply between_symmetry.
assumption.
right; left.
assumption.
assert(Bet A B C).
eapply between_exchange3.
apply between_symmetry.
apply H23.
apply between_symmetry.
assumption.
apply H0.
unfold Col.
left.
assumption.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
unfold Col.
unfold Col in H18.
induction H18.
right; left.
apply between_symmetry.
assumption.
induction H18.
left.
apply between_symmetry.
assumption.
right;right.
apply between_symmetry.
assumption.
Qed.
End T7.