# Lean series 02: Demo

### 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:

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 `simp`licity, 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.