-- Equal sides give equal base angles.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

-- Adapted from Grant Passmore's Imandra Top 100 isosceles theorem:
-- https://github.com/imandra-ai/imandra-100-theorems/blob/main/src/isosceles.iml

module Grace.Cumulus.Geometry.Isosceles
import Plane
import Real.Metric

namespace Euclidean
export open Euclidean

-- Equality of unoriented angles, encoded without arccos or roots.
-- Positivity excludes zero rays. The final sign condition distinguishes
-- equal angles from supplementary angles with the same squared cosine.
predicate EqualAngle (a b c d e f : Set) :=
  0 < Euclidean.distanceSquared(a, b) ∧
  0 < Euclidean.distanceSquared(b, c) ∧
  0 < Euclidean.distanceSquared(d, e) ∧
  0 < Euclidean.distanceSquared(e, f) ∧
  (angleDot(a, b, c) * angleDot(a, b, c)) *
    (Euclidean.distanceSquared(d, e) * Euclidean.distanceSquared(e, f)) =
  (angleDot(d, e, f) * angleDot(d, e, f)) *
    (Euclidean.distanceSquared(a, b) * Euclidean.distanceSquared(b, c)) ∧
  0 ≤ angleDot(a, b, c) * angleDot(d, e, f)

-- The coordinate calculation is confined to cosine_identity. Everything
-- from here on reasons about sides, their lengths, and angles.
theorem angleDot.of_sss (a b c d e f : Point)
  requires firstSide : Euclidean.distanceSquared(a, b) = Euclidean.distanceSquared(d, e)
  requires secondSide : Euclidean.distanceSquared(b, c) = Euclidean.distanceSquared(e, f)
  requires opposite : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(d, f)
  shows angleDot(a, b, c) = angleDot(d, e, f)
proof
  have first := cosine_identity at a, b, c with *
  have second := cosine_identity at d, e, f with *
  have doubled : angleDot(a, b, c) + angleDot(a, b, c) =
      angleDot(d, e, f) + angleDot(d, e, f)
    linear_combination first - second + firstSide + secondSide - opposite
  exact realAddValue.double_cancel with doubled

theorem equalAngle.sss (a b c d e f : Point)
  requires firstRay : a ≠ b
  requires secondRay : b ≠ c
  requires firstSide : Euclidean.distanceSquared(a, b) = Euclidean.distanceSquared(d, e)
  requires secondSide : Euclidean.distanceSquared(b, c) = Euclidean.distanceSquared(e, f)
  requires opposite : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(d, f)
  shows EqualAngle(a, b, c, d, e, f)
proof
  have positiveFirst := Euclidean.distanceSquared.positive at a, b with *
  have positiveSecond := Euclidean.distanceSquared.positive at b, c with *
  have equalDots := angleDot.of_sss at a, b, c, d, e, f with *
  have dotReal := angleDot.real at a, b, c with *
  have sameSign := realMulValue.square_nonnegative with dotReal
  unfold EqualAngle
  refine ⟨positiveFirst, positiveSecond, _, _, _, _⟩
  . rw ← firstSide
    exact positiveFirst
  . rw ← secondSide
    exact positiveSecond
  . rw [← firstSide, ← secondSide, ← equalDots]
    rfl
  . rw ← equalDots
    exact sameSign

-- Compare triangle CAB with triangle CBA: the legs are equal, the base
-- is shared, and the opposite sides are the same equal legs.
theorem isosceles (a b c : Point)
  requires base : a ≠ b
  requires leg : a ≠ c
  requires equalLegs : Euclidean.distanceSquared(a, c) = Euclidean.distanceSquared(b, c)
  shows EqualAngle(c, a, b, c, b, a)
proof
  have ca := Euclidean.distanceSquared.symmetric at c, a with *
  have cb := Euclidean.distanceSquared.symmetric at c, b with *
  have shared := Euclidean.distanceSquared.symmetric at a, b with *
  have first : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b) by cc
  have opposite : Euclidean.distanceSquared(c, b) = Euclidean.distanceSquared(c, a) by cc
  have distinct : c ≠ a
    intro equal
    apply leg
    cc
  exact equalAngle.sss with *

end Euclidean