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
else:
return 1 + list_length(tail(l))
def list_tails(l):
if is_null(l):
return [ [] ] # N.B., a list containing the empty list
else:
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)`

.

- Write a proof sketch of this claim that outlines the proof’s overall trajectory, as described in the reading.
- 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 []
else:
return cons(head(l) + 1, list_inc(tail(l)))
def list_sum(l):
if is_null(l):
return 0
else:
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.)

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.Using

`snoc`

, write a function`list_rev(l)`

that reverses the list`l`

.(

*Hint*: what happens when you traverse`l`

and`snoc`

every element?)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)`

.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?)