-- The centroid and the three medians of a triangle.
-- 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.Centroid
import Parallelogram

namespace Euclidean
export open Euclidean

-- Affine balance, including collinear and collapsed triangles.
predicate Centroid (g a b c : Set) :=
  x(g) + x(g) + x(g) = x(a) + x(b) + x(c) ∧
  y(g) + y(g) + y(g) = y(a) + y(b) + y(c)

def centroid (a b c : Set) : Set :=
  (third(x(a) + x(b) + x(c)),
   third(y(a) + y(b) + y(c)))

-- Directed displacement AG is twice GM. This identity also allows A = G = M;
-- interpreting a quotient of nonzero lengths requires nondegeneracy separately.
predicate MedianRatio (a g m : Set) :=
  x(g) - x(a) = (x(m) - x(g)) + (x(m) - x(g)) ∧
  y(g) - y(a) = (y(m) - y(g)) + (y(m) - y(g))

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

theorem centroid.correct (a b c : Point)
  shows Centroid(centroid(a, b, c), a, b, c)
proof
  have horizontal := x.pair at third(x(a) + x(b) + x(c)), third(y(a) + y(b) + y(c)) with *
  have vertical := y.pair at third(x(a) + x(b) + x(c)), third(y(a) + y(b) + y(c)) with *
  have tripleX := third.add_self at x(a) + x(b) + x(c) with *
  have tripleY := third.add_self at y(a) + y(b) + y(c) with *
  constructor
  . unfold centroid
    cc
  . unfold centroid
    cc

theorem centroid.rotate (a b c g : Point)
  requires center : Centroid(g, a, b, c)
  shows Centroid(g, b, c, a)
proof
  rcases center with ⟨horizontal, vertical⟩
  constructor
  . linear_combination horizontal
  . linear_combination vertical

theorem centroid.unique (a b c g h : Point)
  requires first : Centroid(g, a, b, c)
  requires second : Centroid(h, a, b, c)
  shows g = h
proof
  rcases first with ⟨firstX, firstY⟩
  rcases second with ⟨secondX, secondY⟩
  have tripledX : x(g) + x(g) + x(g) = x(h) + x(h) + x(h) by cc
  have tripledY : y(g) + y(g) + y(g) = y(h) + y(h) + y(h) by cc
  have horizontal := realAddValue.triple_cancel at x(g), x(h) with *
  have vertical := realAddValue.triple_cancel at y(g), y(h) with *
  exact point.ext with *

theorem centroid.median_ratio (a b c g m : Point)
  requires center : Centroid(g, a, b, c)
  requires middle : Midpoint(m, b, c)
  shows MedianRatio(a, g, m)
proof
  rcases center with ⟨centerX, centerY⟩
  rcases middle with ⟨middleX, middleY⟩
  constructor
  . linear_combination centerX + middleX
  . linear_combination centerY + middleY

theorem medianRatio.collinear (a g m : Point)
  requires ratio : MedianRatio(a, g, m)
  shows Collinear(a, g, m)
proof
  unfold Collinear
  unfold directionCross
  rcases ratio with ⟨horizontal, vertical⟩
  linear_combination (y(m) - y(g)) * horizontal - (x(m) - x(g)) * vertical

-- The public median argument uses affine balance and midpoint facts only.
theorem centroid.medians (a b c g m n p : Point)
  requires center : Centroid(g, a, b, c)
  requires first : Midpoint(m, b, c)
  requires second : Midpoint(n, c, a)
  requires third : Midpoint(p, a, b)
  shows MedianRatio(a, g, m) ∧ MedianRatio(b, g, n) ∧ MedianRatio(c, g, p)
proof
  have rotated := centroid.rotate with *
  have again := centroid.rotate at b, c, a, g with *
  have firstRatio := centroid.median_ratio at a, b, c, g, m with *
  have secondRatio := centroid.median_ratio at b, c, a, g, n with *
  have thirdRatio := centroid.median_ratio at c, a, b, g, p with *
  refine ⟨firstRatio, secondRatio, thirdRatio⟩

theorem centroid.concurrency (a b c m n p : Point)
  requires first : Midpoint(m, b, c)
  requires second : Midpoint(n, c, a)
  requires third : Midpoint(p, a, b)
  shows ∃ g, Point(g) ∧ Centroid(g, a, b, c) ∧
    Collinear(a, g, m) ∧ Collinear(b, g, n) ∧ Collinear(c, g, p)
proof
  have point := centroid.point at a, b, c with *
  have center := centroid.correct at a, b, c with *
  have ratios := centroid.medians with *
  rcases ratios with ⟨firstRatio, secondRatio, thirdRatio⟩
  have firstLine := medianRatio.collinear at a, centroid(a, b, c), m with *
  have secondLine := medianRatio.collinear at b, centroid(a, b, c), n with *
  have thirdLine := medianRatio.collinear at c, centroid(a, b, c), p with *
  refine ⟨centroid(a, b, c), point, center, firstLine, secondLine, thirdLine⟩

-- The directed 2:1 relation implies the corresponding squared-length identity.
theorem medianRatio.length (a g m : Point)
  requires ratio : MedianRatio(a, g, m)
  shows Euclidean.distanceSquared(a, g) =
    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m) +
    Euclidean.distanceSquared(g, m) + Euclidean.distanceSquared(g, m)
proof
  rcases ratio with ⟨horizontal, vertical⟩
  have doubledX : (x(m) - x(g)) + (x(m) - x(g)) = x(g) - x(a)
    symm
    exact horizontal
  have doubledY : (y(m) - y(g)) + (y(m) - y(g)) = y(g) - y(a)
    symm
    exact vertical
  have squareX := realMulValue.square_of_double at x(m) - x(g), x(g) - x(a) with *
  have squareY := realMulValue.square_of_double at y(m) - y(g), y(g) - y(a) with *
  have long := Euclidean.distanceSquared.coordinates at a, g with *
  have short := Euclidean.distanceSquared.coordinates at g, m with *
  rw [long, short, squareX, squareY]
  ring

theorem centroid.repeated (a : Point)
  shows centroid(a, a, a) = a
proof
  have point := centroid.point with *
  have first := centroid.correct at a, a, a with *
  have second : Centroid(a, a, a, a)
    constructor
    . rfl
    . rfl
  exact centroid.unique with *

end Euclidean