*Note*: for each reading, you will need to complete a few
exercises These *daily drills* are exercises marked with a double
dagger, **‡**. There are two in this reading, *concrete
equivalences* and *quantified propositions*. You can submit
your answers via plaintext to Gradescope.

Don’t worry if you feel like you didn’t get the right answer for the
daily drills! It is more important that you put in the effort,
*e.g.*, 10 minutes trying out each of the problems, and that you
come to class with any questions about the content and the drills.

# Propositions and Proofs

Our formal model of computation allows us to reason about the
behavior of programs. But to what ends can we apply this reasoning?
Besides merely checking our work, we can also use our formal model to
*prove propositions* about our programs.

**Proposition**: a proposition is an assertion or
statement, potentially provable.

Another word for a proposition is a *claim*. Here are some
example propositions over programs that we could consider:

`len('hello world!')`

is equivalent to`12`

.- There exists a list
`l`

for which`len(l)`

is`0`

. `insertion_sort(l)`

performs more comparison operations than`mergesort(l)`

for any list`l`

.- For any number
`n`

,`2 * n`

is greater than`n`

.

The first proposition is a *fully concrete* proposition of the
sort we have previously considered. The second is an *abstract*
proposition because it involves a variable, here `l`

.

Ultimately, the first two propositions involve equivalences between expressions. But propositions do not need to be restricted to equivalences. The third proposition talks about the number of operations that one expression performs relative to another.

Furthermore, propositions don’t even need to be provable! For
example, the final proposition is not provable. A
*counterexample* to this proposition arises when we consider
`n = -1`

. `2 * -1`

evaluates to `-2`

,
and `-2`

is not greater than `-1`

!

**“True” versus “Provable”**: in our discussion of logic
and its applications to program correctness, we will need to discuss
both *boolean expressions* as well as propositions. There exist
commonalities between both—they involve truth and falseness. However,
booleans exist *inside* our model, *i.e.*, at the level of
programs. Propositions exist *outside* of the model as they
ultimately are statements *about* the model.

To distinguish between the two, we’ll use the terms `True`

and `False`

when discussing booleans and “provable” and
“refutable” when discussing propositions. We should think of boolean
expressions as *evaluating* to `True`

or
`False`

. In contrast, we will employ *logical
reasoning* to show that a proposition is provable or refutable.

## Equivalences Between Expressions

Of the many sorts of propositions possible, we will work exclusively
with *equivalences* in our discussion of program correctness.

**Program Equivalence**: two expressions \(e_1\) and \(e_2\) are equivalent, written \(e_1 \equiv e_2\) (LaTeX:
`\equiv`

, Unicode: ≡) if \(e_1
\longrightarrow^* v\) and \(e_2
\longrightarrow^* v\).

Recall that \(e \longrightarrow
e'\) (“steps to”, LaTeX: `\longrightarrow`

) means
that the (Python) expression \(e\)
takes a single step of evaluation to \(e'\) in our mental model of
computation. The notation \(e
\longrightarrow^* e'\) (“evaluates to”, LaTeX:
`\longrightarrow^*`

) means that \(e\) takes *zero or more steps* to
arrive at \(e'\). With this in
mind, the formal definition of equivalence amounts to saying the
following:

Two expressions are equivalent if they evaluate to

identicalvalues.

Thus, we can prove a claim of program equivalence by using our mental
model to give a step-by-step derivation (an *execution trace*) of
an expression to a final value. If both sides of the equivalence
evaluate to the same value, then we know they are equivalent by our
definition! The execution trace itself is a *proof* that the
equivalence holds.

For example, consider the following recursive definition of
`factorial`

:

```
def factorial(n):
if n == 0:
return 1
else:
return n * factorial(n-1)
```

and subsequent claim about its behavior:

**Claim**: `factorial(3)`

\(\equiv\) `6`

.

We can prove this claim by evaluating the left-hand side of the equivalence and observing that it is identical to the right-hand side:

*Proof*. The left-hand side expression evaluates as
follows:

```
3)
factorial(--> [[
if 3 == 0:
return 1
else:
return 3 * factorial(3-1)
]]--> [[
if False:
return 1
else:
return 3 * factorial(3-1)
]]--> [[
return 3 * factorial(3-1)
]]--> [[
return 3 * factorial(2)
]]--> [[ return 3 * [[
if 2 == 0:
return 1
else:
return 2 * factorial(2-1)
]]
]]--> [[ return 3 * [[
if False:
return 1
else:
return 2 * factorial(2-1)
]]
]]--> [[ return 3 * [[
return 2 * factorial(2-1)
]]
]]--> [[ return 3 * [[
return 2 * factorial(1)
]]
]]--> [[ return 3 * [[ return 2 * [[
if 1 == 0:
return 1
else:
1 * factorial(1-1)
]]
]]
]]--> [[ return 3 * [[ return 2 * [[
if False:
return 1
else:
return 1 * factorial(1-1)
]]
]]
]]--> [[ return 3 * [[ return 2 * [[
return 1 * factorial(1-1)
]]
]]
]]--> [[ return 3 * [[ return 2 * [[
return 1 * factorial(0)
]]
]]
]]--> [[ return 3 * [[ return 2 * [[ return 1 * [[
if 0 == 0:
return 1
else:
return 0 * factorial(0-1)
]]
]]
]]
]]--> [[ return 3 * [[ return 2 * [[ return 1 * [[
if True:
return 1
else:
return 0 * factorial(0-1)
]]
]]
]]
]]--> [[ return 3 * [[ return 2 * [[ return 1 * [[ return 1 ]] ]] ]] ]]
--> [[ return 3 * [[ return 2 * [[ return 1 * 1 ]] ]] ]]
--> [[ return 3 * [[ return 2 * [[ return 1 ]] ]] ]]
--> [[ return 3 * [[ return 2 * 1 ]] ]]
--> [[ return 3 * [[ return 2 ]] ]]
--> [[ return 3 * 2 ]]
--> [[ return 6 ]]
--> 6
```

Whew! This precise step-by-step analysis of the behavior of the expression rigorously proves our claim!

## Formatting Proofs

We will use this standard format for writing formal proofs for the remainder of the course. In summary, we write:

**Claim**: *(The claim to be proven)*

*Proof*. *(The proof of the claim)*

In LaTeX, the `\begin{proof} ... \end{proof}`

environment
is used to typeset proofs. Additionally, in our lab `.tex`

files, we define the `\begin{claim} ... \end{claim}`

with the
`amsthm`

package to typeset claims. Here is a LaTeX template
that uses these environments that you can use to achieve the desired
effect:

```
\begin{claim}
% The claim to be proven
\end{claim}
\begin{proof}
% The proof of the claim
\end{proof}
```

**Exercise (concrete equivalences, ‡)**: Prove the
following claim over concrete expressions:

**Claim**: `1 + 2 + 3`

\(\equiv\)
`(3 * (3 + 1)) / 2`

.

Write our your proof in the format described above.

# Symbolic Execution

Previously, we introduced a model of computation for the Python
programming language. This model allows us to prove program properties
when concrete values are involved. However, we frequently wish to prove
properties where the values are *unknown*. For example, we might
consider a proposition about appending two lists which is accomplished
via the `+`

operator:

For all lists

`l1`

and`l2`

,`len(l1) + len(l2)`

=`len(l1 + l2)`

This proposition ranges over *unknown*, rather than concrete,
lists. We, therefore, need to upgrade our mental model to work with
these unknown quantities.

## Abstract Propositions

Up to this point, we have considered concrete expressions,
*i.e.*, expressions that do not contain variables. What happens
if we allow expressions to contain variables. As an example, consider
the following implementation of boolean `and`

:

```
# N.B. non-short-circuiting version of `and`
def my_and(b1, b2):
if b1:
return b2
else:
return False
```

Now, let’s consider the following equivalence claim:

**Claim**: `my_and(True, b)`

≡
`False`

Here, `b`

is a variable, presumed to be of boolean type.
However, how do we interpret `b`

? It turns out there are two
interpretations we might consider:

- Does there
*exist*a boolean value to`b`

so that the proposition is provable? - Is the proposition provable
*for all*possible boolean values that`b`

can take on?

The former interpretation is called an *existential
quantification* of `b`

. We alternatively say that
`b`

is existentially quantified or is an “existential.”
*Quantification* refers to the fact that our interpretation tells
us “how many” values of `b`

to consider in the proposition.
In existential quantification, we consider a single value.

In contrast, the latter interpretation is called a *universal
quantification* of `b`

. In universal quantification, we
mean that the proposition holds for all possible values of
`b`

. Note that the above proposition is provable if
`b`

is interpreted existentially: if we let `b`

be
`#f`

then:

```
True, b)
my_and(True, False)
≡ my_and(
≡ [[if True:
return False
else:
return False
]]--> [[ return False ]]
--> False
```

However, the proposition does not hold when `b`

is
universally quantified. More specifically, while it holds when
`b`

is `False`

, it does not hold when
`b`

is `True`

.

```
True, b)
my_and(True, True)
≡ my_and(
≡ [[if True:
return True
else:
return False
]]--> [[ return True ]]
--> True
```

Because of this, we must be explicit when introducing variables into
our proposition. For each such variable, we must *declare*
whether it is existentially quantified and universally quantified. To do
so, we can use the words:

*For all*for universal quantification,*e.g.*, “for all lists`l`

\(\ldots\)” and*There exists*for existential quantification,*e.g.*, “there exists a number`n`

…”.

Furthermore, we reason about the variable differently depending on its quantification, as we see in the following sections.

**Exercise (Quantified Propositions)**: write down an
additional *existential* and *universal* claim involving
the `my-and`

function.

## Existential Propositions

If a variable \(x\) appears as an
existential in a proposition, we interpret that variable as: *there
exists* a value for \(x\) such that
the proposition holds. In other words, the proposition is provable if we
can give a *single value* to substitute for \(x\) so that the resulting proposition is
provable. Thus, to prove an existential claim, we can choose such a
value, substitute for the existential variable, and then use concrete
evaluation as before.

As an example, let’s formally prove the existential version of the
`my_and`

claim that we introduced above:

**Claim**: there exists a boolean `b`

such
that `my_and(True, b)`

≡ `False`

.

*Proof*. Let `b`

be `False`

. Then we
have:

```
True, False)
my_and(--> [[
if True:
return False
else:
return False
]]--> [[ return False ]]
--> False
```

Note how our proof has changed now that our proposition is abstract:

- In our claim, we explicitly quantify the variable
`b`

by declaring it existential by using “there exists” to describe it. - In our proof, we explicitly
*choose*a value for the existentially quantified variable (“Let`b`

be`False`

”).

We can also existentially quantify over multiple variables. In these situations, we provide instantiations for each variable but otherwise proceed as normal.

For example, consider the following function that compares two numbers:

```
def compare_score(s1, s2):
if s1 > s2:
return 's1 wins!'
else:
return 's2 wins!'
```

**Claim**: There exists numbers `x`

and
`y`

such that `compare_score(x, y)`

≣
`'s2 wins!`

*Proof*. Let `s1`

= `0`

and
`s2`

= `1`

.

```
0, 1)
compare_score(--> [[
if 0 > 1:
return 's1 wins!'
else:
return 's2 wins!'
]]--> [[
if False:
return 's1 wins!'
else:
return 's2 wins!'
]]--> [[ return 's2 wins!' ]]
--> 's2 wins!'
```

**Exercise (Alternative Instantiations)**: revise the
proof of `compare_score`

above by choosing *alternative
instantiations* for `s1`

and `s2`

and deriving
an alternative execution trace for the expression.

## Universal Quantification

When a variable is universally quantified, it stands for *any
possible* value. Let’s take a look at a simple squaring
function:

```
def square(n):
return n * n
```

And a simple universal claim about this function:

**Claim**: for all numbers `n`

,
`square(n)`

≡ `n * n`

Because the claim holds for all possible values of `n`

, we
can’t *choose* an `n`

like with existentials. Instead,
we must *hold n abstract*,

*i.e.*, consider it to be an arbitrary number, and then proceed with the proof. In effect, because

`n`

is universally quantified, we treat
`n`

like a constant, yet unknown, quantity in our
reasoning.**Variables versus Unknown Constants**: it may seem
pedantic to distinguish between a variable and a constant of unknown
quantity. However, there a subtle yet essential difference between the
two concepts. A variable is an object in a proposition that must be
*quantified* to give it meaning. An unknown constant already has
meaning—it is known to be a single value. However, we don’t assume
anything about the variable’s identity beyond what we already know,
*e.g.*, whether it is a list or a number.

When we use our mental model of computation, we immediately arrive at
a problem: both `square(n)`

and `n * n`

cannot
take any evaluation steps! `square(n)`

cannot step because
`n`

needs to be a value before we perform the function
application, and we said that values were numbers, boolean constants, or
lambdas. `n * n`

cannot step because since we don’t know what
`n`

is, we don’t know what concrete value the multiplication
will produce. We say that both expressions are *stuck*: they are
not values, but they cannot take any additional evaluation steps.

We can’t reconcile the `n * n`

case. Without knowing what
`n`

is, we cannot carry out the multiplication. However, if
we treat the constant-yet-unknown `n`

as a *value*,
then we can proceed with the function application. Furthermore, when we
reach the `return`

statement, we can simply return the stuck
evaluation as the result of the function call instead of trying to
evaluate it to a value first!

```
square(n)--> [[ return n * n ]]
--> n * n
```

Even though the left- and right-hand sides of the equivalence are not values, they are identical. This fact is sufficient to conclude that the two original expressions are equivalent according to our definition of program equivalences! Let’s put these ideas together into a complete proof of the proposition:

**Claim**: for all numbers `n`

,
`square(n)`

≡ `n * n`

.

*Proof*. Let `n`

be an arbitrary number. Then the
left-hand side of the equivalence simplifies as follows:

```
square(n)--> [[ return n * n ]]
--> n * n
```

Which is identical to the right-hand side.

In summary, when we encounter a universally quantified variable in a proposition, we:

- Consider the variable to be a constant, yet unknown value. For convenience, we keep the name of this constant to be the same as the (universally quantified) variable, but we understand that the two are different objects!
- When reasoning about the constant, we assume that it is a value for the purposes of our mental model of computation.

## Case Analysis

Sometimes when we work with universally quantified variables, we can get away without thinking about their actual values. However, more often or not, our reasoning must consider their possible values. This reasoning will ultimately depend on the types of values involved, and this is where our proofs get more intricate in their design!

As an introduction to these concepts, let’s consider the case where
we know the type in question only allows for a *finite set of
values*. At present, only the *boolean type* has this
property. Booleans only allow for two values, `True`

and
`False`

, whereas there are an infinite number of numbers and
functions to choose from!

To see how we can take advantage of the finiteness of the boolean
type in our proofs, let’s consider the following simple claim, again
using the `my_and`

function:

**Claim**: for all booleans `b`

,
`my_and(b, False)`

≡ `False`

.

If we let `b`

be arbitrary, we can begin evaluating the
left-hand expression.

```
False)
my_and(b, --> [[
if b:
return False
else:
return False
]]
```

We can see pretty readily that no matter how the conditional
evaluates, we will return `False`

. Be careful, though; this
intuition is not sufficient for formal proof! We must instead rely on
our evaluation model directly to ultimately show that this intuition is
correct. However, if `b`

is unknown, we don’t know which
branch the conditional will produce.

Thankfully, we assumed that `b`

was a boolean, so it must
either be `True`

or `False`

. Therefore, we can
proceed by *case analysis*: we will consider two separate cases,
`b`

is `True`

and `b`

is
`False`

, and show that the claim holds in *both*
cases. If the claim holds for both cases, we know that the claim holds
for *every possible value of b* and, thus, have
completed the proof.

*Proof*. Let `b`

be an arbitrary boolean. The
left-hand side of the equivalence evaluates as follows:

```
False)
my_and(b, --> [[
if b:
return False
else:
return False
]]
```

Because `b`

is a boolean, either `b`

is
`True`

or `b`

is `False`

.

. Then:`b`

is`True`

`--> [[ if True: return False else: return False ]]--> [[ return False ]] --> False`

. Then:`b`

is`#f`

`--> [[ if False: return False else: return False ]]--> [[ return False ]] --> False`

In both cases, the left-hand side steps to `False`

,
precisely the right-hand side of the equivalence.

**Typesetting Cases**: when performing a case analysis,
it is imperative to state the proof’s different cases explicitly. To
format this in LaTeX, use a bulleted lists, *e.g.*,

```
\verb|b| is a boolean, either \verb|b| is \verb|True| or \verb|b| is \verb|#f|.
Because
\begin{itemize}
\item \textbf{\verb|b| is \verb|True|}. Then:
\begin{verbatim}
--> [[
if True:
return False
else:
return False
]]
--> [[ return False ]]
--> False
\end{verbatim}
\item \textbf{\verb|b| is \verb|False|}. Then:
Then:\begin{verbatim}
--> [[
if False:
return False
else:
return False
]]
--> [[ return False ]]
--> False
\end{verbatim}
\verb|#f|, precisely the right-hand side of the equivalence. In both cases, the left-hand side steps to
```

Note how I bold each case at the start of the bullet to clearly separate the statement of the case from the subsequent proof.

**Exercise (Order of Reasoning)**: in the previous
proof, we performed the case analysis on `b`

*after*
partially evaluating `my_and`

. Rewrite the proof so that the
case analysis happens *before* any evaluation occurs.

**Exercise (Quantified Propositions, ‡)**: consider the
following Python definition of the boolean disjunction, `or`

,
function:

```
def my_or(b1, b2):
if b1:
return True
else:
b2
```

Prove the following claims over this function:

**Claim 1**: there exists booleans`b1`

and`b2`

such that`my_or(b1, b2)`

≡`False`

.**Claim 2**: for all booleans`b`

,`my_or(b, True)`

≡`True`

.