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

[Henning Thielemann]

On Mon, 2 May 2005, 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
> 	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?

There must be some warranty that the resolution with respect to (:) stops 
somewhere. If you are sure that xs is shorter than x then the induction 
will stop sometimes. But if (x:xs) is infinite the induction won't work. I 
think you need some notion of the length of a list or some relation "one 
list is shorter than the other one" in order to explain induction.