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:

(define length
  (lambda (l)
    (match l
      ['() 0]
      [(cons _ tail) (+ 1 (length tail))])))

(define tails
  (lambda (l)
    (match l
      ['() (list '())]
      [(cons _ tail) (cons l (tails tail))])))

And the following claim about these functions:

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. Collaborative refine the solutions into a final form.)

Consider the following Racket functions:

(define list-inc
  (lambda (l)
    (match l
      ['() '()]
      [(cons head tail) (cons (+ 1 head) (list-inc tail))])))

(define sum
  (lambda (l)
    (match l
      ['() 0]
      [(cons head tail) (+ head (sum tail))])))

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, (sum (inc l)) ≡ (+ (length l) (sum l)).

Problem 3: Building Up Facts

(Work on this problem collaboratively with your partner.)

Previously, we wrote an implementation of the (snoc l v) function, which appended an element v to the end of the input list l.

1. Using snoc, write a Racket function (rev l) that reverses the list l.

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

2. Prove the following property of snoc:

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

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

   Claim (Rev Length): for all lists l, (length (rev l)) ≡ (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?)