-- Circumcenters, orthocenters, and Euler's line.
-- 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

module Grace.Cumulus.Geometry.TriangleCenters
import Centroid
import LinearAlgebra.TwoByTwo

namespace Euclidean
export open Euclidean

predicate Circumcenter (o a b c : Set) :=
  Euclidean.distanceSquared(o, a) = Euclidean.distanceSquared(o, b) ∧
  Euclidean.distanceSquared(o, a) = Euclidean.distanceSquared(o, c)

-- Reuse the checked midpoint-of-hypotenuse construction for right triangles.
theorem circumcenter.right_triangle (a b c m : Point)
  requires middle : Midpoint(m, a, b)
  requires right : RightAngle(a, c, b)
  shows Circumcenter(m, a, b, c)
proof
  have radii := right_triangle_circumcenter at a, b, c, m with *
  rcases radii with ⟨first, second⟩
  constructor
  . cc
  . cc

-- Each vertex-to-center direction is perpendicular to its opposite side.
-- Zero directions are allowed; no distinct-line or uniqueness claim is implicit.
predicate Orthocenter (h a b c : Set) :=
  PerpendicularDirections(a, h, b, c) ∧
  PerpendicularDirections(b, h, c, a) ∧
  PerpendicularDirections(c, h, a, b)

-- Given a circumcenter O, construct H = A + B + C - 2O.
def orthocenter (o a b c : Set) : Set :=
  (x(a) + x(b) + x(c) - (x(o) + x(o)),
   y(a) + y(b) + y(c) - (y(o) + y(o)))

theorem orthocenter.point (o a b c : Point)
  shows Point(orthocenter(o, a, b, c))
proof
  unfold orthocenter
  exact pair.point with *

theorem orthocenter.coordinates (o a b c : Point)
  shows x(orthocenter(o, a, b, c)) = x(a) + x(b) + x(c) - (x(o) + x(o)) ∧
    y(orthocenter(o, a, b, c)) = y(a) + y(b) + y(c) - (y(o) + y(o))
proof
  have horizontal := x.pair at x(a) + x(b) + x(c) - (x(o) + x(o)), y(a) + y(b) + y(c) - (y(o) + y(o)) with *
  have vertical := y.pair at x(a) + x(b) + x(c) - (x(o) + x(o)), y(a) + y(b) + y(c) - (y(o) + y(o)) with *
  constructor
  . unfold orthocenter
    exact horizontal
  . unfold orthocenter
    exact vertical

theorem orthocenter.rotate (o a b c : Point)
  shows orthocenter(o, a, b, c) = orthocenter(o, b, c, a)
proof
  have firstPoint := orthocenter.point at o, a, b, c with *
  have secondPoint := orthocenter.point at o, b, c, a with *
  have first := orthocenter.coordinates at o, a, b, c with *
  have second := orthocenter.coordinates at o, b, c, a with *
  rcases first with ⟨firstX, firstY⟩
  rcases second with ⟨secondX, secondY⟩
  have horizontal : x(orthocenter(o, a, b, c)) = x(orthocenter(o, b, c, a)) by linear_combination firstX - secondX
  have vertical : y(orthocenter(o, a, b, c)) = y(orthocenter(o, b, c, a)) by linear_combination firstY - secondY
  exact point.ext with *

-- Equal radii to B and C make AH perpendicular to BC.
theorem orthocenter.altitude (o a b c : Point)
  requires equalRadii : Euclidean.distanceSquared(o, b) = Euclidean.distanceSquared(o, c)
  shows PerpendicularDirections(a, orthocenter(o, a, b, c), b, c)
proof
  have point := orthocenter.point at o, a, b, c with *
  have product := vector.dot_coordinates at a, orthocenter(o, a, b, c), b, c with *
  have firstRadius := Euclidean.distanceSquared.coordinates at o, b with *
  have secondRadius := Euclidean.distanceSquared.coordinates at o, c with *
  rw [firstRadius, secondRadius] at equalRadii
  unfold PerpendicularDirections
  rw product
  have coordinates := orthocenter.coordinates at o, a, b, c with *
  rcases coordinates with ⟨horizontal, vertical⟩
  linear_combination (x(c) - x(b)) * horizontal + (y(c) - y(b)) * vertical - equalRadii

-- The three altitude statements follow by cyclic permutation.
theorem orthocenter.correct (o a b c : Point)
  requires circle : Circumcenter(o, a, b, c)
  shows Orthocenter(orthocenter(o, a, b, c), a, b, c)
proof
  rcases circle with ⟨firstRadii, secondRadii⟩
  have oppositeRadii : Euclidean.distanceSquared(o, b) = Euclidean.distanceSquared(o, c) by cc
  have reversedRadii : Euclidean.distanceSquared(o, c) = Euclidean.distanceSquared(o, a)
    symm
    exact secondRadii
  have first := orthocenter.altitude at o, a, b, c with *
  have second := orthocenter.altitude at o, b, c, a with *
  have third := orthocenter.altitude at o, c, a, b with *
  have rotate := orthocenter.rotate at o, a, b, c with *
  have again := orthocenter.rotate at o, b, c, a with *
  rw [← again, ← rotate] at third
  rw ← rotate at second
  unfold Orthocenter
  refine ⟨first, second, third⟩

-- G lies two thirds of the way from H to O, so HG = 2 GO as directed vectors.
theorem orthocenter.centroid_ratio (o a b c g : Point)
  requires center : Centroid(g, a, b, c)
  shows MedianRatio(orthocenter(o, a, b, c), g, o)
proof
  have point := orthocenter.point at o, a, b, c with *
  unfold MedianRatio
  have coordinates := orthocenter.coordinates at o, a, b, c with *
  rcases coordinates with ⟨horizontal, vertical⟩
  rcases center with ⟨centerX, centerY⟩
  constructor
  . linear_combination centerX - horizontal
  . linear_combination centerY - vertical

-- Euler's line, formulated to include coincident centers without claiming
-- that such points determine a unique line.
theorem euler_line (o a b c g : Point)
  requires circle : Circumcenter(o, a, b, c)
  requires center : Centroid(g, a, b, c)
  shows ∃ h, Point(h) ∧ Orthocenter(h, a, b, c) ∧
    Collinear(h, g, o) ∧ MedianRatio(h, g, o)
proof
  have point := orthocenter.point at o, a, b, c with *
  have altitudes := orthocenter.correct with *
  have ratio := orthocenter.centroid_ratio at o, a, b, c, g with *
  have line := medianRatio.collinear with *
  refine ⟨orthocenter(o, a, b, c), point, altitudes, line, ratio⟩

-- The affine construction collapses to G when O = G.
theorem orthocenter.at_centroid (o a b c : Point)
  requires center : Centroid(o, a, b, c)
  shows orthocenter(o, a, b, c) = o
proof
  have point := orthocenter.point at o, a, b, c with *
  have coordinates := orthocenter.coordinates at o, a, b, c with *
  rcases coordinates with ⟨horizontal, vertical⟩
  rcases center with ⟨centerX, centerY⟩
  have sameX : x(orthocenter(o, a, b, c)) = x(o) by linear_combination horizontal - centerX
  have sameY : y(orthocenter(o, a, b, c)) = y(o) by linear_combination vertical - centerY
  exact point.ext with *

theorem euler_line.coincident (o a b c : Point)
  requires circle : Circumcenter(o, a, b, c)
  requires center : Centroid(o, a, b, c)
  shows Orthocenter(o, a, b, c)
proof
  have altitudes := orthocenter.correct with *
  have same := orthocenter.at_centroid with *
  rwa same at altitudes

-- An altitude condition is a linear equation in the candidate center.
theorem altitude.equation (a h b c : Point)
  requires perpendicular : PerpendicularDirections(a, h, b, c)
  shows (x(c) - x(b)) * x(h) + (y(c) - y(b)) * y(h) =
    (x(c) - x(b)) * x(a) + (y(c) - y(b)) * y(a)
proof
  have product := vector.dot_coordinates at a, h, b, c with *
  unfold PerpendicularDirections at perpendicular
  rw product at perpendicular
  linear_combination perpendicular

-- Two altitudes already determine the center of a noncollinear triangle.
theorem altitudes.unique (a b c h k : Point)
  requires noncollinear : ¬Collinear(a, b, c)
  requires firstAltitude : PerpendicularDirections(a, h, b, c)
  requires secondAltitude : PerpendicularDirections(b, h, c, a)
  requires otherFirstAltitude : PerpendicularDirections(a, k, b, c)
  requires otherSecondAltitude : PerpendicularDirections(b, k, c, a)
  shows h = k
proof
  have nonsingular : (x(c) - x(b)) * (y(a) - y(c)) - (y(c) - y(b)) * (x(a) - x(c)) ≠ 0
    intro zero
    apply noncollinear
    unfold Collinear
    unfold directionCross
    linear_combination zero
  have first := altitude.equation at a, h, b, c with *
  have second := altitude.equation at b, h, c, a with *
  have otherFirst := altitude.equation at a, k, b, c with *
  have otherSecond := altitude.equation at b, k, c, a with *
  have coordinates := LinearSystem2.unique at x(c) - x(b), y(c) - y(b), x(a) - x(c), y(a) - y(c),
    (x(c) - x(b)) * x(a) + (y(c) - y(b)) * y(a),
    (x(a) - x(c)) * x(b) + (y(a) - y(c)) * y(b), x(h), y(h), x(k), y(k) with *
  rcases coordinates with ⟨horizontal, vertical⟩
  exact point.ext with *

theorem orthocenter.unique (a b c h k : Point)
  requires noncollinear : ¬Collinear(a, b, c)
  requires firstCenter : Orthocenter(h, a, b, c)
  requires secondCenter : Orthocenter(k, a, b, c)
  shows h = k
proof
  rcases firstCenter with ⟨firstAltitude, secondAltitude, thirdAltitude⟩
  rcases secondCenter with ⟨otherFirstAltitude, otherSecondAltitude, otherThirdAltitude⟩
  exact altitudes.unique with *

end Euclidean