3

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?

dfeuer
  • 48,079
  • 5
  • 63
  • 167
letter
  • 91
  • 1
  • 7
  • 1
    You may need to generalize the statement so that in involves `sol`. Something like `sol acc n = ... something using moll, acc, n`. Once you prove that by induction, you can set `acc=0` so that the LHS reduces to `doll n` and hopefully the RHS reduces to `moll n`, proving the original goal. – chi Jan 25 '16 at 14:07
  • 1
    I know it's probably not the way it's meant to but in this case I would rather proof that `mol n = 1 + sum [1..n] = doll n` which seems to be easier (both seems to be trivial inductions on first glance) – Random Dev Jan 25 '16 at 14:11
  • Please fix the title. – jub0bs Jan 25 '16 at 14:18
  • btw: as chi hinted you probably want to proof `sol acc n = acc 1 + sum [1..n]` as a *lemma* for the second one – Random Dev Jan 25 '16 at 14:19
  • It pains me to admit it, but I've got the same problem with sol acc n = 1 + sum[1..n] . sol acc 0 = 1 = 1+ sum [1..n] is okay I guess. But how do i prove sol( acc n+n1) n = 1+ sum [1..n+1]? – letter Jan 25 '16 at 14:50
  • Any particular reason you're ignoring the answer, and continuing here in the comments? – Daniel Martin Jan 25 '16 at 15:17

1 Answers1

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)
Daniel Martin
  • 23,083
  • 6
  • 50
  • 70
  • thank you for all. It is helping me quit a lot. unfortunately I'm a real blockhead today. I really dont know how to prove sol x (n+1) == (sol 0 n) + x ? How can I rewrite it, to use induction hypothesis? – letter Jan 25 '16 at 16:01
  • You don't. You prove that `sol x (n+1)` is equal to `(sol 0 (n+1)) + x`. Remember to substitute `n+1` in for `n` wherever it is. (See also the updated answer) – Daniel Martin Jan 25 '16 at 18:01
  • thank you for your patience. without your help, i couldn't possibly grapped the concept – letter Jan 25 '16 at 19:23