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

Jan-Willem Maessen jmaessen at alum.mit.edu
Mon May 2 11:11:18 EDT 2005

```On May 2, 2005, at 8:29 AM, Henning Thielemann wrote:

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

Yes, to prove properties of an infinite (or a cyclic) list,
co-recursion is indicated.  Briefly, we must *assume* that the property
holds for xs, and show that it holds for (x:xs).  We must still show
that it holds for [] if the property is to hold for finite lists as
well.

I'll leave it to others better qualified than myself to flesh this
picture out.  If induction leaves you dubious, you will find
co-induction quite unconvincing. :-)

-Jan-Willem Maessen

> _______________________________________________