Grace/Cumulus/Geometry/Angle.g17

Open in Workbench Download source

Imports

Distance · Isosceles

Declarations

Source

1-- Cosines of angles, the law of cosines, and the isosceles triangle theorem.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.Angle8import Distance9import Isosceles1011namespace Euclidean12export open Euclidean1314-- Section: The cosine of an angle1516-- The cosine of the angle at b between the rays to a and c. An unoriented17-- angle in [0, π] is determined by its cosine, so equal cosines are equal18-- angles; no inverse trigonometric function is needed to compare them.19def cosAngle (a b c : Point) : Real := angleDot(a, b, c) / (distance(b, a) * distance(b, c))2021theorem cosAngle.real (a b c : Point)22  shows Real(cosAngle(a, b, c))23proof24  typecheck2526theorem rayProduct.positive (a b c : Point)27  requires firstRay : a ≠ b28  requires secondRay : c ≠ b29  shows 0 < distance(b, a) * distance(b, c)30proof31  have firstDistinct : b ≠ a32    intro equal33    apply firstRay34    cc35  have secondDistinct : b ≠ c36    intro equal37    apply secondRay38    cc39  have first := distance.positive_of_ne at b, a with *40  have second := distance.positive_of_ne at b, c with *41  exact realMulValue.positive with *4243theorem cosAngle.mul_rays (a b c : Point)44  requires firstRay : a ≠ b45  requires secondRay : c ≠ b46  shows cosAngle(a, b, c) * (distance(b, a) * distance(b, c)) = angleDot(a, b, c)47proof48  have positive := rayProduct.positive at a, b, c with *49  have nonzero : distance(b, a) * distance(b, c) ≠ 050    intro zero51    rw zero at positive52    exact realLess.not_self with realZero.real, positive53  have cancel := realDiv.mul_right at angleDot(a, b, c), distance(b, a) * distance(b, c) with *54  unfold cosAngle55  cc5657-- Section: The law of cosines5859theorem law_of_cosines (a b c : Point)60  requires firstRay : a ≠ b61  requires secondRay : c ≠ b62  shows Euclidean.distanceSquared(a, c) =63    Euclidean.distanceSquared(a, b) + Euclidean.distanceSquared(b, c) - 2 * (distance(a, b) * distance(b, c) * cosAngle(a, b, c))64proof65  have product := cosAngle.mul_rays at a, b, c with *66  have symmetric := distance.symmetric at b, a with *67  rw symmetric at product68  have identity := cosine_identity at a, b, c with *69  linear_combination identity + product + product7071-- Section: Cosines lie in [-1, 1]7273theorem cosAngle.le_one (a b c : Point)74  requires firstRay : a ≠ b75  requires secondRay : c ≠ b76  shows cosAngle(a, b, c) ≤ 177proof78  have positive := rayProduct.positive at a, b, c with *79  have product := cosAngle.mul_rays at a, b, c with *80  have dotReal := angleDot.real at a, b, c with *81  have productReal : Real(distance(b, a) * distance(b, c)) by typecheck82  have upper : angleDot(a, b, c) ≤ distance(b, a) * distance(b, c)83    have productNonnegative := realLess.implies_le with *84    have firstSquare := distance.square at b, a with *85    have secondSquare := distance.square at b, c with *86    have productSquare : (distance(b, a) * distance(b, c)) * (distance(b, a) * distance(b, c)) = Euclidean.distanceSquared(b, a) * Euclidean.distanceSquared(b, c)87      rw [← firstSquare, ← secondSquare]88      ring89    have schwarz := angleDot.cauchy_schwarz at a, b, c with *90    rw ← productSquare at schwarz91    have sign := Real.sign_cases with dotReal92    cases sign with nonpositive | nonnegative93    . have dotLe := realLe.of_subset at angleDot(a, b, c), realZero with realZero.real, nonpositive94      exact realLe.transitive with *95    . have dotLe := realLe.of_subset with realZero.real, nonnegative96      exact realMulValue.le_of_square_le with *97  have scaled : cosAngle(a, b, c) * (distance(b, a) * distance(b, c)) ≤ 1 * (distance(b, a) * distance(b, c))98    rw product99    have one := realMulValue.one_left with productReal100    rwa one101  exact realLe.mul_right_cancel_positive with *102103theorem cosAngle.neg_one_le (a b c : Point)104  requires firstRay : a ≠ b105  requires secondRay : c ≠ b106  shows -(1:R) ≤ cosAngle(a, b, c)107proof108  have positive := rayProduct.positive at a, b, c with *109  have product := cosAngle.mul_rays at a, b, c with *110  have bound := angleDot.lower_bound at a, b, c with *111  have lower : -(distance(b, a) * distance(b, c)) ≤ angleDot(a, b, c)112    have rewrite : angleDot(a, b, c) - (-(distance(b, a) * distance(b, c))) = angleDot(a, b, c) + distance(b, a) * distance(b, c)113      ring114    have nonnegativeDifference : 0 ≤ angleDot(a, b, c) - (-(distance(b, a) * distance(b, c))) by rwa rewrite115    exact realLe.of_nonnegative_difference with *116  have scaled : (-(1:R)) * (distance(b, a) * distance(b, c)) ≤ cosAngle(a, b, c) * (distance(b, a) * distance(b, c))117    rw product118    have negOne : (-(1:R)) * (distance(b, a) * distance(b, c)) = -(distance(b, a) * distance(b, c)) by ring119    rwa negOne120  exact realLe.mul_right_cancel_positive with *121122-- Section: The isosceles triangle theorem123124-- Equal legs give equal base angles, stated as equality of their cosines.125theorem isosceles.cosines (a b c : Point)126  requires base : a ≠ b127  requires leg : a ≠ c128  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)129  shows cosAngle(c, a, b) = cosAngle(c, b, a)130proof131  have ca := Euclidean.distanceSquared.symmetric at c, a with *132  have cb := Euclidean.distanceSquared.symmetric at c, b with *133  have shared := Euclidean.distanceSquared.symmetric at a, b with *134  have first : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b) by cc135  have opposite : Euclidean.distanceSquared(c, b) = Euclidean.distanceSquared(c, a) by cc136  have equalDots := angleDot.of_sss at c, a, b, c, b, a with *137  have legA : distance(a, c) = distance(b, c)138    unfold distance139    cc140  have baseSymmetric := distance.symmetric at a, b with *141  unfold cosAngle142  cc143144end Euclidean145