From Data Definitions to Structural Induction Principles
--------------------------------------------------------

Here is a data definition for a list of z's:

Loz ::= nil | (cons 'z Loz)

Remember from HtDP that we can read off from this data definition a template for functions that consume Lozs:

;; loz-template : Loz -> ???
(defun loz-template (x)
  (cond ((endp x) ...)
	((consp x)
	 ... (car x) ...
	 ... (loz-template (cdr x)) ...)))

And then we can use the template to build functions like:
;; count-zs : Loz -> Number
;; Count the occurrences of 'z in the given Loz
(defun count-zs (x)
  (cond ((endp x) 0)
	((consp x) (if (equal (car x) 'z)
		       (1+ (count-zs (cdr x)))
		     (count-zs (cdr x))))))

;; Let's build a function to test count-zs
;; Loz -> Boolean
;; Check that the number of 'z in a given Loz is equal to the length of the Loz.
(defun test-count-zs (aloz)
  (equal (count-zs aloz) (len aloz)))

;; And now our tests:
(test-count-zs nil)
(test-count-zs (cons 'z nil))
(test-count-zs (cons 'z (cons 'z nil)))

It seems like (test-count-zs L) should produce t for every Loz that we plug in for L.  We can actually prove that using a logical tool called a _structural induction principle_.  A structural induction principle is a rule that lets us prove statements of the form "for all x in D, (predicate? x)".  In the example above, we are interested in the case where D = Loz and predicate? = test-count-zs.

It turns out that every data definition yields a structural induction principle, and we can read it off of the data definition much as we are able to do for the template.

We state the structural induction principle, show how to use it for the test-count-zs example, and then talk about how to read it off from the data definition.  Here it is:

Structural Induction Principle for Loz:
If - (predicate? nil), and 
   - for all x in Loz.[(predicate? x) -> (predicate? (cons 'z x))]
then
for all x in Loz, (predicate? x)

That means that to show for all x in Loz, (predicate? x) we must do two things:
(1) Prove (predicate? nil).  This is usually easy; just evaluate the expression!
(2) Prove that for all x in Loz, [(predicate? x) -> (predicate? (cons 'z x))].  That means we can assume (predicate? x) for some arbitrary x in Loz, and from there we must argue that (predicate? (cons 'z x)) also holds.  The assumption that we are allowed to make is called the _induction hypothesis_ (IH for short).

Why do these two cases suffice?  (1) gives us that (predicate? nil) holds.  Then we use (2) to deduce that (predicate? (cons 'z nil)) holds.  Using (2) again, we can see that (predicate? (cons 'z (cons 'z nil))) holds.  Using (2) again we discover that (predicate? (cons 'z (cons 'z (cons 'z nil)))) holds.  We can keep doing this to show that the predicate? holds for any Loz we choose.  

Let's see how to use the structural induction principle for the test-count-zs example.

THEOREM:  for all x in Loz, (test-count-zs x).
PROOF:
We proceed by structural induction on x.
(1)  (test-count-zs nil) = t by simply evaluating the expression.
(2)  Our induction hypothesis is (test-count-zs x) for some arbitrary x in Loz.  That means we can assume (equal (count-zs x) (len x)).  

(test-count-zs (cons 'z x)) 
  = (equal (count-zs (cons 'z x)) (len (cons 'z x))) [defn of test-count-zs]
  = (equal (1+ (count-zs x)) (len (cons 'z x)))      [defn of count-zs]
  = (equal (1+ (count-zs x)) (1+ (len x)))           [defn of len]
  = (equal (count-zs x) (len x))                     [sub 1 from both sides]

But the last equation is simply our induction hypothesis, and so case (2) holds.

Because case (1) and (2) both hold, the structural induction principle allows us to conclude that for all x in Loz, (test-count-zs x).  
Q.E.D.

FORMULATING THE STRUCTURAL INDUCTION PRINCIPLE FROM THE DATA DEFINITION
-----------------------------------------------------------------------
Now let's see how to read a structural induction principle off of a data definition.  Every structural induction principle has the following shape:

If <hypothesis> ...
then
  for all x : <D>, (predicate? x)

To obtain a structural induction principle, we must subsitute some things in for <hypothess> ... and <D>.  

First, we will create as many hypotheses as there are clauses in the data definition.  For example, Loz has two clauses, and so we would leave room for two hypotheses:

If 
  (1) <hypothesis>, and
  (2) <hypothesis>
then
  for all x : <D>, (predicate? x)

Next, we translate each clause of the data definition into a hypothesis.  Proceed one clause at a time.  There are two possibilities for each clause:  either the clause uses self-reference or it does not.

If the clause does *not* use self-reference, then <hypothesis> is a _base case_.  Proceed as follows:
(b1) If the clause is a value, then replace <hypothesis> with a call of predicate? on the value.
(b2) If the clause is the name of a datatype (say, Data), then choose an unused variable (say, var).  Replace <hypothesis> with "for all var:Data, (predicate? var)".
(b3) If the clause is a constructor-call (like (make-foo A B)), then choose one new variable for each datatype mentioned inside.  Replace <hypothesis> with "for all a:A, b:B, (predicate? (make-foo a b))".

If the clause involves self-reference, then <hypothesis> is an _inductive case_.  Proceed as follows:
(i1) Replace <hypothesis> with "for all <vars> ,[<premise> -> <conclusion>]". 
(i2) For each self-reference, invent a new variable name and replace <vars> with "var_1:<D>, var_2:<D> ...".
(i3) Replace <premise> with "(predicate? var_1) /\ (predicate? var_2) /\ ...", where there is one predicate? application to each variable introduced in step (i2).
(i4) Replace <conclusion> with the text of the clause wrapped in a call to predicate?  EXCEPT:  substitute the variables introduced in step (i2) in for the self references.
(i5) If there are any datatypes still mentioned in the clause that replaced <conclusion>, deal with them as outlined in steps (b2) and (b3).  That is, invent a new variable name for each one, plug the variables in for the datatype names, and wrap a "for all var_1:X, var_2:Y," around the clause (where X and Y are the datatype names being replaced).

Once you have dealt with all of the clauses, the final step is to replace <D> with the name of the datatype being defined.  Let's do the Loz example step by step:

Loz ::= nil | (cons 'z Loz)

We have two clauses, and so we leave room for two hypotheses:

If 
  (1) <hypothesis>, and
  (2) <hypothesis>
then
  for all x : <D>, (predicate? x)

Next, we translate the nil clause into a hypothesis.  There is no self-reference in the nil clause, and so we are dealing with a base case.  Step (b1) applies because nil is just a value.  Therefore we replace the first <hypothesis> by (predicate? nil) to obtain:

If 
  (1) (predicate? nil), and
  (2) <hypothesis>
then
  for all x : <D>, (predicate? x)

Next we deal with the (cons 'z Loz) case.  It has a self-reference, and so we're dealing with an inductive case.  We use step (i1) to obtain:

If 
  (1) (predicate? nil), and
  (2) for all <vars>, [<premise> -> <conclusion>]
then
  for all x : <D>, (predicate? x)

Following step (i2), we will invent one new variable: a.  We obtain:

If 
  (1) (predicate? nil), and
  (2) for all a:<D>, [<premise> -> <conclusion>]
then
  for all x : <D>, (predicate? x)

Step (i3) leads us to this:

If 
  (1) (predicate? nil), and
  (2) for all a:<D>, [(predicate? a) -> <conclusion>]
then
  for all x : <D>, (predicate? x)

Step (i4) gives:

If 
  (1) (predicate? nil), and
  (2) for all a:<D>, [(predicate? a) -> (predicate? (cons 'z a))]
then
  for all x : <D>, (predicate? x)

Step (i5) does not apply here, and so now we just replace <D> with Loz to obtain:

If 
  (1) (predicate? nil), and
  (2) for all a:Loz, [(predicate? a) -> (predicate? (cons 'z a))]
then
  for all x : Loz, (predicate? x)

This is the complete structural induction principle for Loz.

Let's try another:  
LoS ::= nil | (cons Symbol LoS)

Again, we have two clauses, and so we will have two hypotheses.  The first hypothesis is the same as before:  (predicate? nil).

Steps (i1)-(i4) for the second clause yields the hypothesis:
  for all x:<D>,[(predicate? x) -> (predicate? (cons Symbol x))]

Now step (i5) applies because we need to get rid of that 'Symbol' on the right.  So we invent a new variable name, s, replace Symbol with s, and wrap a "for all s:Symbol" around the conclusion of the implication:

  for all x:<D>,[(predicate? x) -> forall n:Number[(predicate? (cons n x))]].

Then, replacing <D> with LoS, the structural induction principle for LoS is:

If (1) (predicate? nil), and
   (2) for all x:LoS,[(predicate? x) -> forall n:Number[(predicate? (cons n x))]]
then
  for all x:LoS, (predicate? x)

Let's try a third example.  Consider this data definition for simple arithmetic expressions:

Arith ::= (make-num Number) | (make-add Arith Arith) | (make-mul Arith Arith)

We have three clauses, and so the structural induction principle has three hypotheses:

If (1) <hypothesis>, and
   (2) <hypothesis>, and
   (3) <hypothesis>
then
  for all e:Arith, (predicate? e)  (I have already replaced <D> with Arith here).

The first clause, (make-num Number) is a base case because there is no self-reference.  Since it is a constructor application, step (b3) applies.  The corresponding hypothesis is:  for all n:Number, (predicate? (make-num n)).

The second clause is an inductive case.  There are two self-references, and so after steps (i1), (i2), and (i3) we have:

  for all x:Arith, y:Arith, [(predicate? x) /\ (predicate? y) -> <conclusion>]


Step (i4) refines this to:
  for all x:Arith, y:Arith, 
     [(predicate? x) /\ (predicate? y) -> (predicate? (make-add x y))]

Step (i5) does not apply, and so this clause is done.

The third clause follows the same pattern as the second clause.  We obtain the hypothesis:
  for all x:Arith, y:Arith, 
     [(predicate? x) /\ (predicate? y) -> (predicate? (make-mul x y))]


Putting these together, our structural induction principle looks like this:

If (1) forall n:Number, (predicate? (make-num n))
   (2)  for all x:Arith, y:Arith, 
           [(predicate? x) /\ (predicate? y) -> (predicate? (make-add x y))]
   (3)  for all x:Arith, y:Arith, 
           [(predicate? x) /\ (predicate? y) -> (predicate? (make-mul x y))]
then
  for all x:Arith, (predicate? x)