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

[Jim Apple]

Echo Nolan wrote:

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

As someone else said, this works for finite lists.

> 	My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) => P(xs)?

Assume there is some finite list ys for which this statement is not 
true. In other words, assume that

p([]) && (p(ys) => p(x:ys))

but

~p(ys)

Then there is then a smallest list ys with such property.

ys /= [], since P([]).
Consider tail ys. It is smaller than ys, so the implication holds for 
it. However, that means that

p(tail ys) => p(head ys : tail ys)

or p(ys). That's a contradiction, so our assumption that there was some 
finite list ys for which the implication ws false is false.

Jim