Getting started with Isabelle: baby examples, cool proof methods

04 May 2022

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

trying and failing to prove 3-2=1

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:

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 ‹q2 = 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.