Recursion to Induction

Now we'll gain first-hand experience proving properties of our recursive designs.

Problem 1: The Structure of Inductive Proof

We use inductive reasoning to prove properties of programs involving recursion. In this problem, we'll incrementally develop all the pieces of an inductive proof concerning the append function over lists:

def cons(x, l):
    return [x, *l]

def append(l1, l2):
    match l1:
        case []:
            return l2
        case [head, *tail]:
            return cons(head, append(tail, l2))

Note

Remember that, unless explicitly stated, you may take the shortcut that a function call evaluates directly to the expression that it would return in a single step.

In the reading, we explored these two claims regarding append:

Claim (left-null-append)

For all lists l, append([], l) ≡ l.

Claim (right-null-append)

For all lists l, append(l, []) ≡ l.

You noted that the right-null-append claim requires more proof machinery than just symbolic execution. We need induction to prove it! Like recursion, inductive proof also has a skeleton we can use as a starting point in understanding this technique. Below is our inductive proof skeleton for claims involving lists with places you should fill in indicated with italicized parentheses: (FILL ME IN!).

Proof Skeleton

Proof. We prove this claim by induction on (The list we are performing case analysis over).

  • The list is empty. (Proof of the claim assuming the list is empty---the base case)

  • The list is non-empty. We assume our induction hypothesis:

    Induction Hypothesis: (The induction hypothesis)

    We must prove:

    (Restatement of proof goal)

    (Proof of the claim assuming the list is non-empty---the inductive case)

Some notes about this skeleton:

  • Because induction is ultimately a case analysis, we must do induction on some object and thus must explicitly identify it. In our case, this is a list, but generally speaking, we can perform induction on any inductively-defined object that we can get our hands on.

  • The proof of the base case, when the list is empty, is usually straightforward. We know the list is empty, so we typically evaluate the goal equivalences to final values and observe that they are identical.

  • In the inductive case, we explicitly name (a) the induction hypothesis and (b) the proof goal. We do as a point of presentation---we want to be clear what we are assuming in our induction hypothesis and how that differs from the proof goal. Recall that the induction hypothesis is the original claim but specialized to the tail of the list we are performing induction over.

  • Finally, in the inductive case, we will likely need to use our induction hypothesis. Like other assumptions, we should be explicit in our prose when we invoke and how we use it to update our proof state.

    Use this skeleton to author a proof of the right-null-append claim.

Problem 2: On Your Own

Consider the following Python function:

def any(f, l):
    match l:
        case []:
            return False
        case [head, *tail]:
            if f(head):
                return True
            else:
                return any(f, tail)

For the following claim, write a formal proof of the claim.

Claim

For any list l, any(lambda (v): False, l) ≡ False.