[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[Echo Nolan]

Hello all,
	My copy of HS: The Craft Of FP just arrived and I was reading
section 8.5 about induction. On page 141, Simon Thompson gives a
method of proving properties of functions on lists:
	1) Prove that the property holds for the null list
	2) Prove that the property holds for (x:xs) under the assumption
		that the property holds for xs.

	My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) => P(xs)?
In other words, how does proof of the property on empty lists and proof
that the property holds on (x:xs) under the assumption that it holds on
xs give proof that it holds on all lists? Isn't there a recursive
dependency here? You are defining the proof for lists with at least one
element based on the assumption that it holds for all lists, right? How
does this get you a proof of the general property if it depends on the
assumption of the general property?

Regards and thanks,
Echo Nolan.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050502/7ace438a/attachment.bin