CSC 208-01 (Spring 2023)

Lab: List Induction Practice

In this lab, you will practice writing inductive proofs of list properties using the techniques introduced in the reading.

Please note that the problems will direct you how to work on these problems with your partner so that you can optimize your practice time. Some problems should be done together; others allow you to work independently and then come back to share results. Please make sure to follow these directions rather than just diving the work in half and going your separate ways!

In this lab, you may evaluate any recursive function to its chosen conditional branch in a single step.

Problem 1: Warm-Up

(Work on this problem collaboratively with your partner.)

Consider the following Racket functions:

def list_length(l):
    if is_null(l):
        return 0
        return 1 + list_length(tail(l))

def list_tails(l):
    if is_null(l):
        return [ [] ]  # N.B., a list containing the empty list
        return cons(l, (list_tails(tail(l))))

And the following claim about these functions:

Claim (Length of Tails): for all lists l, list_length(list_tails(l)) ≡ 1 + list_length(l).

  1. Write a proof sketch of this claim that outlines the proof’s overall trajectory, as described in the reading.
  2. Write a formal proof of this claim following your sketch.

Problem 2: A World Apart

(Work on each part individually and present your work to your partner when you finish. Collaboratively refine the solutions into a final form.)

Consider the following Racket functions:

def list_inc(l):
    if is_null(l):
        return []
        return cons(head(l) + 1, list_inc(tail(l)))

def list_sum(l):
    if is_null(l):
        return 0
        return head(l) + list_sum(tail(l))

For the following claim, (i) develop a proof sketch and (ii) a formal proof of the claim based on that sketch.

Claim: for any list of numbers l, list_sum(list_inc(l)) ≡ list_length(l) + list_sum(l).

Problem 3: Building Up Facts

(Work on this problem collaboratively with your partner.)

  1. Write an implementation of a function list_snoc(l, v) that takes a list l and an element v as input and returns l but with v appended onto the end of l. In other words, snoc is “backwards-cons,” adding the element to the end of the list instead of the front.

  2. Using snoc, write a function list_rev(l) that reverses the list l.

    (Hint: what happens when you traverse l and snoc every element?)

  3. Prove the following property of snoc:

    Claim (Snoc Length): for all lists l and values v, list_length(list_snoc(l, v)) ≡ 1 + list_length(l).

  4. Use the property of snoc to prove the following partial correctness property of rev:

    Claim (Rev Length): for all lists l, list_length(list_rev(l)) ≡ list_length(l).

    (Hint: where do you get stuck in the rev proof? Can you get the proof goal into a form where the Snoc Length property can help you?)