To prove equality of two function definitions inductively

Question

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?

Answer 1

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)