Theory Desargues_Property

theory Desargues_Property
  imports Main Projective_Plane_Axioms Pappus_Property Pascal_Property
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We formalize Desargues's property, @{term "desargues_prop"}, that states that if two triangles are perspective 
from a point, then they are perspective from a line. 
Note that some planes satisfy that property and some others don't, hence Desargues's property is
not a theorem though it is a theorem in projective space geometry. 
›

section ‹Desargues's Property›

context projective_plane
begin

lemma distinct3_def:
  "distinct [A, B, C] = (A ≠ B ∧ A ≠ C ∧ B ≠ C)"
  by auto

definition triangle :: "['point, 'point, 'point] ⇒ bool" where
"triangle A B C ≡ distinct [A,B,C] ∧ (line A B ≠ line A C)"

definition meet_in :: "'line ⇒ 'line => 'point => bool " where
"meet_in l m P ≡ incid P l ∧ incid P m"

lemma meet_col_1:
  assumes "meet_in (line A B) (line C D) P"
  shows "col A B P"
  using assms col_def incidA_lAB incidB_lAB meet_in_def 
  by blast

lemma meet_col_2:
  assumes "meet_in (line A B) (line C D) P"
  shows "col C D P"
  using assms meet_col_1 meet_in_def 
  by auto

definition meet_3_in :: "['line, 'line, 'line, 'point] ⇒ bool" where
"meet_3_in l m n P ≡ meet_in l m P ∧ meet_in l n P"

lemma meet_all_3:
  assumes "meet_3_in l m n P"
  shows "meet_in m n P"
  using assms meet_3_in_def meet_in_def 
  by auto

lemma meet_comm:
  assumes "meet_in l m P"
  shows "meet_in m l P"
  using assms meet_in_def 
  by auto

lemma meet_3_col_1:
  assumes "meet_3_in (line A B) m n P"
  shows "col A B P"
  using assms meet_3_in_def meet_col_2 meet_in_def 
  by auto

lemma meet_3_col_2:
  assumes "meet_3_in l (line A B) n P"
  shows "col A B P"
  using assms col_def incidA_lAB incidB_lAB meet_3_in_def meet_in_def 
  by blast

lemma meet_3_col_3:
  assumes "meet_3_in l m (line A B) P"
  shows "col A B P"
  using assms meet_3_col_2 meet_3_in_def 
  by auto

lemma distinct7_def: "distinct [A,B,C,D,E,F,G] = ((A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D) ∧ (A ≠ E) ∧ (A ≠ F) ∧ (A ≠ G) ∧
(B ≠ C) ∧ (B ≠ D) ∧ (B ≠ E) ∧ (B ≠ F) ∧ (B ≠ G) ∧
(C ≠ D) ∧ (C ≠ E) ∧ (C ≠ F) ∧ (C ≠ G) ∧
(D ≠ E) ∧ (D ≠ F) ∧ (D ≠ G) ∧
(E ≠ F) ∧ (E ≠ G) ∧
(F ≠ G))"
  by auto


(* From now on we give less general statements on purpose to avoid a lot of uninteresting 
degenerate cases, since we can hardly think of any interesting application where one would need 
to instantiate a statement on such degenerate case, hence our statements and proofs will be more 
textbook-like. For the working mathematician the only thing that probably matters is the main
theorem without considering all the degenerate cases for which the statement might still hold. *)

definition desargues_config :: 
  "['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool" where
"desargues_config A B C A' B' C' M N P R ≡ distinct [A,B,C,A',B',C',R] ∧ ¬ col A B C 
∧ ¬ col A' B' C' ∧ distinct [(line A A'),(line B B'),(line C C')] ∧ 
meet_3_in (line A A') (line B B') (line C C') R ∧ (line A B) ≠ (line A' B') ∧ 
(line B C) ≠ (line B' C') ∧ (line A C) ≠ (line A' C') ∧ meet_in (line B C) (line B' C') M ∧
meet_in (line A C) (line A' C') N ∧ meet_in (line A B) (line A' B') P"

lemma distinct7_rot_CW:
  assumes "distinct [A,B,C,D,E,F,G]"
  shows "distinct [C,A,B,F,D,E,G]"
  using assms distinct7_def 
  by auto

(* Desargues configurations are stable under any rotation (i,j,k) of {1,2,3} *)
lemma desargues_config_rot_CW:
  assumes "desargues_config A B C A' B' C' M N P R"
  shows "desargues_config C A B C' A' B' P M N R"
  by (smt assms col_rot_CW desargues_config_def distinct3_def distinct7_rot_CW line_comm 
      meet_3_in_def meet_all_3 meet_comm)

lemma desargues_config_rot_CCW:
  assumes "desargues_config A B C A' B' C' M N P R"
  shows "desargues_config B C A B' C' A' N P M R"
  by (simp add: assms desargues_config_rot_CW)

(* With the two following definitions we repackage the definition of a Desargues configuration in a 
"high-level", i.e. textbook-like, way. *)

definition are_perspective_from_point :: 
  "['point, 'point, 'point, 'point, 'point, 'point, 'point] ⇒ bool" where
"are_perspective_from_point A B C A' B' C' R ≡ distinct [A,B,C,A',B',C',R] ∧ triangle A B C ∧
triangle A' B' C' ∧ distinct [(line A A'),(line B B'),(line C C')] ∧ 
meet_3_in (line A A') (line B B') (line C C') R"

definition are_perspective_from_line ::
  "['point, 'point, 'point, 'point, 'point, 'point] ⇒ bool" where
"are_perspective_from_line A B C A' B' C' ≡ distinct [A,B,C,A',B',C'] ⟶ triangle A B C ⟶
triangle A' B' C' ⟶ line A B ≠ line A' B' ⟶ line A C ≠ line A' C' ⟶ line B C ≠ line B' C' ⟶
col (inter (line A B) (line A' B')) (inter (line A C) (line A' C')) (inter (line B C) (line B' C'))"

lemma meet_in_inter:
  assumes "l ≠ m"
  shows "meet_in l m (inter l m)"
  by (simp add: incid_inter_left incid_inter_right meet_in_def)

lemma perspective_from_point_desargues_config:
  assumes "are_perspective_from_point A B C A' B' C' R" and "line A B ≠ line A' B'" and 
    "line A C ≠ line A' C'" and "line B C ≠ line B' C'"
  shows "desargues_config A B C A' B' C' (inter (line B C) (line B' C')) (inter (line A C) (line A' C')) 
    (inter (line A B) (line A' B')) R"
  unfolding desargues_config_def distinct7_def distinct3_def

  using assms are_perspective_from_point_def  apply auto
      apply (smt (z3) ax_uniqueness col_2cycle col_line_ext_1 incidB_lAB line_ext_def mem_Collect_eq triangle_def)
  apply (smt (z3) ax_uniqueness col_def incidA_lAB line_comm triangle_def)
  using meet_in_inter apply presburger+
  done

(* Now, we state Desargues's property in a textbook-like form *)
definition desargues_prop :: "bool" where
"desargues_prop ≡ 
∀A B C A' B' C' P. 
  are_perspective_from_point A B C A' B' C' P ⟶ are_perspective_from_line A B C A' B' C'"

end

end