## Getting started with Isabelle: baby examples, cool proof methods

[examples

Isabelle

newbies

sledgehammer

]
For absolute beginners, proof assistants are daunting. Everything you do seems to go wrong. So let’s have some super simple examples that show how to get started while highlighting some pitfalls.

### An algebraic identity

First, a note of caution: Isabelle/HOL is great at inferring types in expressions, but the simplest examples might well be ambiguous, leading to frustration.
For example, it should be trivial to prove $3-2=1$ using `auto`

, but it fails. Hovering with your mouse near the blue dot in the left margin, or checking the Output panel, you might see a hint about a missing type constraint:

Isabelle sees that the problem involves numbers, but it can’t infer a precise type and therefore it’s not clear whether substraction is even meaningful. So it’s wise always to include an explicit type constraint in problems involving numeric types. You can also use CTRL-hover (CMD-hover on Macs) to inspect the type of any variable in Isabelle/jEdit. (More on this next week!)

In the following trivial algebraic identity (due to Kevin Buzzard), we specify the type of `x`

using fixes.
It’s trivial to prove, using a single call to the simplifier.

lemma fixes x::real shows "(x+y)*(x+2*y)*(x+3*y) = x^3 + 6*x^2*y + 11*x*y^2 + 6*y^3" by (simp add: algebra_simps eval_nat_numeral)

The arguments given to the simplifier are critical:

`algebra_simps`

is a bundle of simplification rules (*simprules*), containing the obvious algebraic laws: associativity and commutativity to arrange terms into a canonical order, and distributive laws to multiply out all the terms.`eval_nat_numeral`

is a single simprule that expands numerals such as 3 and 47055833459 from their internal symbolic binary notation into unary notation as a series of`Suc`

applications to`0`

. (Sadly, the second example will not terminate.)

The `Suc`

form is necessary to trigger the simplification $a^{n+1}=a\times a^n$; this identity is called `power_Suc`

, but it is a *default simprule*, meaning we don’t need to mention it.

With both rules included, `simp`

solves the problem. Using only one of them makes the expressions blow up. A skill you need to develop is figuring out what to do when faced with a sea of symbols: did you use too many simplification rules, or too few?
A good strategy is to simplify with the fewest possible rules and gradually add more.
Gigantic formulas are impossible to grasp, but close inspection sometimes reveals subexpressions that could be eliminated through the use of another simprule.

### A numerical inequality

The next example, also due to Kevin, is to show that $\sqrt 2 + \sqrt 3 < \sqrt 10$. One obvious approach is to get rid of some of the radicals by squaring both sides. So we state the corresponding formula as a lemma using have and open a proof using the same simplification rules as in the previous example. It leaves us with the task of showing $2(\sqrt 2\sqrt 3) < 5$. Repeating the previous idea, we use have to state that formula with both sides squared, then apply those simplification rules again. (It works because $24<25$.) Curiously, the show commands, although both inferring $x<y$ from $x^2<y^2$, require different formal justifications, both found by sledgehammer. The rest of the proof below was typed in manually.

lemma "sqrt 2 + sqrt 3 < sqrt 10" proof - have "(sqrt 2 + sqrt 3)^2 < (sqrt 10)^2" proof (simp add: algebra_simps eval_nat_numeral) have "(2 * (sqrt 2 * sqrt 3))^2 < 5 ^ 2" by (simp add: algebra_simps eval_nat_numeral) then show "2 * (sqrt 2 * sqrt 3) < 5" by (smt (verit, best) power_mono) qed then show ?thesis by (simp add: real_less_rsqrt) qed

But there’s a much simpler way to prove the theorem above: by numerical evaluation using Johannes Hölzl’s amazing approximation tactic.

lemma "sqrt 2 + sqrt 3 < sqrt 10" by (approximation 10)

Is it cheating? No. Working out the inequality by hand calculation is absolutely a proof. The algebraic proof above is less work for somebody who doesn’t trust calculators. However, the ability to decide such questions by calculation (interval arithmetic, to be precise) is a huge labour-saver.

lemma "x ∈ {0.999..1.001} ⟹ ¦pi - 4 * arctan x¦ < 0.0021" by (approximation 20)

To use this wonder-working tool, your theory file needs to import the library theory `HOL-Decision_Procs.Approximation`

.

While we are talking about automatic tactics, Chaieb’s `sos`

deserves a mention. It uses sum of squares methods to decide real polynomial inequalities.

lemma fixes a::real shows "(a*b + b * c + c*a)^3 ≤ (a^2 + a * b + b^2) * (b^2 + b * c + c^2) * (c^2 + c*a + a^2)" by sos

A decision procedure, it always settles the question, but with too many variables you won’t live long enough to see the result. To use it, your theory needs to import `HOL-Library.Sum_of_Squares`

.

### The square root of two is irrational

I contrived this example to demonstrate sledgehammer and especially how beautifully it interacts with the development of a structured proof. I knew the mathematical proof already, so the point was to formalise it using sledgehammer alone, without reference to other formal proofs. It also illustrates some tricky points requiring numeric types.

The irrationality of $\sqrt2$ is stated in terms of $\mathbb Q$, which in Isabelle/HOL is a weird polymorphic set: it is the range of the function `of_rat`

, which embeds type `rat`

into larger types such as `real`

and `complex`

.
So the proof begins by assuming that
sqrt 2 ∈ ℚ,
thus obtaining `q`

of type `rat`

such that
`sqrt`

2 = of_rat q and after that,
q^2 = 2.
Sledgehammer was unable to derive this in a single step from the assumption, and this step-by-step approach (thinking of a simple intermediate property) is the simplest way to give sledgehammer a hint.

We next obtain `m`

and `n`

such that

"coprime m n" "q = of_int m / of_int n"

Two tricks here are knowing that `coprime`

is available, and using the embedding `of_int`

to ensure that `m`

and `n`

are integers (far better than simply declaring `m`

and `n`

to have type `int`

, when Isabelle may insert embeddings in surprising places).
Next we state the goal

```
"of_int m ^ 2 / of_int n ^ 2 = (2::rat)"
```

Now a *super-important point*: the embeddings `of_nat`

, `of_int`

, `of_real`

specify their domain type, but their range type **can be anything** belonging to a suitably rich type class. Since 2 can also have many types, the `2::rat`

is necessary to ensure that we are talking about the rationals.

The proof continues with the expected argument of showing that 2 is a divisor of both `m`

and `n`

, contradicting the fact that they are coprime.

lemma "sqrt 2 ∉ ℚ" proof assume "sqrt 2 ∈ ℚ" then obtain q::rat where "sqrt 2 = of_rat q" using Rats_cases by blast then have "q^2 = 2" by (metis abs_numeral of_rat_eq_iff of_rat_numeral_eq of_rat_power power2_eq_square real_sqrt_mult_self) then obtain m n where "coprime m n" "q = of_int m / of_int n" by (metis Fract_of_int_quotient Rat_cases) then have "of_int m ^ 2 / of_int n ^ 2 = (2::rat)" by (metis ‹q⇧^{2}= 2› power_divide) then have 2: "of_int m ^ 2 = (2::rat) * of_int n ^ 2" by (metis division_ring_divide_zero double_eq_0_iff mult_2_right mult_zero_right nonzero_divide_eq_eq) then have "2 dvd m" by (metis (mono_tags, lifting) even_mult_iff even_numeral of_int_eq_iff of_int_mult of_int_numeral power2_eq_square) then obtain r where "m = 2*r" by blast then have "2 dvd n" by (smt (verit) "2" ‹even m› dvdE even_mult_iff mult.left_commute mult_cancel_left of_int_1 of_int_add of_int_eq_iff of_int_mult one_add_one power2_eq_square) then show False using ‹coprime m n› ‹m = 2 * r› by simp qed

**Every step** in this proof was obtained by sledgehammer. The main skill involves thinking up the right intermediate goals when sledgehammer fails, and typing them in.
Yes, formal proof really is just another sort of coding.

You can download the theory file `Baby.thy`

.
You might want to generalise the example to show that the square root of every prime is irrational. The `prime`

predicate and supporting theory can be imported from
`HOL-Computational_Algebra.Primes`

.

Give it a try. Isabelle is easy to install and comes with plenty of documentation.