Quelle  Triangle.thy

(*
  File:    Triangle.thy
  Author:  Manuel Eberl <manuel@pruvisto.org>

  Sine and cosine laws, angle sum in a triangle, congruence theorems,
  Isosceles Triangle Theorem
*)

section ‹Basic Properties of Triangles›
theory Triangle
imports
  Angles
begin

text ‹
 We prove a number of basic geometric properties of triangles. All theorems hold
 in any real inner product space.
 ›
subsection ‹Thales' theorem›

theorem thales:
  fixes A B C :: "'a :: real_inner"
  assumes "dist B (midpoint A C) = dist A C / 2"
  shows   "orthogonal (A - B) (C - B)"
proof -
  have "dist A C ^ 2 = dist B (midpoint A C) ^ 2 * 4"
    by (subst assms) (simp add: field_simps power2_eq_square)
  thus ?thesis
    by (auto simp: orthogonal_def dist_norm power2_norm_eq_inner midpoint_def
                   algebra_simps inner_commute)
qed

subsection ‹Sine and cosine laws›

text ‹
 The proof of the Law of Cosines follows trivially from the definition of the angle,
 the definition of the norm in vector spaces with an inner product and the bilinearity
 of the inner product.
 ›

lemma cosine_law_vector:
  "norm (u - v) ^ 2 = norm u ^ 2 + norm v ^ 2 - 2 * norm u * norm v * cos (vangle u v)"
  by (simp add: power2_norm_eq_inner cos_vangle algebra_simps inner_commute)

lemma cosine_law_triangle:
  "dist b c ^ 2 = dist a b ^ 2 + dist a c ^ 2 - 2 * dist a b * dist a c * cos (angle b a c)"
  using cosine_law_vector[of "b - a" "c - a"]
  by (simp add: dist_norm angle_def vangle_commute norm_minus_commute)


text ‹
 According to our definition, angles are always between $0$ and $\pi$ and therefore,
 the sign of an angle is always non-negative. We can therefore look at
 $\sin(\alpha)^2$, which we can express in terms of $\cos(\alpha)$ using the
 identity $\sin(\alpha)^2 + \cos(\alpha)^2 = 1$. The remaining proof is then a
 trivial consequence of the definitions.
 ›
lemma sine_law_triangle:
  "sin (angle a b c) * dist b c = sin (angle b a c) * dist a c" (is "?A = ?B")
proof (cases "a = b")
  assume neq: "a ≠ b"
  show ?thesis
  proof (rule power2_eq_imp_eq)
    from neq have "(sin (angle a b c) * dist b c) ^ 2 * dist a b ^ 2 =
                     dist a b ^ 2 * dist b c ^ 2 - ((a - b) ∙ (c - b)) ^ 2"
      by (simp add: sin_squared_eq cos_angle dist_commute field_simps)
    also have "… = dist a b ^ 2 * dist a c ^ 2 - ((b - a) ∙ (c - a)) ^ 2"
      by (simp only: dist_norm power2_norm_eq_inner)
         (simp add: power2_eq_square algebra_simps inner_commute)
    also from neq have "… = (sin (angle b a c) * dist a c) ^ 2 * dist a b ^ 2"
      by (simp add: sin_squared_eq cos_angle dist_commute field_simps)
    finally show "?A^2 = ?B^2" using neq by (subst (asm) mult_cancel_right) simp_all
  qed (auto intro!: mult_nonneg_nonneg sin_angle_nonneg)
qed simp_all


text ‹
 The following forms of the Law of Sines/Cosines are more convenient for eliminating
 sines/cosines from a goal completely.
 ›

lemma cosine_law_triangle':
  "2 * dist a b * dist a c * cos (angle b a c) = (dist a b ^ 2 + dist a c ^ 2 - dist b c ^ 2)"
  using cosine_law_triangle[of b c a] by simp

lemma cosine_law_triangle'':
  "cos (angle b a c) = (dist a b ^ 2 + dist a c ^ 2 - dist b c ^ 2) / (2 * dist a b * dist a c)"
  using cosine_law_triangle[of b c a] by simp

lemma sine_law_triangle':
  "b ≠ c ==> sin (angle a b c) = sin (angle b a c) * dist a c / dist b c"
  using sine_law_triangle[of a b c] by (simp add: divide_simps)

lemma sine_law_triangle'':
  "b ≠ c ==> sin (angle c b a) = sin (angle b a c) * dist a c / dist b c"
  using sine_law_triangle[of a b c] by (simp add: divide_simps angle_commute)


subsection ‹Sum of angles›

context
begin

private lemma gather_squares: "a * (a * b) = a^2 * (b :: real)"
  by (simp_all add: power2_eq_square)

private lemma eval_power: "x ^ numeral n = x * x ^ pred_numeral n"
  by (subst numeral_eq_Suc, subst power_Suc) simp

text ‹
 The proof that the sum of the angles in a triangle is $\pi$ is somewhat more
 involved. Following the HOL Light proof by John Harrison, we first prove
 that $\cos(\alpha + \beta + \gamma) = -1$ and $\alpha + \beta + \gamma \in [0;3\pi)$,
 which then implies the theorem.

 The main work is proving $\cos(\alpha + \beta + \gamma)$. This is done using the
 addition theorems for the sine and cosine, then using the Laws of Sines to eliminate
 all $\sin$ terms save $\sin(\gamma)^2$, which only appears squared in the remaining goal.
 We then use $\sin(\gamma)^2 = 1 - \cos(\gamma)^2$ to eliminate this term and apply
 the law of cosines to eliminate this term as well.

 The remaining goal is a non-linear equation containing only the length of the sides
 of the triangle. It can be shown by simple algebraic rewriting.
 ›
lemma angle_sum_triangle:
  assumes "a ≠ b ∨ b ≠ c ∨ a ≠ c"
  shows   "angle c a b + angle a b c + angle b c a = pi"
proof (rule cos_minus1_imp_pi)
  show "cos (angle c a b + angle a b c + angle b c a) = - 1"
  proof (cases "a ≠ b")
    case True
    thus "cos (angle c a b + angle a b c + angle b c a) = -1"
      apply (simp add: cos_add sin_add cosine_law_triangle'' field_simps
                       sine_law_triangle''[of a b c] sine_law_triangle''[of b a c]
                       angle_commute dist_commute gather_squares sin_squared_eq)
      apply (simp add: eval_power algebra_simps dist_commute)
      done
  qed (insert assms, auto)

  show "angle c a b + angle a b c + angle b c a < 3 * pi"
  proof (rule ccontr)
    assume "¬(angle c a b + angle a b c + angle b c a < 3 * pi)"
    with angle_le_pi[of c a b] angle_le_pi[of a b c] angle_le_pi[of b c a]
      have A: "angle c a b = pi" "angle a b c = pi" by simp_all
    thus False using angle_eq_pi_imp_dist_additive[of c a b]
                     angle_eq_pi_imp_dist_additive[of a b c] by (simp add: dist_commute)
  qed
qed (auto intro!: add_nonneg_nonneg angle_nonneg)

end


subsection ‹Congruence Theorems›

text ‹
 If two triangles agree on two angles at a non-degenerate side, the third angle
 must also be equal.
 ›
lemma similar_triangle_aa:
  assumes "b1 ≠ c1" "b2 ≠ c2"
  assumes "angle a1 b1 c1 = angle a2 b2 c2"
  assumes "angle b1 c1 a1 = angle b2 c2 a2"
  shows   "angle b1 a1 c1 = angle b2 a2 c2"
proof -
  from assms angle_sum_triangle[of a1 b1 c1] angle_sum_triangle[of a2 b2 c2, symmetric]
    show ?thesis by (auto simp: algebra_simps angle_commute)
qed

text ‹
 A triangle is defined by its three angles and the lengths of three sides up to congruence.
 Two triangles are congruent if they have their angles are the same and their sides have
 the same length.
 ›

locale congruent_triangle =
  fixes a1 b1 c1 :: "'a :: real_inner" and a2 b2 c2 :: "'b :: real_inner"
  assumes sides':  "dist a1 b1 = dist a2 b2" "dist a1 c1 = dist a2 c2" "dist b1 c1 = dist b2 c2"
      and angles': "angle b1 a1 c1 = angle b2 a2 c2" "angle a1 b1 c1 = angle a2 b2 c2"
                   "angle a1 c1 b1 = angle a2 c2 b2"
begin

lemma sides:
  "dist a1 b1 = dist a2 b2" "dist a1 c1 = dist a2 c2" "dist b1 c1 = dist b2 c2"
  "dist b1 a1 = dist a2 b2" "dist c1 a1 = dist a2 c2" "dist c1 b1 = dist b2 c2"
  "dist a1 b1 = dist b2 a2" "dist a1 c1 = dist c2 a2" "dist b1 c1 = dist c2 b2"
  "dist b1 a1 = dist b2 a2" "dist c1 a1 = dist c2 a2" "dist c1 b1 = dist c2 b2"
  using sides' by (simp_all add: dist_commute)

lemma angles:
  "angle b1 a1 c1 = angle b2 a2 c2" "angle a1 b1 c1 = angle a2 b2 c2" "angle a1 c1 b1 = angle a2 c2 b2"
  "angle c1 a1 b1 = angle b2 a2 c2" "angle c1 b1 a1 = angle a2 b2 c2" "angle b1 c1 a1 = angle a2 c2 b2"
  "angle b1 a1 c1 = angle c2 a2 b2" "angle a1 b1 c1 = angle c2 b2 a2" "angle a1 c1 b1 = angle b2 c2 a2"
  "angle c1 a1 b1 = angle c2 a2 b2" "angle c1 b1 a1 = angle c2 b2 a2" "angle b1 c1 a1 = angle b2 c2 a2"
  using angles' by (simp_all add: angle_commute)

end

lemmas congruent_triangleD = congruent_triangle.sides congruent_triangle.angles



text ‹
 Given two triangles that agree on a subset of its side lengths and angles that are
 sufficient to define a triangle uniquely up to congruence, one can conclude that they
 must also agree on all remaining quantities, i.e. that they are congruent.

 The following four congruence theorems state what constitutes such a uniquely-defining
 subset of quantities. Each theorem states in its name which quantities are required and
 in which order (clockwise or counter-clockwise): an ``s'' stands for a side,
 an ``a'' stands for an angle.

 The lemma ``congruent-triangleI-sas, for example, requires that two adjacent sides and the
 angle inbetween are the same in both triangles.
 ›

lemma congruent_triangleI_sss:
  fixes a1 b1 c1 :: "'a :: real_inner" and a2 b2 c2 :: "'b :: real_inner"
  assumes "dist a1 b1 = dist a2 b2"
  assumes "dist b1 c1 = dist b2 c2"
  assumes "dist a1 c1 = dist a2 c2"
  shows   "congruent_triangle a1 b1 c1 a2 b2 c2"
proof -
  have A: "angle a1 b1 c1 = angle a2 b2 c2"
    if "dist a1 b1 = dist a2 b2" "dist b1 c1 = dist b2 c2" "dist a1 c1 = dist a2 c2"
    for a1 b1 c1 :: 'a and a2 b2 c2 :: 'b
  proof -
    from that cosine_law_triangle''[of a1 b1 c1] cosine_law_triangle''[of a2 b2 c2]
      show ?thesis by (intro cos_angle_eqD) (simp add: dist_commute)
  qed
  from assms show ?thesis by unfold_locales (auto intro!: A simp: dist_commute)
qed

lemmas congruent_triangle_sss = congruent_triangleD[OF congruent_triangleI_sss]

lemma congruent_triangleI_sas:
  assumes "dist a1 b1 = dist a2 b2"
  assumes "dist b1 c1 = dist b2 c2"
  assumes "angle a1 b1 c1 = angle a2 b2 c2"
  shows   "congruent_triangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_triangleI_sss)
  show "dist a1 c1 = dist a2 c2"
  proof (rule power2_eq_imp_eq)
    from cosine_law_triangle[of a1 c1 b1] cosine_law_triangle[of a2 c2 b2] assms
      show "(dist a1 c1)² = (dist a2 c2)²" by (simp add: dist_commute)
  qed simp_all
qed fact+

lemmas congruent_triangle_sas = congruent_triangleD[OF congruent_triangleI_sas]

lemma congruent_triangleI_aas:
  assumes "angle a1 b1 c1 = angle a2 b2 c2"
  assumes "angle b1 c1 a1 = angle b2 c2 a2"
  assumes "dist a1 b1 = dist a2 b2"
  assumes "¬collinear {a1,b1,c1}"
  shows   "congruent_triangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_triangleI_sas)
  from ‹¬collinear {a1,b1,c1}› have neq: "a1 ≠ b1" by auto
  with assms(3) have neq': "a2 ≠ b2" by auto
  have A: "angle c1 a1 b1 = angle c2 a2 b2" using neq neq' assms
    using angle_sum_triangle[of a1 b1 c1] angle_sum_triangle[of a2 b2 c2]
    by simp
  from assms have B: "angle b1 a1 c1 ∈ {0<..<pi}"
    by (intro not_collinear_angle) (simp_all add: insert_commute)
  from sine_law_triangle[of c1 a1 b1] sine_law_triangle[of c2 a2 b2] assms A B
    show "dist b1 c1 = dist b2 c2"
    by (auto simp: angle_commute dist_commute sin_angle_zero_iff)
qed fact+

lemmas congruent_triangle_aas = congruent_triangleD[OF congruent_triangleI_aas]

lemma congruent_triangleI_asa:
  assumes "angle a1 b1 c1 = angle a2 b2 c2"
  assumes "dist a1 b1 = dist a2 b2"
  assumes "angle b1 a1 c1 = angle b2 a2 c2"
  assumes "¬collinear {a1, b1, c1}"
  shows   "congruent_triangle a1 b1 c1 a2 b2 c2"
proof (rule congruent_triangleI_aas)
  from assms have neq: "a1 ≠ b1" "a2 ≠ b2" by auto
  show "angle b1 c1 a1 = angle b2 c2 a2"
    by (rule similar_triangle_aa) (insert assms neq, simp_all add: angle_commute)
qed fact+

lemmas congruent_triangle_asa = congruent_triangleD[OF congruent_triangleI_asa]


subsection ‹Isosceles Triangle Theorem›

text ‹
 We now prove the Isosceles Triangle Theorem: in a triangle where two sides have
 the same length, the two angles that are adjacent to only one of the two sides
 must be equal.
 ›
lemma isosceles_triangle:
  assumes "dist a c = dist b c"
  shows   "angle b a c = angle a b c"
  by (rule congruent_triangle_sss) (insert assms, simp_all add: dist_commute)


text ‹
 For the non-degenerate case (i.e. the three points are not collinear), We also
 prove the converse.
 ›
lemma isosceles_triangle_converse:
  assumes "angle a b c = angle b a c" "¬collinear {a,b,c}"
  shows   "dist a c = dist b c"
  by (rule congruent_triangle_asa[OF assms(1) _ _ assms(2)])
     (simp_all add: dist_commute angle_commute assms)


subsection‹Contributions by Lukas Bulwahn›
  
lemma Pythagoras:
  fixes A B C :: "'a :: real_inner"
  assumes "orthogonal (A - C) (B - C)"
  shows "(dist B C) ^ 2 + (dist C A) ^ 2 = (dist A B) ^ 2"
proof -
  from assms have "cos (angle A C B) = 0"
    by (metis orthogonal_iff_angle cos_pi_half)
  from this show ?thesis
    by (simp add: cosine_law_triangle[of A B C] dist_commute)
qed

lemma isosceles_triangle_orthogonal_on_midpoint:
  fixes A B C :: "'a :: euclidean_space"
  assumes "dist C A = dist C B"
  shows "orthogonal (C - midpoint A B) (A - midpoint A B)"
proof (cases "A = B")
  assume "A ≠ B"
  let ?M = "midpoint A B"
  from ‹A ≠ B› have "angle A ?M C = pi - angle B ?M C"
    by (intro angle_inverse between_midpoint)
       (auto simp: between_midpoint eq_commute[of _ "midpoint A B" for A B])
  moreover have "angle A ?M C = angle C ?M B"
  proof -
    have congruence: "congruent_triangle C A ?M C B ?M"
    proof (rule congruent_triangleI_sss)
      show "dist C A = dist C B" using assms .
      show "dist A ?M = dist B ?M" by (simp add: dist_midpoint)
      show "dist C (midpoint A B) = dist C (midpoint A B)" ..
    qed
    from this show ?thesis by (simp add: congruent_triangle.angles(6))
  qed
  ultimately have "angle A ?M C = pi / 2" by (simp add: angle_commute)
  from this show ?thesis
    by (simp add: orthogonal_iff_angle orthogonal_commute)
next
  assume "A = B"
  from this show ?thesis
    by (simp add: orthogonal_clauses(1))
qed

end