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^{1}.

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)
```

`refl`

s 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).

^{1}

Sometimes even GitHub copilot can generate some correct proof code. But what I had in mind is some kind of AI assisted heuristically proof searching, instead of blindly NLP like code generation.