Library Hilbert_facts
In this file we prove some facts using Hilbert's axioms.
Require Import Classical.
Require Import hilbert_axioms.
Module HilbertFacts (M:Hilbert).
Import M.
Lemma not_between_right : forall A B:Point, ~ Bet A B B.
Proof.
intros.
unfold not;intro;subst.
assert (~ Bet B B A /\ ~ Bet B A B).
apply between_only_one;assumption.
decompose [and] H0;clear H0.
apply between_comm in H.
auto.
Qed.
Hint Resolve not_between_right.
Lemma not_between_left : forall A B:Point, ~ Bet A A B.
Proof.
intros.
unfold not;intro;subst.
assert (~ Bet A B A /\ ~ Bet A A B).
apply between_only_one;assumption.
decompose [and] H0;clear H0.
auto.
Qed.
Hint Resolve not_between_left.
Hint Immediate between_comm.
Section SomeProofs.
Variable A B C : Point.
Lemma between_only_one_left : A<>B -> A<>C -> B<>C -> Bet A B C -> ~(Bet B C A) .
Proof with intuition.
intros.
assert (~(Bet B C A) /\ ~(Bet B A C)).
apply between_only_one...
intuition.
Qed.
Lemma between_only_one_right : A<>B -> A<>C -> B<>C ->
Bet A B C -> ~(Bet B A C).
intros.
assert (~(Bet B C A) /\ ~(Bet B A C)).
apply between_only_one;assumption.
intuition.
Qed.
Lemma Col_comm_left : Col A B C -> Col B A C.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_right : Col A B C -> Col A C B.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_middle : Col A B C -> Col C B A.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_all : Col A B C -> Col C A B /\ Col C B A /\ Col A C B /\ Col B C A.
unfold Col.
intros.
intuition;elim H;intros;exists x;intuition.
Qed.
Lemma existspointline : forall l:Line, exists P:Point, ~ Incid P l.
Proof.
intro.
elim plan.
intros a [b [c H]].
elim (classic (~ Incid a l));intros.
exists a;auto.
elim (classic (~ Incid b l));intros.
exists b;auto.
elim (classic (~ Incid c l));intros.
exists c;auto.
unfold Col in H.
assert (exists l:Line, Incid a l /\ Incid b l /\ Incid c l).
exists l.
apply NNPP;tauto.
intuition.
Qed.
Lemma col_eq_1 : A<>C -> Col A A C.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
Lemma col_eq_2 : A<>C -> Col A C A.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
Lemma col_eq_3 : C<>A -> Col C A A.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
End SomeProofs.
Hint Resolve col_eq_1 col_eq_2 col_eq_3.
Hint Extern 1 (False) => subst.
End HilbertFacts.
Require Import hilbert_axioms.
Module HilbertFacts (M:Hilbert).
Import M.
Lemma not_between_right : forall A B:Point, ~ Bet A B B.
Proof.
intros.
unfold not;intro;subst.
assert (~ Bet B B A /\ ~ Bet B A B).
apply between_only_one;assumption.
decompose [and] H0;clear H0.
apply between_comm in H.
auto.
Qed.
Hint Resolve not_between_right.
Lemma not_between_left : forall A B:Point, ~ Bet A A B.
Proof.
intros.
unfold not;intro;subst.
assert (~ Bet A B A /\ ~ Bet A A B).
apply between_only_one;assumption.
decompose [and] H0;clear H0.
auto.
Qed.
Hint Resolve not_between_left.
Hint Immediate between_comm.
Section SomeProofs.
Variable A B C : Point.
Lemma between_only_one_left : A<>B -> A<>C -> B<>C -> Bet A B C -> ~(Bet B C A) .
Proof with intuition.
intros.
assert (~(Bet B C A) /\ ~(Bet B A C)).
apply between_only_one...
intuition.
Qed.
Lemma between_only_one_right : A<>B -> A<>C -> B<>C ->
Bet A B C -> ~(Bet B A C).
intros.
assert (~(Bet B C A) /\ ~(Bet B A C)).
apply between_only_one;assumption.
intuition.
Qed.
Lemma Col_comm_left : Col A B C -> Col B A C.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_right : Col A B C -> Col A C B.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_middle : Col A B C -> Col C B A.
unfold Col.
intros.
elim H;intros.
exists x.
intuition.
Qed.
Lemma Col_comm_all : Col A B C -> Col C A B /\ Col C B A /\ Col A C B /\ Col B C A.
unfold Col.
intros.
intuition;elim H;intros;exists x;intuition.
Qed.
Lemma existspointline : forall l:Line, exists P:Point, ~ Incid P l.
Proof.
intro.
elim plan.
intros a [b [c H]].
elim (classic (~ Incid a l));intros.
exists a;auto.
elim (classic (~ Incid b l));intros.
exists b;auto.
elim (classic (~ Incid c l));intros.
exists c;auto.
unfold Col in H.
assert (exists l:Line, Incid a l /\ Incid b l /\ Incid c l).
exists l.
apply NNPP;tauto.
intuition.
Qed.
Lemma col_eq_1 : A<>C -> Col A A C.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
Lemma col_eq_2 : A<>C -> Col A C A.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
Lemma col_eq_3 : C<>A -> Col C A A.
Proof.
intros.
unfold Col.
assert (exists l : Line, Incid A l /\ Incid C l).
apply line_existence;auto.
destruct H0 as [l H0].
exists l;intuition.
Qed.
End SomeProofs.
Hint Resolve col_eq_1 col_eq_2 col_eq_3.
Hint Extern 1 (False) => subst.
End HilbertFacts.