Library ProjectiveGeometry.Plane.hexamys_desargues
Require Export hexamys.
Lemma hexamy_desargues_gen_case :
hexamy ->
forall O A B C A' B' C' I J K P Q,
line A B <> line B C ->
line A' B' <> line B' C' ->
line A' B' <> line A B ->
line B' C' <> line B C ->
line O A <> line O C ->
line A' C' <> line A C ->
O<>A -> O<>B -> O<>C ->
O<>A' -> O<>B' -> O<>C' ->
O<>I -> O<>J -> O<>K ->
A<>B -> A<>C ->
A<>A' -> A<>B' -> A<>C' ->
A<>I -> A<>J -> A<>K ->
B<>C ->
B<>A' -> B<>B' -> B<>C' ->
B<>I -> B<>J -> B<>K ->
C<>A' -> C<>B' -> C<>C' ->
C<>I -> C<>J -> C<>K ->
A'<>B' -> A'<>C' ->
A'<>I -> A'<>J -> A'<>K ->
B'<>C' ->
B'<>I -> B'<>J -> B'<>K ->
C'<>I -> C'<>J -> C'<>K ->
I<>J -> I<>K ->
J<>K ->
P<>C -> A<>Q ->
P<>C'-> A'<>Q ->
Q<>C'-> A'<>P ->
Col P B C ->
Col P A' B' ->
Col Q A B ->
Col Q B' C' ->
Col O A A' ->
Col O B B' ->
Col O C C' ->
Col A' C' I ->
Col A C I ->
Col A B J ->
Col A' B' J ->
Col B C K ->
Col B' C' K ->
Col I J K.
Proof.
intros.
geo_norm.
remove_line_occ.
collapse.
not_eq P Q.
not_eq A P.
not_eq C Q.
hexamy_proof A A' P C C' Q A Q C' A' P C.
Qed.
Ltac not_eq_4pt A B C D := match goal with
H1: ?Incid A ?l,
H2: ?Incid B ?l,
H3: ?Incid C ?m,
H4: ?Incid D ?m|- _ => not_eq l m
end.
Lemma desargues_cevian_case :
hexamy ->
forall O A B C A' B' C' P Q R PI,
line A B <> line B C ->
line A' B' <> line B' C' ->
line A' B' <> line A B ->
line B' C' <> line B C ->
line O A <> line O C ->
line A' C' <> line A C ->
A<>B -> B<>C -> A<>C ->
A'<>B' -> B'<>C' -> A'<>C' ->
A <> A' -> B <> B' -> C<>C' ->
O <> A -> O<> B -> O<>C ->
O <> A' -> O<> B' -> O<> C' ->
PI = inter (line O B) (line P Q) ->
A' <> inter (line A' C') (line A PI) ->
Col O A A' ->
Col O B B' ->
Col O C C' ->
Col A' C' Q ->
Col A C Q ->
Col A B P ->
Col A' B' P ->
Col B C R ->
Col B' C' R ->
Col A' B C ->
Col B' A C ->
Col C' A B ->
forall II, Col O B II -> Col P Q II -> O<>II ->
Col P Q R.
Proof.
intro hexa;
intros.
geo_norm.
remove_line_occ.
elim (uniqdec.eq_point_dec P Q);intros.
subst Q;create_line P R lPR;firstorder.
create_inter P Q B C R1.
create_inter P Q B' C' R2.
assert (R1 = R2).
create_inter A' C' A II L.
not_eq L B'.
create_inter A B L B' N.
not_eq A L.
create_inter A L C C' M.
collapse.
remove_line_occ.
assert (Col L N B') by firstorder.
not_eq II A.
not_eq P A'.
not_eq l8 l7.
not_eq A P.
not_eq B' II.
not_eq P II.
not_eq l0 l3.
not_eq Q C.
not_eq II Q.
not_eq l10 l9.
not_eq O Q.
not_eq l2 l3.
not_eq B' Q.
not_eq II L.
not_eq_4pt L B' A P.
not_eq_4pt B' II P A'.
not_eq_4pt II A A' L.
not_eq_4pt P II L A'.
not_eq_4pt II B' A' A.
not_eq A II.
not_eq A' II.
not_eq L P.
not_eq B' P.
not_eq B' A.
not_eq A' L.
assert (Col O N Q) by
hexamy_proof A' L B' II A P A' A P II B' L.
geo_norm;collapse.
not_eq x l7.
not_eq x l5.
not_eq x x0.
not_eq C II.
not_eq B II.
not_eq B Q.
not_eq A Q.
not_eq_4pt C B O II.
not_eq_4pt B A II Q.
not_eq_4pt A O Q C.
not_eq_4pt C O II A.
not_eq_4pt O Q A B.
not_eq_4pt Q II B C.
assert (Col R1 M N) by
hexamy_proof C B A O II Q C O Q II A B.
geo_norm.
not_eq C' Q.
not_eq C' II.
not_eq Q L.
not_eq O L.
not_eq_4pt C' B' O II.
not_eq_4pt B' Q II L.
not_eq_4pt Q O L C'.
not_eq_4pt C' O II L.
not_eq_4pt O Q L B'.
not_eq_4pt Q II B' C'.
not_eq L C'.
assert (Col R2 M N) by
hexamy_proof C' B' Q O II L C' O Q II L B'.
geo_norm.
cases_line x1 x2.
auto.
collapse.
intuition.
subst R2.
geo_norm;collapse;solve_col.
Qed.
Lemma hexamy_desargues_gen_case :
hexamy ->
forall O A B C A' B' C' I J K P Q,
line A B <> line B C ->
line A' B' <> line B' C' ->
line A' B' <> line A B ->
line B' C' <> line B C ->
line O A <> line O C ->
line A' C' <> line A C ->
O<>A -> O<>B -> O<>C ->
O<>A' -> O<>B' -> O<>C' ->
O<>I -> O<>J -> O<>K ->
A<>B -> A<>C ->
A<>A' -> A<>B' -> A<>C' ->
A<>I -> A<>J -> A<>K ->
B<>C ->
B<>A' -> B<>B' -> B<>C' ->
B<>I -> B<>J -> B<>K ->
C<>A' -> C<>B' -> C<>C' ->
C<>I -> C<>J -> C<>K ->
A'<>B' -> A'<>C' ->
A'<>I -> A'<>J -> A'<>K ->
B'<>C' ->
B'<>I -> B'<>J -> B'<>K ->
C'<>I -> C'<>J -> C'<>K ->
I<>J -> I<>K ->
J<>K ->
P<>C -> A<>Q ->
P<>C'-> A'<>Q ->
Q<>C'-> A'<>P ->
Col P B C ->
Col P A' B' ->
Col Q A B ->
Col Q B' C' ->
Col O A A' ->
Col O B B' ->
Col O C C' ->
Col A' C' I ->
Col A C I ->
Col A B J ->
Col A' B' J ->
Col B C K ->
Col B' C' K ->
Col I J K.
Proof.
intros.
geo_norm.
remove_line_occ.
collapse.
not_eq P Q.
not_eq A P.
not_eq C Q.
hexamy_proof A A' P C C' Q A Q C' A' P C.
Qed.
Ltac not_eq_4pt A B C D := match goal with
H1: ?Incid A ?l,
H2: ?Incid B ?l,
H3: ?Incid C ?m,
H4: ?Incid D ?m|- _ => not_eq l m
end.
Lemma desargues_cevian_case :
hexamy ->
forall O A B C A' B' C' P Q R PI,
line A B <> line B C ->
line A' B' <> line B' C' ->
line A' B' <> line A B ->
line B' C' <> line B C ->
line O A <> line O C ->
line A' C' <> line A C ->
A<>B -> B<>C -> A<>C ->
A'<>B' -> B'<>C' -> A'<>C' ->
A <> A' -> B <> B' -> C<>C' ->
O <> A -> O<> B -> O<>C ->
O <> A' -> O<> B' -> O<> C' ->
PI = inter (line O B) (line P Q) ->
A' <> inter (line A' C') (line A PI) ->
Col O A A' ->
Col O B B' ->
Col O C C' ->
Col A' C' Q ->
Col A C Q ->
Col A B P ->
Col A' B' P ->
Col B C R ->
Col B' C' R ->
Col A' B C ->
Col B' A C ->
Col C' A B ->
forall II, Col O B II -> Col P Q II -> O<>II ->
Col P Q R.
Proof.
intro hexa;
intros.
geo_norm.
remove_line_occ.
elim (uniqdec.eq_point_dec P Q);intros.
subst Q;create_line P R lPR;firstorder.
create_inter P Q B C R1.
create_inter P Q B' C' R2.
assert (R1 = R2).
create_inter A' C' A II L.
not_eq L B'.
create_inter A B L B' N.
not_eq A L.
create_inter A L C C' M.
collapse.
remove_line_occ.
assert (Col L N B') by firstorder.
not_eq II A.
not_eq P A'.
not_eq l8 l7.
not_eq A P.
not_eq B' II.
not_eq P II.
not_eq l0 l3.
not_eq Q C.
not_eq II Q.
not_eq l10 l9.
not_eq O Q.
not_eq l2 l3.
not_eq B' Q.
not_eq II L.
not_eq_4pt L B' A P.
not_eq_4pt B' II P A'.
not_eq_4pt II A A' L.
not_eq_4pt P II L A'.
not_eq_4pt II B' A' A.
not_eq A II.
not_eq A' II.
not_eq L P.
not_eq B' P.
not_eq B' A.
not_eq A' L.
assert (Col O N Q) by
hexamy_proof A' L B' II A P A' A P II B' L.
geo_norm;collapse.
not_eq x l7.
not_eq x l5.
not_eq x x0.
not_eq C II.
not_eq B II.
not_eq B Q.
not_eq A Q.
not_eq_4pt C B O II.
not_eq_4pt B A II Q.
not_eq_4pt A O Q C.
not_eq_4pt C O II A.
not_eq_4pt O Q A B.
not_eq_4pt Q II B C.
assert (Col R1 M N) by
hexamy_proof C B A O II Q C O Q II A B.
geo_norm.
not_eq C' Q.
not_eq C' II.
not_eq Q L.
not_eq O L.
not_eq_4pt C' B' O II.
not_eq_4pt B' Q II L.
not_eq_4pt Q O L C'.
not_eq_4pt C' O II L.
not_eq_4pt O Q L B'.
not_eq_4pt Q II B' C'.
not_eq L C'.
assert (Col R2 M N) by
hexamy_proof C' B' Q O II L C' O Q II L B'.
geo_norm.
cases_line x1 x2.
auto.
collapse.
intuition.
subst R2.
geo_norm;collapse;solve_col.
Qed.