Library cong
Require Export axioms.
Require Export general_tactics.
Section T1.
Context `{M:Tarski}.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Lemma cong_reflexivity : forall A B,
Cong A B A B.
Proof.
intros.
apply (cong_inner_transitivity B A A B);
apply cong_pseudo_reflexivity.
Qed.
Lemma cong_symmetry : forall A B C D : Tpoint,
Cong A B C D -> Cong C D A B.
Proof.
intros.
eapply cong_inner_transitivity.
apply H.
apply cong_reflexivity.
Qed.
Lemma cong_transitivity : forall A B C D E F : Tpoint,
Cong A B C D -> Cong C D E F -> Cong A B E F.
Proof.
intros.
eapply cong_inner_transitivity; eauto using cong_symmetry.
Qed.
Lemma cong_left_commutativity : forall A B C D,
Cong A B C D -> Cong B A C D.
Proof.
intros.
eapply cong_inner_transitivity.
apply cong_symmetry.
apply cong_pseudo_reflexivity.
assumption.
Qed.
Lemma cong_right_commutativity : forall A B C D,
Cong A B C D -> Cong A B D C.
Proof.
intros.
apply cong_symmetry.
apply cong_symmetry in H.
apply cong_left_commutativity.
assumption.
Qed.
Lemma cong_trivial_identity : forall A B : Tpoint,
Cong A A B B.
Proof.
intros.
prolong A B E A A.
eapply cong_inner_transitivity.
apply H0.
assert(B=E).
eapply cong_identity.
apply H0.
subst.
apply cong_reflexivity.
Qed.
Lemma cong_reverse_identity : forall A C D,
Cong A A C D -> C=D.
Proof.
intros.
apply cong_symmetry in H.
eapply cong_identity.
apply H.
Qed.
Lemma cong_commutativity : forall A B C D,
Cong A B C D -> Cong B A D C.
Proof.
intros.
apply cong_left_commutativity.
apply cong_right_commutativity.
assumption.
Qed.
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.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Definition OFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A B A' B' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong B D B' D'.
Lemma five_segments_with_def : forall A B C D A' B' C' D',
OFSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
unfold OFSC.
intros;spliter.
apply (five_segments A A' B B'); assumption.
Qed.
Axiom eq_dec_points : forall A B : Tpoint, A=B \/ ~ A=B.
Lemma cong_diff : forall A B C D : Tpoint, A <> B -> Cong A B C D -> C <> D.
Proof.
intros.
intro.
subst.
apply H.
eauto using cong_identity.
Qed.
Definition Cong_3 := fun A1 A2 A3 B1 B2 B3 => Cong A1 A2 B1 B2 /\ Cong A1 A3 B1 B3 /\ Cong A2 A3 B2 B3.
Lemma cong_3_sym : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
unfold Cong_3.
intuition.
Qed.
Hint Resolve cong_3_sym : Cong.
Lemma cong_3_swap : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 B A C B' A' C'.
Proof.
unfold Cong_3.
intuition.
Qed.
Lemma cong_3_swap_2 : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 A C B A' C' B'.
Proof.
unfold Cong_3.
intuition.
Qed.
Hint Resolve cong_3_swap cong_3_swap_2 : Cong3.
Hint Unfold Cong_3 : Cong3.
Lemma cong3_transitivity : forall A0 B0 C0 A1 B1 C1 A2 B2 C2,
Cong_3 A0 B0 C0 A1 B1 C1 -> Cong_3 A1 B1 C1 A2 B2 C2 -> Cong_3 A0 B0 C0 A2 B2 C2.
unfold Cong_3.
intros.
spliter.
repeat split.
eapply cong_transitivity.
apply H.
assumption.
eapply cong_transitivity.
apply H3.
assumption.
eapply cong_transitivity.
apply H4.
assumption.
Qed.
Hint Resolve cong3_transitivity : Cong3.
Lemma l2_l1 : forall 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.
intros.
induction (eq_dec_points A B).
subst B.
assert (A'=B').
eapply (cong_identity _ _ A).
Cong.
subst.
Cong.
assert (Cong C A C' A')
by (apply (five_segments _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity).
Cong.
Qed.
Lemma construction_unicity : forall 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.
intros.
assert (Cong A x A y) by
(apply cong_transitivity with (C:=B) (D:=C);auto using cong_symmetry).
assert (Cong Q x Q y)
by (apply (l2_l1 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_segments_with_def in H6.
apply cong_identity in H6.
assumption.
assumption.
Qed.
End T1.
Require Export general_tactics.
Section T1.
Context `{M:Tarski}.
Ltac prolong A B x C D :=
assert (sg:= segment_construction A B C D);
ex_and sg x.
Lemma cong_reflexivity : forall A B,
Cong A B A B.
Proof.
intros.
apply (cong_inner_transitivity B A A B);
apply cong_pseudo_reflexivity.
Qed.
Lemma cong_symmetry : forall A B C D : Tpoint,
Cong A B C D -> Cong C D A B.
Proof.
intros.
eapply cong_inner_transitivity.
apply H.
apply cong_reflexivity.
Qed.
Lemma cong_transitivity : forall A B C D E F : Tpoint,
Cong A B C D -> Cong C D E F -> Cong A B E F.
Proof.
intros.
eapply cong_inner_transitivity; eauto using cong_symmetry.
Qed.
Lemma cong_left_commutativity : forall A B C D,
Cong A B C D -> Cong B A C D.
Proof.
intros.
eapply cong_inner_transitivity.
apply cong_symmetry.
apply cong_pseudo_reflexivity.
assumption.
Qed.
Lemma cong_right_commutativity : forall A B C D,
Cong A B C D -> Cong A B D C.
Proof.
intros.
apply cong_symmetry.
apply cong_symmetry in H.
apply cong_left_commutativity.
assumption.
Qed.
Lemma cong_trivial_identity : forall A B : Tpoint,
Cong A A B B.
Proof.
intros.
prolong A B E A A.
eapply cong_inner_transitivity.
apply H0.
assert(B=E).
eapply cong_identity.
apply H0.
subst.
apply cong_reflexivity.
Qed.
Lemma cong_reverse_identity : forall A C D,
Cong A A C D -> C=D.
Proof.
intros.
apply cong_symmetry in H.
eapply cong_identity.
apply H.
Qed.
Lemma cong_commutativity : forall A B C D,
Cong A B C D -> Cong B A D C.
Proof.
intros.
apply cong_left_commutativity.
apply cong_right_commutativity.
assumption.
Qed.
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.
Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.
Definition OFSC := fun A B C D A' B' C' D' =>
Bet A B C /\ Bet A' B' C' /\
Cong A B A' B' /\ Cong B C B' C' /\
Cong A D A' D' /\ Cong B D B' D'.
Lemma five_segments_with_def : forall A B C D A' B' C' D',
OFSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
unfold OFSC.
intros;spliter.
apply (five_segments A A' B B'); assumption.
Qed.
Axiom eq_dec_points : forall A B : Tpoint, A=B \/ ~ A=B.
Lemma cong_diff : forall A B C D : Tpoint, A <> B -> Cong A B C D -> C <> D.
Proof.
intros.
intro.
subst.
apply H.
eauto using cong_identity.
Qed.
Definition Cong_3 := fun A1 A2 A3 B1 B2 B3 => Cong A1 A2 B1 B2 /\ Cong A1 A3 B1 B3 /\ Cong A2 A3 B2 B3.
Lemma cong_3_sym : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 A' B' C' A B C.
Proof.
unfold Cong_3.
intuition.
Qed.
Hint Resolve cong_3_sym : Cong.
Lemma cong_3_swap : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 B A C B' A' C'.
Proof.
unfold Cong_3.
intuition.
Qed.
Lemma cong_3_swap_2 : forall A B C A' B' C',
Cong_3 A B C A' B' C' -> Cong_3 A C B A' C' B'.
Proof.
unfold Cong_3.
intuition.
Qed.
Hint Resolve cong_3_swap cong_3_swap_2 : Cong3.
Hint Unfold Cong_3 : Cong3.
Lemma cong3_transitivity : forall A0 B0 C0 A1 B1 C1 A2 B2 C2,
Cong_3 A0 B0 C0 A1 B1 C1 -> Cong_3 A1 B1 C1 A2 B2 C2 -> Cong_3 A0 B0 C0 A2 B2 C2.
unfold Cong_3.
intros.
spliter.
repeat split.
eapply cong_transitivity.
apply H.
assumption.
eapply cong_transitivity.
apply H3.
assumption.
eapply cong_transitivity.
apply H4.
assumption.
Qed.
Hint Resolve cong3_transitivity : Cong3.
Lemma l2_l1 : forall 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.
intros.
induction (eq_dec_points A B).
subst B.
assert (A'=B').
eapply (cong_identity _ _ A).
Cong.
subst.
Cong.
assert (Cong C A C' A')
by (apply (five_segments _ _ _ _ _ _ _ _ H1 );auto using cong_trivial_identity, cong_commutativity).
Cong.
Qed.
Lemma construction_unicity : forall 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.
intros.
assert (Cong A x A y) by
(apply cong_transitivity with (C:=B) (D:=C);auto using cong_symmetry).
assert (Cong Q x Q y)
by (apply (l2_l1 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_segments_with_def in H6.
apply cong_identity in H6.
assumption.
assumption.
Qed.
End T1.