EuclideanDistance
Euclidean distance, the triangle inequality, and the law of cosines
1-- Euclidean distance, the triangle inequality, and the law of cosines.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 EuclideanDistance8import Grace.Cumulus.Geometry.Angle910-- Distances are square roots of squared distances; the square root is a11-- real function, defined from the least-upper-bound property.12theorem distance_squared (a b : Point)13 shows distance(a, b) * distance(a, b) = distanceSquared(a, b)14proof15 exact distance.square at a, b with *1617-- The triangle inequality for Euclidean distance in the plane.18theorem triangle (a b c : Point)19 shows distance(a, c) ≤ distance(a, b) + distance(b, c)20proof21 exact distance.triangle at a, b, c with *2223-- The law of cosines, with the cosine of the angle at b.24theorem cosines (a b c : Point)25 requires firstRay : a ≠ b26 requires secondRay : c ≠ b27 shows distanceSquared(a, c) =28 distanceSquared(a, b) + distanceSquared(b, c) - 2 * (distance(a, b) * distance(b, c) * cosAngle(a, b, c))29proof30 exact law_of_cosines at a, b, c with *3132-- A right angle has cosine zero, so the law of cosines becomes Pythagoras.33theorem right_angle_cosine (a b c : Point)34 requires firstRay : a ≠ b35 requires secondRay : c ≠ b36 requires right : RightAngle(a, b, c)37 shows cosAngle(a, b, c) = 038proof39 have positive := rayProduct.positive at a, b, c with *40 have product := cosAngle.mul_rays at a, b, c with *41 unfold RightAngle at right42 rw right at product43 have nonzero : distance(b, a) * distance(b, c) ≠ 044 intro zero45 rw zero at positive46 exact realLess.not_self with realZero.real, positive47 have cosReal := cosAngle.real at a, b, c with *48 have productReal : Real(distance(b, a) * distance(b, c)) by typecheck49 have zeroProduct : 0 * (distance(b, a) * distance(b, c)) = 0 by exact realMulValue.zero_left with productReal50 have equation : cosAngle(a, b, c) * (distance(b, a) * distance(b, c)) = 0 * (distance(b, a) * distance(b, c))51 rw zeroProduct52 exact product53 have le := realLe.reflexive at cosAngle(a, b, c) * (distance(b, a) * distance(b, c)) with *54 have forward : cosAngle(a, b, c) * (distance(b, a) * distance(b, c)) ≤ 0 * (distance(b, a) * distance(b, c))55 rw ← equation56 exact le57 have backward : 0 * (distance(b, a) * distance(b, c)) ≤ cosAngle(a, b, c) * (distance(b, a) * distance(b, c))58 rw ← equation59 exact le60 have upper := realLe.mul_right_cancel_positive at cosAngle(a, b, c), realZero, distance(b, a) * distance(b, c) with *61 have lower := realLe.mul_right_cancel_positive at realZero, cosAngle(a, b, c), distance(b, a) * distance(b, c) with *62 exact realLe.antisymmetric at cosAngle(a, b, c), realZero with *63