PythagorasStarter

Using the first Imandra Top 100 port through the public geometry API

Open in Workbench View on GitHub

1-- Using the first Imandra Top 100 port through the public geometry API.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module PythagorasStarter7import Grace.Cumulus.Geometry89theorem right_triangle (a₁ a₂ b₁ b₂ c₁ c₂ : Real)10  requires right : Plane.RightAt(a₁, a₂, b₁, b₂, c₁, c₂)11  shows Plane.distanceSquared(a₁, a₂, b₁, b₂) =12    Plane.distanceSquared(a₁, a₂, c₁, c₂) + Plane.distanceSquared(b₁, b₂, c₁, c₂)13proof14  exact Plane.pythagoras at a₁, a₂, b₁, b₂, c₁, c₂ with15    assumption, assumption, assumption, assumption, assumption, assumption, right1617theorem coordinate_axes (x y : Real)18  shows Plane.distanceSquared(x, 0, 0, y) = x * x + y * y19proof20  unfold Plane.distanceSquared21  ring22