feat(archive/100-theorems-list): add proof of Heron's formula (#6989)

This proves Heron's Formula for triangles, which happens to be Theorem 57 on Freek's 100 Theorems.

archive/100-theorems-list/57_herons_formula.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2021 Matt Kempster. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Kempster
+-/
+import geometry.euclidean.triangle
+import analysis.special_functions.trigonometric
+
+/-!
+# Freek № 57: Heron's Formula
+
+This file proves Theorem 57 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/),
+also known as Heron's formula, which gives the area of a triangle based only on its three sides'
+lengths.
+
+## References
+
+* https://en.wikipedia.org/wiki/Herons_formula
+
+-/
+
+open real euclidean_geometry
+open_locale real euclidean_geometry
+
+local notation `√` := real.sqrt
+
+variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
+  [normed_add_torsor V P]
+
+include V
+
+/-- Heron's formula: The area of a triangle with side lengths `a`, `b`, and `c` is
+  `√(s * (s - a) * (s - b) * (s - c))` where `s = (a + b + c) / 2` is the semiperimeter.
+  We show this by equating this formula to `a * b * sin γ`, where `γ` is the angle opposite
+  the side `c`.
+ -/
+theorem heron {p1 p2 p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) :
+  let a := dist p1 p2, b := dist p3 p2, c := dist p1 p3, s := (a + b + c) / 2 in
+  1/2 * a * b * sin (∠ p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c)) :=
+begin
+  intros a b c s,
+  let γ := ∠ p1 p2 p3,
+  obtain := ⟨(dist_pos.mpr h1).ne', (dist_pos.mpr h2).ne'⟩,
+  have cos_rule : cos γ = (a * a + b * b - c * c) / (2 * a * b) := by field_simp [mul_comm, a,
+    dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle p1 p2 p3],
+  let numerator := (2*a*b)^2 - (a*a + b*b - c*c)^2,
+  let denominator := (2*a*b)^2,
+  have split_to_frac : 1 - cos γ ^ 2 = numerator / denominator := by field_simp [cos_rule],
+  have numerator_nonneg : 0 ≤ numerator,
+  { have frac_nonneg: 0 ≤ numerator / denominator := by linarith [split_to_frac, cos_sq_le_one γ],
+    cases div_nonneg_iff.mp frac_nonneg,
+    { exact h.left },
+    { simpa [h1, h2] using le_antisymm h.right (pow_two_nonneg _) } },
+  have ab2_nonneg : 0 ≤ (2 * a * b) := by norm_num [mul_nonneg, dist_nonneg],
+  calc  1/2 * a * b * sin γ
+      = 1/2 * a * b * (√numerator / √denominator) : by rw [sin_eq_sqrt_one_sub_cos_sq,
+                                                          split_to_frac, sqrt_div numerator_nonneg];
+                                                      simp [angle_nonneg, angle_le_pi]
+  ... = 1/4 * √((2*a*b)^2 - (a*a + b*b - c*c)^2)  : by { field_simp [ab2_nonneg], ring }
+  ... = 1/4 * √(s * (s-a) * (s-b) * (s-c) * 4^2)  : by { simp only [s], ring_nf }
+  ... = √(s * (s-a) * (s-b) * (s-c))              : by rw [sqrt_mul', sqrt_sqr, div_mul_eq_mul_div,
+                                                          one_mul, mul_div_cancel];
+                                                      norm_num,
+end

docs/100.yaml

@@ -184,6 +184,9 @@
   title  : The Hermite-Lindemann Transcendence Theorem
 57:
   title  : Heron’s Formula
+  links :
+    mathlib archive : https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/57_herons_formula.lean
+  author : Matt Kempster
 58:
   title  : Formula for the Number of Combinations
   decls  :

src/analysis/special_functions/trigonometric.lean

@@ -1141,13 +1141,26 @@ sin_add_pi_div_two x ▸ sin_pos_of_mem_Ioo ⟨by linarith [hx.1], by linarith [
 lemma cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Icc (-(π / 2)) (π / 2)) : 0 ≤ cos x :=
 sin_add_pi_div_two x ▸ sin_nonneg_of_mem_Icc ⟨by linarith [hx.1], by linarith [hx.2]⟩
 
+lemma cos_nonneg_of_neg_pi_div_two_le_of_le {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ π / 2) :
+  0 ≤ cos x :=
+cos_nonneg_of_mem_Icc ⟨hl, hu⟩
+
 lemma cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) : cos x < 0 :=
 neg_pos.1 $ cos_pi_sub x ▸ cos_pos_of_mem_Ioo ⟨by linarith, by linarith⟩
 
 lemma cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} (hx₁ : π / 2 ≤ x) (hx₂ : x ≤ π + π / 2) :
   cos x ≤ 0 :=
 neg_nonneg.1 $ cos_pi_sub x ▸ cos_nonneg_of_mem_Icc ⟨by linarith, by linarith⟩
 
+lemma sin_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ π) :
+  sin x = sqrt (1 - cos x ^ 2) :=
+by rw [← abs_sin_eq_sqrt_one_sub_cos_sq, abs_of_nonneg (sin_nonneg_of_nonneg_of_le_pi hl hu)]
+
+lemma cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ π / 2) :
+  cos x = sqrt (1 - sin x ^ 2) :=
+by rw [← abs_cos_eq_sqrt_one_sub_sin_sq,
+  abs_of_nonneg (cos_nonneg_of_neg_pi_div_two_le_of_le hl hu)]
+
 lemma sin_nat_mul_pi (n : ℕ) : sin (n * π) = 0 :=
 by induction n; simp [add_mul, sin_add, *]
 

src/data/complex/exponential.lean

@@ -1035,6 +1035,14 @@ by rw [←sin_sq_add_cos_sq x, add_sub_cancel']
 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
 eq_sub_iff_add_eq.2 $ sin_sq_add_cos_sq _
 
+lemma abs_sin_eq_sqrt_one_sub_cos_sq (x : ℝ) :
+  abs' (sin x) = sqrt (1 - cos x ^ 2) :=
+by rw [← sin_square, sqrt_sqr_eq_abs]
+
+lemma abs_cos_eq_sqrt_one_sub_sin_sq (x : ℝ) :
+  abs' (cos x) = sqrt (1 - sin x ^ 2) :=
+by rw [← cos_square', sqrt_sqr_eq_abs]
+
 lemma inv_one_add_tan_sq {x : ℝ} (hx : cos x ≠ 0) : (1 + tan x ^ 2)⁻¹ = cos x ^ 2  :=
 have complex.cos x ≠ 0, from mt (congr_arg re) hx,
 of_real_inj.1 $ by simpa using complex.inv_one_add_tan_sq this