Elementary Geometry In Agda

I'm playing with Agda recently, and since some of my friends' teacher are working on human understandable AI assisted theory proving. And IMO type theory base theorem prover is a better way than algebra-based proof methods (eg. Wenjun Wu's method) to generate human understandable proofs. And I do hope we can have an AI version of Agsy¹.

I'll start with Στοιχεῖα, the source of geometry.

I'll show how to prove Proposition 1, and introduce how to represent the definitions and postulates here.

To(We can) construct an equilateral triangle on a given finite straight-line. —— Στοιχεῖα

So we need to define what is a finite straight-line, and what is an equilateral triangle.

And the proof process use circles, which also needs to be defined.

Definitions

Point

So let's start with the most basic thing: a point.

record Point : Set where
    constructor newPoint
    field
        pointId : ℕ

We give each point an id here, to disguise different points.

And we can represent the proportion two points are identical by the following type:

data PointEq (x : Point) : Point → Set where
  refl : PointEq x x

Line Segment

Now we can define a line segment:

record LineSegment : Set where
    constructor lineSeg
    field
        from : Point
        to : Point
        lineLength : ℚ
        nonNegative : NonNegative lineLength

Note we require the length of the line segment's length to be a non-negative rational number.

We use rational number here, because we often needs to take point of n-section on a line segment, since rational number is almost closed under division, it's convenient to represent line length in this way.

Though not used in this post, we can define a function to cast zero-length line segment back and forth to a single point.

And we can "reverse" a line:

line-sym : (LineSegment) → LineSegment
line-sym ls = lineSeg (LineSegment.to ls) (LineSegment.from ls) (LineSegment.lineLength ls) (LineSegment.nonNegative ls)

Circle

Similarly, we can define a circle:

record Circle : Set where
    constructor circle
    field
        center : Point
        radius : ℚ
        nonNegative : NonNegative radius

Triangle

I adopt the edge based definition of triangle here, which is more easy to use.

record Triangle : Set where
  constructor from-edges
  field
    edge0 : LineSegment
    edge1 : LineSegment
    edge2 : LineSegment
    .edgesConnected : 
        (PointEq (LineSegment.to edge0) (LineSegment.from edge1)) ×
        (PointEq (LineSegment.to edge1) (LineSegment.from edge2)) ×
        (PointEq (LineSegment.to edge2) (LineSegment.from edge0))

And we can define equilateral triangle like this:

is-equilateral : (t : Triangle) → Set
is-equilateral (from-edges edge0 edge1 edge2 _) = 
    (LineSegment.lineLength edge0 ℚ.≃ LineSegment.lineLength edge1) ×
     (LineSegment.lineLength edge0 ℚ.≃ LineSegment.lineLength edge2)

Postulates

There are two postulates in Στοιχεῖα hidden in these definitions:

• We can draw a straight-line from any point to any point.
• We can draw a circle with any center and radius.

These two are all we need this time.

However, there's several missing postulates in Στοιχεῖα, which made the proof in it not very rigorous, we'll see later.

Common Notions

These are basically equivalent to the propositions in Agda's stdlib, especially Data.Rational.Properties.

The proof

The proposition

We can write it as:

equilateral-triangle : (line : LineSegment) → .{ 0ℚ < LineSegment.lineLength line }
    → Σ (Triangle) (λ t → is-equilateral t)

Which can be read as:

Given a line segment line, which length is > 0, there exist a triangle which is equilateral.

And it's equivalent to the origin proposition.

According to the book, we can draw two circles and use the intersection point as the third vertex of the triangle, however, Εὐκλείδης made a mistake here, since there's no way to proof intersection point exists.

Let's just posulate it:

circle-intersection : (c1 c2 : Circle) 
    → (connectMidLine : LineSegment)
    → (PointEq (Circle.center c1) (LineSegment.from connectMidLine)) 
    → (PointEq (Circle.center c2) (LineSegment.to connectMidLine))
    → .{
        (LineSegment.lineLength connectMidLine) < (Circle.radius c1) + (Circle.radius c2)
    }
    → .{
        ∣ (Circle.radius c1) - (Circle.radius c2) ∣ < (LineSegment.lineLength connectMidLine)
    }
    → (Σ (Point × Point) (λ (p1 , p2) →
        (LineSegment × LineSegment) × (LineSegment × LineSegment)
    ))

circle-intersection c1 c2 connectMidLine c1Mid c2Mid = 
    let p0 = newPoint 0
        p1 = newPoint 1
    in (p0 , p1) , (
        ((lineSeg (Circle.center c1) p0 (Circle.radius c1) (Circle.nonNegative c1)) , 
         (lineSeg (Circle.center c2) p0 (Circle.radius c2)) (Circle.nonNegative c2)), 
        ((lineSeg (Circle.center c1) p1 (Circle.radius c1) (Circle.nonNegative c1)) , 
         (lineSeg (Circle.center c2) p1 (Circle.radius c2)) (Circle.nonNegative c2))
    )

Note we have to provide evidence here that the length of the connecting-circle-center line is less than the sum of the radius of the two circles, and abs(difference of the radius of the two circles) is less than the length of the connecting line, so there can be two intersection points exists.

So basically the proof can be written as:

equilateral-triangle line {p} = 
    let c1 = circle (LineSegment.from line) (LineSegment.lineLength line) (LineSegment.nonNegative line)
        c2 = circle (LineSegment.to line) (LineSegment.lineLength line) (LineSegment.nonNegative line)
        ((p0 , p1) , ((l0 , l1), _)) = circle-intersection c1 c2 line PointEq.refl PointEq.refl {?} {?}
    in
        (from-edges line l1 (line-sym l0) (refl , refl , refl)) , (refl , refl)

refls here are just proofs for things that are obviously equal.

For the ? parts, we need to fill in evidence for lineLength line + lineLength line > lineLength line and ∣ lineLength line - lineLength line ∣ < lineLength line, which is surprisingly hard:

For lineLength line + lineLength line > lineLength line, which is actually means for a positive numbers, sum of two such numbers is greater than itself, we need to use the monoˡ property of + on rational number, which is equivalent with Common Notion 5 of the book.

x<x+x : (x : ℚ) → 0ℚ < x → (x < x + x)
x<x+x x p = (begin-strict
        x       ≡⟨ (sym ∘ +-identityˡ) x ⟩
        0ℚ + x  <⟨ +-monoˡ-< x p ⟩
        x + x
    ∎)
    where open ℚ.≤-Reasoning

For ∣ lineLength line - lineLength line ∣ < lineLength line, first we prove ∣x - x∣ ≡ 0

x-x≡0 : (x : ℚ) → (x - x ≡ 0ℚ)
x-x≡0 x = (begin
    x - x   ≡⟨ +-comm (x) (- x) ⟩
    - x + x ≡⟨ +-inverseˡ x ⟩
    0ℚ      ∎)
    where open ≡-Reasoning

p≡0⇒∣p∣≡0 : {p : ℚ} → p ≡ 0ℚ → ∣ p ∣ ≡ 0ℚ
p≡0⇒∣p∣≡0 eqz = trans (ℚ.0≤p⇒∣p∣≡p (≤-reflexive (sym eqz))) eqz

And then:

∣x-x∣<x : (x : ℚ) → 0ℚ < x → ∣ x - x ∣ < x
∣x-x∣<x x p = (begin-strict
    ∣ x - x ∣   ≡⟨ p≡0⇒∣p∣≡0 (x-x≡0 x) ⟩
    0ℚ          <⟨ p ⟩
    x           ∎)
    where open ℚ.≤-Reasoning

Then we can fill the ?s, and get the final proof:

equilateral-triangle : (line : LineSegment) → .{ 0ℚ < LineSegment.lineLength line }
    → Σ (Triangle) (λ t → is-equilateral t)
equilateral-triangle line {p} = 
    let c1 = circle (LineSegment.from line) (LineSegment.lineLength line) (LineSegment.nonNegative line)
        c2 = circle (LineSegment.to line) (LineSegment.lineLength line) (LineSegment.nonNegative line)
        ((p0 , p1) , ((l0 , l1), _)) = circle-intersection c1 c2 line PointEq.refl PointEq.refl {x<x+x (LineSegment.lineLength line) p} {∣x-x∣<x (LineSegment.lineLength line) p}
    in
        (from-edges line l1 (line-sym l0) (refl , refl , refl)) , (refl , refl)

Now you see the basic idea of how to use the agda to prove propositions in elementary geometry.

What's next?

There remains a lot of work to do. For example, how to define angles (I may use 1ℚ as right angle because postulates in the book are based on right angles.), and how to present the relations of lines and points (maybe intersect-on-point and parallel, etc).