Induction for lists

We will now introduce an induction principle for lists. It is derived directly from the definition of the list datatype.

Induction Principle (Lists)

P []        P (t) => P (h :: t) forall l. P (l)

Proposition (Interchange)

The rev function and the append operator obey an interchange law since the following holds for all 'a lists l1 and l2.

rev (l1 @ l2) = rev l2 @ rev l1

Exercise

Prove by structural induction that for all 'a lists l1 and l2:

length (l1 @ l2) = length l1 + length l2

Proposition (Involution)

The rev function is an involution, i.e. it always undoes its own work, since rev (rev l) = l.

NEXT ·  UP ·  PREVIOUS ·  CONTENTS ·  INDEX