Grace/Cumulus/Geometry/Pythagoras.g17

Open in Workbench Download source

Imports

Real.Ring · Real.Natural

Declarations

Source

1-- Pythagoras 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 Passmore67-- Adapted from Grant Passmore's Imandra Top 100 theorem 4:8-- https://github.com/imandra-ai/imandra-100-theorems/blob/main/src/pythagoras.iml910module Grace.Cumulus.Geometry.Pythagoras11import Real.Ring12import Real.Natural1314namespace Plane15export open Plane1617def distanceSquared (a₁ a₂ b₁ b₂ : Real) : Real :=18  (a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂)1920predicate RightAt (a₁ a₂ b₁ b₂ c₁ c₂ : Real) :=21  (a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂) = 02223-- The coordinate statement matches the Imandra theorem over six reals.24-- Orthogonality is sufficient; nondegeneracy is not needed for this identity.25theorem pythagoras_coordinates (a₁ a₂ b₁ b₂ c₁ c₂ : Real)26  requires perpendicular :27    (a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂) = 028  shows (a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂) =29    (a₁ - c₁) * (a₁ - c₁) + (a₂ - c₂) * (a₂ - c₂) +30    (b₁ - c₁) * (b₁ - c₁) + (b₂ - c₂) * (b₂ - c₂)31proof32  have identity : ((a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂)) +33    (2:R) * ((a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂)) =34    (a₁ - c₁) * (a₁ - c₁) + (a₂ - c₂) * (a₂ - c₂) +35    (b₁ - c₁) * (b₁ - c₁) + (b₂ - c₂) * (b₂ - c₂)36    ring37  rw perpendicular at identity38  simpa [realMulValue.zero_right, realAddValue.zero_right] using identity3940theorem pythagoras (a₁ a₂ b₁ b₂ c₁ c₂ : Real)41  requires right : RightAt(a₁, a₂, b₁, b₂, c₁, c₂)42  shows distanceSquared(a₁, a₂, b₁, b₂) =43    distanceSquared(a₁, a₂, c₁, c₂) + distanceSquared(b₁, b₂, c₁, c₂)44proof45  unfold RightAt at right46  unfold distanceSquared47  have coordinates := pythagoras_coordinates at a₁, a₂, b₁, b₂, c₁, c₂ with *48  ring4950end Plane51