Friday, June 28, 2024

01 - First Proof

Task

Let's start with a very simple task. Imagine we're given the following fact.

a=4

Our task is to prove that

a>1

Here, a, 1 and 4 are all natural numbers. 


Maths

It seems trivially obvious that if a=4 then a>1. 

The challenge we'll often face writing proofs in Lean is getting inside intuitively easy tasks to think about them in a more structured way.

How can we justify a>1, given a=4? The question we're asking is whether 4>1. To answer this, we appeal to the fact that the natural numbers are ordered by the “greater than” > relation. 

Let's now try to write down these thoughts in a structured way.

a=4given fact◻>1by the ordering of natural numbers

That wasn't too difficult.


Code

Let's now look at a Lean program that proves a>1, given a=4, just as we did above.


-- 01 - First Proof

import Mathlib.Tactic

example {a : ℕ} (h1: a = 4) : a > 1 := by
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

This is our first look at Lean code, so we'll only make some initial observations, and allow ourselves to become familiar with Lean code gradually over the coming chapters.

The proof starts on the line beginning with example. This rather long line states the theorem we want to prove.

  • The {a : ℕ} tells Lean the variable a is a natural number. 
  • Next we have (h1 : a = 4) which is the given fact. It's given a label h1 so we can refer to it later by name.
  • After that we have the statement we want to prove, a > 1. 
  • Finally there is a := by which signals to Lean that we're about to prove that statement. 
The last three lines of code, from calc to norm_num, are the proof of the theorem. For now, let's just look at the last two.
  • We state that a = 4, and justify it by referring to the given fact, previously labelled h1.
  • We complete the proof by saying this is > 1, and justify it by the ordering of natural numbers. We'll talk more about norm_num below.


Tactics

That last line of the Lean proof justified 4>1 by the ordering of natural numbers. How did this happen?

The natural numbers are described by the Peano axioms. On top of these axioms, we can define addition, then the “greater than” > relation. 

We did not go that deep in our maths proof!

For a large body of fundamental results, there's no need to prove them every time we use them. Maths would be very tedious if we had to prove something like 4>1, or 8>0, every time we used it!

The same idea applies to Lean proofs. 

Many of those fundamental results and common methods have been written in Lean and packaged up as tactics, ready for us to use. So norm_num is a tactic that includes knowledge about the order created by the “greater than” relation on natural numbers. It also includes knowledge about how to do arithmetic like 3+4, which we'll see in the next chapter.


Exercise

The Lean program above proves a>1 given a=4. Change it to prove a<10 given a=4.

The norm_num tactic understands “less than”, as well as “greater than”.


at