Theory Complex_Angles

theory Complex_Angles

imports Complex_Geometry.Elementary_Complex_Geometry

begin
section ‹Introduction›

text ‹
Morley's trisector theorem states that in any triangle, 
the three points of intersection of the adjacent angle trisectors 
form an equilateral triangle, 
called the first Morley triangle or simply the Morley triangle. This theorem is
listed in the 100 theorem list \cite{source3}.

In this theory, we define some basics elements on complex geometry such as
axial symmetry, rotations. We also define basic property of congruent triangles in the
complex field following the model already presented in the afp \cite{Triangle-AFP}
In addition we demonstrate sines law in the complex context.

Finally we prove the Morley theorem using Alain Connes's proof \cite{source1}.
›
section ‹Angles between three complex›

definition angle_c_def:‹angle_c a b c ≡ ∠ (a-b) (c-b)›

lemma angle_c_commute_pi:
  assumes ‹angle_c a b c = pi›
  shows "angle_c a b c =  angle_c c b a"
  using angle_c_def assms ang_vec_sym_pi by presburger

lemma angle_c_commute:
  assumes ‹angle_c a b c ≠ pi›
  shows "angle_c a b c =  -angle_c c b a"
  using angle_c_def assms ang_vec_sym by presburger

lemma angle_c_sum:
  assumes 1:‹a - b≠0› and 2:‹c - b≠ 0› and 3:‹b-d ≠ 0›
  shows‹⇂angle_c a b c + angle_c c b d⇃ = angle_c a b d›
  using angle_c_def canon_ang_sum by force


lemma collinear_angle:‹collinear a b c ⟹ a≠b ⟹ b≠c ⟹ c≠a ⟹ angle_c a b c = 0 ∨ angle_c a b c = pi›
  unfolding collinear_def unfolding angle_c_def  
  by (metis ang_vec_def arg_div collinear_def collinear_sym2' is_real_arg2 right_minus_eq)

lemma cdist_commute:‹cdist a b = cdist b a›
  by (simp add: norm_minus_commute)

lemma angle_sum_triangle:
  assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c"
  shows   "⇂∠ (c-a) (b-a) + ∠ (a-b) (c-b)  + ∠ (b-c) (a-c)⇃ = pi"
proof -
  have f0:‹b-a ≠ 0› ‹c-a≠0› ‹b-c≠0› using h by auto
  then have ‹∠c (c-a) (b-a) = abs (Arg ((b-a)/(c-a)))› 
    unfolding ang_vec_def ang_vec_c_def 
    apply(subst arg_div[OF f0(1) f0(2), symmetric])
    by(simp) 
  have ‹(b-a)/(c-a) = rcis (cmod ((b-a)/(c-a))) (Arg ((b-a)/(c-a)))›
    by (simp add: rcis_cmod_Arg)
  have ‹(b-a)/(c-a) * (c-b)/(a-b) * (a-c)/(b-c) = -1›
    using h  
    by (smt (z3) divide_eq_0_iff divide_eq_minus_1_iff f0(1,2,3) minus_diff_eq mult_minus_right
        nonzero_eq_divide_eq times_divide_eq_left) 
  then have ‹Arg ((b-a)/(c-a) * (c-b)/(a-b) * (a-c)/(b-c)) = pi› 
    by (metis arg_cis cis_pi pi_canonical)
  then have ‹Arg ((b-a)/(c-a) * (c-b)/(a-b) * (a-c)/(b-c))
 = ⇂Arg ((b-a)/(c-a) * (c-b)/(a-b)) + Arg ((a-c)/(b-c))⇃›
    using arg_mult f0 
    by (metis (no_types, lifting) Arg_zero arg_mult divide_divide_eq_left' pi_neq_zero times_divide_eq_left
        times_divide_eq_right) 
  then have ‹⇂Arg ((b-a)/(c-a) * (c-b)/(a-b)) + Arg ((a-c)/(b-c))⇃
=⇂Arg ((b-a)/(c-a)) + Arg ((c-b)/(a-b)) + Arg ((a-c)/(b-c))⇃›
    by (metis (no_types, lifting) arg_mult canon_ang_arg canon_ang_sum divide_eq_0_iff eq_iff_diff_eq_0 h
        no_zero_divisors times_divide_eq_right)
  then show ?thesis
    using
      ‹Arg ((b - a) / (c - a) * (c - b) / (a - b) * (a - c) / (b - c)) = ⇂Arg ((b - a) / (c - a) * (c - b) / (a - b)) + Arg ((a - c) / (b - c))⇃›
      ‹Arg ((b - a) / (c - a) * (c - b) / (a - b) * (a - c) / (b - c)) = pi› arg_div h by force
qed

lemma angle_sum_triangle_c:
  assumes h:"a ≠ b ∧ b ≠ c ∧ a ≠ c"
  shows   "⇂angle_c c a b + angle_c a b c  + angle_c b c a⇃ = pi"
  unfolding angle_c_def
  using h by (smt (z3) angle_sum_triangle h)


lemma angle_sum_triangle':
  assumes h:"a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0"
  shows   "⇂∠ (-a) b + ∠ (-b) c  + ∠ (-c) a⇃ = pi"
proof -
  have f0:‹a ≠ 0› ‹b≠0› ‹c≠0› using h by auto
  have ‹b/(-a) * a/(-c) * c/(-b) = -1›
    using h by(auto) 
  then have f10:‹Arg (b/(-a) * a/(-c) * c/(-b)) = pi› 
    by (metis arg_cis cis_pi pi_canonical)
  then have f1:‹Arg (b/(-a) * a/(-c) * c/(-b))
 = ⇂Arg (b/(-a) * a/(-c)) + Arg (c/(-b))⇃›
    using arg_mult f0 
    by (metis ‹b / - a * a / - c * c / - b = - 1› divide_eq_0_iff divide_eq_minus_1_iff
        times_divide_eq_right)
  then have f2:‹⇂Arg (b/(-a) * a/(-c)) + Arg (c/(-b))⇃
=⇂Arg (b/(-a)) + Arg (a/(-c)) + Arg (c/(-b))⇃›
    by (metis (no_types, lifting) arg_mult canon_ang_arg canon_ang_sum divide_eq_0_iff f0(1,2,3)
        neg_0_equal_iff_equal no_zero_divisors times_divide_eq_right)  
  then show ?thesis
    using f1 f2 arg_div h 
    by (smt (verit) f10 add.left_commute ang_vec_def neg_equal_0_iff_equal)
qed

lemma ang_c_in:‹angle_c a b c ∈ {-pi<..pi}›
  unfolding angle_c_def by(auto simp: canon_ang) 

lemma angle_c_aac:‹angle_c a a c = ⇂Arg (c-a)⇃›
  by (simp add: Arg_zero angle_c_def)

lemma angle_c_caa:‹angle_c c a a = ⇂-Arg (c-a)⇃›
  by (simp add: Arg_zero angle_c_def)

lemma angle_c_neq0:‹angle_c p q r ≠ 0  ⟹ p≠r ›
  unfolding angle_c_def 
  by force

end