Lists and simplification rules: More difficult when using @ rather than #?

Question

While working through exercises in the Isabelle tutorials, I encountered a situation that confuses me. Why is it that the below lemma involving prepending to a list is proved so easily:

lemma ‹count_list xs x = n ⟹ count_list (x # xs) x = Suc n›
  by simp

While this one involving appending is not?

lemma ‹count_list xs x = n ⟹ count_list (xs @ [x]) x = Suc n›
  apply auto (* just does some minor rewriting *)
  (* What should be go here? try/try0 are of no help. *)
  done

I assume this has something to do with how the implementation of @ is more involved than # due to the internal implementation of lists (# is just another constructor while @ involves recursion), but what makes it so much more difficult to prove with and how do you account for that?

Answer 1

This has nothing to do with the ‘implementation’ of @. It has something to do with the ‘implementation’ of count_list (but I would say ‘definition’ rather than ‘implementation’).

Like most functions on lists, count_list is defined recursively (using the primrec command), which generates rules called count_list.simps that are added to the simpset (the set of rules that the simplifier uses for rewriting automatically).

If you type in thm count_list.simps, you will probably get something like this:

count_list [] ?y = 0
count_list (?x # ?xs) ?y = 
  (if ?x = ?y then count_list ?xs ?y + 1 else count_list ?xs ?y)

Since they are in the simpset, the simplifier that is invoked as a part of auto will always rewrite any instance of the left-hand side to the right-hand side.

Therefore, the first theorem you gave can be proven by a single step of rewriting with the second of these two rules and some more simplification. On that note, an equivalent and more usable formulation of that theorem would be count_list (x # xs) x = Suc (count_list xs x).

Similarly, I would very much suggest to reformulate your second lemma as count_list (xs @ [x]) x = Suc (count_list xs x).

Now why does auto not solve this? First of all, for this kind of goal, the only relevant part of auto for this kind of goal is the simplifier, so you might as well have written simp_all here. And the reason why that cannot solve the goal is that there it has no simplification rule for something like count_list (… @ …). You will have to prove this yourself.

When you want to prove a property of a recursively-defined function, the usual approach is to do an induction that mirrors the recursive definition:

lemma ‹count_list (xs @ [x]) x = Suc (count_list xs x)›
  apply (induction xs)
  apply simp_all
  done

Or more compactly:

lemma ‹count_list (xs @ [x]) x = Suc (count_list xs x)›
  by (induction xs) simp_all

But I would actually recommend the following more general lemma:

lemma ‹count_list (xs @ ys) x = count_list xs x + count_list ys x›
  by (induction xs) simp_all

In fact, it is reasonable to give this fact a name and add it to the simp set as it makes a good rewrite rule:

lemma count_list_append [simp]:
    ‹count_list (xs @ ys) x = count_list xs x + count_list ys x›
  by (induction xs) simp_all

In case you're wondering why I did induction on xs here and not on ys: since the recursive definition of count_list pattern-matches on the first list element and the remaining list, one must do induction on the first list (i.e. xs) so that the induction step talks about (x # xs) @ ys, which simplifies to x # (xs @ ys) and then one can apply the induction hypothesis.

Note that simp_all (or auto) were sufficient to prove the induction goals in the above proof; once you tell Isabelle to do induction and what kind of induction, the rest of the proof is again just simple rewriting.