Machine Logic

Introductory example: Fibonacci numbers

13 Oct 2021

Let’s see what mathematics looks like in Isabelle/HOL. This post is not a self-contained tutorial; it simply aims to show a simple recursive definition and a couple of proofs by induction. Some good (and bad) points about machine proof should become obvious. There are links to further reading at the end.

So here is the definition of the Fibonacci function:

fun fib :: "nat ⇒ nat" where
    "fib 0 = 0"
  | "fib (Suc 0) = 1"
  | "fib (Suc (Suc n)) = fib n + fib (Suc n)"

This looks familiar enough except for the successor function, Suc, which is part of the definition of the natural numbers. Ugly perhaps but easy enough to get used to. The successor of $n$ is simply $n+1$.

Facts about fib are typically proved by induction, and most of us know to match the induction principle to the form of the recursion: with two base cases (for 0 and 1) and an induction step that has induction hypotheses for each of the two recursive calls. We begin with a trivial example:

lemma fib_positive: "fib (Suc n) > 0"
  by (induction n rule: fib.induct) auto

The proof of fib_positive is by induction (a version tailored to fib as outlined above) followed by general automation. It’s trivial and nobody should want to see more of the proof. But the next example is a distinctly nontrivial identity:

lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
  by (induction n rule: fib.induct) (auto simp: distrib_left)

The machine proof resembles the previous one except for a reference (distrib_left) to a distributive law, but the logical reasoning generated by auto is completely different. The calculation is complicated enough to be written out in any text, yet Isabelle’s built-in automation doesn’t need any hints: it proves a statement that is genuinely nonobvious. This will not always be the case!

The next example is different again, a claim that is plausible without an obvious proof. Here we need to flesh out the proof, with an explicit reference to the third case (the induction step):

lemma coprime_fib_Suc: "coprime (fib n) (fib (Suc n))"
proof (induction n rule: fib.induct)
  case (3 n)
  then show ?case
    by (metis coprime_iff_gcd_eq_1 fib.simps(3) gcd.commute gcd_add1)
qed auto

This undoubtedly cryptic code already tells us what formal proofs can look like. We can see that it’s an induction and that the third case has been singled out for special treatment. The list of identifiers in the penultimate line are the names of known facts used to prove the induction step. The base cases are proved automatically (qed auto). Even the induction step was proved automatically. Isabelle has a subsystem, sledgehammer, that can analyse a statement to be proved and actually generate Isabelle proof text to prove it. The penultimate line, which contains the heart of the proof, was given to us for free. Sledgehammer can be called using a single mouse click.

To run this example yourself, you need to install Isabelle (it’s easy!) and perhaps read some introductory documentation. The file containing this example can be downloaded.