How do I do the induction to establish the statement moll n = doll n, with
moll 0 = 1 --(m.1)
moll n = moll ( n-1) + n --(m.2)
doll n = sol 0 n --(d.1)
where
sol acc 0 = acc +1 --(d.2)
sol acc n = sol ( acc + n) (n-1) -- ? (d.2)
I tried to prove the base case for n = 0
doll 0 = (d.2) = 1 = (m.1) = moll 0 , which is correct.
Now for n+1, show that
moll 2n = doll (n + 1)
=> doll (n + 1) = (d.2) = soll (acc + n + 1) n
But what now? How can I simplify it any further?
You've got a mistake in your n+1 step. I suspect this is because you're new to Haskell and its precedence rules.
moll (n+1) is not, as you write moll 2n - I'm assuming that by that you mean moll (2*n), since moll 2n is a haskell syntax error.
In any case, moll (n+1) is in fact moll n + n + 1, or, with extra parentheses added just to be explicit:
(moll n) + (n + 1)
That is, you apply moll to n and then you add n + 1 to the result of that.
From here you should be able to apply the induction hypothesis and go forward.
More explicitly, since you seem to still be having trouble:
moll (n+1) == (moll n) + (n + 1) (by m.2)
== (doll n) + (n + 1) (by induction hypot.)
== (sol 0 n) + (n + 1) (by d.1)
Now, as a lemma:
sol x n == (sol 0 n) + x
This can be proved by induction on n. It's obviously true for n equal to 0.
For the lemma's induction step:
sol x (n+1) == (sol (x + (n+1)) n) (By d.2, for (n+1) > 0)
== (sol 0 n) + (x + (n+1)) (By the induction hypot.)
== (sol 0 n) + (n+1) + x (This is just math; re-arranging)
== ((sol 0 n) + (n+1)) + x
== (sol (n+1) n) + x (By the induction hypot. again)
== (sol 0 (n+1)) + x (By d.2 again)
That second time I used the induction hypothesis may seem a bit odd, but remember that the induction hypothesis says:
sol x n == (sol 0 n) + x
For all x. Therefore, I can apply it to anything added to (sol 0 n), including n+1.
Now, back to the main proof, using our lemma:
moll (n+1) == (sol 0 n) + (n + 1) (we had this before)
== sol (n+1) n (by our lemma)
== sol 0 (n+1) (by d.2)
== doll (n+1) (by d.1)