Theory More_Transcendental
section ‹Introduction›
text ‹The complex plane or some of its parts (e.g., the unit disc or the upper half plane) are often
taken as the domain in which models of various geometries (both Euclidean and non-Euclidean ones)
are formalized. The complex plane gives simpler and more compact formulas than the Cartesian plane.
Within complex plane is easier to describe geometric objects and perform the calculations (usually
shedding some new light on the subject). We give a formalization of the extended complex
plane (given both as a complex projective space and as the Riemann sphere), its objects (points,
circles and lines), and its transformations (Möbius transformations).›
section ‹Related work›
text‹During the last decade, there have been many results in formalizing
geometry in proof-assistants. Parts of Hilbert’s seminal book
,,Foundations of Geometry'' \cite{hilbert} have been formalized both
in Coq and Isabelle/Isar. Formalization of first two groups of axioms
in Coq, in an intuitionistic setting was done by Dehlinger et
al. \cite{hilbert-coq}. First formalization in Isabelle/HOL was done
by Fleuriot and Meikele \cite{hilbert-isabelle}, and some further
developments were made in master thesis of Scott \cite{hilbert-scott}.
Large fragments of Tarski's geometry \cite{tarski} have been
formalized in Coq by Narboux et al. \cite{narboux-tarski}. Within Coq,
there are also formalizations of von Plato’s constructive geometry by
Kahn \cite{vonPlato,von-plato-formalization}, French high school
geometry by Guilhot \cite{guilhot} and ruler and compass geometry by
Duprat \cite{duprat2008}, etc.
In our previous work \cite{petrovic2012formalizing}, we have already
formally investigated a Cartesian model of Euclidean geometry.
›
section ‹Background theories›
text ‹In this section we introduce some basic mathematical notions and prove some lemmas needed in the rest of our
formalization. We describe:
▪ trigonometric functions,
▪ complex numbers,
▪ systems of two and three linear equations with two unknowns (over arbitrary fields),
▪ quadratic equations (over real and complex numbers), systems of quadratic and real
equations, and systems of two quadratic equations,
▪ two-dimensional vectors and matrices over complex numbers.
›
subsection ‹Library Additions for Trigonometric Functions›
theory More_Transcendental
imports Complex_Main
begin
text ‹Additional properties of @{term sin} and @{term cos} functions that are later used in proving
conjectures for argument of complex number.›
text ‹Sign of trigonometric functions on some characteristic intervals.›
lemma cos_lt_zero_on_pi2_pi [simp]:
assumes "x > pi/2" and "x ≤ pi"
shows "cos x < 0"
using cos_gt_zero_pi[of "pi - x"] assms
by simp
text ‹Value of trigonometric functions in points $k\pi$ and $\frac{\pi}{2} + k\pi$.›
lemma sin_kpi [simp]:
fixes k::int
shows "sin (k * pi) = 0"
by (simp add: sin_zero_iff_int2)
lemma cos_odd_kpi [simp]:
fixes k::int
assumes "odd k"
shows "cos (k * pi) = -1"
proof (cases "k ≥ 0")
case True
hence "odd (nat k)"
using ‹odd k›
by (auto simp add: even_nat_iff)
thus ?thesis
using ‹k ≥ 0› cos_npi[of "nat k"]
by auto
next
case False
hence "-k ≥ 0" "odd (nat (-k))"
using ‹odd k›
by (auto simp add: even_nat_iff)
thus ?thesis
using cos_npi[of "nat (-k)"]
by auto
qed
lemma cos_even_kpi [simp]:
fixes k::int
assumes "even k"
shows "cos (k * pi) = 1"
proof (cases "k ≥ 0")
case True
hence "even (nat k)"
using ‹even k›
by (simp add: even_nat_iff)
thus ?thesis
using ‹k ≥ 0› cos_npi[of "nat k"]
by auto
next
case False
hence "-k ≥ 0" "even (nat (-k))"
using ‹even k›
by (auto simp add: even_nat_iff)
thus ?thesis
using cos_npi[of "nat (-k)"]
by auto
qed
lemma sin_pi2_plus_odd_kpi [simp]:
fixes k::int
assumes "odd k"
shows "sin (pi / 2 + k * pi) = -1"
using assms
by (simp add: sin_add)
lemma sin_pi2_plus_even_kpi [simp]:
fixes k::int
assumes "even k"
shows "sin (pi / 2 + k * pi) = 1"
using assms
by (simp add: sin_add)
text ‹Solving trigonometric equations and systems with special values (0, 1, or -1) of sine and cosine functions›
lemma cos_0_iff_canon:
assumes "cos φ = 0" and "-pi < φ" and "φ ≤ pi"
shows "φ = pi/2 ∨ φ = -pi/2"
proof-
obtain k::int where "odd k" "φ = k * pi/2"
using cos_zero_iff_int[of φ] assms(1)
by auto
thus ?thesis
proof (cases "k > 1 ∨ k < -1")
case True
hence "k ≥ 3 ∨ k ≤ -3"
using ‹odd k›
by (smt dvd_refl even_minus)
hence "φ ≥ 3*pi/2 ∨ φ ≤ -3*pi/2"
using mult_right_mono[of k "-3" "pi / 2"]
using ‹φ = k * pi/2›
by auto
thus ?thesis
using ‹- pi < φ› ‹φ ≤ pi›
by auto
next
case False
hence "k = -1 ∨ k = 0 ∨ k = 1"
by auto
hence "k = -1 ∨ k = 1"
using ‹odd k›
by auto
thus ?thesis
using ‹φ = k * pi/2›
by auto
qed
qed
lemma sin_0_iff_canon:
assumes "sin φ = 0" and "-pi < φ" and "φ ≤ pi"
shows "φ = 0 ∨ φ = pi"
proof-
obtain k::int where "even k" "φ = k * pi/2"
using sin_zero_iff_int[of φ] assms(1)
by auto
thus ?thesis
proof (cases "k > 2 ∨ k < 0")
case True
hence "k ≥ 4 ∨ k ≤ -2"
using ‹even k›
by (smt evenE)
hence "φ ≥ 2*pi ∨ φ ≤ -pi"
proof
assume "4 ≤ k"
hence "4 * pi/2 ≤ φ"
using mult_right_mono[of "4" "k" "pi/2"]
by (subst ‹φ = k * pi/2›) auto
thus ?thesis
by simp
next
assume "k ≤ -2"
hence "-2*pi/2 ≥ φ"
using mult_right_mono[of "k" "-2" "pi/2"]
by (subst ‹φ = k * pi/2›, auto)
thus ?thesis
by simp
qed
thus ?thesis
using ‹- pi < φ› ‹φ ≤ pi›
by auto
next
case False
hence "k = 0 ∨ k = 1 ∨ k = 2"
by auto
hence "k = 0 ∨ k = 2"
using ‹even k›
by auto
thus ?thesis
using ‹φ = k * pi/2›
by auto
qed
qed
lemma cos0_sin1:
assumes "cos φ = 0" and "sin φ = 1"
shows "∃ k::int. φ = pi/2 + 2*k*pi"
proof-
from ‹cos φ = 0›
obtain k::int where "odd k" "φ = k * (pi / 2)"
using cos_zero_iff_int[of "φ"]
by auto
then obtain k'::int where "k = 2*k' + 1"
using oddE by blast
hence "φ = pi/2 + (k' * pi)"
using ‹φ = k * (pi / 2)›
by (auto simp add: field_simps)
hence "even k'"
using ‹sin φ = 1› sin_pi2_plus_odd_kpi[of k']
by auto
thus ?thesis
using ‹φ = pi /2 + (k' * pi)›
unfolding even_iff_mod_2_eq_zero
by auto
qed
lemma cos1_sin0:
assumes "cos φ = 1" and "sin φ = 0"
shows "∃ k::int. φ = 2*k*pi"
proof-
from ‹sin φ = 0›
obtain k::int where "even k" "φ = k * (pi / 2)"
using sin_zero_iff_int[of "φ"]
by auto
then obtain k'::int where "k = 2*k'"
using evenE by blast
hence "φ = k' * pi"
using ‹φ = k * (pi / 2)›
by (auto simp add: field_simps)
hence "even k'"
using ‹cos φ = 1› cos_odd_kpi[of k']
by auto
thus ?thesis
using ‹φ = k' * pi›
using assms(1) cos_one_2pi_int by auto
qed
text ‹Sine is injective on $[-\frac{\pi}{2}, \frac{\pi}{2}]$›
lemma sin_inj:
assumes "-pi/2 ≤ α ∧ α ≤ pi/2" and "-pi/2 ≤ α' ∧ α' ≤ pi/2"
assumes "α ≠ α'"
shows "sin α ≠ sin α'"
using assms
using sin_monotone_2pi[of α α'] sin_monotone_2pi[of α' α]
by (cases "α < α'") auto
text ‹Periodicity of trigonometric functions›
text ‹The following are available in HOL-Decision\_Procs.Approximation\_Bounds, but we want to avoid
that dependency›
lemma sin_periodic_nat [simp]:
fixes n :: nat
shows "sin (x + n * (2 * pi)) = sin x"
proof (induct n arbitrary: x)
case (Suc n)
have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi"
unfolding Suc_eq_plus1 distrib_right
by (auto simp add: field_simps)
show ?case unfolding split_pi_off using Suc by auto
qed auto
lemma sin_periodic_int [simp]:
fixes i :: int
shows "sin (x + i * (2 * pi)) = sin x"
proof(cases "0 ≤ i")
case True
thus ?thesis
using sin_periodic_nat[of x "nat i"]
by auto
next
case False hence i_nat: "i = - real (nat (-i))" by auto
have "sin x = sin (x + i * (2 * pi) - i * (2 * pi))" by auto
also have "… = sin (x + i * (2 * pi))"
unfolding i_nat mult_minus_left diff_minus_eq_add by (rule sin_periodic_nat)
finally show ?thesis by auto
qed
lemma cos_periodic_nat [simp]:
fixes n :: nat
shows "cos (x + n * (2 * pi)) = cos x"
proof (induct n arbitrary: x)
case (Suc n)
have split_pi_off: "x + (Suc n) * (2 * pi) = (x + n * (2 * pi)) + 2 * pi"
unfolding Suc_eq_plus1 distrib_right
by (auto simp add: field_simps)
show ?case unfolding split_pi_off using Suc by auto
qed auto
lemma cos_periodic_int [simp]:
fixes i :: int
shows "cos (x + i * (2 * pi)) = cos x"
proof(cases "0 ≤ i")
case True
thus ?thesis
using cos_periodic_nat[of x "nat i"]
by auto
next
case False hence i_nat: "i = - real (nat (-i))" by auto
have "cos x = cos (x + i * (2 * pi) - i * (2 * pi))" by auto
also have "… = cos (x + i * (2 * pi))"
unfolding i_nat mult_minus_left diff_minus_eq_add by (rule cos_periodic_nat)
finally show ?thesis by auto
qed
text ‹Values of both sine and cosine are repeated only after multiples of $2\cdot \pi$›
lemma sin_cos_eq:
fixes a b :: real
assumes "cos a = cos b" and "sin a = sin b"
shows "∃ k::int. a - b = 2*k*pi"
proof-
from assms have "sin (a - b) = 0" "cos (a - b) = 1"
using sin_diff[of a b] cos_diff[of a b]
by auto
thus ?thesis
using cos1_sin0
by auto
qed
text ‹The following two lemmas are consequences of surjectivity of cosine for the range $[-1, 1]$.›
lemma ex_cos_eq:
assumes "-pi/2 ≤ α ∧ α ≤ pi/2"
assumes "a ≥ 0" and "a < 1"
shows "∃ α'. -pi/2 ≤ α' ∧ α' ≤ pi/2 ∧ α' ≠ α ∧ cos (α - α') = a"
proof-
have "arccos a > 0" "arccos a ≤ pi/2"
using ‹a ≥ 0› ‹a < 1›
using arccos_lt_bounded arccos_le_pi2
by auto
show ?thesis
proof (cases "α - arccos a ≥ - pi/2")
case True
thus ?thesis
using assms ‹arccos a > 0› ‹arccos a ≤ pi/2›
by (rule_tac x = "α - arccos a" in exI) auto
next
case False
thus ?thesis
using assms ‹arccos a > 0› ‹arccos a ≤ pi/2›
by (rule_tac x = "α + arccos a" in exI) auto
qed
qed
lemma ex_cos_gt:
assumes "-pi/2 ≤ α ∧ α ≤ pi/2"
assumes "a < 1"
shows "∃ α'. -pi/2 ≤ α' ∧ α' ≤ pi/2 ∧ α' ≠ α ∧ cos (α - α') > a"
proof-
have "∃ a'. a' ≥ 0 ∧ a' > a ∧ a' < 1"
using ‹a < 1›
using divide_strict_right_mono[of "2*a + (1 - a)" 2 2]
by (rule_tac x="if a < 0 then 0 else a + (1-a)/2" in exI) (auto simp add: field_simps)
then obtain a' where "a' ≥ 0" "a' > a" "a' < 1"
by auto
thus ?thesis
using ex_cos_eq[of α a'] assms
by auto
qed
text ‹The function @{term atan2} is a generalization of @{term arctan} that takes a pair of coordinates
of non-zero points returns its angle in the range $[-\pi, \pi)$.›
definition atan2 where
"atan2 y x =
(if x > 0 then arctan (y/x)
else if x < 0 then
if y > 0 then arctan (y/x) + pi else arctan (y/x) - pi
else
if y > 0 then pi/2 else if y < 0 then -pi/2 else 0)"
lemma atan2_bounded:
shows "-pi ≤ atan2 y x ∧ atan2 y x < pi"
using arctan_bounded[of "y/x"] zero_le_arctan_iff[of "y/x"] arctan_le_zero_iff[of "y/x"] zero_less_arctan_iff[of "y/x"] arctan_less_zero_iff[of "y/x"]
using divide_neg_neg[of y x] divide_neg_pos[of y x] divide_pos_pos[of y x] divide_pos_neg[of y x]
unfolding atan2_def
by (simp (no_asm_simp)) auto
end