Lab: Assumptions in proofs

Shorthand for Program Derivations

Most of the functions we will encounter from this point forward are simple conditionals, but our mental model can be quite verbose in these situations. Consider the following toy function:

def f(x):
    if 0 < x + 2:
        return "hello"
    else:
        return "goodbye"

For example, in our model, the function call f(1) evaluates as follows:

--> f(1)
--> { if 0 < 1 + 2:
         return "hello"
      else:
         return "goodbye" }
--> { if 0 < 3
         return "hello"
      else:
         return "goodbye" }
--> { if True
         return "hello"
      else:
         return "goodbye" }
-->  { return "hello" }
--> "hello"

While precise, these steps will obscure the broader argument we are trying to make for our program.

To make our program derivations more readable, we will use shorthand for this lab when evaluating function calls:

You are free to evaluate a function call directly to the returned expression that ultimately executed by the function.

If the statement-expression above came about from a function call, say f(1), we would write the evaluation of that call as:

     f(1) 
-->* "hello"

Skipping over the explicit execution of the statement-expression that the function call evaluates to in our model. We use the notation -->* (LaTeX: \longrightarrow^*, Unicode: ⟶*) to mean that multiple evaluation steps happened between the two lines of the derivation.

Be aware that whenever we skip steps, we introduce the possibility of making an error in our reasoning! So double-check your work whenever you skip steps in this manner!

Problem : Symbolic Reasoning with Xor

Consider the following definition of the boolean xor function:

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

Prove the following claims about this function:

~~~ admonish question title=”Claim (Xor can return true)” There exists a boolean b such that xor(True, b) ≡ True.

~~~ admonish question title="Claim (Xor cancellation)"
For any boolean `b`, `xor(b, b)` ≡ `False`.

~~~ admonish question title=”Claim (Xor equivalence)” For any pair of booleans b1 and b2, xor(b1, b2) ≡ and(or(b1, b2), not(and(b1, b2))).

For this final equivalence, you may evaluate individual calls to `and`, `or`, and `not`, in a single step of evaluation.


## Problem: Narrowing Down the Possibilities

Consider the following Python functions:

~~~python
def f1(name):
    if name == "Alice":
        return 0            # Point A
    elif name == "Bob":
        return 1            # Point B
    elif name == "Carol":
        return 2            # Point C
    elif name != "Daniel":
        return 3            # Point D
    elif name != "Emily":
        return 4            # Point E

def f2(x, y):
    if y >= 1:
        return 0            # Point A
    elif x >= 1: 
        return 1            # Point B
    elif x == -1:
        return 2            # Point C
    elif x <= -5 or y >= 3:
        return 3            # Point D
    elif x == 0:
        return 4            # Point E
    elif x == y:
        return 5            # Point F

For each of the functions:

1. Identify the types of each of the parameters
2. Describe the set of assumptions we know are true about the parameters inside each branch at each labeled point, i.e., when that branch’s guard is True.
3. Are each of the conditionals exhaustive? If not, describe what values are not covered by the if-else statements.

Problem: Capture

Consider the following Python function that computes a report for a student given their current grades in a course:

def report(hw_avg, quiz1, quiz2, quiz3):
    if hw_avg > 90 and quiz1 > 90 and quiz2 > 90 and quiz3 > 90:
        return "excelling"
    elif: hw_avg > 75 and quiz1 <= quiz2 and quiz2 <= quiz3:
        return "progressing"
    elif: hw_avg < 60 or quiz1 < 60 or quiz2 < 60 or quiz3 < 60:
        return "needs help"
    else:
        return "just fine"

1. Describe the preconditions (both in terms of types and general constraints) on the parameters.
2. Describe the conditions under which report(hw_avg, quiz1, quiz2, quiz3) will return "just fine". Describe them in terms of properties that ought to hold on each parameter to the function.
3. Are there any conditions under which the function reports an inappropriate string, given the arguments and your interpretation of the function’s intended behavior?

Problem: Looking Ahead

In this problem, we’ll motivate our discussion for next period on recursion and induction. Consider the standard append function for lists.

# Our standard list helper functions...
def is_empty(l):
    return len(l) == 0

def head(l):
    return l[0]

def tail(l):
    return l[1:]

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

def append(l1, l2):
    if is_empty(l1):
        return l2
    else:
        return cons(head(l1), append(tail(l1), l2))

Part 1: Simple Reasoning About Append

While the function is recursive, our substitutive model of computation is capable of modeling the behavior of this function. Thus, we can prove properties about append just like any other function. Prove this one as an exercise:

~~~admonish problem title=”Claim (Nil is an Identity on the Left)” For any list l, append([], l) ≡ l.

### Part 2: (Not) Commutativity

We say that an operation is _commutative_ if we can swap the order of the objects involved, _i.e._, if x ≡ y then y ≡ x and vice versa.
This is true for some operations, _e.g._, integers and addition, but not other, _e.g._, integers and subtraction.
It turns out that `append` is not commutative for lists!
Prove this fact by way of a counterexample:

~~~admonish problem title="Claim (Append is Not Commutative)"
There exists lists `l1` and `l2` such that `append(l1, l2)` \\( \not\equiv \\) `append(l2, l1)`.

Part 3: A Humble Attempt

Because append is not commutative, this means that just because the empty list is an identity on the left-hand side of the function, it is not necessarily an identity on the right-hand side. With a little bit of thought, though, we can convince ourselves this ought to be the case. However, proving this fact is deceptively difficult! Attempt to prove this claim:

~~~admonish problem title=”Claim (Nil Is An Identity on the Right)” For any list l, append(l, []) ≡ l. ~~~

(Hint: you can perform case analysis on each new list you encounter in your proof, even the tail of the original list!)

At some point, you will get stuck, ideally at a point where you start seeing that your reasoning will go on infinitely. Check with an instructor that you have indeed gotten stuck at the “right point.”

Part 4: Reflection

Finally, reflect on your experience. Answering the following questions in a few sentences each:

• Why were you able to directly prove the left-identity claim?
• Why is the right-identity claim more difficult to prove?
• What information do you need in order to break the chain of infinite reason that you found in the previous proof?