[Haskell-cafe] Induction (help!)

[Brent Yorgey]

On Wed, May 7, 2008 at 8:01 PM, PR Stanley <prstanley at ntlworld.com> wrote:

> So, when you apply the function to the first element in the set - e.g. Zero
> or Nil in the case of lists - you're actually testing to see the function
> works. Then in the inductive step you base everything on the assumption that
> p holds for some n and of course if that's true then p must hold for Succ n
> but you have to prove this by taking Succ from n and thus going bakc to its
> predecessor which is also the hypothesis p(n).
> So, to reiterate
> assumption: if hypothesis then conclusion
>        if p(n) then p(Succ n)
> proof of assumption if p(Succ n) = Succ(p(n)) then we've won. If pn+1) =
> p(n) + p(1) then we have liftoff!
> I'm not going to go any further in case I'm once again on the wrong track.
> Cheers
> Paul
>

You've got the right idea.  I should point out that it doesn't make sense to
say p(Succ n) = Succ(p(n)),  p(x) represents some statement that is either
true or false, so it doesn't make sense to say Succ(p(n)).  But I think you
are on the right track.

-Brent
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080508/154ad486/attachment.htm