My research and investigations

The HOL theorem-prover includes tactics on induction, a standard technique for proofs involving a recursive data structure.

For example, the whole numbers can be constructed recursively as follows: starting from 0, successive numbers can be obtained by adding 1 to the predecessor: n to n+1. So if a property P can be shown such that:

  1. P is valid for 0, and
  2. If P is valid for n, it is also valid for n+1.

Then we can claim that the property P is valid for all whole number n.

Similarly, the list data structure can be constructed recursively as: starting from the empty list [], elements are inserted into the list (h::t), with head h and tail t. If tail t = [], the list has one element [h]. If tail = [k], the list has two elements [h; k], and so on.

Corresponding to the induction for proofs involving whole number properties, there is Structural Induction for proofs involving lists:

  1. Property P is valid for [], and
  2. If P is valid for list t, it is also valid for list (h::t).

The we can claim that the property P is valid for all lists.

Usually the base case (1) is trivial, easily proved by some fundamental results from definition.

The trick to prove the step case (2) is to match the pattern of the induction hypothesis: P is valid for t, to the pattern in the goal: P is valid for (h::t).

Sometimes the definition provides decomposition of the pattern (h::t) to t, then the step case is easy to match.
Otherwise, the best strategy is:

  • figure out what’s the stumbling block,
  • formulate a lemma that can solve the stumbling block,
  • prove the lemma.

It is the solving of stumbling blocks that make theorem-proving endeavours interesting.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: