-- Pythagoras in the Cartesian plane over the Dedekind reals.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

-- Adapted from Grant Passmore's Imandra Top 100 theorem 4:
-- https://github.com/imandra-ai/imandra-100-theorems/blob/main/src/pythagoras.iml

module Grace.Cumulus.Geometry.Pythagoras
import Real.Ring
import Real.Natural

namespace Plane
export open Plane

def distanceSquared (a₁ a₂ b₁ b₂ : Real) : Real :=
  (a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂)

predicate RightAt (a₁ a₂ b₁ b₂ c₁ c₂ : Real) :=
  (a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂) = 0

-- The coordinate statement matches the Imandra theorem over six reals.
-- Orthogonality is sufficient; nondegeneracy is not needed for this identity.
theorem pythagoras_coordinates (a₁ a₂ b₁ b₂ c₁ c₂ : Real)
  requires perpendicular :
    (a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂) = 0
  shows (a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂) =
    (a₁ - c₁) * (a₁ - c₁) + (a₂ - c₂) * (a₂ - c₂) +
    (b₁ - c₁) * (b₁ - c₁) + (b₂ - c₂) * (b₂ - c₂)
proof
  have identity : ((a₁ - b₁) * (a₁ - b₁) + (a₂ - b₂) * (a₂ - b₂)) +
    (2:R) * ((a₁ - c₁) * (b₁ - c₁) + (a₂ - c₂) * (b₂ - c₂)) =
    (a₁ - c₁) * (a₁ - c₁) + (a₂ - c₂) * (a₂ - c₂) +
    (b₁ - c₁) * (b₁ - c₁) + (b₂ - c₂) * (b₂ - c₂)
    ring
  rw perpendicular at identity
  simpa [realMulValue.zero_right, realAddValue.zero_right] using identity

theorem pythagoras (a₁ a₂ b₁ b₂ c₁ c₂ : Real)
  requires right : RightAt(a₁, a₂, b₁, b₂, c₁, c₂)
  shows distanceSquared(a₁, a₂, b₁, b₂) =
    distanceSquared(a₁, a₂, c₁, c₂) + distanceSquared(b₁, b₂, c₁, c₂)
proof
  unfold RightAt at right
  unfold distanceSquared
  have coordinates := pythagoras_coordinates at a₁, a₂, b₁, b₂, c₁, c₂ with *
  ring

end Plane