Divides

Posted on 2017-04-09 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 Divides
  ( div, _test_div, main_div
  ) where

import Testing
import Booleans
import Not
import And
import NaturalNumbers
import Plus
import Times
import LessThanOrEqualTo
import DivisionAlgorithm

With the division algorithm in hand we can define what it means for one natural number to divide another.

We define $\ndiv : \nats \times \nats \rightarrow \bool$ by \[\ndiv(a,b) = \iszero(\nrem(b,a)).\]

In Haskell:

div :: (Natural n, Equal n) => n -> n -> Bool
div a b = isZero (rem b a)

Now $\ndiv$ is to $\ntimes$ as $\nleq$ is to $\nplus$ as follows.

Let $a,b \in \nats$. Then $\ndiv(a,b) = \btrue$ if and only if there exists $c \in \nats$ such that $b = \ntimes(c,a)$.

Suppose first that $\ndiv(a,b) = \btrue$. Letting $(q,r) = \ndivalg(b,a)$, we have $r = \zero$, so that \[b = \nplus(\ntimes(q,a),r) = \ntimes(q,a)\] as claimed.

Conversely, suppose there is a natural number $c$ such that $b = \ntimes(c,a)$. If $a = \zero$, then in fact $b = \zero$, and we have $\nrem(b,a) = \zero$, so that $\ndiv(a,b)$. Suppose instead that $a = \next(d)$. Since \[b = \nplus(\ntimes(c,\next(d)),\zero)\] and \[\nleq(\zero,\next(d)),\] we have \[(c,\zero) = \ndivalg(b,a).\] Thus $\nrem(b,a) = \zero$ as needed.

From here the usual properties of divisibility are straightforward. First, $\ndiv$ interacts with $\zero$ and $\next(\zero)$.

Let $a \in \nats$. We have the following.

$\ndiv(a,\zero)$.
If $\ndiv(\zero,a)$, then $a = \zero$.
$\ndiv(\next(\zero),a)$.
If $\ndiv(a,\next(\zero))$, then $a = \next(\zero)$.

Note that $\zero = \ntimes(\zero,a)$.
We have $c \in \nats$ such that $a = \ntimes(c,\zero) = \zero$.
Note that $a = \ntimes(a,\next(\zero))$.
We’ve seen that if $\ntimes(a,b) = \next(\zero)$ then $a = b = \next(\zero)$.

_test_div_zero_right :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_div_zero_right _ =
  testName "div(a,0) == true" $
  \a -> eq (div a zero) true


_test_div_zero_left :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_div_zero_left _ =
  testName "if div(0,a) then eq(a,0)" $
  \a -> if div zero a
    then eq a zero
    else true


_test_div_one_left :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_div_one_left _ =
  testName "div(next(0),a)" $
  \a -> div (next zero) a


_test_div_one_right :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_div_one_right _ =
  testName "if div(a,next(0)) then eq(a,next(0))" $
  \a -> if div a (next zero)
    then eq a (next zero)
    else true

And $\ndiv$ is reflexive, antisymmetric, and transitive.

Let $a,b,c \in \nats$. We have the following.

$\ndiv(a,a)$.
If $\ndiv(a,b)$ and $\ndiv(b,a)$, then $a = b$.
If $\ndiv(a,b)$ and $\ndiv(b,c)$, then $\ndiv(a,c)$.

Note that $a = \ntimes(\next(\zero),a)$.
First suppose $a = \zero$. Since $\ndiv(a,b)$, we have $b = 0$ as needed. Now suppose $a = \next(d)$. We have $h,k \in \nats$ such that $a = \ntimes(h,b)$ and $b = \ntimes(k,a)$; now \[\begin{eqnarray*} & & \ntimes(\next(\zero),\next(d)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-left} = & \next(d) \\ & = & b \\ & = & \ntimes(\ntimes(h,k),b) \\ & = & \ntimes(\ntimes(h,k),\next(d)); \end{eqnarray*}\] so we have $\ntimes(h,k) = \next(\zero)$, and thus $h = k = \next(\zero)$, so that $a = b$ as claimed.
We have $h,k \in \nats$ such that $b = \ntimes(h,a)$ and $c = \ntimes(k,b)$. now \[c = \ntimes(\ntimes(h,k),a),\] and thus $\ndiv(a,c)$.

_test_div_reflexive :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_div_reflexive _ =
  testName "div(a,a) == true" $
  \a -> eq (div a a) true


_test_div_antisymmetric :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_div_antisymmetric _ =
  testName "if and(div(a,b),div(b,a)) then eq(a,b)" $
  \a b -> if and (div a b) (div b a)
    then eq a b
    else true


_test_div_transitive :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_div_transitive _ =
  testName "if and(div(a,b),div(b,c)) then div(a,c)" $
  \a b c -> if and (div a b) (div b c)
    then div a c
    else true

And $\ndiv$ interacts with the rest of arithmetic.

Let $a,b,c,d \in \nats$. We have the following.

$\ndiv(a,\ntimes(b,a))$.
If $\ndiv(c,a)$, $c \neq \zero$, and $\ntimes(a,b) = \ntimes(c,d)$, then $\ndiv(b,d)$.
If $\ndiv(c,a)$ and $\ndiv(c,b)$ then $\ndiv(c,\nplus(a,b))$.
If $\ndiv(d,a)$ and $\ndiv(d,c)$ and $\nplus(a,b) = c$, then $\ndiv(d,b)$.
If $b \neq \zero$ and $\ndiv(a,b)$ then $\nleq(a,b)$.

We have $\ntimes(b,a) = \ntimes(b,a)$.
Say $a = \ntimes(c,u)$. Now \[\ntimes(c,\ntimes(u,b)) = \ntimes(c,d),\] so that $d = \ntimes(u,b)$. Thus $\ndiv(b,d)$ as claimed.
Say $a = \ntimes(h,c)$ and $b = \ntimes(k,c)$. Then by distributivity we have \[\begin{eqnarray*} & & \nplus(a,b) \\ & = & \nplus(\ntimes(h,c),\ntimes(k,c)) \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-plus-distribute-right} = & \ntimes(\nplus(h,k),c) \end{eqnarray*}\] as needed.
We consider two cases: either $d = \zero$ or $d = \next(m)$ for some $m$. If $d = \zero$, then we have $a = c = \zero$, and thus $b = \zero$. So $\ndiv(d,b)$ as claimed. Suppose now that $d = \next(m)$. Now $a = \ntimes(d,u)$ and $c = \ntimes(d,v)$ for some $u$ and $v$. Letting $(q,r) = \ndivalg(b,d)$, we have \[b = \nplus(\ntimes(q,d),r).\] Now \[\begin{eqnarray*} & & \ntimes(d,v) \\ & = & c \\ & = & \nplus(a,b) \\ & = & \nplus(\ntimes(d,u),\nplus(\ntimes(q,d),r)) \\ & = & \nplus(\ntimes(d,\nplus(u,q)),r) \end{eqnarray*}\] so that \[r = \nminus(\ntimes(d,v),\ntimes(d,\nplus(u,q))) = \ntimes(d,\nminus(v,\nplus(u,q))).\] Now $\nleq(r,m)$, so if $\nminus(v,\nplus(u,q)) \neq \zero$ we have $\nleq(\next(m),m)$, a contradiction. So we must have $\nminus(v,\nplus(u,q)) = \zero$, and thus $r = \zero$. So $\ndiv(d,b)$ as claimed.
Say $b = \ntimes(k,a)$; since $b \neq \zero$, we must also have $k \neq \zero$; say $k = \next(d)$. Then \[\begin{eqnarray*} & & b \\ & = & \ntimes(k,a) \\ & = & \ntimes(\next(k),a) \\ & \href{/posts/arithmetic-made-difficult/Times.html#cor-times-up-next} = & \nplus(\ntimes(k,a),a) \end{eqnarray*}\] so that $\nleq(a,b)$.

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


_test_div_times_swap :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> n -> Bool)
_test_div_times_swap _ =
  testName "if div(c,a) and not(isZero(c)) and eq(times(a,b),times(c,d)) then div(b,d)" $
  \a b c d -> if and (and (div c a) (not (isZero c))) (eq (times a b) (times c d))
    then div b d
    else true


_test_div_plus :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_div_plus _ =
  testName "if and(div(c,a),div(c,b)) then div(c,plus(a,b))" $
  \a b c -> if and (div c a) (div c b)
    then div c (plus a b)
    else true


_test_div_plus_transfer :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> n -> Bool)
_test_div_plus_transfer _ =
  testName "if div(d,a) and div(d,c) and eq(plus(a,b),c) then div(d,b)" $
  \a b c d -> if and (and (div d a) (div d c)) (eq c (plus a b))
    then div d b
    else true


_test_div_leq :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_div_leq _ =
  testName "if div(a,b) and not(isZero(b)) then leq(a,b)" $
  \a b -> if and (div a b) (not (isZero b))
    then leq a b
    else true

$\ndiv$ interacts with $\nquo$.

Let $a,b,c \in \nats$. Then we have the following.

If $\ndiv(b,a)$ and $c \neq \zero$, then \[\nquo(\ntimes(a,c),\ntimes(b,c)) = \nquo(a,b).\]
If $\ndiv(b,a)$, then $\nquo(\ntimes(c,a),b) = \ntimes(c,\nquo(a,b))$.

We consider two cases: either $b = \zero$ or $b \neq \zero$. If $b = \zero$ then we have $a = \zero$, and \[\begin{eqnarray*} & & \nquo(a,b) \\ & = & \nquo(\zero,\zero) \\ & = & \nquo(\ntimes(\zero,c),\ntimes(\zero,c)) \\ & = & \nquo(\ntimes(a,c),\ntimes(b,c)) \end{eqnarray*}\] as claimed. Suppose instead that $b \neq \zero$; say $b = \next(m)$. Since $\ndiv(b,a)$, we have $a = \ntimes(d,b)$ for some $d$; since $\nleq(\zero,m)$, by the uniqueness of quotients by nonzero divisors we have $d = \nquo(a,b)$. But also \[\ntimes(a,c) = \ntimes(d,\ntimes(b,c)),\] and since $\ntimes(b,c) \neq \zero$ we again have \[d = \nquo(\ntimes(a,c),\ntimes(b,c))\] by the uniqueness of quotients by nonzero divisors. Thus \[\nquo(a,b) = \nquo(\ntimes(a,c),\ntimes(b,c))\] as claimed.
We consider two cases: either $b = \zero$ or $b \neq \zero$. If $b = \zero$, we have $a = \zero$. Now \[\begin{eqnarray*} & & \nquo(\ntimes(c,a),b) \\ & = & \nquo(\zero,\zero) \\ & = & \zero \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-zero-right} = & \ntimes(c,\zero) \\ & = & \ntimes(c,\nquo(a,b)) \end{eqnarray*}\] as claimed. Suppose then that $b \neq \zero$; say $b = \next(m)$. Now say $a = \ntimes(q,b)$, and by the uniqueness of quotients by a nonzero divisor, we have $q = \nquo(a,b)$. Now $\ntimes(c,a) = \ntimes(\ntimes(c,q),b)$, and again by the uniqueness of quotients by a nonzero divisor we have \[\begin{eqnarray*} & & \nquo(\ntimes(c,a),b) \\ & = & \ntimes(c,q) \\ & = & \ntimes(c,\nquo(a,b)) \end{eqnarray*}\] as claimed.

_test_div_quo_times_cancel :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_div_quo_times_cancel _ =
  testName "if div(b,a) and not(isZero(c)) then quo(times(a,c),times(b,c)) == quo(a,b)" $
  \a b c -> if and (div b a) (not (isZero c))
    then eq (quo (times c a) (times c b)) (quo a b)
    else true


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

We’ll call the next result the Cross Multiplication Theorem.

Let $a,b,c,d \in \nats$ such that $\ndiv(b,a)$ and $\ndiv(d,c)$ and $b,d \neq \zero$. Then \[\ntimes(a,d) = \ntimes(b,c)\] if and only if $\nquo(a,b) = \nquo(c,d).$$

Since $b$ and $d$ are both not zero, using the uniqueness of quotients by nonzero divisors we have \[\ntimes(a,d) = \ntimes(b,c)\] if and only if \[\nquo(\ntimes(a,d),b) = c\] if and only if \[\ntimes(d,\nquo(a,b)) = c\] if and only if \[\nquo(a,b) = \nquo(c,d)\] as claimed.

_test_div_cross_multiplication :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> n -> Bool)
_test_div_cross_multiplication _ =
  testName "if div(b,a) and div(d,c) and b /= 0 and d /= 0 then times(a,d) == times(b,c) iff quo(a,b) == quo(c,d)" $
  \a b c d -> if and (and (div b a) (div d c)) (and (not (isZero b)) (not (isZero d)))
    then eq
      (eq (times a d) (times b c))
      (eq (quo a b) (quo c d))
    else true

Testing

Suite:

_test_div ::
  ( TypeName n, Natural n, Equal n, Arbitrary n, Show n
  , TypeName b, Equal b, Boolean b
  ) => Int -> Int -> n -> b -> IO ()
_test_div size cases n p = do
  testLabel2 "div" n p

  let args = testArgs size cases

  runTest args (_test_div_zero_right n)
  runTest args (_test_div_zero_left n)
  runTest args (_test_div_one_left n)
  runTest args (_test_div_one_right n)
  runTest args (_test_div_reflexive n)
  runTest args (_test_div_antisymmetric n)
  runTest args (_test_div_transitive n)
  runTest args (_test_div_times n)
  runTest args (_test_div_times_swap n)
  runTest args (_test_div_plus n)
  runTest args (_test_div_plus_transfer n)
  runTest args (_test_div_leq n)
  runTest args (_test_div_quo_times_cancel n)
  runTest args (_test_div_quo_times_interchange n)
  runTest args (_test_div_cross_multiplication n)

Main:

main_div :: IO ()
main_div = do
  _test_div 50 100 (zero :: Unary) (true :: Bool)