Synthetic Euclidean geometry
As promised last time in the intro, we'll look into some concrete examples now. Well, at least as concrete as you can get in synthetic Euclidean geometry – forget about point coordinates and your favorite analytic computations. What follows are simplified excerpts from my friend André's dissertation thesis on formalizing Euclid's elements (by the way, this is how I first got into Lean, and in hindsight it seems like a pretty accessible way).
(Note: We will write everything in Lean4, so feel free to follow along online or locally. And don't forget you can see the current state in the infoview after placing your cursor inside the code!)
import Mathlib.Data.Real.Basic
universe u1 u2 u3
class incidence_geometry :=
(point : Type u1)
(line : Type u2)
(circle : Type u3)
(length : point → point → ℝ)
(B : point → point → point → Prop) -- Betweenness
(length_nonneg : ∀ (a b : point), 0 ≤ length a b)
(length_symm : ∀ (a b : point), length a b = length b a)
(length_eq_zero_iff : ∀ {a b : point}, length a b = 0 ↔ a = b)
(length_sum_of_B : ∀ {a b c : point},
B a b c → length a b + length b c = length a c)
(ne_12_of_B : ∀ {a b c : point}, B a b c → a ≠ b )
(ne_13_of_B : ∀ {a b c : point}, B a b c → a ≠ c )
(ne_23_of_B : ∀ {a b c : point}, B a b c → b ≠ c )
variable [i : incidence_geometry]
open incidence_geometry
This is the minimal setup, let's not worry too much about the details. Basically, we're declaring that we'll work with points, lines and circles, while having a function that measures the length of two points and a predicate that states if three points lie on a single line in the given order. (Notice how we never say what these things are? That's exactly the synthetic approach means.) We also have some axioms about these functions – not quite the ones suggested by Euclid, but they'll do for now.
Let's see out first lemma now!
lemma len_pos_of_neq (ab : a ≠ b) : 0 < length a b := by sorry
The parentheses after the name of the lemma contain named input assumptions, while the statement after the colon is exactly what we are trying to prove (let's call it the goal; you can also see it in the infoview after the ⊢ symbol). (If you like, you can think of lemmas and theorems as functions with the inputs and output separated by a colon.)
After :=, a proof should follow; the by keyword performs a switch to the tactic mode (more on that later) and sorry means that we didn't manage to finish the proof just yet, and we want the compiler to be patient with us. (Actually, sorry introduces another axiom, so we should only use it in unfinished projects, otherwise we risk arriving at a contradiction in our theory.) Let's fix that now:
lemma len_pos_of_neq (ab : a ≠ b) : 0 < length a b :=
Ne.lt_of_le' (length_eq_zero_iff.not.mpr ab) (length_nonneg a b)
Isn't the statement exciting? Well…not really, it's just a simple consequence of the length axioms. The proof might not look that enlightening either, but let that not slow us down.
Modular design
At this point you might be a little confused and/or discouraged. Weren't we supposed to do some actual math? The thing is, most lemmas are just small building blocks whose value becomes clear only in the grand scheme of things (kind of reminiscent of the Linux modular philosophy — each function should do only one thing, but do it well). Put differently:
Lemma 1 (Euclid-Hernández-Espiet) Every proof becomes manageable if you attack it with a long series of lemmas functioning as API – no matter how small or trivial they seem.
Lemma 2 ↑What these guys said.
Lemma 3 Well then…Lemma 1 implies Lemma 2.
Lemma 4 In fact, they are equivalent.
Alright, you get the point. Still, the proofs of such statements might not be simple at all and capturing them succinctly is a craft in its own right. Consider the following example:
theorem length_sum_perm_of_B' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a := by
have ab : a ≠ b := ne_12_of_B Babc
have ab_pos : 0 < length a b := len_pos_of_neq ab
constructor
exact ab_pos
rw [length_symm] at ab_pos
exact ab_pos
Hopefully you can kind of see what's happening here (check out the infoview). Briefly:
- the
havekeyword introduces another hypothesis to our context based on the ones we already had, constructorsplits a conjunction in the goal into two separate goals,exactcloses the current goal by matching it with a hypothesis at our disposal,rwrewrites an equality coming from an earlier lemma at a statement in our context.
Here's an equivalent one-line proof (using |> for pipelining, ▸ for type casting, and ⟨⟩ for creating composite expressions):
theorem length_sum_perm_of_B'' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a :=
⟨ ne_12_of_B Babc |> len_pos_of_neq,
ne_12_of_B Babc |> length_symm a b ▸ len_pos_of_neq⟩
And an even shorter version, using the powerful simplifier simp:
theorem length_sum_perm_of_B''' (Babc : B a b c) :
0 < length a b ∧ 0 < length b a := by
simp [length_symm b, Babc.length_pos]
The first proof gives us the human-readable details and the second constructs the proof terms directly, but the last one is preferred in many contexts for its simplicity, as we can ignore the low-level details. But even this might not be good enough – what if the theorem statement is much longer?
theorem length_sum_perm_of_B (Babc : B a b c) :
0 < length a b ∧ 0 < length b a ∧ 0 < length b c ∧
0 < length c b ∧ 0 < length a c ∧ 0 < length c a ∧
length a b + length b c = length a c ∧
length b a + length b c = length a c ∧
length b a + length c b = length a c ∧
length b a + length b c = length c a ∧
length b a + length c b = length c a ∧
length a b + length c b = length a c ∧
length a b + length b c = length c a ∧
length a b + length c b = length c a
:= by sorry
(In case you're skeptical — this is not a contrived example, but an actual problem that needed solving in the project.)
Even though there's no real mathematical content, proving this using only the methods mentioned so far would be very tedious. (Correction: with simp it's actually quite easy, try it as an exercise.). Instead, we can use powerful tactics – Lean's approach to automation. More on writing them in the next blog post!
If you have any suggestions for improving this blog post, please let me know.