Multiplication

Posted on 2017-03-31 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

$\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}$ $\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}$ $\newcommand{\a}{a}$ $\newcommand{\b}{b}$ $\newcommand{\c}{c}$ $\newcommand{\p}{p}$ $\newcommand{\q}{q}$ $\newcommand{\r}{r}$ $\newcommand{\s}{s}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\bool}{\mathbb{B}}$ $\newcommand{\btrue}{\mathsf{true}}$ $\newcommand{\bfalse}{\mathsf{false}}$ $\newcommand{\bnot}{\mathsf{not}}$ $\newcommand{\band}{\mathbin{\mathsf{and}}}$ $\newcommand{\bor}{\mathbin{\mathsf{or}}}$ $\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}$ $\newcommand{\beq}{\mathsf{eq}}$ $\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}$ $\newcommand{\id}{\mathsf{id}}$ $\newcommand{\compose}{\mathsf{compose}}$ $\newcommand{\const}{\mathsf{const}}$ $\newcommand{\apply}{\mathsf{apply}}$ $\newcommand{\flip}{\mathsf{flip}}$ $\newcommand{\flipB}{\mathsf{flip2}}$ $\newcommand{\flipC}{\mathsf{flip3}}$ $\newcommand{\flipD}{\mathsf{flip4}}$ $\newcommand{\flipE}{\mathsf{flip5}}$ $\newcommand{\clone}{\mathsf{clone}}$ $\newcommand{\cloneC}{\mathsf{clone3}}$ $\newcommand{\composeAonB}{\mathsf{compose1on2}}$ $\newcommand{\composeAonC}{\mathsf{compose1on3}}$ $\newcommand{\composeAonD}{\mathsf{compose1on4}}$ $\newcommand{\composeBonA}{\mathsf{compose2on1}}$ $\newcommand{\composeBonB}{\mathsf{compose2on2}}$ $\newcommand{\composeConA}{\mathsf{compose3on1}}$ $\newcommand{\ptrue}{\mathsf{ptrue}}$ $\newcommand{\pfalse}{\mathsf{pfalse}}$ $\newcommand{\pnot}{\mathsf{pnot}}$ $\newcommand{\pand}{\mathbin{\mathsf{pand}}}$ $\newcommand{\por}{\mathbin{\mathsf{por}}}$ $\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}$ $\newcommand{\fst}{\mathsf{first}}$ $\newcommand{\snd}{\mathsf{second}}$ $\newcommand{\dup}{\mathsf{dup}}$ $\newcommand{\tup}{\mathsf{tup}}$ $\newcommand{\tSwap}{\mathsf{swap}_{\times}}$ $\newcommand{\tPair}{\mathsf{pair}_{\times}}$ $\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}$ $\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}$ $\newcommand{\tupL}{\mathsf{tupL}}$ $\newcommand{\tupR}{\mathsf{tupR}}$ $\newcommand{\uncurry}{\mathsf{uncurry}}$ $\newcommand{\curry}{\mathsf{curry}}$ $\newcommand{\lft}{\mathsf{left}}$ $\newcommand{\rgt}{\mathsf{right}}$ $\newcommand{\either}{\mathsf{either}}$ $\newcommand{\uSwap}{\mathsf{swap}_{+}}$ $\newcommand{\uPair}{\mathsf{pair}_{+}}$ $\newcommand{\uAssocL}{\mathsf{assocL}_{+}}$ $\newcommand{\uAssocR}{\mathsf{assocR}_{+}}$ $\newcommand{\isLft}{\mathsf{isLeft}}$ $\newcommand{\isRgt}{\mathsf{isRight}}$ $\newcommand{\nats}{\mathbb{N}}$ $\newcommand{\zero}{\mathsf{0}}$ $\newcommand{\next}{\mathsf{next}}$ $\newcommand{\unnext}{\mathsf{unnext}}$ $\newcommand{\iszero}{\mathsf{isZero}}$ $\newcommand{\prev}{\mathsf{prev}}$ $\newcommand{\natrec}{\mathsf{natrec}}$ $\newcommand{\simprec}{\mathsf{simprec}}$ $\newcommand{\bailrec}{\mathsf{bailrec}}$ $\newcommand{\mutrec}{\mathsf{mutrec}}$ $\newcommand{\dnatrec}{\mathsf{dnatrec}}$ $\newcommand{\normrec}{\mathsf{normrec}}$ $\newcommand{\findsmallest}{\mathsf{findsmallest}}$ $\newcommand{\mnormrec}{\mathsf{mnormrec}}$ $\newcommand{\nequal}{\mathsf{eq}}$ $\newcommand{\nplus}{\mathsf{plus}}$ $\newcommand{\ntimes}{\mathsf{times}}$ $\newcommand{\nleq}{\mathsf{leq}}$ $\newcommand{\ngeq}{\mathsf{geq}}$ $\newcommand{\nminus}{\mathsf{minus}}$ $\newcommand{\nmax}{\mathsf{max}}$ $\newcommand{\nmin}{\mathsf{min}}$ $\newcommand{\ndivalg}{\mathsf{divalg}}$ $\newcommand{\nquo}{\mathsf{quo}}$ $\newcommand{\nrem}{\mathsf{rem}}$ $\newcommand{\ndiv}{\mathsf{div}}$ $\newcommand{\ngcd}{\mathsf{gcd}}$ $\newcommand{\ncoprime}{\mathsf{coprime}}$ $\newcommand{\nlcm}{\mathsf{lcm}}$ $\newcommand{\nmindiv}{\mathsf{mindiv}}$ $\newcommand{\nisprime}{\mathsf{isPrime}}$ $\newcommand{\npower}{\mathsf{power}}$ $\newcommand{\nchoose}{\mathsf{choose}}$ $\newcommand{\dom}{\mathsf{dom}}$ $\newcommand{\cod}{\mathsf{cod}}$ $\newcommand{\lists}[1]{\mathsf{List}(#1)}$ $\newcommand{\nil}{\mathsf{nil}}$ $\newcommand{\cons}{\mathsf{cons}}$ $\newcommand{\uncons}{\mathsf{uncons}}$ $\newcommand{\isnil}{\mathsf{isNil}}$ $\newcommand{\tail}{\mathsf{tail}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\foldr}{\mathsf{foldr}}$ $\newcommand{\foldl}{\mathsf{foldl}}$ $\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}$ $\newcommand{\unfoldN}{\mathsf{unfoldN}}$ $\newcommand{\dfoldr}{\mathsf{dfoldr}}$ $\newcommand{\cfoldr}{\mathsf{cfoldr}}$ $\newcommand{\bfoldr}{\mathsf{bfoldr}}$ $\newcommand{\dbfoldr}{\mathsf{dbfoldr}}$ $\newcommand{\lfoldr}{\mathsf{lfoldr}}$ $\newcommand{\snoc}{\mathsf{snoc}}$ $\newcommand{\revcat}{\mathsf{revcat}}$ $\newcommand{\rev}{\mathsf{rev}}$ $\newcommand{\last}{\mathsf{last}}$ $\newcommand{\cat}{\mathsf{cat}}$ $\newcommand{\addlength}{\mathsf{addlength}}$ $\newcommand{\length}{\mathsf{length}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\at}{\mathsf{at}}$ $\newcommand{\map}{\mathsf{map}}$ $\newcommand{\range}{\mathsf{range}}$ $\newcommand{\zip}{\mathsf{zip}}$ $\newcommand{\zipPad}{\mathsf{zipPad}}$ $\newcommand{\unzip}{\mathsf{unzip}}$ $\newcommand{\prefix}{\mathsf{prefix}}$ $\newcommand{\suffix}{\mathsf{suffix}}$ $\newcommand{\lcp}{\mathsf{lcp}}$ $\newcommand{\lcs}{\mathsf{lcs}}$ $\newcommand{\all}{\mathsf{all}}$ $\newcommand{\any}{\mathsf{any}}$ $\newcommand{\tails}{\mathsf{tails}}$ $\newcommand{\inits}{\mathsf{inits}}$ $\newcommand{\filter}{\mathsf{filter}}$ $\newcommand{\elt}{\mathsf{elt}}$ $\newcommand{\addcount}{\mathsf{addcount}}$ $\newcommand{\count}{\mathsf{count}}$ $\newcommand{\repeat}{\mathsf{repeat}}$ $\newcommand{\sublist}{\mathsf{sublist}}$ $\newcommand{\infix}{\mathsf{infix}}$ $\newcommand{\select}{\mathsf{select}}$ $\newcommand{\unique}{\mathsf{unique}}$ $\newcommand{\delete}{\mathsf{delete}}$ $\newcommand{\dedupeL}{\mathsf{dedupeL}}$ $\newcommand{\dedupeR}{\mathsf{dedupeR}}$ $\newcommand{\common}{\mathsf{common}}$ $\newcommand{\disjoint}{\mathsf{disjoint}}$ $\newcommand{\sublists}{\mathsf{sublists}}$ $\newcommand{\take}{\mathsf{take}}$ $\newcommand{\drop}{\mathsf{drop}}$ $\newcommand{\takeBut}{\mathsf{takeBut}}$ $\newcommand{\dropBut}{\mathsf{dropBut}}$ $\newcommand{\takeWhile}{\mathsf{takeWhile}}$ $\newcommand{\dropWhile}{\mathsf{dropWhile}}$

This page is part of a series on Arithmetic Made Difficult.

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

{-# LANGUAGE NoImplicitPrelude #-}
module Times
 ( times, _test_times, main_times
 ) where

import Testing
import Booleans
import NaturalNumbers
import SimpleRecursion
import Plus

Natural number multiplication has signature $\nats \times \nats \rightarrow \nats$, so we might hope to define it as $\Theta = \simprec(\varphi)(\mu)$ for some appropriate $\varphi$ and $\mu$. Using the universal property of simple recursion and how we want multiplication to behave, note that on the one hand we want $\Theta(\zero,m) = \zero$ for all $m$, while on the other hand we have $\Theta(\zero,m) = \varphi(m)$. So apparently we need $\varphi(m) = \zero$ for all $m$.

Similarly, we want $\Theta(\next(n),m) = \nplus(\Theta(n,m),m)$, but we also have \[\Theta(\next(n),m) = \mu(n,m,\Theta(n,m)).\] So apparently we need $\mu(n,m,k) = \nplus(k,m)$.

With this in mind, we define a binary operation $\ntimes$ on $\nats$ as follows.

Let $\varphi : \nats \rightarrow \nats$ be given by $\varphi(m) = \zero$, and let $\mu : \nats \times \nats \times \nats \rightarrow \nats$ be given by $\mu(k,a,b) = \nplus(b,a)$. We then define $\ntimes : \nats \times \nats \rightarrow \nats$ by \[\ntimes = \simprec(\varphi)(\mu).\]

In Haskell:

times :: (Natural n) => n -> n -> n
times = simpleRec phi mu
  where
    phi _ = zero
    mu _ a b = plus b a

Since $\ntimes$ is defined in terms of simple recursion, it is the unique solution to a set of functional equations.

$\ntimes$ is the unique map $f : \nats \times \nats \rightarrow \nats$ with the property that for all $a,b \in \nats$, we have \[\left\{\begin{array}{l} f(\zero,b) = \zero \\ f(\next(a),b) = \nplus(f(a,b),b). \end{array}\right.\]

_test_times_zero_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> Bool)
_test_times_zero_left _ f =
  testName "times(0,a) == 0" $
  \a -> eq (f zero a) zero


_test_times_next_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> Bool)
_test_times_next_left _ f =
  testName "times(next(a),b) == plus(times(a,b),b)" $
  \a b -> eq (f (next a) b) (plus (f a b) b)

Next we establish a version of the universal property of $\ntimes$ with the arguments reversed.

The following hold for all natural numbers $a$ and $b$.

$\ntimes(a,\zero) = \zero$.
$\ntimes(a,\next(b)) = \nplus(\ntimes(a,b),a)$.

We proceed by induction on $a$. For the base case, note that $\ntimes(\zero,\zero) = \zero$. For the inductive step, suppose we have $\ntimes(a,\zero) = \zero$ for some $a$. Then \[\begin{eqnarray*} & & \ntimes(\next(a),\zero) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\zero),\zero) \\ & \hyp{\ntimes(a,\zero) = \zero} = & \nplus(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \zero \end{eqnarray*}\] as needed.
We proceed by induction on $a$. For the base case, we have \[\begin{eqnarray*} & & \ntimes(\zero,\next(b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \zero \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \nplus(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \nplus(\ntimes(\zero,b),\zero) \end{eqnarray*}\] as needed. For the inductive step, suppose we have $\ntimes(a,\next(b)) = \nplus(\ntimes(a,b),a)$ for some $a$. Now \[\begin{eqnarray*} & & \ntimes(\next(a),\next(b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\next(b)),\next(b)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(\ntimes(a,\next(b)),b)) \\ & \hyp{\ntimes(a,\next(b)) = \nplus(\ntimes(a,b),a)} = & \next(\nplus(\nplus(\ntimes(a,b),a),b)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \next(\nplus(\ntimes(a,b),\nplus(a,b))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-commutative} = & \next(\nplus(\ntimes(a,b),\nplus(b,a))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \next(\nplus(\nplus(\ntimes(a,b),b),a)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \next(\nplus(\ntimes(\next(a),b),a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \nplus(\ntimes(\next(a),b),\next(a)) \end{eqnarray*}\] as needed.

_test_times_zero_right :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> Bool)
_test_times_zero_right _ f =
  testName "0 == times(a,0)" $
  \a -> eq (f a zero) zero


_test_times_next_right :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> Bool)
_test_times_next_right _ f =
  testName "times(a,next(b)) == plus(times(a,b),a)" $
  \a b -> eq (f a (next b)) (plus (f a b) a)

$\next(\zero)$ is neutral under $\ntimes$.

For all $a \in \nats$, we have

$\ntimes(\next(\zero),a) = a$.
$\ntimes(a,\next(\zero)) = a$.

Note first that for all $a$, we have \[\begin{eqnarray*} & & \ntimes(\next(\zero),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(\zero,a),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \nplus(\zero,a) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & a \end{eqnarray*}\] as claimed.
We proceed by induction on $a$. For the base case, note that $\ntimes(\zero,\next(\zero)) = \zero$. For the inductive step, suppose we have $\ntimes(a,\next(\zero)) = a$ for some $a$. Now \[\begin{eqnarray*} & & \ntimes(\next(a),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\next(\zero)),\next(\zero)) \\ & \hyp{\ntimes(a,\next(\zero)) = a} = & \nplus(a,\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(a,\zero)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \next(a) \end{eqnarray*}\] as needed.

_test_times_one_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> Bool)
_test_times_one_left _ f =
  testName "a == times(1,a)" $
  \a -> eq a (f (next zero) a)


_test_times_one_right :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> Bool)
_test_times_one_right _ f =
  testName "a == times(a,1)" $
  \a -> eq a (f a (next zero))

$\ntimes$ is commutative.

For all $a,b \in \nats$ we have $\ntimes(a,b) = \ntimes(b,a)$.

We proceed by induction on $a$. For the base case, note that \[\ntimes(\zero,b) = \zero = \ntimes(b,\zero)\] as needed. For the inductive step, suppose we have $\ntimes(a,b) = \ntimes(b,a)$ for some $a$. Now \[\begin{eqnarray*} & & \ntimes(\next(a),b) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,b),b) \\ & \hyp{\ntimes(a,b) = \ntimes(b,a)} = & \nplus(\ntimes(b,a),b) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-next-right} = & \ntimes(b,\next(a)) \end{eqnarray*}\] as needed.

_test_times_commutative :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> Bool)
_test_times_commutative _ f =
  testName "times(a,b) == times(b,a)" $
  \a b -> eq (f a b) (f b a)

$\ntimes$ distributes over $\nplus$.

For all $a,b,c, \in \nats$, we have the following.

$\ntimes(a,\nplus(b,c)) = \nplus(\ntimes(a,b),\ntimes(a,c))$.
$\ntimes(\nplus(a,b),c) = \nplus(\ntimes(a,c),\ntimes(b,c))$.

We proceed by induction on $a$. For the base case, we have \[\ntimes(\zero,\nplus(b,c)) = \zero = \nplus(\zero,\zero) = \nplus(\ntimes(\zero,b),\ntimes(\zero,c))\] as needed. For the inductive step, suppose we have $\ntimes(a,\nplus(b,c)) = \nplus(\ntimes(a,b),\ntimes(a,c))$ for all $b$ and $c$ for some $a$. Now \[\begin{eqnarray*} & & \ntimes(\next(a),\nplus(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\nplus(b,c)),\nplus(b,c)) \\ & \hyp{\ntimes(a,\nplus(b,c)) = \nplus(\ntimes(a,b),\ntimes(a,c))} = & \nplus(\nplus(\ntimes(a,b),\ntimes(a,c)),\nplus(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(\nplus(\nplus(\ntimes(a,b),\ntimes(a,c)),b),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(\nplus(\ntimes(a,b),\nplus(\ntimes(a,c),b)),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-commutative} = & \nplus(\nplus(\ntimes(a,b),\nplus(b,\ntimes(a,c))),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(\nplus(\nplus(\ntimes(a,b),b),\ntimes(a,c)),c) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(\nplus(\ntimes(a,b),b),\nplus(\ntimes(a,c),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(\next(a),b),\nplus(\ntimes(a,c),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(\next(a),b),\ntimes(\next(a),c)) \end{eqnarray*}\] as needed.
We have \[\begin{eqnarray*} & & \ntimes(\nplus(a,b),c) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \ntimes(c,\nplus(a,b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-plus-distribute-left} = & \nplus(\ntimes(c,a),\ntimes(c,b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \nplus(\ntimes(a,c),\ntimes(c,b)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \nplus(\ntimes(a,c),\ntimes(b,c)) \end{eqnarray*}\] as claimed.

_test_times_distributive_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> n -> Bool)
_test_times_distributive_left _ f =
  testName "times(a,plus(b,c)) == plus(times(a,b),times(a,c))" $
  \a b c -> eq (f a (plus b c)) (plus (f a b) (f a c))


_test_times_distributive_right :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> n -> Bool)
_test_times_distributive_right _ f =
  testName "times(plus(a,b),c) == plus(times(a,c),times(b,c))" $
  \a b c -> eq (f (plus a b) c) (plus (f a c) (f b c))

$\ntimes$ is associative,

For all $a,b,c \in \nats$, we have \[\ntimes(\ntimes(a,b),c) = \ntimes(a,\ntimes(b,c)).\]

We proceed by induction on $a$. For the base case, we have \[\begin{eqnarray*} & & \ntimes(\zero,\ntimes(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \zero \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \ntimes(\zero,c) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-zero} = & \ntimes(\ntimes(\zero,b),c) \end{eqnarray*}\] as needed. For the inductive step, suppose we have $\ntimes(a,\ntimes(b,c)) = \ntimes(\ntimes(a,b),c)$ for all $b$ and $c$ for some $a$. Then \[\begin{eqnarray*} & & \ntimes(\ntimes(\next(a),b),c) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \ntimes(\nplus(\ntimes(a,b),b),c) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-plus-distribute-right} = & \nplus(\ntimes(\ntimes(a,b),c),\ntimes(b,c)) \\ & \hyp{\ntimes(a,\ntimes(b,c)) = \ntimes(\ntimes(a,b),c)} = & \nplus(\ntimes(a,\ntimes(b,c)),\ntimes(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \ntimes(\next(a),\ntimes(b,c)) \end{eqnarray*}\] as needed.

_test_times_associative :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> n -> Bool)
_test_times_associative _ f =
  testName "times(times(a,b),c) == times(a,times(b,c))" $
  \a b c -> eq (f (f a b) c) (f a (f b c))

$\ntimes$ is almost cancellative.

For all $a,b,c \in \nats$, we have the following.

If $\ntimes(\next(a),b) = \ntimes(\next(a),c)$ then $b = c$.
If $\ntimes(b,\next(a)) = \ntimes(c,\next(a))$ then $b = c$.

This proof will be a little different: we will use induction twice; first on $b$, and then on $c$. To this end, let \[B = \{ b \in \nats \mid \forall c, \forall a,\ \mathrm{if}\ \ntimes(\next(a),b) = \ntimes(\next(a),c)\ \mathrm{then}\ b = c \}\] and given $b \in \nats$ let \[C(b) = \{ c \in \nats \mid \forall a,\ \mathrm{if}\ \ntimes(\next(a),b) = \ntimes(\next(a),c)\ \mathrm{then}\ b = c \}.\] We wish to show that $B = \nats$ by induction. For the base case, we need to show that $b = \zero \in B$; for this it suffices to show that $C(\zero) = \nats$, which we do by induction. For the base case $c = \zero$, we have $b = c$ regardless of $a$. For the inductive step suppose we have $c \in C(\zero)$ for some $c$. Note that \[\begin{eqnarray*} & & \ntimes(\next(a),\next(c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\next(c)),\next(c)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(\ntimes(a,\next(c)),c)) \end{eqnarray*}\] while \[\ntimes(\next(a),b) = \ntimes(\next(a),\zero) = \zero;\] in particular, the statement \[\ntimes(\next(a),\next(c)) = \ntimes(\next(a),b)\] is false, so that $\next(c) \in C(\zero)$ vacuously. So we have $C(\zero) = \nats$, and thus $\zero \in B$. For the inductive step, suppose we have $b \in B$; we wish to show that $\next(b) \in B$, or equivalently that $C(\next(b)) = \nats$. We proceed by induction on $c$ again. The base case $c = \zero$ holds vacuously. For the inductive step, suppose we have $c \in C(\next(b))$. Now suppose further that \[\ntimes(\next(a),\next(b)) = \ntimes(\next(a),\next(c)).\] Note that \[\begin{eqnarray*} & & \ntimes(\next(a),\next(c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(a,\next(c)),\next(c)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(\ntimes(a,\next(c)),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \next(\nplus(\ntimes(\next(c),a),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \next(\nplus(\nplus(\ntimes(c,a),a),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-commutative} = & \next(\nplus(\nplus(\ntimes(a,c),a),c)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \next(\nplus(\ntimes(a,c),\nplus(a,c))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-commutative} = & \next(\nplus(\ntimes(a,c),\nplus(c,a))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \next(\nplus(\nplus(\ntimes(a,c),c),a)) \end{eqnarray*}\] The analogous statement holds for $b$. So we have \[\begin{eqnarray*} & & \beq(\next(\nplus(\nplus(\ntimes(a,b),b),a)),\next(\nplus(\nplus(\ntimes(a,c),c),a))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-next-injective} = & \beq(\nplus(\nplus(\ntimes(a,b),b),a),\nplus(\nplus(\ntimes(a,c),c),a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-right-cancel} = & \beq(\nplus(\ntimes(a,b),b),\nplus(\ntimes(a,c),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \beq(\ntimes(\next(a),b),\nplus(\ntimes(a,c),c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \beq(\ntimes(\next(a),b),\ntimes(\next(a),c)) \\ & \hyp{\beq(\ntimes(\next(a),b),\ntimes(\next(a),c)) = \beq(b,c)} = & \beq(b,c) \end{eqnarray*}\] as needed.
Suppose \[\ntimes(b,\next(a)) = \ntimes(c,\next(a)).\] Then we have \[\ntimes(\next(a),b) = \ntimes(\next(a),c),\] so that b = c$ as claimed.

_test_times_cancellative_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> n -> Bool)
_test_times_cancellative_left _ f =
  testName "if times(next(c),a) == times(next(c),b) then a == b" $
  \a b c -> if eq (f (next c) a) (f (next c) b)
    then eq a b
    else true


_test_times_cancellative_right :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> n -> n -> Bool)
_test_times_cancellative_right _ f =
  testName "if times(a,next(c)) == plus(b,next(c)) then a == b" $
  \a b c -> if eq (f a (next c)) (f b (next c))
    then eq a b
    else true

As a special case, $\ntimes(\next(\next(\zero)),-)$ is equivalent to a $\nplus$.

For all $a \in \nats$ we have \[\ntimes(\next(\next(\zero)),a) = \nplus(a,a).\]

Note that \[\begin{eqnarray*} & & \ntimes(\next(\next(\zero)),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(\next(\zero),a),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-left} = & \nplus(a,a) \end{eqnarray*}\] as claimed.

_test_times_two_left :: (Natural n, Equal n)
  => n -> (n -> n -> n) -> Test (n -> Bool)
_test_times_two_left _ f =
  testName "times(next(next(zero)),a) == plus(a,a)" $
  \a -> eq (plus a a) (f (next (next zero)) a)

Testing

_test_times :: (TypeName n, Natural n, Equal n, Arbitrary n, Show n)
  => Int -> Int -> n -> (n -> n -> n) -> IO ()
_test_times size cases n f = do
  testLabel1 "times" n

  let args = testArgs size cases

  runTest args (_test_times_zero_left n f)
  runTest args (_test_times_next_left n f)
  runTest args (_test_times_zero_right n f)
  runTest args (_test_times_next_right n f)
  runTest args (_test_times_one_left n f)
  runTest args (_test_times_one_right n f)
  runTest args (_test_times_commutative n f)
  runTest args (_test_times_distributive_left n f)
  runTest args (_test_times_distributive_right n f)
  runTest args (_test_times_associative n f)
  runTest args (_test_times_cancellative_left n f)
  runTest args (_test_times_cancellative_right n f)
  runTest args (_test_times_two_left n f)

I used a much smaller number of test cases this time, because these run much more slowly than the tests for plus. The culprit is _test_times_associative. What’s happening is that multiplication of Nats is inherently slow; it’s implemented as iterated addition, which itself is iterated N.

The problem lies in our representation of the natural numbers. A better representation might make a more efficient times possible.

main_times :: IO ()
main_times = do
  _test_times 40 100 (zero :: Unary) times