Grace/Cumulus/Geometry/Heron.g17

Open in Workbench Download source

Imports

Distance · Lines · Real.AbsoluteValue

Declarations

Source

1-- Heron's formula: the area of a triangle from its three side lengths.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Geometry.Heron8import Distance9import Lines10import Real.AbsoluteValue1112namespace Euclidean13export open Euclidean1415-- Twice the area of the triangle abc is the absolute value of the cross16-- product of its two sides at a.17def doubleArea (a b c : Point) : Real := abs(directionCross(a, b, a, c))1819def area (a b c : Point) : Real := doubleArea(a, b, c) / 22021theorem doubleArea.real (a b c : Point)22  shows Real(doubleArea(a, b, c))23proof24  typecheck2526theorem area.real (a b c : Point)27  shows Real(area(a, b, c))28proof29  typecheck3031theorem doubleArea.nonnegative (a b c : Point)32  shows 0 ≤ doubleArea(a, b, c)33proof34  have cross := directionCross.real at a, b, a, c with *35  unfold doubleArea36  exact abs.nonnegative with cross3738theorem doubleArea.square (a b c : Point)39  shows doubleArea(a, b, c) * doubleArea(a, b, c) =40    directionCross(a, b, a, c) * directionCross(a, b, a, c)41proof42  have cross := directionCross.real at a, b, a, c with *43  have product := abs.mul at directionCross(a, b, a, c),44    directionCross(a, b, a, c) with *45  have nonnegative := realMulValue.square_nonnegative at46    directionCross(a, b, a, c) with *47  have same := abs.of_nonnegative with nonnegative48  unfold doubleArea49  rw ← product50  exact same5152theorem area.twice (a b c : Point)53  shows (2:R) * area(a, b, c) = doubleArea(a, b, c)54proof55  have nonzero := realAddValue.two_nonzero56  unfold area57  exact realDiv.mul_left with *5859theorem area.nonnegative (a b c : Point)60  shows 0 ≤ area(a, b, c)61proof62  have real := area.real at a, b, c with *63  have twice := area.twice at a, b, c with *64  have nonnegative := doubleArea.nonnegative at a, b, c with *65  linarith6667-- Heron's formula in squared form: sixteen times the squared area is a68-- polynomial in the squared side lengths.69theorem heron.squared (a b c : Point)70  shows (16:R) * (area(a, b, c) * area(a, b, c)) =71    2 * distanceSquared(a, b) * distanceSquared(b, c) +72    2 * distanceSquared(b, c) * distanceSquared(c, a) +73    2 * distanceSquared(c, a) * distanceSquared(a, b) -74    distanceSquared(a, b) * distanceSquared(a, b) -75    distanceSquared(b, c) * distanceSquared(b, c) -76    distanceSquared(c, a) * distanceSquared(c, a)77proof78  have twice := area.twice at a, b, c with *79  have square := doubleArea.square at a, b, c with *80  have ab := distanceSquared.coordinates at a, b with *81  have bc := distanceSquared.coordinates at b, c with *82  have ca := distanceSquared.coordinates at c, a with *83  have sixteen : (16:R) * (area(a, b, c) * area(a, b, c)) =84      4 * (((2:R) * area(a, b, c)) * ((2:R) * area(a, b, c)))85    ring86  rw [sixteen, twice, square, ab, bc, ca]87  unfold directionCross88  ring8990def semiperimeter (a b c : Point) : Real :=91  (distance(b, c) + distance(c, a) + distance(a, b)) / 29293theorem semiperimeter.twice (a b c : Point)94  shows (2:R) * semiperimeter(a, b, c) =95    distance(b, c) + distance(c, a) + distance(a, b)96proof97  have nonzero := realAddValue.two_nonzero98  unfold semiperimeter99  exact realDiv.mul_left with *100101-- Heron's formula: with s the semiperimeter and p, q, r the side lengths,102-- the area is √(s(s − p)(s − q)(s − r)).103theorem heron (a b c : Point)104  shows area(a, b, c) =105    √(semiperimeter(a, b, c) *106      (semiperimeter(a, b, c) - distance(b, c)) *107      (semiperimeter(a, b, c) - distance(c, a)) *108      (semiperimeter(a, b, c) - distance(a, b)))109proof110  have twiceS := semiperimeter.twice at a, b, c with *111  have pSquare := distance.square at b, c with *112  have qSquare := distance.square at c, a with *113  have rSquare := distance.square at a, b with *114  have squared := heron.squared at a, b, c with *115  have expand : (16:R) * (semiperimeter(a, b, c) *116      (semiperimeter(a, b, c) - distance(b, c)) *117      (semiperimeter(a, b, c) - distance(c, a)) *118      (semiperimeter(a, b, c) - distance(a, b))) =119    ((2:R) * semiperimeter(a, b, c)) *120      ((2:R) * semiperimeter(a, b, c) - 2 * distance(b, c)) *121      ((2:R) * semiperimeter(a, b, c) - 2 * distance(c, a)) *122      ((2:R) * semiperimeter(a, b, c) - 2 * distance(a, b))123    ring124  have key : (16:R) * (area(a, b, c) * area(a, b, c)) =125      (16:R) * (semiperimeter(a, b, c) *126        (semiperimeter(a, b, c) - distance(b, c)) *127        (semiperimeter(a, b, c) - distance(c, a)) *128        (semiperimeter(a, b, c) - distance(a, b)))129    rw [expand, twiceS, squared, ← pSquare, ← qSquare, ← rSquare]130    ring131  have product : area(a, b, c) * area(a, b, c) =132      semiperimeter(a, b, c) *133        (semiperimeter(a, b, c) - distance(b, c)) *134        (semiperimeter(a, b, c) - distance(c, a)) *135        (semiperimeter(a, b, c) - distance(a, b))136    linarith137  have nonnegative := area.nonnegative at a, b, c with *138  have squareNonnegative := realMulValue.square_nonnegative at139    area(a, b, c) with *140  rw product at squareNonnegative141  have typed := NonnegativeReal.of_le with squareNonnegative142  exact sqrt.unique with nonnegative, product143144end Euclidean145