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