CMSC 27100 — Lecture 4

We want to prove the following proposition.

For all strings $\mathbf u$ and $\mathbf v$, $|\mathbf u \cdot \mathbf v| = |\mathbf u| + |\mathbf v|$.

Division

Now, we'll take a trip back to grade school and think about division again. When we divide two integers, we may not get an integer as a result. That is, the integers may not divide evenly. So we either give up or keep working with the rational number that we get.

However, there is a way to define a notion of division for integers that produces integers in a meaningful way. Recall that if we divide two numbers $a$ by $b$, if $a$ is a multiple of $b$ (if $b \mid a$), we get an integer $q$ which we call the quotient. But if $a$ isn't a multiple of $b$, we get a remainder $r$.

The following theorem, the Division Theorem, formally states that whenever we divide two numbers $a$ and $b$, we will always be able to "get" the integers $q$ and $r$ (they exist) and that they're unique (that when we do division we always get the same answer).

For all integers $n$ and $d \gt 0$, there exist unique integers $q$ and $r$ such that $n = d \cdot q + r$ and $0 \leq r \lt d$.

What might this theorem look like in first-order logic? \[\forall n,d (d \gt 0 \rightarrow \exists q,r (n = d \cdot q + r \wedge 0 \leq r \wedge r \lt d)).\] Here's an example of how to express the idea that you only want to consider certain elements of the domain. Many mathematicians would write something like $\forall n, d \gt 0$ as shorthand, but here, we write more formally that we consider all $n$ and $d$ and condition the rest of the statement on $d \gt 0$. This is exactly what we're saying when we say "for all integers $d \gt 0$", that we really care about integers $d$ if they are greater than 0.

Now, this is not quite what we want since we only state that $q$ and $r$ exist. How do we express the idea that they are unique—that they're the only elements in our domain for which this property holds?

Suppose we have $P(x)$ and we want to argue that there is only one element for which $P(x)$ holds. We may jump to trying to show that this has to be the case, but that's not where we're headed yet. All we want to do is express this idea.

One way to think about this is to consider the question of what happens if there is an element, say $y$, such that $P(y)$ holds. Well, if $x$ is really unique, then it has to be the case that $y$ is really $x$. So our expression looks like the following: \[\exists x (P(x) \wedge \forall y (P(y) \rightarrow x = y)).\]

This says that there exists an element $x$ such that $P(x)$ holds and if $P(y)$ holds for any $y$, it must be the case that $x = y$.

This means that to prove this theorem, we can break it down into two steps:

1. showing that the appropriate integers $q$ and $r$ exist (this is proving $P(x)$ holds in the above formula), and then
2. showing that these $q$ and $r$ are unique (this is proving $\forall y(P(y) \rightarrow x = y)$).

So first, we need to show that these integers exist. This means we need to exhibit such integers. The obvious way to do this is to show how to find them. We will devise an algorithm for computing $q$ and $r$. Such a proof is also called a constructive proof, since we show how to "construct" the object we're trying to prove exists.

Existence

First, we'll need the following definition.

The function $\operatorname{divmod} : \mathbb N \times \mathbb N \rightarrow \mathbb N \times \mathbb N$ is defined inductively on $n$ by: \begin{align*} \operatorname{divmod}(0,d) &= (0,0) \\ \operatorname{divmod}(n+1,d) &= \begin{cases} (q', r' + 1) & \text{if $r'+1 \neq d$, where $(q',r') = \operatorname{divmod}(n,d)$,} \\ (q' + 1, 0) & \text{otherwise.} \end{cases} \end{align*}

This looks complicated, but we can easily turn it into a fairly simple function:

def divmod(n: int, d: int) -> tuple[int,int]:
    if n == 0:
        return (0,0)
    else:
        (q1,r1) = divmod(n-1,d)
        if r1 + 1 != d:
            return (q1, r1 + 1)
        else:
            return (q1 + 1, 0)

We can try to trace through the code here to see what is being computed. Observe that in the recursive case, $n$ ever only decreases by one and both $q$ and $r$ increase by one. So what's going on here? Basically, this algorithm counts down from $n$, increasing the remainder counter $r$. If $r$ ever hits $d$, we know that we've counted a multiple of $d$, so we increase our quotient counter $q$ by one and reset $r$ to 0.

Note that divmod is a built-in function. Helpfully, the Python documentation tells us that the result of divmod(n,d) is supposed to be (n // d, n % d), which is what we want. Of course, the difficult part is proving that this is the case. Like many algorithms you'll prove correctness for in the future, this will be done by induction.

For all natural numbers $n$ and $d$, if $\operatorname{divmod}(n,d) = (q,r)$, then $n = q \cdot d + r$ with $d \neq 0$ and $r \lt d$.

This gets us almost all the way there, except that we've only defined $\operatorname{divmod}$ on $\mathbb N$. Since the claim of the Division Theorem is for integers, we will need to somehow extend our definition to $\mathbb Z$.

To see how to do this, we consider an integer $n$ that isn't a natural number. Then $-n$ is a natural number and we have that $-n = q \cdot d + r$ by what we've just proved. This gives us $n = -q \cdot d - r$. Now, we need to make the remainder a positive integer between $0$ and $d$. We can do this simply by adding $d$ to it: \[-q \cdot d - r = (-q-1) \cdot d + (d-r).\] So we have for $n \lt 0$ that $\operatorname{divmod}(n,d) = (-q-1, d-r)$ where $-n = q \cdot d + r$.