Grace/Cumulus/Geometry/Parallelogram.g17

Open in Workbench Download source

Imports

Lines

Declarations

Source

1-- Parallelograms, diagonal bisection, and Varignon's midpoint 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.Parallelogram8import Lines910namespace Euclidean11export open Euclidean1213-- The affine parallelogram identity, allowing degenerate configurations.14-- Opposite directed sides agree. Nonzero-side hypotheses are supplied when15-- asserting ParallelSegments; coincident supporting lines remain allowed.16predicate Parallelogram (a b c d : Set) := vector(a, b) = vector(d, c)1718theorem parallelogram.rotate (a b c d : Point)19  requires shape : Parallelogram(a, b, c, d)20  shows Parallelogram(b, c, d, a)21proof22  unfold Parallelogram at shape23  obtain ⟨horizontal, vertical⟩ := vector.equal_iff.forward with shape24  have other : x(c) - x(b) = x(d) - x(a) ∧25      y(c) - y(b) = y(d) - y(a)26    constructor27    . linear_combination -horizontal28    . linear_combination -vertical29  unfold Parallelogram30  exact vector.equal_iff.backward with other3132theorem parallelogram.opposite_lengths (a b c d : Point)33  requires shape : Parallelogram(a, b, c, d)34  shows Euclidean.distanceSquared(a, b) = Euclidean.distanceSquared(d, c) ∧35    Euclidean.distanceSquared(b, c) = Euclidean.distanceSquared(a, d)36proof37  have other := parallelogram.rotate with *38  unfold Parallelogram at shape39  unfold Parallelogram at other40  constructor41  . unfold Euclidean.distanceSquared42    cc43  . unfold Euclidean.distanceSquared44    cc4546theorem parallelogram.parallel (a b c d : Point)47  requires shape : Parallelogram(a, b, c, d)48  requires first : a ≠ b49  requires second : d ≠ c50  shows ParallelSegments(a, b, d, c)51proof52  unfold Parallelogram at shape53  obtain ⟨horizontal, vertical⟩ := vector.equal_iff.forward with shape54  have cross : directionCross(a, b, d, c) = 055    simp [directionCross]56    ring57  unfold ParallelSegments58  refine ⟨first, second, cross⟩5960-- Diagonals that bisect one another give the same affine parallelogram.61theorem parallelogram.of_bisected_diagonals (a b c d m : Point)62  requires first : Midpoint(m, a, c)63  requires second : Midpoint(m, b, d)64  shows Parallelogram(a, b, c, d)65proof66  rcases first with ⟨firstX, firstY⟩67  rcases second with ⟨secondX, secondY⟩68  have components : x(b) - x(a) = x(c) - x(d) ∧69      y(b) - y(a) = y(c) - y(d)70    constructor71    . linear_combination secondX - firstX72    . linear_combination secondY - firstY73  unfold Parallelogram74  exact vector.equal_iff.backward with components7576theorem parallelogram.bisects (a b c d m : Point)77  requires shape : Parallelogram(a, b, c, d)78  requires first : Midpoint(m, a, c)79  shows Midpoint(m, b, d)80proof81  unfold Parallelogram at shape82  obtain ⟨horizontal, vertical⟩ := vector.equal_iff.forward with shape83  rcases first with ⟨firstX, firstY⟩84  constructor85  . linear_combination firstX + horizontal86  . linear_combination firstY + vertical8788theorem parallelogram.diagonals (a b c d : Point)89  requires shape : Parallelogram(a, b, c, d)90  shows ∃ m, Point(m) ∧ Midpoint(m, a, c) ∧ Midpoint(m, b, d)91proof92  have point := midpoint.point at a, c with *93  have first := midpoint.correct at a, c with *94  have second := parallelogram.bisects with *95  refine ⟨midpoint(a, c), point, first, second⟩9697theorem parallelogram.iff_diagonals (a b c d : Point)98  shows Parallelogram(a, b, c, d) ↔99    ∃ m, Point(m) ∧ Midpoint(m, a, c) ∧ Midpoint(m, b, d)100proof101  constructor102  . intro shape103    exact parallelogram.diagonals with *104  . intro center105    rcases center with ⟨m, point, first, second⟩106    exact parallelogram.of_bisected_diagonals with *107108-- The two pairs of side midpoints are midsegments of triangles sharing AC.109-- Both directed midsegments are half of that same directed diagonal.110theorem varignon (a b c d m n p q : Point)111  requires first : Midpoint(m, a, b)112  requires second : Midpoint(n, b, c)113  requires third : Midpoint(p, c, d)114  requires fourth : Midpoint(q, d, a)115  shows Parallelogram(m, n, p, q)116proof117  have firstReversed := midpoint.symmetric at a, b, m with *118  have thirdReversed := midpoint.symmetric at c, d, p with *119  unfold Parallelogram120  exact midsegment.equal_vectors with *121122-- Nonzero original diagonals give nonzero sides of the midpoint figure.123-- No convexity or simplicity assumption is needed for this affine result.124theorem varignon.parallel (a b c d m n p q : Point)125  requires first : Midpoint(m, a, b)126  requires second : Midpoint(n, b, c)127  requires third : Midpoint(p, c, d)128  requires fourth : Midpoint(q, d, a)129  requires firstDiagonal : a ≠ c130  requires secondDiagonal : b ≠ d131  shows ParallelSegments(m, n, q, p) ∧ ParallelSegments(n, p, m, q)132proof133  have shape := varignon at a, b, c, d, m, n, p, q with *134  have rotated := parallelogram.rotate at m, n, p, q with *135  have firstReversed := midpoint.symmetric at a, b, m with *136  have secondReversed := midpoint.symmetric at b, c, n with *137  have thirdReversed := midpoint.symmetric at c, d, p with *138  have fourthReversed := midpoint.symmetric at d, a, q with *139  have mn := midsegment.distinct at a, c, b, m, n with *140  have qp := midsegment.distinct at a, c, d, q, p with *141  have np := midsegment.distinct at b, d, c, n, p with *142  have mq := midsegment.distinct at b, d, a, m, q with *143  have opposite := parallelogram.parallel at m, n, p, q with *144  have other := parallelogram.parallel at n, p, q, m with *145  refine ⟨opposite, other⟩146147theorem varignon.constructed (a b c d : Point)148  shows Parallelogram(midpoint(a, b), midpoint(b, c),149    midpoint(c, d), midpoint(d, a))150proof151  have mPoint := midpoint.point at a, b with *152  have nPoint := midpoint.point at b, c with *153  have pPoint := midpoint.point at c, d with *154  have qPoint := midpoint.point at d, a with *155  have first := midpoint.correct at a, b with *156  have second := midpoint.correct at b, c with *157  have third := midpoint.correct at c, d with *158  have fourth := midpoint.correct at d, a with *159  exact varignon at a, b, c, d, midpoint(a, b), midpoint(b, c), midpoint(c, d), midpoint(d, a) with *160161end Euclidean162