Grace/Cumulus/Geometry/Midpoint.g17

Open in Workbench Download source

Imports

Circle

Declarations

Source

1-- Midpoints, medians, and perpendicular bisectors in the Euclidean plane.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 Passmore67module Grace.Cumulus.Geometry.Midpoint8import Circle910namespace Euclidean11export open Euclidean1213-- The midpoint is constructed from coordinates.14def midpoint (a b : Set) : Set :=15  (half(x(a) + x(b)), half(y(a) + y(b)))1617theorem midpoint.point (a b : Point)18  shows Point(midpoint(a, b))19proof20  have ax := x.real at a with assumption21  have ay := y.real at a with assumption22  have bx := x.real at b with assumption23  have byReal := y.real at b with assumption24  have sumX := realAddValue.real with ax, bx25  have sumY := realAddValue.real with ay, byReal26  have halfX := half.real with sumX27  have halfY := half.real with sumY28  unfold midpoint29  exact pair.point with halfX, halfY3031theorem midpoint.correct (a b : Point)32  shows Midpoint(midpoint(a, b), a, b)33proof34  have ax := x.real at a with assumption35  have ay := y.real at a with assumption36  have bx := x.real at b with assumption37  have byReal := y.real at b with assumption38  have sumX := realAddValue.real with ax, bx39  have sumY := realAddValue.real with ay, byReal40  have halfX := half.real with sumX41  have halfY := half.real with sumY42  have horizontal := x.pair with halfX, halfY43  have vertical := y.pair with halfX, halfY44  have doubleX := half.add_self with sumX45  have doubleY := half.add_self with sumY46  constructor47  . unfold midpoint48    cc49  . unfold midpoint50    cc5152theorem midpoint.unique (a b m n : Point)53  requires first : Midpoint(m, a, b)54  requires second : Midpoint(n, a, b)55  shows m = n56proof57  rcases first with ⟨firstX, firstY⟩58  rcases second with ⟨secondX, secondY⟩59  have doubledX : x(m) + x(m) = x(n) + x(n) by cc60  have doubledY : y(m) + y(m) = y(n) + y(n) by cc61  have horizontal := realAddValue.double_cancel with doubledX62  have vertical := realAddValue.double_cancel with doubledY63  exact point.ext with *6465theorem midpoint.symmetric (a b m : Point)66  requires middle : Midpoint(m, a, b)67  shows Midpoint(m, b, a)68proof69  rcases middle with ⟨horizontal, vertical⟩70  have ax := x.real at a with assumption71  have ay := y.real at a with assumption72  have bx := x.real at b with assumption73  have byReal := y.real at b with assumption74  have swapX := realAddValue.commutative with ax, bx75  have swapY := realAddValue.commutative with ay, byReal76  constructor77  . cc78  . cc7980theorem midpoint.equidistant (a b m : Point)81  requires middle : Midpoint(m, a, b)82  shows Euclidean.distanceSquared(m, a) = Euclidean.distanceSquared(m, b)83proof84  rcases middle with ⟨horizontal, vertical⟩85  have first := Euclidean.distanceSquared.coordinates at m, a with *86  have second := Euclidean.distanceSquared.coordinates at m, b with *87  rw [first, second]88  linear_combination (x(a) - x(b)) * horizontal + (y(a) - y(b)) * vertical8990-- Opposite radius vectors have opposite dot products with every vector.91theorem midpoint.opposite_dots (a b m p : Point)92  requires middle : Midpoint(m, a, b)93  shows angleDot(p, m, a) + angleDot(p, m, b) = 094proof95  rcases middle with ⟨horizontal, vertical⟩96  have first := angleDot.coordinates at p, m, a with *97  have second := angleDot.coordinates at p, m, b with *98  rw [first, second]99  linear_combination (x(p) - x(m)) * horizontal + (y(p) - y(m)) * vertical100101-- Apollonius' median theorem. The two smaller triangles share a median;102-- their cosine terms cancel because the two half-base vectors are opposite.103theorem apollonius (a b m p : Point)104  requires middle : Midpoint(m, a, b)105  shows Euclidean.distanceSquared(p, a) + Euclidean.distanceSquared(p, b) =106    Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(p, m) +107    Euclidean.distanceSquared(m, a) + Euclidean.distanceSquared(m, a)108proof109  have first := cosine_identity at p, m, a with *110  have second := cosine_identity at p, m, b with *111  have opposite := midpoint.opposite_dots at a, b, m, p with *112  have halves := midpoint.equidistant with *113  linear_combination first + second - (2:R) * opposite - halves114115-- The locus of points equidistant from A and B is their perpendicular116-- bisector. RightAngle denotes orthogonality, including the zero vector;117-- thus the midpoint itself belongs to the locus. For a proper base, A ≠ B.118theorem perpendicular_bisector (a b m p : Point)119  requires middle : Midpoint(m, a, b)120  shows Euclidean.distanceSquared(p, a) = Euclidean.distanceSquared(p, b) ↔121    RightAngle(p, m, a)122proof123  have median := apollonius at a, b, m, p with *124  constructor125  . intro equalSides126    have doubled : Euclidean.distanceSquared(p, a) + Euclidean.distanceSquared(p, a) =127        (Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(m, a)) +128        (Euclidean.distanceSquared(p, m) + Euclidean.distanceSquared(m, a))129      linear_combination median + equalSides130    have pythagorean := realAddValue.double_cancel with doubled131    exact pythagoras_converse at p, m, a with *132  . intro perpendicular133    have pythagorean := Euclidean.pythagoras at p, m, a with *134    linear_combination (2:R) * pythagorean - median135136-- The median from the apex of an isosceles triangle is an altitude.137theorem isosceles_median_perpendicular (a b c m : Point)138  requires middle : Midpoint(m, a, b)139  requires equalLegs : Euclidean.distanceSquared(c, a) = Euclidean.distanceSquared(c, b)140  shows RightAngle(c, m, a)141proof142  exact perpendicular_bisector.forward at a, b, m, c with *143144-- The same diameter identity proves both Thales and its converse.145-- This is an orthogonality statement; endpoint exclusions are unnecessary.146theorem right_iff_on_diameter_circle (a b p m : Point)147  requires middle : Midpoint(m, a, b)148  shows RightAngle(a, p, b) ↔ OnCircle(p, m, a)149proof150  have identity := diameter_identity at a, b, p, m with *151  constructor152  . intro right153    unfold RightAngle at right154    unfold OnCircle155    linear_combination right - identity156  . intro onCircle157    unfold OnCircle at onCircle158    unfold RightAngle159    linear_combination identity + onCircle160161-- The midpoint of the hypotenuse is equidistant from all three vertices.162theorem right_triangle_circumcenter (a b p m : Point)163  requires middle : Midpoint(m, a, b)164  requires right : RightAngle(a, p, b)165  shows Euclidean.distanceSquared(m, p) = Euclidean.distanceSquared(m, a) ∧166    Euclidean.distanceSquared(m, p) = Euclidean.distanceSquared(m, b)167proof168  have onCircle := right_iff_on_diameter_circle.forward at a, b, p, m with *169  have halves := midpoint.equidistant with *170  have pm := Euclidean.distanceSquared.symmetric at p, m with *171  have am := Euclidean.distanceSquared.symmetric at a, m with *172  unfold OnCircle at onCircle173  constructor174  . cc175  . cc176177-- A circle's center lies on the perpendicular bisector of each chord.178-- When the chord is a diameter the center equals its midpoint; the179-- orthogonality formulation includes that case.180theorem circle_center_chord (a b center through m : Point)181  requires endpointA : OnCircle(a, center, through)182  requires endpointB : OnCircle(b, center, through)183  requires middle : Midpoint(m, a, b)184  shows RightAngle(center, m, a)185proof186  unfold OnCircle at endpointA187  unfold OnCircle at endpointB188  have first := Euclidean.distanceSquared.symmetric at center, a with *189  have second := Euclidean.distanceSquared.symmetric at center, b with *190  have equalRadii : Euclidean.distanceSquared(center, a) = Euclidean.distanceSquared(center, b) by cc191  exact perpendicular_bisector.forward at a, b, m, center with *192193end Euclidean194