Grace/Cumulus/Geometry/Lines.g17

Open in Workbench Download source

Imports

Midpoint

Declarations

Source

1-- Collinearity and the triangle midsegment theorem.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.Lines8import Midpoint910namespace Euclidean11export open Euclidean1213def directionCross (a b c d : Point) : Real :=14  (x(b) - x(a)) * (y(d) - y(c)) -15  (y(b) - y(a)) * (x(d) - x(c))1617predicate Collinear (a b c : Set) := directionCross(a, b, a, c) = 01819-- Algebraic orthogonality of directed segments, permitting zero directions.20predicate PerpendicularDirections (a b c d : Set) :=21  dot(vector(a, b), vector(c, d)) = 02223-- Parallel directions of nonzero segments. Coincident supporting lines24-- are allowed; this predicate does not assert that two lines are disjoint.25predicate ParallelSegments (a b c d : Set) :=26  a ≠ b ∧ c ≠ d ∧ directionCross(a, b, c, d) = 02728theorem directionCross.real (a b c d : Point)29  shows Real(directionCross(a, b, c, d))30proof31  unfold directionCross32  typecheck3334theorem midpoint.collinear (a b m : Point)35  requires middle : Midpoint(m, a, b)36  shows Collinear(a, m, b)37proof38  rcases middle with ⟨horizontal, vertical⟩39  have doubled : directionCross(a, m, a, b) + directionCross(a, m, a, b) = (0:R) + (0:R)40    unfold directionCross41    linear_combination -(y(b) - y(a)) * horizontal + (x(b) - x(a)) * vertical42  unfold Collinear43  exact realAddValue.double_cancel with realZero.real, doubled4445-- Twice the displacement between two side midpoints is the third side.46theorem midsegment.direction (a b c m n : Point)47  requires first : Midpoint(m, c, a)48  requires second : Midpoint(n, c, b)49  shows (x(n) - x(m)) + (x(n) - x(m)) = x(b) - x(a) ∧50    (y(n) - y(m)) + (y(n) - y(m)) = y(b) - y(a)51proof52  rcases first with ⟨firstX, firstY⟩53  rcases second with ⟨secondX, secondY⟩54  constructor55  . linear_combination firstX - secondX56  . linear_combination firstY - secondY5758theorem midsegment.distinct (a b c m n : Point)59  requires first : Midpoint(m, c, a)60  requires second : Midpoint(n, c, b)61  requires base : a ≠ b62  shows m ≠ n63proof64  rcases first with ⟨firstX, firstY⟩65  rcases second with ⟨secondX, secondY⟩66  intro equal67  rw equal at firstX68  rw equal at firstY69  have horizontal : x(a) = x(b) by linear_combination firstX - secondX70  have vertical : y(a) = y(b) by linear_combination firstY - secondY71  have same := point.ext with *72  exact base with same7374theorem midsegment.parallel (a b c m n : Point)75  requires first : Midpoint(m, c, a)76  requires second : Midpoint(n, c, b)77  requires base : a ≠ b78  shows ParallelSegments(m, n, a, b)79proof80  have direction := midsegment.direction at a, b, c, m, n with *81  rcases direction with ⟨horizontal, vertical⟩82  have distinct := midsegment.distinct with *83  have area := directionCross.real at m, n, a, b with *84  have doubled : directionCross(m, n, a, b) + directionCross(m, n, a, b) = (0:R) + (0:R)85    unfold directionCross86    linear_combination (y(b) - y(a)) * horizontal - (x(b) - x(a)) * vertical87  have parallel := realAddValue.double_cancel with area, realZero.real, doubled88  unfold ParallelSegments89  refine ⟨distinct, base, parallel⟩9091-- The midsegment has half the length of the third side, stated in squares.92theorem midsegment.length (a b c m n : Point)93  requires first : Midpoint(m, c, a)94  requires second : Midpoint(n, c, b)95  shows Euclidean.distanceSquared(a, b) =96    Euclidean.distanceSquared(m, n) + Euclidean.distanceSquared(m, n) +97    Euclidean.distanceSquared(m, n) + Euclidean.distanceSquared(m, n)98proof99  have direction := midsegment.direction at a, b, c, m, n with *100  rcases direction with ⟨horizontal, vertical⟩101  have base := Euclidean.distanceSquared.coordinates at a, b with *102  have segment := Euclidean.distanceSquared.coordinates at m, n with *103  rw [base, segment]104  have squareX := realMulValue.square_of_double with horizontal105  have squareY := realMulValue.square_of_double with vertical106  rw [squareX, squareY]107  ring108109-- Midsegments with the same directed base have the same displacement.110-- This is the geometric bridge used by Varignon's theorem.111theorem midsegment.equal_vectors (a b c d m n p q : Point)112  requires firstM : Midpoint(m, c, a)113  requires firstN : Midpoint(n, c, b)114  requires secondP : Midpoint(p, d, a)115  requires secondQ : Midpoint(q, d, b)116  shows vector(m, n) = vector(p, q)117proof118  have first := midsegment.direction at a, b, c, m, n with *119  have second := midsegment.direction at a, b, d, p, q with *120  rcases first with ⟨firstX, firstY⟩121  rcases second with ⟨secondX, secondY⟩122  have horizontal : x(n) - x(m) = x(q) - x(p)123    apply realAddValue.double_cancel124    . cc125  have vertical : y(n) - y(m) = y(q) - y(p)126    apply realAddValue.double_cancel127    . cc128  have components : x(n) - x(m) = x(q) - x(p) ∧129      y(n) - y(m) = y(q) - y(p)130    refine ⟨horizontal, vertical⟩131  exact vector.equal_iff.backward with components132133end Euclidean134