Grace/Cumulus/Geometry/Plane.g17

Open in Workbench Download source

Imports

Pythagoras · Real.Squares

Declarations

Source

1-- Points and vectors in the Cartesian plane over the Dedekind reals.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.Plane8import Pythagoras9import Real.Squares1011namespace Euclidean12export open Euclidean1314-- Points are ordered pairs of reals.15predicate Point (p : Set) := ∃ a ∈ ℝ, ∃ b ∈ ℝ, p = (a, b)1617defunique coordinateX (p : Set) (a ∈ ℝ) := ∃ b ∈ ℝ, p = (a, b)18requires point : Point(p)19proof20  unfold Point at point21  exact point2223uniqueness24  intros a aMember first c cMember second25  obtain ⟨b, bMember, firstPair⟩ := first26  obtain ⟨d, dMember, secondPair⟩ := second27  have same : (a, b) = (c, d)28    cc29  have coordinates := orderedPair.injective at a, b, c, d with same30  tauto3132def x (p : Point) : Real := coordinateX(p)3334defunique coordinateY (p : Set) (b ∈ ℝ) := p = (x(p), b)35requires point : Point(p)36proof37  have selected := coordinateX.selected at p with point38  rcases selected with ⟨realX, b, realB, pair⟩39  witness b40  constructor41  . exact realB42  . unfold x43    exact pair4445uniqueness46  intros b bMember first d dMember second47  have same : (x(p), b) = (x(p), d)48    cc49  have coordinates := orderedPair.injective at x(p), b, x(p), d with same50  tauto5152def y (p : Point) : Real := coordinateY(p)5354theorem x.real (p : Point)55  shows Real(x(p))56proof57  obtain ⟨realX, rest⟩ := coordinateX.selected at p with assumption58  unfold x59  exact realX6061theorem y.real (p : Point)62  shows Real(y(p))63proof64  obtain ⟨realY, pair⟩ := coordinateY.selected at p with assumption65  unfold y66  exact realY6768theorem coordinates (p : Point)69  shows p = (x(p), y(p))70proof71  obtain ⟨realY, pair⟩ := coordinateY.selected at p with assumption72  simp [y]7374theorem pair.point (a b : Real)75  shows Point((a, b))76proof77  unfold Point78  have ha : a ∈ ℝ by simp [Real]79  have hb : b ∈ ℝ by simp [Real]80  refine ⟨a, ha, b, hb, rfl⟩8182theorem x.pair (a b : Real)83  shows x((a, b)) = a84proof85  have point := pair.point at a, b with *86  have coords := coordinates with point87  have equal := orderedPair.injective with coords88  simp8990theorem y.pair (a b : Real)91  shows y((a, b)) = b92proof93  have point := pair.point at a, b with *94  have coords := coordinates with point95  have equal := orderedPair.injective with coords96  simp9798theorem point.ext (p q : Point)99  requires horizontal : x(p) = x(q)100  requires vertical : y(p) = y(q)101  shows p = q102proof103  have pCoords := coordinates at p with assumption104  have qCoords := coordinates at q with assumption105  cc106107-- A displacement is another pair of real coordinates.108def vector (a b : Set) : Set := (x(b) - x(a), y(b) - y(a))109def dot (u v : Point) : Real := x(u) * x(v) + y(u) * y(v)110def normSquared (u : Point) : Real := dot(u, u)111def distanceSquared (a b : Point) : Real := normSquared(vector(a, b))112113theorem vector.point (a b : Point)114  shows Point(vector(a, b))115proof116  have ax := x.real at a with assumption117  have ay := y.real at a with assumption118  have bx := x.real at b with assumption119  have byReal := y.real at b with assumption120  have horizontal := realSubValue.real with bx, ax121  have vertical := realSubValue.real with byReal, ay122  unfold vector123  exact pair.point with horizontal, vertical124125theorem vector.x (a b : Point)126  shows x(vector(a, b)) = x(b) - x(a)127proof128  have ax := x.real at a with assumption129  have ay := y.real at a with assumption130  have bx := x.real at b with assumption131  have byReal := y.real at b with assumption132  have horizontal := realSubValue.real with bx, ax133  have vertical := realSubValue.real with byReal, ay134  unfold vector135  exact x.pair with horizontal, vertical136137theorem vector.y (a b : Point)138  shows y(vector(a, b)) = y(b) - y(a)139proof140  have ax := x.real at a with assumption141  have ay := y.real at a with assumption142  have bx := x.real at b with assumption143  have byReal := y.real at b with assumption144  have horizontal := realSubValue.real with bx, ax145  have vertical := realSubValue.real with byReal, ay146  unfold vector147  exact y.pair with horizontal, vertical148149-- Dot products of two directed segments in their endpoint coordinates.150theorem vector.dot_coordinates (a b c d : Point)151  shows dot(vector(a, b), vector(c, d)) =152    (x(b) - x(a)) * (x(d) - x(c)) + (y(b) - y(a)) * (y(d) - y(c))153proof154  have firstX := vector.x at a, b with *155  have firstY := vector.y at a, b with *156  have secondX := vector.x at c, d with *157  have secondY := vector.y at c, d with *158  unfold dot159  cc160161-- Equality of displacements can be used without exposing ordered-pair encodings.162theorem vector.equal_iff (a b c d : Set)163  shows vector(a, b) = vector(c, d) ↔164    x(b) - x(a) = x(d) - x(c) ∧ y(b) - y(a) = y(d) - y(c)165proof166  constructor167  . intro equal168    unfold vector at equal169    exact orderedPair.injective with equal170  . intro components171    rcases components with ⟨horizontal, vertical⟩172    unfold vector173    cc174175theorem dot.real (u v : Point)176  shows Real(dot(u, v))177proof178  have ux := x.real at u with assumption179  have uy := y.real at u with assumption180  have vx := x.real at v with assumption181  have vy := y.real at v with assumption182  have horizontal := realMulValue.real with ux, vx183  have vertical := realMulValue.real with uy, vy184  unfold dot185  exact realAddValue.real with horizontal, vertical186187theorem normSquared.real (u : Point)188  shows Real(normSquared(u))189proof190  unfold normSquared191  exact dot.real with *192193theorem distanceSquared.real (a b : Point)194  shows Real(distanceSquared(a, b))195proof196  have displacement := vector.point at a, b with *197  unfold distanceSquared198  exact normSquared.real with displacement199200theorem distanceSquared.coordinates (a b : Point)201  shows distanceSquared(a, b) =202    (x(b) - x(a)) * (x(b) - x(a)) + (y(b) - y(a)) * (y(b) - y(a))203proof204  unfold distanceSquared205  unfold normSquared206  unfold dot207  have coordinateRule1 := vector.x at a, b with *208  rw coordinateRule1209  have coordinateRule2 := vector.y at a, b with *210  rw coordinateRule2211  rfl212213theorem normSquared.nonnegative (u : Point)214  shows 0 ≤ normSquared(u)215proof216  have ux := x.real with assumption217  have uy := y.real with assumption218  unfold normSquared219  unfold dot220  exact realAddValue.sum_squares_nonnegative with ux, uy221222theorem distanceSquared.symmetric (a b : Point)223  shows distanceSquared(a, b) = distanceSquared(b, a)224proof225  have coordinateRule3 := distanceSquared.coordinates at a, b with *226  rw coordinateRule3227  have coordinateRule4 := distanceSquared.coordinates at b, a with *228  rw coordinateRule4229  ring230231theorem distanceSquared.nonnegative (a b : Point)232  shows 0 ≤ distanceSquared(a, b)233proof234  have displacement := vector.point at a, b with *235  unfold distanceSquared236  exact normSquared.nonnegative with displacement237238theorem distanceSquared.zero_iff (a b : Point)239  shows distanceSquared(a, b) = 0 ↔ a = b240proof241  have ax := x.real at a with assumption242  have ay := y.real at a with assumption243  have bx := x.real at b with assumption244  have byReal := y.real at b with assumption245  have dx := realSubValue.real with bx, ax246  have dy := realSubValue.real with byReal, ay247  have xx := realMulValue.square_nonnegative with dx248  have yy := realMulValue.square_nonnegative with dy249  have formula := distanceSquared.coordinates at a, b with *250  constructor251  . intro zeroDistance252    rw formula at zeroDistance253    have squareX := realAddValue.nonnegative_eq_zero with xx, yy, zeroDistance254    have reversed : (y(b) - y(a)) * (y(b) - y(a)) + (x(b) - x(a)) * (x(b) - x(a)) = 0 by ring255    have squareY := realAddValue.nonnegative_eq_zero with yy, xx, reversed256    have zeroX := realMulValue.square_eq_zero_iff.forward with squareX257    have zeroY := realMulValue.square_eq_zero_iff.forward with squareY258    have equalX : x(a) = x(b) by linear_combination -zeroX259    have equalY : y(a) = y(b) by linear_combination -zeroY260    exact point.ext with *261  . intro equal262    rw equal263    have coordinateRule5 := distanceSquared.coordinates at b, b with *264    rw coordinateRule5265    ring266267theorem distanceSquared.positive (a b : Point)268  requires distinct : a ≠ b269  shows 0 < distanceSquared(a, b)270proof271  have nonnegative := distanceSquared.nonnegative at a, b with *272  have nonzero : distanceSquared(a, b) ≠ 0273    intro zeroDistance274    have equal := distanceSquared.zero_iff.forward with *275    exact distinct with equal276  exact Real.positive_of_nonnegative_of_ne_zero with nonnegative, nonzero277278-- The middle point is the vertex of the angle.279def angleDot (a b c : Point) : Real := dot(vector(b, a), vector(b, c))280281predicate RightAngle (a b c : Set) := angleDot(a, b, c) = 0282283theorem angleDot.real (a b c : Point)284  shows Real(angleDot(a, b, c))285proof286  have first := vector.point at b, a with *287  have second := vector.point at b, c with *288  unfold angleDot289  exact dot.real with first, second290291theorem angleDot.coordinates (a b c : Point)292  shows angleDot(a, b, c) =293    (x(a) - x(b)) * (x(c) - x(b)) + (y(a) - y(b)) * (y(c) - y(b))294proof295  unfold angleDot296  unfold dot297  have coordinateRule6 := vector.x at b, a with *298  rw coordinateRule6299  have coordinateRule7 := vector.x at b, c with *300  rw coordinateRule7301  have coordinateRule8 := vector.y at b, a with *302  rw coordinateRule8303  have coordinateRule9 := vector.y at b, c with *304  rw coordinateRule9305  rfl306307-- The cosine-law identity, stated without division or square roots.308theorem cosine_identity (a b c : Point)309  shows distanceSquared(a, c) + angleDot(a, b, c) + angleDot(a, b, c) =310    distanceSquared(a, b) + distanceSquared(b, c)311proof312  have coordinateRule10 := distanceSquared.coordinates at a, c with *313  rw coordinateRule10314  have coordinateRule11 := distanceSquared.coordinates at a, b with *315  rw coordinateRule11316  have coordinateRule12 := distanceSquared.coordinates at b, c with *317  rw coordinateRule12318  have coordinateRule13 := angleDot.coordinates at a, b, c with *319  rw coordinateRule13320  ring321322theorem pythagoras (a b c : Point)323  requires right : RightAngle(a, b, c)324  shows distanceSquared(a, c) = distanceSquared(a, b) + distanceSquared(b, c)325proof326  have identity := cosine_identity at a, b, c with *327  unfold RightAngle at right328  linear_combination identity - (2:R) * right329330end Euclidean331