# Problem 1: Equivalence Propositions

Exploring a model for interesting corner cases and behavior is one
thing. However, we are ultimately interested in using our model to
*formally prove* properties of programs. We call such properties
**propositions**, statements about the world that are
(potentially) provable. A **proof** is a logical argument
that the proposition is indeed true.

There are many kinds of propositions we might consider when we think
about program correctness. The most fundamental of these is *program
equivalence*, asserting that two programs produce the same
value.

Let’s try writing our first proof and writing it down in LaTeX: Here is a recursive function definition over lists:

```
# One of our helper functions to get Scheme-like list behavior
# from Python lists. l[1:] returns all the elements of l,
# starting with index 1, i.e., without the head.
def tail(l):
return l[1:]
def list_length(l):
if l == []:
return 0
else:
return 1 + list_length(tail(l))
```

We will prove the following claim:

**Claim**: `(list_length [21, 7, 4])`

≡
`3`

.

The equivalence symbol (≡), LaTeX: `\equiv`

) acts like
equality in that it asserts that the left- and right-hand sides of the
symbol are equivalent. We say that two programs are equivalent if they
evaluate to the same final value.

Before we write anything, we must prove the claim first! To show that an equivalence between two expressions holds, it is sufficient to show that both sides evaluate to

*identical values*. The right-hand side of the equivalence is already a value,`3`

, so we need to show that the left-side of the equivalence evaluates to this same value. Use our mental model of computation to give an evaluation trace of`my_length([21, 7, 4])`

.Now, let’s write the proof in your lab write-up. When writing proofs, we will always:

- Restate the claim.
- Give the proof.

For example, here is a proof of a simple arithmetic equivalence in this style:

~~~latex

And here it is it looks (roughly) when rendered:

**Claim**:`(- (* 5 (expt 2 3)) 1)`

≡`39`

.*Proof*. The left-hand side of the equivalence evaluates as follows:`(- (* 5 (expt 2 3)) 1) --> (- (* 5 8) 1) --> (- 40 1) --> 39 □`

(

*Note*: the long arrow`-->`

is really`- - >`

but the font I use for the website supports ligatures which renders the arrow as a single character instead.)

# Problem 2: More Equivalences

Consider the following additional Racket functions:

```
# Helpers for Scheme-like manipulation of Python lists
def head(l):
return l[0]
def cons(x, l):
return [x] + l
def tail(l):
return l[1:]
def list_replicate(x, n):
if n == 0:
return 0
else:
return cons(x, list_replicate(x, n-1))
def list_append(l1, l2):
if l1 == []:
return l2
else:
return cons(head(l1), append(tail(l1), l2))
define list_filter(f, l):if l == []:
return []
elif f(head(l)):
return cons(head(l), list_filter(f, tail(l)))
else:
return list_filter(f, tail(l))
```

Prove the following statements of equivalence. In your derivations, you may evaluate a function call to the (yet-to-be-evaluated) expression it returns in a single step of execution.

`list_replicate('!', 3)`

≡`['!', '!', '!']`

.`(list_length(list_append [1, 2] [3, 4, 5]))`

≡`list_length([1, 2]) + list_length([3, 4, 5])`

`list_length(list_filter(lambda x: x >= 0, [1, 2, 3, 4, 5])) <= 5`

≡`True`

# Problem 3: Or Not

Consider the following definition of the boolean `xor`

function:

```
def xor(b1, b2):
if b1:
return not b2
else:
return b2
```

Prove the following claims about this function: In your derivations, you may evaluate a function call to the (yet-to-be-evaluated) expression it returns in a single step of execution.

**Claim (Xor can return true)**: There exists a boolean
`b`

such that `xor(True, b)`

≡
`True`

.

**Claim (Xor cancellation)**: For any boolean
`b`

, `xor(b, b)`

≡ `False`

.

**Claim (Xor equivalence)**: For any pair of booleans
`b1`

and `b2`

, `xor(b1, b2)`

≡
`(b1 or b2) and (not (b1 and b2))`

.

# Problem 4: Dispute (Optional)

Show that the following equivalence *does not* hold by
carrying through the evaluation and observing that both sides evaluate
to different values.

`list_append(['a', 'b', 'c'], ['d'])`

≡`list_append(['d'], ['a', 'b', 'c'])`