-- Midpoints, medians, and perpendicular bisectors in the Euclidean plane.
-- 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.Midpoint
import Circle

namespace Euclidean
export open Euclidean

-- The midpoint is constructed from coordinates.
def midpoint (a b : Set) : Set :=
  (half(x(a) + x(b)), half(y(a) + y(b)))

theorem midpoint.point (a b : Point)
  shows Point(midpoint(a, b))
proof
  have ax := x.real at a with assumption
  have ay := y.real at a with assumption
  have bx := x.real at b with assumption
  have byReal := y.real at b with assumption
  have sumX := realAddValue.real with ax, bx
  have sumY := realAddValue.real with ay, byReal
  have halfX := half.real with sumX
  have halfY := half.real with sumY
  unfold midpoint
  exact pair.point with halfX, halfY

theorem midpoint.correct (a b : Point)
  shows Midpoint(midpoint(a, b), a, b)
proof
  have ax := x.real at a with assumption
  have ay := y.real at a with assumption
  have bx := x.real at b with assumption
  have byReal := y.real at b with assumption
  have sumX := realAddValue.real with ax, bx
  have sumY := realAddValue.real with ay, byReal
  have halfX := half.real with sumX
  have halfY := half.real with sumY
  have horizontal := x.pair with halfX, halfY
  have vertical := y.pair with halfX, halfY
  have doubleX := half.add_self with sumX
  have doubleY := half.add_self with sumY
  constructor
  . unfold midpoint
    cc
  . unfold midpoint
    cc

theorem midpoint.unique (a b m n : Point)
  requires first : Midpoint(m, a, b)
  requires second : Midpoint(n, a, b)
  shows m = n
proof
  rcases first with ⟨firstX, firstY⟩
  rcases second with ⟨secondX, secondY⟩
  have doubledX : x(m) + x(m) = x(n) + x(n) by cc
  have doubledY : y(m) + y(m) = y(n) + y(n) by cc
  have horizontal := realAddValue.double_cancel with doubledX
  have vertical := realAddValue.double_cancel with doubledY
  exact point.ext with *

theorem midpoint.symmetric (a b m : Point)
  requires middle : Midpoint(m, a, b)
  shows Midpoint(m, b, a)
proof
  rcases middle with ⟨horizontal, vertical⟩
  have ax := x.real at a with assumption
  have ay := y.real at a with assumption
  have bx := x.real at b with assumption
  have byReal := y.real at b with assumption
  have swapX := realAddValue.commutative with ax, bx
  have swapY := realAddValue.commutative with ay, byReal
  constructor
  . cc
  . cc

theorem midpoint.equidistant (a b m : Point)
  requires middle : Midpoint(m, a, b)
  shows Euclidean.distanceSquared(m, a) = Euclidean.distanceSquared(m, b)
proof
  rcases middle with ⟨horizontal, vertical⟩
  have first := Euclidean.distanceSquared.coordinates at m, a with *
  have second := Euclidean.distanceSquared.coordinates at m, b with *
  rw [first, second]
  linear_combination (x(a) - x(b)) * horizontal + (y(a) - y(b)) * vertical

-- Opposite radius vectors have opposite dot products with every vector.
theorem midpoint.opposite_dots (a b m p : Point)
  requires middle : Midpoint(m, a, b)
  shows angleDot(p, m, a) + angleDot(p, m, b) = 0
proof
  rcases middle with ⟨horizontal, vertical⟩
  have first := angleDot.coordinates at p, m, a with *
  have second := angleDot.coordinates at p, m, b with *
  rw [first, second]
  linear_combination (x(p) - x(m)) * horizontal + (y(p) - y(m)) * vertical

-- Apollonius' median theorem. The two smaller triangles share a median;
-- their cosine terms cancel because the two half-base vectors are opposite.
theorem apollonius (a b m p : Point)
  requires middle : Midpoint(m, a, b)
  shows Euclidean.distanceSquared(p, a) + Euclidean.distanceSquared(p, b) =
    Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(p, m) +
    Euclidean.distanceSquared(m, a) + Euclidean.distanceSquared(m, a)
proof
  have first := cosine_identity at p, m, a with *
  have second := cosine_identity at p, m, b with *
  have opposite := midpoint.opposite_dots at a, b, m, p with *
  have halves := midpoint.equidistant with *
  linear_combination first + second - (2:R) * opposite - halves

-- The locus of points equidistant from A and B is their perpendicular
-- bisector. RightAngle denotes orthogonality, including the zero vector;
-- thus the midpoint itself belongs to the locus. For a proper base, A ≠ B.
theorem perpendicular_bisector (a b m p : Point)
  requires middle : Midpoint(m, a, b)
  shows Euclidean.distanceSquared(p, a) = Euclidean.distanceSquared(p, b) ↔
    RightAngle(p, m, a)
proof
  have median := apollonius at a, b, m, p with *
  constructor
  . intro equalSides
    have doubled : Euclidean.distanceSquared(p, a) + Euclidean.distanceSquared(p, a) =
        (Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(m, a)) +
        (Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(m, a))
      linear_combination median + equalSides
    have pythagorean := realAddValue.double_cancel with doubled
    exact pythagoras_converse at p, m, a with *
  . intro perpendicular
    have pythagorean := Euclidean.pythagoras at p, m, a with *
    linear_combination (2:R) * pythagorean - median

-- The median from the apex of an isosceles triangle is an altitude.
theorem isosceles_median_perpendicular (a b c m : Point)
  requires middle : Midpoint(m, a, b)
  requires equalLegs : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b)
  shows RightAngle(c, m, a)
proof
  exact perpendicular_bisector.forward at a, b, m, c with *

-- The same diameter identity proves both Thales and its converse.
-- This is an orthogonality statement; endpoint exclusions are unnecessary.
theorem right_iff_on_diameter_circle (a b p m : Point)
  requires middle : Midpoint(m, a, b)
  shows RightAngle(a, p, b) ↔ OnCircle(p, m, a)
proof
  have identity := diameter_identity at a, b, p, m with *
  constructor
  . intro right
    unfold RightAngle at right
    unfold OnCircle
    linear_combination right - identity
  . intro onCircle
    unfold OnCircle at onCircle
    unfold RightAngle
    linear_combination identity + onCircle

-- The midpoint of the hypotenuse is equidistant from all three vertices.
theorem right_triangle_circumcenter (a b p m : Point)
  requires middle : Midpoint(m, a, b)
  requires right : RightAngle(a, p, b)
  shows Euclidean.distanceSquared(m, p) = Euclidean.distanceSquared(m, a) ∧
    Euclidean.distanceSquared(m, p) = Euclidean.distanceSquared(m, b)
proof
  have onCircle := right_iff_on_diameter_circle.forward at a, b, p, m with *
  have halves := midpoint.equidistant with *
  have pm := Euclidean.distanceSquared.symmetric at p, m with *
  have am := Euclidean.distanceSquared.symmetric at a, m with *
  unfold OnCircle at onCircle
  constructor
  . cc
  . cc

-- A circle's center lies on the perpendicular bisector of each chord.
-- When the chord is a diameter the center equals its midpoint; the
-- orthogonality formulation includes that case.
theorem circle_center_chord (a b center through m : Point)
  requires endpointA : OnCircle(a, center, through)
  requires endpointB : OnCircle(b, center, through)
  requires middle : Midpoint(m, a, b)
  shows RightAngle(center, m, a)
proof
  unfold OnCircle at endpointA
  unfold OnCircle at endpointB
  have first := Euclidean.distanceSquared.symmetric at center, a with *
  have second := Euclidean.distanceSquared.symmetric at center, b with *
  have equalRadii : Euclidean.distanceSquared(center, a) = Euclidean.distanceSquared(center, b) by cc
  exact perpendicular_bisector.forward at a, b, m, center with *

end Euclidean