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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
