Library bet
Require Export cong.
Section T2.
Context `{M:Tarski}.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition Col (A B C : Tpoint) : Prop := Bet A B C \/ Bet B C A \/ Bet C A B.
Lemma bet_col : forall A B C, Bet A B C -> Col A B C.
Proof.
intros;unfold Col;auto.
Qed.
Lemma between_trivial : forall A B : Tpoint, Bet A B B.
Proof.
intros.
prolong A B x B B.
assert (x = B)
by (apply cong_identity in H0;auto).
subst;assumption.
Qed.
Lemma between_symmetry : forall A B C : Tpoint, Bet A B C -> Bet C B A.
Proof.
intros.
assert (Bet B C C).
apply between_trivial.
assert(exists x, Bet B x B /\ Bet C x A)
by (eapply inner_pasch;eauto).
ex_and H1 x.
apply between_identity in H1.
subst;assumption.
Qed.
Lemma between_trivial2 : forall A B : Tpoint, Bet A A B.
Proof.
intros.
apply between_symmetry.
apply between_trivial.
Qed.
Lemma between_egality : forall A B C : Tpoint, Bet A B C -> Bet B A C -> A = B.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet A x A)
by (apply (inner_pasch A B C);assumption).
ex_and H1 x.
apply between_identity in H1.
apply between_identity in H2.
congruence.
Qed.
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) |- _ =>
assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);apply cong_symmetry;assumption|idtac];smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);assumption|idtac];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.
Lemma between_inner_transitivity : forall A B C D, Bet A B D -> Bet B C D -> Bet A B C.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet C x A).
eapply inner_pasch;eauto.
ex_and H1 x.
Between.
Qed.
Lemma between_exchange3 : forall A B C D, Bet A B C -> Bet A C D -> Bet B C D.
Proof.
intros.
assert (exists x, Bet C x C /\ Bet B x D)
by (eapply inner_pasch;eBetween).
ex_and H1 x.
Between.
Qed.
Lemma outer_transitivity_between2 : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
Proof.
intros.
prolong A C x C D.
assert (x = D).
apply (construction_unicity B C C D);
try assumption.
apply (between_exchange3 A B C x); assumption.
apply cong_reflexivity.
subst x;assumption.
Qed.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 : Between.
Lemma between_exchange2 : forall A B C D, Bet A B D -> Bet B C D -> Bet A C D.
intros.
induction (eq_dec_points B C);eBetween.
Qed.
Hint Resolve between_exchange2 : Between.
Lemma outer_transitivity_between : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A B D.
eBetween.
Qed.
Lemma between_exchange4 : forall A B C D, Bet A B C -> Bet A C D -> Bet A B D.
eBetween.
Qed.
Hint Resolve outer_transitivity_between between_exchange4.
Definition Bet_4 := fun A1 A2 A3 A4 =>
Bet A1 A2 A3 /\ Bet A2 A3 A4 /\ Bet A1 A3 A4 /\ Bet A1 A2 A4.
Lemma l_3_9_4 : forall A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 -> Bet_4 A4 A3 A2 A1.
Proof.
unfold Bet_4.
intros;spliter;Between.
Qed.
Lemma two_distinct_points : exists x, exists y: Tpoint, x <> y.
Proof.
assert (ld:=lower_dim).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
unfold Col in H.
induction (eq_dec_points A B).
subst A.
exists B.
exists C.
Between.
firstorder.
Qed.
Lemma point_construction_different : forall A B, exists C, Bet A B C /\ B <> C.
Proof.
intros.
assert (tdp := two_distinct_points).
ex_elim tdp x.
ex_elim H y.
prolong A B E x y.
exists E.
show_distinct B E.
apply cong_symmetry in H1.
apply cong_identity in H1.
intuition.
intuition.
Qed.
Lemma another_point : forall A: Tpoint, exists B, A<>B.
Proof.
intros.
assert (pcd := point_construction_different A A).
ex_and pcd B.
exists B;assumption.
Qed.
Lemma l3_17 : forall A B C A' B' P,
Bet A B C -> Bet A' B' C -> Bet A P A' -> exists Q, Bet P Q C /\ Bet B Q B'.
Proof.
intros.
assert (exists Q', Bet B' Q' A /\ Bet P Q' C)
by (eapply inner_pasch;eBetween).
ex_and H2 x.
assert (exists y, Bet x y C /\ Bet B y B')
by (eapply inner_pasch;eBetween).
ex_and H4 y.
exists y;eBetween.
Qed.
End T2.
Section T2.
Context `{M:Tarski}.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Definition Col (A B C : Tpoint) : Prop := Bet A B C \/ Bet B C A \/ Bet C A B.
Lemma bet_col : forall A B C, Bet A B C -> Col A B C.
Proof.
intros;unfold Col;auto.
Qed.
Lemma between_trivial : forall A B : Tpoint, Bet A B B.
Proof.
intros.
prolong A B x B B.
assert (x = B)
by (apply cong_identity in H0;auto).
subst;assumption.
Qed.
Lemma between_symmetry : forall A B C : Tpoint, Bet A B C -> Bet C B A.
Proof.
intros.
assert (Bet B C C).
apply between_trivial.
assert(exists x, Bet B x B /\ Bet C x A)
by (eapply inner_pasch;eauto).
ex_and H1 x.
apply between_identity in H1.
subst;assumption.
Qed.
Lemma between_trivial2 : forall A B : Tpoint, Bet A A B.
Proof.
intros.
apply between_symmetry.
apply between_trivial.
Qed.
Lemma between_egality : forall A B C : Tpoint, Bet A B C -> Bet B A C -> A = B.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet A x A)
by (apply (inner_pasch A B C);assumption).
ex_and H1 x.
apply between_identity in H1.
apply between_identity in H2.
congruence.
Qed.
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) |- _ =>
assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);apply cong_symmetry;assumption|idtac];smart_subst X2
| H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
assert (X1=X2);[apply cong_identity with (A:=X1) (B:=X2) (C:=X3);assumption|idtac];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.
Lemma between_inner_transitivity : forall A B C D, Bet A B D -> Bet B C D -> Bet A B C.
Proof.
intros.
assert (exists x, Bet B x B /\ Bet C x A).
eapply inner_pasch;eauto.
ex_and H1 x.
Between.
Qed.
Lemma between_exchange3 : forall A B C D, Bet A B C -> Bet A C D -> Bet B C D.
Proof.
intros.
assert (exists x, Bet C x C /\ Bet B x D)
by (eapply inner_pasch;eBetween).
ex_and H1 x.
Between.
Qed.
Lemma outer_transitivity_between2 : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
Proof.
intros.
prolong A C x C D.
assert (x = D).
apply (construction_unicity B C C D);
try assumption.
apply (between_exchange3 A B C x); assumption.
apply cong_reflexivity.
subst x;assumption.
Qed.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 : Between.
Lemma between_exchange2 : forall A B C D, Bet A B D -> Bet B C D -> Bet A C D.
intros.
induction (eq_dec_points B C);eBetween.
Qed.
Hint Resolve between_exchange2 : Between.
Lemma outer_transitivity_between : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A B D.
eBetween.
Qed.
Lemma between_exchange4 : forall A B C D, Bet A B C -> Bet A C D -> Bet A B D.
eBetween.
Qed.
Hint Resolve outer_transitivity_between between_exchange4.
Definition Bet_4 := fun A1 A2 A3 A4 =>
Bet A1 A2 A3 /\ Bet A2 A3 A4 /\ Bet A1 A3 A4 /\ Bet A1 A2 A4.
Lemma l_3_9_4 : forall A1 A2 A3 A4, Bet_4 A1 A2 A3 A4 -> Bet_4 A4 A3 A2 A1.
Proof.
unfold Bet_4.
intros;spliter;Between.
Qed.
Lemma two_distinct_points : exists x, exists y: Tpoint, x <> y.
Proof.
assert (ld:=lower_dim).
ex_elim ld A.
ex_elim H B.
ex_elim H0 C.
unfold Col in H.
induction (eq_dec_points A B).
subst A.
exists B.
exists C.
Between.
firstorder.
Qed.
Lemma point_construction_different : forall A B, exists C, Bet A B C /\ B <> C.
Proof.
intros.
assert (tdp := two_distinct_points).
ex_elim tdp x.
ex_elim H y.
prolong A B E x y.
exists E.
show_distinct B E.
apply cong_symmetry in H1.
apply cong_identity in H1.
intuition.
intuition.
Qed.
Lemma another_point : forall A: Tpoint, exists B, A<>B.
Proof.
intros.
assert (pcd := point_construction_different A A).
ex_and pcd B.
exists B;assumption.
Qed.
Lemma l3_17 : forall A B C A' B' P,
Bet A B C -> Bet A' B' C -> Bet A P A' -> exists Q, Bet P Q C /\ Bet B Q B'.
Proof.
intros.
assert (exists Q', Bet B' Q' A /\ Bet P Q' C)
by (eapply inner_pasch;eBetween).
ex_and H2 x.
assert (exists y, Bet x y C /\ Bet B y B')
by (eapply inner_pasch;eBetween).
ex_and H4 y.
exists y;eBetween.
Qed.
End T2.