Dealing with descriptions in Isabelle/HOL: least, greatest, whatever

08 Jun 2022

[ examples  Isabelle  newbies  descriptions  sledgehammer  David Hilbert  ]

A description is a term that designates “the least”, “the greatest” or simply “any” x such that Φ(x): it describes the desired value (or simply any suitable value) in the language of its properties. The built-in facts governing Min, Max, etc. are straightforward, but getting what you want from them is often frustrating. Let’s take a look at a few contrived, but (I hope) illustrative examples, leaving all the proofs to sledgehammer.

The range of description operators

A great variety of functions are available. Here are the main ones:

Unsurprisingly, some of these are defined in terms of others, with Eps as the base primitive. Type classes play a major role. For example, a type in class wellorder is guaranteed to have suitable Least elements for any non-False predicate.

A silly theorem statement

The following nonsensical “theorem” will be the basis for a couple of simple examples. We are given a set 𝒮 of nonempty open balls (in a metric space) and a set L of lists of natural numbers. Our task is to prove something or other.

lemma
  fixes 𝒮 :: "'a::metric_space set set" and L :: "nat list set"
  assumes "𝒮 ⊆ {ball x r | x r. r>0}" and "L ≠ {}"
  shows "P 𝒮 L"

Example 1: defining the radius and centre of a ball

Every element of 𝒮 has the form ball x r, where x is its centre and r is its necessarily positive radius:

  have "⋀B. B ∈ 𝒮 ⟹ ∃x. ∃r>0. B = ball x r"
    using assms by blast

Whenever you have such a forall-exists fact, you can transform it into exists-forall, obtaining a function. Note that the transformation from $\forall x.\, \exists y.\, \Phi(x,y)$ into $\exists f.\, \forall x.\, \Phi(x,\,f(x))$ can require AC, in general. You could define $f$ explicitly using Hilbert’s epsilon, but there’s an easier way. All you have to do is write out the properties you want, as long as they are clearly based on the previous forall-exists result. For the proof, simply call metis. Here, we get two functions at the same time!

  then obtain centre rad where rad: "⋀B. B ∈ 𝒮 ⟹ rad B > 0"
                         and centre: "⋀B. B ∈ 𝒮 ⟹ B = ball (centre B) (rad B)"
    by metis

If you try this and the metis call hangs, it’s likely that your forall-exists formula is too complicated (or just wrong). Simplify it by making definitions.

Example 2: What is the minimum radius?

The infimum of all the radii of the balls in 𝒮 is easily defined. It exists because there’s a lower bound (zero). The use of the image operator is typical: this is the simplest way to denote the set of all radii of elements of 𝒮.

  define infrad where "infrad ≡ Inf (rad ` 𝒮)"

The key property of the infimum is that no other ball in 𝒮 has a smaller radius.

  have "infrad ≤ rad B" if "B ∈ 𝒮" for B
    by (smt (verit, best) bdd_below.I cINF_lower image_iff infrad_def rad that)

It’s possible for the infimum of a set to be strictly smaller than every element; for example, the infimum of the set of positive reals is zero. But if the set is finite and nonempty, its infimum is actually an element.

  have "∃B ∈ 𝒮. rad B = infrad" if "finite 𝒮" "𝒮 ≠ {}"
    by (smt (verit) empty_is_image finite_imageI finite_less_Inf_iff imageE infrad_def that)

Example 3: Find a list of minimum length

If you want to grab an element minimising some attribute, obtain the minimum value of the attribute first. Here, we define the minimum of all the lengths of the lists in L. Note, again, the use of the image operator.

  define minl where "minl = Inf (length ` L)"

Now we can obtain an element of L of length minl. It exists because the set L is non-empty. That set does not have to be finite because every set of natural numbers has a least element.

  obtain l0 where  "l0 ∈ L" "length l0 = minl"
    by (metis Inf_nat_def1 empty_is_image imageE minl_def ‹L ≠ {}›)

Now we check the key property, namely that the length of l0 is minimal among the lengths of every element of L.

  then have "length l0 ≤ length l" if "l ∈ L" for l
    by (simp add: cINF_lower minl_def that)

Final remarks

Novices often seem to let their formulas get too large. Remember to use definitions to keep your formulas small, especially in situations such as these. You may wonder whether minl needed to be defined at all, as it’s almost nothing. And indeed l0 can still be obtained, but the proof is an order of magnitude slower: simplicity really matters here. And just a reminder, every one of the proofs above was found by sledgehammer.