Proof on tree size using Isabelle

Question

I'm trying to learn a little bit about Isabelle and proofs in general, and it's uses in Programming Language Theory. I'm following a book, "Concrete Semantics with Isabelle/HOL". I'm still in the beggining.

I was able to do the first exercises, but I got to a point where I noticed I just don't know what I'm doing. I just solved a question where I spent some time failing to prove something, than tried changing one little thing and it magically worked. Can someone explain what exactly is happening?

Ok, so here is what the question is basically about:

We had to make a simple tree structure with no data, like:

datatype tree0 = Tip | Node "tree0" "tree0"

The question ask us to make a function nodes t that count the number of nodes and leafs on the tree. Then, it provides a function:

fun explode :: "nat ⇒ tree0 ⇒ tree0" where
"explode 0 t = t" |
"explode (Suc n) t = explode n (Node t t)"

And ask us to provide an equation for the number of elements (nodes t) of the exploded tree, based on N and T, and prove that this equation is correct.

The equation I found was: nodes(explode n t) = (2^n)*(nodes t + 1) - 1

Which I tried proving using induction on "n" alone.

lemma aft_tree: "nodes(explode n t) = (2^n)*(nodes t + 1) - 1"
apply(induct n)    
apply(auto)
apply(simp add: exp_grow)
apply(simp add: algebra_simps)

done

After "apply(auto)", the goal changed to:

goal (1 subgoal):
 1. ⋀n. nodes (explode n t) = 2 ^ n + 2 ^ n * nodes t - Suc 0 ⟹
         nodes (explode n (Node t t)) = 2 * 2 ^ n + 2 * 2 ^ n * nodes t - Suc 0

So, I thought that proving nodes(explode n (Node t t)) = 2*nodes(explode n t) + 1 would solve it. So I made a lemma for it, proved it and added the next two "simp"s.

But the proof failed, with:

goal (1 subgoal):
 1. ⋀n. nodes (explode n t) = 2 ^ n + nodes t * 2 ^ n - Suc 0 ⟹
         Suc (2 * 2 ^ n + nodes t * (2 * 2 ^ n) - Suc (Suc 0)) =
         2 * 2 ^ n + nodes t * (2 * 2 ^ n) - Suc 0 

I don't quite get why this doesn't end the proof. I wondered if I was just proving the wrong thing, or maybe I'm just mixing everything up.

After this, I removed the simplification based on exp_grow, and tried generalizing the proof for "t". So I got:

lemma aft_tree: "nodes(explode n t) = (2^n)*(nodes t + 1) - 1"
apply(induct n arbitrary: t)
apply(auto)
apply(simp add: algebra_simps)
done

Which worked! And I just couldn't understand what happend. I tried following this proof step by step. After auto, the goal is:

goal (1 subgoal):
 1. ⋀n t. (⋀t. nodes (explode n t) = 2 ^ n + 2 ^ n * nodes t - Suc 0) ⟹
           2 ^ n + (2 ^ n + 2 ^ n * (nodes t + nodes t)) - Suc 0 =
           2 * 2 ^ n + 2 * 2 ^ n * nodes t - Suc 0

And it's proved on algebra_simps. I don't understand what happened, and why it didn't work on the first time. I think I'm misunderstanding everything. It has been a while since I took an Algebra course, and maybe I'm doing the proof by induction wrong. I was able to do the other questions, but this one left me a little lost :(

So, can someone help me on this? What am I getting wrong here?

Answer 1

Your first goal is provable, but is somewhat non-trivial arithmetic. I believe that the issue is essentially Isabelle not knowing that $$S(x - 2) = x -1$$ is true for arbitrary $x$, and indeed, this property is false in general, if $x<2$! This is because $x-2=0$ in Isabelle for $x=1$.

Here this doesn't occur, because $x=2\cdot 2^n$, so $x\geq 2$ for all $n\in\mathbb{N}$. But the simplifier doesn't know this. Adding a lemma along those lines, or making sure 2*nodes(explode n t) + 1 doesn't get simplified to S(2*nodes(explode n t)) should solve your issue.

Alternately, you could re-cast your whole proof in $\mathbb{Z}$, where subtraction behaves more sanely.