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

[Clive Brettingham-Moore]

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.
>
>  
>
>  
>