Grace/Cumulus/Geometry/Isosceles.g17

Open in Workbench Download source

Imports

Plane · Real.Metric

Declarations

Source

1-- Equal sides give equal base angles.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 Passmore67-- Adapted from Grant Passmore's Imandra Top 100 isosceles theorem:8-- https://github.com/imandra-ai/imandra-100-theorems/blob/main/src/isosceles.iml910module Grace.Cumulus.Geometry.Isosceles11import Plane12import Real.Metric1314namespace Euclidean15export open Euclidean1617-- Equality of unoriented angles, encoded without arccos or roots.18-- Positivity excludes zero rays. The final sign condition distinguishes19-- equal angles from supplementary angles with the same squared cosine.20predicate EqualAngle (a b c d e f : Set) :=21  0 < Euclidean.distanceSquared(a, b) ∧22  0 < Euclidean.distanceSquared(b, c) ∧23  0 < Euclidean.distanceSquared(d, e) ∧24  0 < Euclidean.distanceSquared(e, f) ∧25  (angleDot(a, b, c) * angleDot(a, b, c)) *26    (Euclidean.distanceSquared(d, e) * Euclidean.distanceSquared(e, f)) =27  (angleDot(d, e, f) * angleDot(d, e, f)) *28    (Euclidean.distanceSquared(a, b) * Euclidean.distanceSquared(b, c)) ∧29  0 ≤ angleDot(a, b, c) * angleDot(d, e, f)3031-- The coordinate calculation is confined to cosine_identity. Everything32-- from here on reasons about sides, their lengths, and angles.33theorem angleDot.of_sss (a b c d e f : Point)34  requires firstSide : Euclidean.distanceSquared(a, b) = Euclidean.distanceSquared(d, e)35  requires secondSide : Euclidean.distanceSquared(b, c) = Euclidean.distanceSquared(e, f)36  requires opposite : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(d, f)37  shows angleDot(a, b, c) = angleDot(d, e, f)38proof39  have first := cosine_identity at a, b, c with *40  have second := cosine_identity at d, e, f with *41  have doubled : angleDot(a, b, c) + angleDot(a, b, c) =42      angleDot(d, e, f) + angleDot(d, e, f)43    linear_combination first - second + firstSide + secondSide - opposite44  exact realAddValue.double_cancel with doubled4546theorem equalAngle.sss (a b c d e f : Point)47  requires firstRay : a ≠ b48  requires secondRay : b ≠ c49  requires firstSide : Euclidean.distanceSquared(a, b) = Euclidean.distanceSquared(d, e)50  requires secondSide : Euclidean.distanceSquared(b, c) = Euclidean.distanceSquared(e, f)51  requires opposite : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(d, f)52  shows EqualAngle(a, b, c, d, e, f)53proof54  have positiveFirst := Euclidean.distanceSquared.positive at a, b with *55  have positiveSecond := Euclidean.distanceSquared.positive at b, c with *56  have equalDots := angleDot.of_sss at a, b, c, d, e, f with *57  have dotReal := angleDot.real at a, b, c with *58  have sameSign := realMulValue.square_nonnegative with dotReal59  unfold EqualAngle60  refine ⟨positiveFirst, positiveSecond, _, _, _, _⟩61  . rw ← firstSide62    exact positiveFirst63  . rw ← secondSide64    exact positiveSecond65  . rw [← firstSide, ← secondSide, ← equalDots]66    rfl67  . rw ← equalDots68    exact sameSign6970-- Compare triangle CAB with triangle CBA: the legs are equal, the base71-- is shared, and the opposite sides are the same equal legs.72theorem isosceles (a b c : Point)73  requires base : a ≠ b74  requires leg : a ≠ c75  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)76  shows EqualAngle(c, a, b, c, b, a)77proof78  have ca := Euclidean.distanceSquared.symmetric at c, a with *79  have cb := Euclidean.distanceSquared.symmetric at c, b with *80  have shared := Euclidean.distanceSquared.symmetric at a, b with *81  have first : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b) by cc82  have opposite : Euclidean.distanceSquared(c, b) = Euclidean.distanceSquared(c, a) by cc83  have distinct : c ≠ a84    intro equal85    apply leg86    cc87  exact equalAngle.sss with *8889end Euclidean90