Theory Desargues_3D

theory Desargues_3D
  imports Main Higher_Projective_Space_Rank_Axioms Matroid_Rank_Properties
begin

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

text ‹
Contents:
▪ We prove Desargues's theorem: if two triangles ABC and A'B'C' are perspective from a point P (ie. 
the lines AA', BB' and CC' are concurrent in P), then they are perspective from a line (ie. the points
‹α = BC ∩ B'C'›, ‹β = AC ∩ A'C'› and ‹γ = AB ∩ A'B'› are collinear).
In this file we restrict ourself to the case where the two triangles ABC and A'B'C' are not coplanar. 
›

section ‹Desargues's Theorem: The Non-coplanar Case›

context higher_projective_space_rank
begin

definition desargues_config_3D :: 
  "['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool" 
  where "desargues_config_3D A B C A' B' C' P α β γ ≡ rk {A, B, C} = 3 ∧ rk {A', B', C'} = 3 ∧ 
rk {A, A', P} = 2 ∧ rk {B, B', P} = 2 ∧ rk {C, C', P} = 2 ∧ rk {A, B, C, A', B', C'} ≥ 4 ∧ 
rk {B, C, α} = 2 ∧ rk {B', C', α} = 2 ∧ rk {A, C, β} = 2 ∧ rk {A', C', β} = 2 ∧ rk {A, B, γ} = 2 ∧
rk {A', B', γ} = 2"

lemma coplanar_4 :
  assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" 
  shows "rk {A, B, C, α} = 3"
proof-
  have f1:"rk {A, B, C, α} ≥ 3" 
    using matroid_ax_2
    by (metis assms(1) empty_subsetI insert_mono)
  have "rk {A, B, C, α} + rk {B, C} ≤ rk {A, B, C} + rk {B, C, α}" 
    using matroid_ax_3_alt
    by (metis Un_insert_right add_One_commute add_mono assms(1) assms(2) matroid_ax_2_alt 
        nat_1_add_1 numeral_plus_one rk_singleton semiring_norm(3) sup_bot.right_neutral)
  then have f2:"rk {A, B, C, α} ≤ 3"
    by (metis Un_insert_right add_One_commute assms(2) matroid_ax_2_alt numeral_plus_one 
        semiring_norm(3) sup_bot.right_neutral)
  from f1 and f2 show "rk {A, B, C, α} = 3" 
    by auto
qed

lemma desargues_config_3D_coplanar_4 :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, α} = 3" and "rk {A', B', C', α} = 3"
proof-
  show "rk {A, B, C, α} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4 
    by blast
  show "rk {A', B', C', α} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4 
    by blast
qed

lemma coplanar_4_bis :
  assumes "rk {A, B, C} = 3" and "rk {A, C, β} = 2"
  shows "rk {A, B, C, β} = 3"
  by (smt assms(1) assms(2) coplanar_4 insert_commute)

lemma desargues_config_3D_coplanar_4_bis :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, β} = 3" and "rk {A', B', C', β} = 3"
proof-
  show "rk {A, B, C, β} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_bis 
    by auto
  show "rk {A', B', C', β} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_bis 
    by auto
qed

lemma coplanar_4_ter :
  assumes "rk {A, B, C} = 3" and "rk {A, B, γ} = 2"
  shows "rk {A, B, C, γ} = 3"
  by (smt assms(1) assms(2) coplanar_4 insert_commute)

lemma desargues_config_3D_coplanar_4_ter :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, γ} = 3" and "rk {A', B', C', γ} = 3"
proof-
  show "rk {A, B, C, γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_ter 
    by auto
  show "rk {A', B', C', γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_ter 
    by auto
qed

lemma coplanar_5 :
  assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, C, β} = 2"
  shows "rk {A, B, C, α, β} = 3"
proof-
  have f1:"rk {A, B, C, α} = 3" 
    using coplanar_4
    by (smt One_nat_def Un_assoc Un_commute add.commute add_Suc_right assms(1) assms(2) insert_is_Un 
        le_antisym matroid_ax_2_alt numeral_2_eq_2 numeral_3_eq_3 one_add_one)
  have f2:"rk {A, B, C, β} = 3" 
    using coplanar_4_bis
    by (smt One_nat_def Un_assoc Un_commute add.commute add_Suc_right assms(1) assms(3) insert_is_Un 
        le_antisym matroid_ax_2_alt numeral_2_eq_2 numeral_3_eq_3 one_add_one)
  from f1 and f2 show "rk {A, B, C, α, β} = 3" 
    using matroid_ax_3_alt'
    by (metis Un_assoc assms(1) insert_is_Un)
qed

lemma desargues_config_3D_coplanar_5 :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, α, β} = 3" and "rk {A', B', C', α, β} = 3"
proof-
  show "rk {A, B, C, α, β} = 3"
    using assms desargues_config_3D_def coplanar_5 
    by auto
  show "rk {A', B', C', α, β} = 3"
    using assms desargues_config_3D_def coplanar_5 
    by auto
qed


lemma coplanar_5_bis :
  assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, B, γ} = 2"
  shows "rk {A, B, C, α, γ} = 3"
  by (smt assms coplanar_5 insert_commute)

lemma desargues_config_3D_coplanar_5_bis :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, α, γ} = 3" and "rk {A', B', C', α, γ} = 3"
proof-
  show "rk {A, B, C, α, γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_5_bis 
    by auto
  show "rk {A', B', C', α, γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_5_bis 
    by auto
qed

lemma coplanar_6 :
  assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, B, γ} = 2" and "rk {A, C, β} = 2"
  shows "rk {A, B, C, α, β, γ} = 3"
proof-
  have f1:"rk {A, B, C, α, γ} = 3" 
    using coplanar_5_bis assms(1) assms(2) assms(3) 
    by auto
  have f2:"rk {A, B, C, α, β} = 3"
    using coplanar_5 assms(1) assms(2) assms(4) 
    by auto
  have f3:"rk {A, B, C, α} = 3" 
    using coplanar_4 assms(1) assms(2) 
    by auto
  from f1 and f2 and f3 show "rk {A, B, C, α, β, γ} = 3" 
    using matroid_ax_3_alt'[of "{A, B, C, α}" "β" "γ"]
    by (metis Un_insert_left sup_bot.left_neutral)
qed

lemma desargues_config_3D_coplanar_6 :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, α, β, γ} = 3" and "rk {A', B', C', α, β, γ} = 3"
proof-
  show "rk {A, B, C, α, β, γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_6 
    by auto
  show "rk {A', B', C', α, β, γ} = 3"
    using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_6 
    by auto
qed

lemma desargues_config_3D_non_coplanar :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {A, B, C, A', B', C', α, β, γ} ≥ 4" 
proof-
  have "rk {A, B, C, A', B', C'} ≤ rk {A, B, C, A', B', C', α, β, γ}" 
    using matroid_ax_2 
    by auto
  thus "4 ≤ rk {A, B, C, A', B', C', α, β, γ}" 
    using matroid_ax_2 assms desargues_config_3D_def[of A B C A' B' C' P α β γ] 
    by linarith
qed

theorem desargues_3D :
  assumes "desargues_config_3D A B C A' B' C' P α β γ"
  shows "rk {α, β, γ} ≤ 2"
proof-
  have "rk {A, B, C, A', B', C', α, β, γ} + rk {α, β, γ} ≤ rk {A, B, C, α, β, γ} + rk {A', B', C', α, β, γ}"
    using matroid_ax_3_alt[of "{α, β, γ}" "{A, B, C, α, β, γ}" "{A', B', C', α, β, γ}"]
    by (simp add: insert_commute)
  then have "rk {α, β, γ} ≤ rk {A, B, C, α, β, γ} + rk {A', B', C', α, β, γ} - rk {A, B, C, A', B', C', α, β, γ}"
    by linarith
  thus "rk {α, β, γ} ≤ 2" 
    using assms desargues_config_3D_coplanar_6 desargues_config_3D_non_coplanar
    by fastforce
qed

end

end