Variations of Inductive Proof

We have learned that operations and proofs over inductively-defined objects follow from their inductive definitions. For example, recall the inductive definition of a list:

Definition (List): a list is either:

Empty, or
Non-empty, a combination of a head element and the rest of the list, its tail.

But this isn’t the only way of defining the infinite possibilities of a list into a finite set of cases. For example, here is an alternative definition:

Definition (List): a list is either:

Empty, or
A singleton list containing exactly one element, or
Non-empty with at least two elements and a tail.

This definition differs from the previous one because it explicitly calls out the singleton list case. Both definitions are equivalent—every possible list is described by exactly one of the cases in each definition. But in some situations, using an alternative inductive definition is appropriate to better fit the operation we are describing or reasoning about.

We’ll look at an inductive proof that takes advantage of this alternative definition. This is just one example of the variations we might encounter when performing inductive proof. There are many others out there, more than we can cover in the brief time we have in this course. However, be aware that these variations exist, but they all ultimately rest on our basic definition of inductive reasoning:

Definition (Induction): a proof by induction is a proof that proceeds by case analysis on the inductive structure of an object where you may assume an inductive hypothesis in the inductive cases of the proof.

Case Study: Intersperse

In a previous reading, we introduced the intersperse function takes an element x and a list l and returns a new list that puts x (in-between) each element of l.

(define intersperse
  (lambda (v l)
    (cond
      [(null? l)       '()]
      [(null? (cdr l)) (list (car l))]
      [else (cons (car l) (cons v (intersperse v (cdr l))))])))

Suppose we want to prove the following claim:

Claim (Length of Intersperse): for all values v and lists l. If (not (null? l)) = #t then (length (intersperse v l)) = (- (* 2 (length l)) 1).

Note that intersperse is defined according to our alternative, singleton-based definition of a list ((null? (cdr l)) checks to see if the list has example one element). Our proof, therefore, follows the cases outlined by this definition. If the cases include recursive sub-structure, i.e., tails of lists drawn from the subject of the inductive proof, then we gain the induction hypotheses for all of these sub-structures. These are our inductive cases whereas cases with no recursive sub-structures are called base cases.

Here is a formal proof the claim as an exemplar of the concepts we’ve learned this week along with some of these additional concerns we’ve introduced such as using an alternative definition of lists. Study this proof carefully, paying attention to its structure and formatting.

Proof. Let v be an arbitrary value and l be an arbitrary list. We assume that (not (null? l)) = #t, i.e., l is non-empty. We proceed by induction on the structure of l.

l is empty. By assumption, we know that (not (null? l)). Thus, we do not need to consider this case.
(null? (cdr l)), l has one element. The left-hand side of the equality evaluates as follows:
```
(length (intersperse v l)) -->* (length (list (car l))) -->* 1
```
And the right-side evaluates to:
```
(- (* 2 (length l)) 1) -->* (- (* 2 1) 1) -->* 1.
```
l is non-empty with more than one element. We assume our inductive hypothesis holds:

IH: If (not (null? (cdr l))) then (length (intersperse v (car l))) = (- (* 2 (length (car l))) 1).

We must prove:

Goal: (length (intersperse v l)) = (- (* 2 (length l)) 1).

The left-hand side of the equality evaluates to:
```
     (length (intersperse v l))
-->  (length (cons (car l) (cons v (intersperse v (cdr l)))))
-->* (+ 2 (intersperse v (cdr l)))`
```
In this case, we know that l has at least two elements, so (not (null? (cdr l))). Therefore, our induction hypothesis applies and so we can rewrite this final quantity to:
```
(+ 2 (- (* 2 (length (cdr l))) 1)
```
The right-hand side of the equality evaluates to:
```
    (- (* 2 (length l)) 1)
--> (- (* 2 (+ 1 (length (cdr l)))) 1)
```
By arithmetic, the following identities hold:
```
  (+ 2 (- (* 2 (length (cdr l))) 1)
≡ (- (* 2 (length (cdr l))) 1)
≡ (- (* 2 (+ 1 (length (cdr l)))) 1)
= (- (+ 2 (* 2 (length (cdr l)))) 1)
= (- (* 2 (length (cdr l))) 1)
```
So both sides of the equality evaluate to (- (* 2 (length (cdr l))) 1), completing the proof.

Racket’s syntax makes the final arithmetic derivations a little hard to read. It is more instructive to convert the expressions to equivalent arithmetic expressions (letting \(X\) = (length (cdr l))) to see what is going on:

\[ 2 + (2X -1) = 2X - 1. \]

and

\[ 2(1 + X) - 1 = 2 + 2X - 1 = 2X - 1. \]

Also note that our claim is the form of a conditional: “if … then … ,” i.e., a logical implication! This means that our induction hypothesis must also be of this form! When trying to prove an implication, we assume the “if” portion (the premise) and go on the prove the “then” portion (the conclusion). However, if we assume that an implication is true, we must first prove the “if” portion and then we can go on to assume the “then” portion.

Exercise (Proof Busters, Intersperse Edition, ‡): consider the following implementation of intersperse where we do not introduce a special case for a 1-element list:

(define intersperse
  (lambda (v l)
    (cond
      [(null? l)       '()]
      [else (cons (car l) (cons v (intersperse v (cdr l))))])))

This implementation is not correct. (If you don’t see why, I encourage you to experiment with the function in DrRacket!)

Nevertheless, try applying the above proof to these function. How does the proof change? The claim should not hold for this function—where does the proof go wrong in your analysis?

CSC/MAT 208 (Spring 2024)

Reading: Variations on Inductive Proof

Variations of Inductive Proof

Case Study: Intersperse