CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to prove that a recursive function has some value

Here is a trivial function and a lemma:

fun count_from where
  "count_from y 0 = []"
| "count_from y (Suc x) = y # count_from (Suc y) x"

lemma "count_from 3 5 = [3,4,5,6,7]"

It's just an example. The real function is more complicated.

Could you please suggest how to prove such a lemmas?

I redefined the function using tail-recursion and proved the lemma as follows:

fun count_from2 where
  "count_from2 y 0 ys = ys"
| "count_from2 y (Suc x) ys = count_from2 (Suc y) x (ys @ [y])"

lemma "count_from2 3 5 [] = xs ⟹ xs = [3,4,5,6,7]"
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  apply simp
  apply (drule_tac s="xs" in sym)
  apply (erule count_from2.elims)
  by auto

For sure it's not an adequate solution.

I have a several questions:

  1. Is it preferred to define functions using tail-recursion? Does it usually simplifies theorem proving?
  2. Why function simplification rules (count_from.simps or count_from2.simps) can't be applied?
  3. Should I define an introduction rules to prove the first lemma?
  4. Is it possible to apply a function induction rule to prove such a lemmas?

Upvotes: 1

Views: 128

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8278

Your question might be better phrased as ‘How do I evaluate a recursively-defined function and get that evaluation as a theorem?’

The answer is that usually the simplifier should do a decent job at evaluating it. The problem here is that numerals like 1, 2, 3 use a binary representation of the natural numbers, whereas the function is defined by pattern matching on 0 and Suc. This is the reason why your simps cannot be applied: they only match on terms of the form count_from ?y 0 or count_from ?y (Suc ?x) and count_from 3 5 is neither.

What you can do to move things along is to use the theorem collection eval_nat_numeral, which simply rewrites numerals like 1, 2, 3 into successor notation:

lemma "count_from 3 5 = [3,4,5,6,7]"
  by (simp add: eval_nat_numeral)

Another possibility are the code_simp and eval proof methods which try to prove a statement that is ‘executable’ in some sense by evaluating it and checking that you get True. They both work fine here:

lemma "count_from 3 5 = [3,4,5,6,7]"
  by code_simp

The difference between the two is that code_simp uses the simplifier, which gives you a ‘proper’ proof that goes through the Isabelle kernel (but this can be very slow for bigger examples), whereas eval uses the code generator as a trusted oracle and is thus potentially less trustworthy (although I have never seen a problem in practice) but much faster.

As for your other questions: No, I don't see how induction applies here. I don't know what you mean by defining introduction rules (what would they look like?). And tail-recursion does not really have any advantages for proving things – in fact, if you ‘artificially’ make function definitions tail-recursive as you have done for count_from2 you actually make things slightly more difficult, since any properties you want to prove then require additional generalisation before you can prove them by induction. A classic example is normal vs tail-recursive list reversal (I think you can find that in the ‘Programming and Proving’ tutorial).

Also note that a function very much like your count_from already exists in the library: It is called upt :: nat ⇒ nat ⇒ nat list and has custom syntax of the form [a..<b]. It gives you the list of natural numbers between a and b-1 in ascending order. It is a good idea to look at the ‘What's in Main’ document to get an idea for what.

Upvotes: 3

Related Questions