Intro to Interactive Theorem Proving

Proving properties about code is an important task in ensuring that code is correct (see my previous post on model-checking). Unfortunately, it's sometimes impossible to automatically prove certain properties about code.

Can we manually prove properties about code?

Interactive Theorem Proving

Thankfully, people smarter than I have invented tools which allow us to write proofs about code that can be verified by a computer. But how do we write such a proof?

Let's say we have a very simple example of a function:

def times_two (n : Nat) : Nat :=
  n * 2

And we want to know that for every input is less than or equal to its output:

def check_times_two (n: Nat) : n ≤ times_two n := sorry

To start a tactic proof, we use the by keyword:

def check_times_two (n: Nat) : n ≤ times_two n := by

The Lean language server then shows us the following:

Tactic state
1 goal
n : ℕ
⊢ n ≤ times_two n

telling us that we have a variable n (a natural number) and that we still need to show that n is always less than times_two of n. So how would we complete this proof on paper?

First, I would rewrite times_two n as n * 2. Then, I would probably prove the statement inductively. For n = 0, the statement holds, since 0 * 2 = 0. Then, for the inductive case (n + 1 ≤ (n + 1) * 2), we can rewrite our goal as n + 1 ≤ n * 2 + 1 * 2 -> n + 1 ≤ n * 2 + 2 -> n ≤ n * 2 + 1, and since we know that n ≤ n * 2 (the inductive hypothesis), we know that n ≤ n * 2 + 1.

So how do we write that in Lean? Let's start by rewriting times_two n as n * 2:

def check_times_two (n: Nat) : n ≤ times_two n := by
  unfold times_two

so our tactic state is now:

Tactic state
1 goal
n : ℕ
⊢ n ≤ n * 2

Then, let's start our inductive proof:

def check_times_two (n: Nat) : n ≤ times_two n := by
  unfold times_two
  induction n

so our tactic state is now:

Tactic state
2 goals
case zero
⊢ 0 ≤ 0 * 2
case succ
n✝ : ℕ
a✝ : n✝ ≤ n✝ * 2
⊢ n✝ + 1 ≤ (n✝ + 1) * 2

(in other words we need to prove the zero case and the inductive case).

First, let's prove the zero case:

def check_times_two (n: Nat) : n ≤ times_two n := by
  unfold times_two
  induction n
  case zero => exact Nat.zero_le _

this proves that 0 ≤ 0 * 2 because (for natural numbers) 0 is less than or equal to all numbers (in this case 0 * 2).

Then, let's tackle the inductive case:

def check_times_two (n: Nat) : n ≤ times_two n := by
  unfold times_two
  induction n
  case zero => exact Nat.zero_le _
  case succ n ih => -- n + 1 ≤ (n + 1) * 2
    rw [Nat.right_distrib] -- n + 1 ≤ n * 2 + 1 * 2
    rw [Nat.one_mul] -- n + 1 ≤ n * 2 + 2
    rw [@Nat.add_le_add_iff_right] -- n ≤ n * 2 + 1
    exact Nat.le_add_right_of_le ih -- x ≤ y → x ≤ y + 1

This is essentially an exact translation of the paper proof we had into a proof that our computer can understand and verify the correctness of. But Lean is much more powerful than this. If we used automations, we could prove this much more easily:

def check_times_two (n: Nat) : n ≤ times_two n := by
  unfold times_two
  linarith

linarith is a tactic which checks for contradictions in linear relations. Since nothing was contradictory, Lean can accept this as a proof of the property.

Now, let's try our hand at a slightly more complex example:

def fibonacci (n: Nat) : Nat :=
    if n = 0 then
        1
    else if n = 1 then
        1
    else
        (fibonacci (n - 1)) + (fibonacci (n - 2))

def check_fibonacci (n: Nat) : fibonacci n ≤ fibonacci (n + 1) := sorry

Starting our proof gives the following tactic state:

Tactic state
1 goal
n : ℕ
⊢ fibonacci n ≤ fibonacci (n + 1)

Let's prove this inductively:

def check_fibonacci (n: Nat) : fibonacci n ≤ fibonacci (n + 1) := by
  induction n

which gives us this tactic state:

Tactic state
2 goals
case zero
⊢ fibonacci 0 ≤ fibonacci (0 + 1)
case succ
n✝ : ℕ
a✝ : fibonacci n✝ ≤ fibonacci (n✝ + 1)
⊢ fibonacci (n✝ + 1) ≤ fibonacci (n✝ + 1 + 1)

Let's tackle the zero case:

def check_fibonacci (n: Nat) : fibonacci n ≤ fibonacci (n + 1) := by
  induction n
  case zero =>
    simp [fibonacci]

For this part of the proof, we use simp. simp is a very powerful tactic which can automatically leverage hypotheses in your environment in order to simplify your goal. In this case, the original goal was fibonacci 0 ≤ fibonacci (0 + 1), which it rewrites to fibonacci 0 ≤ fibonacci 1. Then, since we allow it to use the definition of fibonacci (the [fibonacci] part), it reduces them to if n = 0 .... Finally, it evaluates both of those definitions, which in this case are both equivalent to 1, and 1 ≤ 1.

Finally, let's finish up with the inductive case:

def check_fibonacci (n: Nat) : fibonacci n ≤ fibonacci (n + 1) := by
  induction n
  case zero =>
    simp [fibonacci]
  case succ n ih =>

so the tactic state is now:

Tactic state
1 goal
n : ℕ
ih : fibonacci n ≤ fibonacci (n + 1)
⊢ fibonacci (n + 1) ≤ fibonacci (n + 1 + 1)

To prove this, let's reduce the fibonacci on the right hand side to fibonacci (n + 1) + fibonacci n, and we automatically know fibonacci (n + 1) ≤ fibonacci (n + 1) + fibonacci n since that's really x ≤ x + y. In Lean:

def check_fibonacci (n: Nat) : fibonacci n ≤ fibonacci (n + 1) := by
  induction n
  case zero =>
    simp [fibonacci]
  case succ n ih =>
    conv => -- let's change what the goal looks like
      rhs -- focus on the right-hand side of the goal
      unfold fibonacci -- expand the definition of fibonacci
    exact Nat.le.intro rfl -- the goal is now true by reflexivity

Interactive Theorem Proving#

Interactive Theorem Proving