Thursday, 14 April 2011

A Theorem-Proving Exercise for Novices

Listening to:

Louis Armstrong, Ain’t Misbehavin’.


I have used this exercise as a good one for getting a student up to speed with a proof-assistant such as HOL4.

Using your theorem-proving system of choice, define the notion of sublist, a binary relation on lists l1 and l2, which is true if and only if all the elements of l1 appear in l2 in the same order. Naturally, l2 may contain other elements.

For example, [1,2,3] is a sub-list of [0,1,2,2,4,5,6,3,10], but is not a sub-list of [1,4,3,2].

Having defined this relation in whatever way seems most natural, prove that it is reflexive, anti-symmetric and transitive.