Although the answer to the original question was sort of embedded in the discussion, a quick read of the replies suggested that no one had made the simple clarification. 2) Prove that the property holds for (x:xs) under the assumption that the property holds for xs. It's not a general property it is a specific one, this is more clearly stated thus: 2) Prove that the property holds for (x:xs) given that it holds for a list xs. Now, from 1 you already have a list xs =[], and then you have (x:[]) = [x], then (x2:[x]) = [x2,x] ... I think that you can see where this is going. This is an example of a useful type of proof called proof by induction, which are related to natural numbers and counting. Induction gets a little uncertain with infinities which is what most of the posts where about, in summary: Haskell has infinite lists, infinite lists must be handled seperately in the proof. Wikipedia has a fairly conventional explanation of induction http://en.wikipedia.org/wiki/Mathematical_induction C Echo Nolan wrote:
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 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.