# Subtraction

Posted on 2017-04-02 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Minus
( minus, _test_minus, main_minus
) where

import Testing
import Booleans
import And
import DisjointUnions
import NaturalNumbers
import BailoutRecursion
import Plus
import Times

We’d eventually like to solve some equations; for instance, one of the simplest equations we can construct with the tools we have so far is $\nplus(a,x) = b$ where $$a$$ and $$b$$ are in $$\nats$$. Putting on our third-grader hat of course the solution to $$b = a+x$$ is $$x = b-a$$. So we’ll call this solution “b minus a”. Our goal in this post is to give a constructive characterization for subtraction.

There’s a hitch: whereas sums and products of natural numbers always exist, differences do not; $$5 - 2 = 3$$ is a natural number, but $$5 - 7 = ?$$ is not. So the signature of minus cannot be $$\nats \times \nats \rightarrow \nats$$. What is it then? How should we handle this?

I can think of three options. First, we can just declare that $$b-a$$ is not defined if the difference is not a natural number. The corresponding algorithm would then just error out. This should be avoided if possible.

The second option is to implement so-called truncated subtraction, so that anytime $$b-a$$ is not a natural number we simply call it 0. This also is not ideal, since now $$b-a$$ always exists, but the equation $$b = a + (b-a)$$ is no longer an identity and we cannot tell just from the value of $$b-a$$ whether it holds or not.

The third option is a blend of the first two. We can attach an extra element to $$\nats$$, say $$\ast$$, and then say $$b-a = \ast$$ if $$b-a$$ is not a natural number. This allows us to distinguish when $$b-a$$ does not exist but keeps the minus function total. So our signature for minus will be $\nats \times \nats \rightarrow 1 + \nats,$ where $$1 = \{\ast\}$$.

Define maps $$\varphi : \nats \rightarrow 1 + \nats$$ by $\varphi(x) = \left\{\begin{array}{ll} \rgt(\zero) & \mathrm{if}\ x == \zero \\ \lft(\ast) & \mathrm{otherwise}; \end{array}\right.$ $$\beta : \nats \times \nats \rightarrow \bool$$ by $\beta(a,b) = \left\{\begin{array}{ll} \btrue & \mathrm{if}\ b = \zero \\ \bfalse & \mathrm{otherwise}; \end{array}\right.$ $$\psi : \nats \times \nats \rightarrow 1 + \nats$$ by $\psi(a,b) = \rgt(\next(a));$ and $$\omega : \nats \times \nats \rightarrow \nats$$ by $\omega(a,b) = \prev(b).$

Now define $$\nminus : \nats \times \nats \rightarrow 1 + \nats$$ by $\nminus = \bailrec(\varphi)(\beta)(\psi)(\omega).$

minus :: (Natural n) => n -> n -> Union () n
minus = bailoutRec phi beta psi omega
where
phi x = if isZero x
then rgt zero
else lft ()

beta _ b = isZero b

psi a _ = rgt (next a)

omega _ b = prev b

Woo! Since $$\nminus$$ is defined in terms of bailout recursion, it is the unique solution to a system of functional equations.

$$\nminus$$ is the unique map $$f : \nats \times \nats \rightarrow 1 + \nats$$ with the property that for all $$a,b \in \nats$$, we have $\left\{\begin{array}{l} f(\zero,b) = \bif{\iszero(b)}{\rgt(\zero)}{\lft(\ast)} \\ f(\next(a),b) = \bif{\iszero(b)}{\rgt(\next(a))}{\nminus(a,\prev(b))}. \end{array}\right.$

_test_minus_zero_left :: (Natural n, Equal n)
=> n -> Test (n -> Bool)
_test_minus_zero_left _ =
testName "minus(0,b) == if(isZero(b),rgt(0),lft(*))" $\b -> if eq (isZero b) true then eq (minus zero b) (rgt zero) else eq (minus zero b) (lft ()) _test_minus_next_left :: (Natural n, Equal n) => n -> Test (n -> n -> Bool) _test_minus_next_left _ = testName "minus(next(a),b) == if(isZero(b),rgt(next(a)),minus(a,prev(b)))"$
\a b -> if eq (isZero b) true
then eq (minus (next a) b) (rgt (next a))
else eq (minus (next a) b) (minus a (prev b))

Here are some special cases:

For all $$n \in \nats$$ we have the following.

1. $$\nminus(n,\zero) = \rgt(n)$$.
2. $$\nminus(\zero,\next(n)) = \lft(\ast)$$.
1. If $$n = \zero$$, then $\begin{eqnarray*} & & \nminus(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#cor-minus-up-zero} = & \bif{\iszero(\zero)}{\rgt(\zero)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-zero} = & \bif{\btrue}{\rgt(\zero)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \rgt(\zero) \end{eqnarray*}$ as claimed. If $$n = \next(m)$$, we have $\begin{eqnarray*} & & \nminus(\next(m),\zero) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#cor-minus-up-next} = & \bif{\iszero(\zero)}{\rgt(\next(m))}{\nminus(m,\prev(\zero))} \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-zero} = & \bif{\btrue}{\rgt(\next(m))}{\nminus(m,\prev(\zero))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \rgt(\next(m)) \end{eqnarray*}$ as claimed.
2. We have $\begin{eqnarray*} & & \nminus(\zero,\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#cor-minus-up-zero} = & \bif{\iszero(\next(n))}{\rgt(\zero)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-next} = & \bif{\bfalse}{\rgt(\zero)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \lft(\ast) \end{eqnarray*}$ as claimed.
_test_minus_nat_zero :: (Natural n, Equal n)
=> n -> Test (n -> Bool)
_test_minus_nat_zero _ =
testName "minus(n,0) == rgt(n)" $\n -> eq (minus n zero) (rgt n) _test_minus_zero_next :: (Natural n, Equal n) => n -> Test (n -> Bool) _test_minus_zero_next _ = testName "minus(0,next(n)) == lft(ast)"$
\n -> eq (minus zero (next n)) (lft ())

We can “cancel” $$\next$$s on both arguments of a $$\nminus$$.

Let $$a,b \in \nats$$. Then we have $\nminus(\next(b),\next(a)) = \nminus(b,a).$

We have $\begin{eqnarray*} & & \nminus(\next(b),\next(a)) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#cor-minus-up-next} = & \bif{\iszero(\next(a))}{\rgt(\next(b))}{\nminus(b,\prev(\next(a)))} \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-next} = & \bif{\bfalse}{\rgt(\next(b))}{\nminus(b,\prev(\next(a)))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \nminus(b,\prev(\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-prev-next} = & \nminus(b,a) \end{eqnarray*}$ as claimed.

_test_minus_next_next :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_minus_next_next _ =
testName "minus(next(b),next(a)) == minus(b,a)" $\a b -> eq (minus (next b) (next a)) (minus b a) Another important special case. Let $$a \in \nats$$. Then we have $\nminus(a,\next(a)) = \lft(\ast).$ We proceed by induction on $$a$$. For the base case $$a = \zero$$ we have $\begin{eqnarray*} & & \nminus(\zero,\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-zero-next} = & \lft(\ast) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$a$$; now $\begin{eqnarray*} & & \nminus(\next(a),\next(\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-cancel} = & \nminus(a,\next(a)) \\ & \hyp{\nminus(a,\next(a)) = \lft(\ast)} = & \lft(\ast) \end{eqnarray*}$ as needed. _test_minus_nat_next :: (Natural n, Equal n) => n -> Test (n -> Bool) _test_minus_nat_next _ = testName "minus(a,next(a)) == lft(*)"$
\a -> eq (minus a (next a)) (lft ())

The next result shows that $$\nminus$$ gives a solution to the equation $$b = \nplus(a,x)$$.

Let $$a,b,c \in \nats$$. Then the following are equivalent.

1. $$\nminus(b,a) = \rgt(c)$$.
2. $$b = \nplus(a,c)$$.

First we show (1) implies (2) by induction on $$b$$. For the base case, suppose we have $$\nminus(\zero,a) = \rgt(c)$$. Now $\begin{eqnarray*} & & \rgt(c) \\ & \hyp{\nminus(\zero,a) = \rgt(c)} = & \nminus(\zero,a) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#cor-minus-up-zero} = & \bif{\iszero(a)}{\rgt(\zero)}{\lft(\ast)} \end{eqnarray*}$ as needed. If $$\iszero(a) = \bfalse$$, we have $$\rgt(c) = \lft(\ast)$$, which is absurd. So $$\iszero(a) = \btrue$$, and thus $$a = \zero$$, and moreover $$\rgt(c) = \rgt(\zero)$$, so $$c = \zero$$. Then $$\zero = \nplus(a,c)$$ as needed. For the inductive step, suppose the result holds for all $$a$$ and $$c$$ for some $$b$$, and suppose further that $$\nminus(\next(b),a) = \rgt(c)$$. If $$a = \zero$$, we have $\begin{eqnarray*} & & \rgt(c) \\ & \hyp{\nminus(\next(b),a) = \rgt(c)} = & \nminus(\next(b),\zero) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-nat-zero} = & \rgt(\next(b)) \end{eqnarray*}$ so that $$\next(b) = c = \nplus(c,\zero)$$ as needed. Suppose instead that $$a = \next(d)$$ for some $$d$$. Now $\begin{eqnarray*} & & \rgt(c) \\ & \hyp{\nminus(\next(b),a) = \rgt(c)} = & \nminus(\next(b),a) \\ & \hyp{a = \next(d)} = & \nminus(\next(b),\next(d)) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-cancel} = & \nminus(b,d) \end{eqnarray*}$ and thus $$\nplus(d,c) = b$$. But then $\begin{eqnarray*} & & \next(b) \\ & \hyp{b = \nplus(d,c)} = & \next(\nplus(d,c)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \nplus(\next(d),c) \\ & \hyp{a = \next(d)} = & \nplus(a,c) \end{eqnarray*}$ as needed.

Next we show that (2) implies (1) by induction on $$a$$. For the base case $$a = \zero$$, if $$b = \nplus(a,c) = c$$ then $$\nminus(b,\zero) = b = c$$ as needed. For the inductive step, suppose the implication holds for all $$b$$ and $$c$$ for some $$a$$. In particular, if $$\nplus(a,c) = b$$, then $$\nminus(b,a) = \rgt(c)$$. Suppose further that $$b = \nplus(\next(a),c)$$. Now $$b = \next(\nplus(a,c)) = \next(d)$$ for some $$d$$, where $$\nminus(d,a) = \rgt(c)$$. Then we have $\begin{eqnarray*} & & \nminus(b,\next(a)) \\ & \hyp{b = \next(\nplus(a,c))} = & \nminus(\next(\nplus(a,c)),\next(a)) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-cancel} = & \nminus(\nplus(a,c),a) \\ & \hyp{d = \nplus(a,c)} = & \nminus(d,a) \\ & \hyp{\nminus(d,a) = \rgt(c)} = & \rgt(c) \end{eqnarray*}$ as needed.

_test_minus_plus_equiv :: (Natural n, Equal n)
=> n -> Test (n -> n -> n -> Bool)
_test_minus_plus_equiv _ =
testName "(minus(b,a) == rgt(c)) == (plus(a,c) == b)" $\a b c -> eq (eq (minus b a) (rgt c)) (eq (plus a c) b) Now $$\nminus$$ inherits several properties from $$\nplus$$. For instance, $$\nminus$$ is cancellative. Let $$a,b,c \in \nats$$. Then the following are equivalent. 1. If $$\nminus(b,a) = \nminus(b,c)$$ and $$\isRgt(\nminus(b,a)) = \btrue$$, then $$a = c$$. 2. If $$\nminus(a,b) = \nminus(c,b)$$ and $$\isRgt(\nminus(a,b)) = \btrue$$, then $$a = c$$. 1. Say $\nminus(b,a) = \rgt(d) = \nminus(b,c).$ Now $\nplus(a,d) = b = \nplus(c,d)$ and thus $$a = c$$ as claimed. 2. Say $\nminus(a,b) = \rgt(d) = \nminus(c,b).$ Now $a = \nplus(b,d) = c$ as claimed. _test_minus_cancellative_left :: (Natural n, Equal n) => n -> Test (n -> n -> n -> Bool) _test_minus_cancellative_left _ = testName "if minus(b,a) == minus(b,c) == rgt(d) then a == c"$
\a b c -> if and (eq (minus b a) (minus b c)) (isRgt (minus b a))
then eq a c
else true

_test_minus_cancellative_right :: (Natural n, Equal n)
=> n -> Test (n -> n -> n -> Bool)
_test_minus_cancellative_right _ =
testName "if minus(a,b) == minus(c,b) == rgt(d) then a == c" $\a b c -> if and (eq (minus a b) (minus c b)) (isRgt (minus a b)) then eq a c else true $$\nminus$$ “undoes” $$\nplus$$. Let $$a,b \in \nats$$. Then we have the following. 1. $$\nminus(\nplus(b,a),b) = \rgt(a)$$. 2. $$\nminus(\nplus(a,b),b) = \rgt(a)$$. 1. We have $$\nplus(b,a) = \nplus(b,a)$$, so that $$\nminus(\nplus(b,a),b) = \rgt(a)$$ as claimed. 2. We have $\nminus(\nplus(a,b),b) = \nminus(\nplus(b,a),b) = \rgt(a)$ as claimed. _test_minus_plus_right :: (Natural n, Equal n) => n -> Test (n -> n -> Bool) _test_minus_plus_right _ = testName "minus(plus(b,a),b) == rgt(a)"$
\a b -> eq (minus (plus b a) b) (rgt a)

_test_minus_plus_left :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_minus_plus_left _ =
testName "minus(plus(a,b),b) == rgt(a)" $\a b -> eq (minus (plus a b) b) (rgt a) We are able to rearrange $$\nminus$$ expressions (a little bit). Let $$a,b,c,d \in \nats$$. Then the following hold. 1. If $$\nminus(b,a) = \rgt(c)$$, then $$\nminus(\next(b),a) = \rgt(\next(c))$$. 2. If $$\nminus(b,a) = \rgt(c)$$, then $$\nminus(b,c) = \rgt(a)$$. 3. If $$\nminus(b,a) = \rgt(c)$$, then $$\nminus(\nplus(b,d),a) = \rgt(\nplus(c,d))$$. 1. Since $$\nminus(b,a) = \rgt(c)$$, we have $$\nplus(a,c) = b$$, so that $\nplus(a,\next(c)) = \next(\nplus(a,c)) = \next(b).$ Thus we have $\nminus(\next(b),a) = \rgt(\next(c))$ as claimed. 2. Since $$\nminus(b,a) = \rgt(c)$$, we have $$b = \nplus(a,c) = \nplus(c,a)$$, so that $$\nminus(b,c) = \rgt(a)$$ as claimed. 3. Suppose $$\nminus(b,a) = \rgt(c)$$; then $$b = \nplus(a,c)$$. Now $\nplus(b,d) = \nplus(\nplus(a,c),d) = \nplus(a,\nplus(c,d)),$ so that $\nminus(\nplus(b,d),a) = \rgt(\nplus(c,d))$ as claimed. _test_minus_next_left_cond :: (Natural n, Equal n) => n -> Test (n -> n -> Bool) _test_minus_next_left_cond _ = testName "if minus(b,a) == rgt(c) then minus(next(b),a) == rgt(next(c))"$
\a b -> case minus b a of
Right c -> eq (minus (next b) a) (rgt (next c))
Left () -> true

_test_minus_swap :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_minus_swap _ =
testName "if minus(b,a) == rgt(c) then minus(b,c) == rgt(a)" $\a b -> case minus b a of Right c -> eq (minus b c) (rgt a) Left () -> true _test_minus_plus :: (Natural n, Equal n) => n -> Test (n -> n -> n -> Bool) _test_minus_plus _ = testName "if minus(b,a) == rgt(c) then minus(plus(b,d),a) == rgt(plus(c,d))"$
\a b d -> case minus b a of
Right c -> eq (minus (plus b d) a) (rgt (plus c d))
Left () -> true

Given natural numbers $$a$$ and $$b$$, either $$\nminus(a,b)$$ or $$\nminus(b,a)$$ is of the form $$\rgt(c)$$ for some $$c$$.

Let $$a,b \in \nats$$. If $$\nminus(a,b) = \lft(\ast)$$, then $$\nminus(b,a) = \rgt(c)$$ for some $$c$$.

We proceed by induction on $$a$$. For the base case $$a = \zero$$, if $$\nminus(\zero,b) = \lft(\ast)$$ we have $$b \neq \zero$$ and $$\nminus(b,\zero) = \rgt(b)$$ as needed.

For the inductive step, suppose the implication holds for all $$b$$ for some $$a$$. Suppose further that $$\nminus(\next(a),b) = \lft(\ast)$$. If $$b = \zero$$, note that $$\nminus(\next(a),\zero) = \lft(\zero)$$ is false, so the implication holds vacuously. If $$b = \next(d)$$ for some $$d$$, then we have $\lft(\ast) = \nminus(\next(a),b) = \nminus(\next(a),\next(d)) = \nminus(a,d).$ By the induction hypothesis we have $\nminus(d,a) = \rgt(c)$ for some $$c$$, so that $\nminus(b,a) = \nminus(\next(d),a) = \rgt(\next(c))$ as needed.

_test_minus_flip :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_minus_flip _ =
testName "if minus(a,b) == lft(*) then isRgt(minus(b,a))" $\a b -> if eq (minus a b) (lft ()) then isRgt (minus b a) else true $$\ntimes$$ distributes over $$\nminus$$. Let $$a,b,c \in \nats$$. If $$\nminus(a,b) = \rgt(d)$$ for some $$d \in \nats$$, then $\nminus(\ntimes(c,a),\ntimes(c,b)) = \rgt(\ntimes(c,d)).$ We proceed by induction on $$a$$. For the base case $$a = \zero$$, suppose we have $$\nminus(\zero,b) = \rgt(d)$$; then $$d = \zero$$ and $$b = \zero$$. Now $\begin{eqnarray*} & & \nminus(\ntimes(c,a),\ntimes(c,b)) \\ & \let{a = \zero} = & \nminus(\ntimes(c,\zero),\ntimes(c,b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \nminus(\zero,\ntimes(c,b)) \\ & \let{b = \zero} = & \nminus(\zero,\ntimes(c,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \nminus(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-nat-zero} = & \rgt(\zero) \end{eqnarray*}$ and $\begin{eqnarray*} & & \rgt(\ntimes(c,d)) \\ & \let{d = \zero} = & \rgt(\ntimes(c,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \rgt(\zero) \end{eqnarray*}$ as claimed. For the inductive step, suppose the equality holds for some $$a \in \nats$$ and suppose that $$\nminus(\next(a),b) = \rgt(d)$$. Then we have $\begin{eqnarray*} & & \nminus(\ntimes(c,\next(a)),\ntimes(c,b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-next-right} = & \nminus(\nplus(\ntimes(c,a),c),\ntimes(c,b)) \\ & = & \nplus(\nminus(\ntimes(c,a),\ntimes(c,b)),c) \\ & = & \nplus(\ntimes(c,\nminus(a,b)),c) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-next-right} = & \ntimes(c,\next(\nminus(a,b))) \\ & = & \ntimes(c,\nminus(\next(a),b)) \end{eqnarray*}$ as needed. _test_minus_times_dist_left :: (Natural n, Equal n) => n -> Test (n -> n -> n -> Bool) _test_minus_times_dist_left _ = testName "if (minus(a,b) == rgt(d)) then minus(times(c,a),times(c,b)) == rgt(times(c,d))"$
\a b c -> case (minus a b) of
Right d -> eq
(minus (times c a) (times c b))
(rgt (times c d))
Left () -> true

## Testing

_test_minus ::
( TypeName n, Natural n, Equal n, Arbitrary n, Show n
) => Int -> Int -> n -> IO ()
_test_minus size cases n = do
testLabel1 "minus" n
let args = testArgs size cases

runTest args (_test_minus_zero_left n)
runTest args (_test_minus_next_left n)
runTest args (_test_minus_nat_zero n)
runTest args (_test_minus_zero_next n)
runTest args (_test_minus_next_next n)
runTest args (_test_minus_nat_next n)
runTest args (_test_minus_plus_equiv n)
runTest args (_test_minus_cancellative_left n)
runTest args (_test_minus_cancellative_right n)
runTest args (_test_minus_plus_right n)
runTest args (_test_minus_plus_left n)
runTest args (_test_minus_next_left_cond n)
runTest args (_test_minus_swap n)
runTest args (_test_minus_plus n)
runTest args (_test_minus_flip n)
runTest args (_test_minus_times_dist_left n)

Main:

main_minus :: IO ()
main_minus = do
_test_minus 30 50 (zero :: Unary)