Is Prime

Posted on 2017-04-13 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 IsPrime
  ( mindiv, prime, _test_prime, main_prime
  ) where

import Testing
import Functions
import Flip
import Booleans
import And
import DisjointUnions
import NaturalNumbers
import LessThanOrEqualTo
import Divides
import GreatestCommonDivisor
import FindSmallest

Today we’ll nail down what it means for a natural number to be prime. Typically this is done by saying something like “a natural number other than 0 or 1 is prime if it is not divisible by any natural number besides itself and 1” and from there, arguing that this property can be checked using trial division. As is typical in this series, we will turn this around – defining primes to be those numbers which are detected by trial division (i.e. an algorithm) and then proving that such numbers have the divisibility properties we expect.

In fact we’ll do a little more: instead of simply using trial division to detect whether a natural number \(n\) is prime, we can use it to find the smallest divisor of \(n\). If the smallest divisor is \(n\) itself, then \(n\) is prime. To make this work we have to define “smallest divisor” in such a way that the trivial divisor \(\next(\zero)\) is excluded. We will call this function that finds the smallest divisor \(\nmindiv\), and intuitively it should have the signature \(\nats \rightarrow \nats\).

Define \(\sigma : \nats \rightarrow \bool^{\nats}\) by \[\sigma(a)(b) = \div(b,a),\] and define \(\varphi : \nats \rightarrow 1 + \nats\) piecewise by \[\nmindiv(n) = \left\{\begin{array}{ll} \rgt(\zero) & \mathrm{if}\ n = \zero \\ \rgt(\next(\zero)) & \mathrm{if}\ n = \next(\zero) \\ \findsmallest(\sigma(n))(m,\next(\next(\zero))) & \mathrm{if}\ n = \next(\next(m)). \end{array}\right.\] Now define \(\nmindiv : \nats \rightarrow \nats\) by \[\nmindiv(n) = \either(\const(n),\id)(\varphi(n)).\]

In Haskell:

mindiv :: (Natural n, Equal n) => n -> n
mindiv n = either (const n) id (phi n)
  where
    phi t = case unnext t of
      Left () -> rgt zero
      Right k -> case unnext k of
        Left () -> rgt (next zero)
        Right m -> findSmallest (sigma n) m (next (next zero))

    sigma = flip div

Almost by definition, \(\nmindiv(a)\) is the smallest divisor of \(a\) in a precise sense.

Let \(a \in \nats\) with \(\nleq(\next(\next(\zero)),a)\). Then we have the following.

\(\nleq(\next(\next(\zero)),\nmindiv(a))\) and \(\ndiv(\nmindiv(a),a)\).
If \(\nleq(\next(\next(\zero)),k)\) and \(\ndiv(k,a)\), then \(\nleq(\nmindiv(a),k)\).

If \(a = \next(\next(m))\) for some \(m\), we have \[\begin{eqnarray*} & & \nmindiv(a) \\ & = & \nmindiv(\next(\next(m))) \\ & = & \either(\const(a),\id)(\findsmallest(\sigma(a))(m,\next(\next(\zero)))). \end{eqnarray*}\] We have two possibilities for \(\findsmallest(\sigma(a))(m,\next(\next(\zero))) = Q\).

Suppose \(Q = \rgt(t)\); then we have \[\begin{eqnarray*} & & \either(\const(a),\id)(Q) \\ & = & \either(\const(a),\id)(\rgt(t)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \id(t) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & t \end{eqnarray*}\] By the properties of \(\findsmallest(\sigma(a))\) we have \(\nleq(\next(\next(\zero)),t)\) and \(\nleq(t,\next(m))\) (so \(t \neq \zero\) and \(t \neq \next(\zero)\)) and \(\ndiv(t,a)\), and moreover if \(\nleq(\next(\next(\zero)),k)\) and \(\nleq(k,\next(m))\) and \(\ndiv(k,a)\) then \(\nleq(t,k)\) as claimed.

Suppose instead that \(Q = \lft(\ast)\); then we have \[\begin{eqnarray*} & & \either(\const(a),\id)(Q) \\ & = & \either(\const(a),\id)(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(a)(\ast) \\ & = & a. \end{eqnarray*}\] Again by the properties of \(\findsmallest(\sigma(a))\), there does not exist \(k\) such that \(\nleq(\next(\next(\zero)),k)\) and \(\nleq(k,\next(m))\) and \(\ndiv(k,a)\) as claimed.

_test_mindiv_div :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_mindiv_div _ =
  testName "if leq(next(next(zero)),a) then leq(next(next(zero)),mindiv(a)) and div(mindiv(a),a)" $
  \a -> if leq (next (next zero)) a
    then and (leq (next (next zero)) (mindiv a)) (div (mindiv a) a)
    else true


_test_mindiv_min :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_mindiv_min _ =
  testName "if leq(next(next(zero)),k) and div(k,a) then leq(mindiv(a),k)" $
  \a k -> if and (leq (next (next zero)) k) (div k a)
    then leq (mindiv a) k
    else true

Now we define a boolean function \(\nisprime\) as follows.

Define \(\nisprime : \nats \rightarrow \bool\) by \[\nisprime(a) = \left\{ \begin{array}{ll} \bfalse & \mathrm{if} a = \zero\ \mathrm{or}\ a = \next(\zero) \\ \beq(a,\nmindiv(a)) & \mathrm{otherwise}. \end{array} \right.\]

In Haskell:

prime :: (Natural n, Equal n) => n -> Bool
prime a = if leq a (next zero)
  then false
  else eq a (mindiv a)

It is straightforward to show that \(\nisprime\) is equivalent to the usual definition.

Let \(a \in \nats\). Then the following are equivalent.

\(\nisprime(a) = \btrue\).
\(a \neq \zero\) and \(a \neq \next(\zero)\), and if \(u,v \in \nats\) such that \(a = \ntimes(u,v)\), then \((u,v)\) is either \((\next(\zero),a)\) or \((a,\next(\zero))\).
\(a \neq \zero\) and \(a \neq \next(\zero)\), and if \(u,v \in \nats\) such that \(\ndiv(a,\ntimes(u,v))\), then either \(\ndiv(a,u)\) or \(\ndiv(a,v)\).

\((1)\) implies \((2)\): Suppose \(\nisprime(a) = \btrue\). Certainly \(a \neq \zero\) and \(a \neq \next(\zero)\) (by definition), and we have \(a = \nmindiv(a)\). Suppose now that \(a = \ntimes(u,v)\); we consider three cases for \(u\). If \(u = \zero\) we have \(a = \zero\), a contradiction. If \(u = \next(\zero)\), then \(v = a\). If \(a \neq \zero\) and \(a \neq \next(\zero)\), we have \(\ndiv(u,a)\), so that \(\nleq(\nmindiv(a),u)\); thus \(\nleq(a,u)\). But also \(\nleq(u,a)\), so that \(u = a\), and thus \(v = \next(\zero)\) as claimed.

\((2)\) implies \((3)\): Of course \(a \neq \zero\) and \(a \neq \next(\zero)\). Say \(\ndiv(a,\ntimes(u,v))\), and consider \(\ngcd(a,u)\). In particular, we have \(a = \ntimes(k,\ngcd(a,u))\) for some \(k\). There are two possibilities: if \(\ngcd(a,u) = a\), then \(\ndiv(a,u)\), and if \(\ngcd(a,u) = \next(\zero)\), then \(\ndiv(a,v)\) by Euclid’s lemma.

\((3)\) implies \((1)\): It suffices to show that if \(a \neq \zero\) and \(a \neq \next(\zero)\) then \(\nmindiv(a) = a\). To this end, let \(d = \nmindiv(a)\) and write \(a = \ntimes(\nmindiv(a),k)\). Suppose \(\ndiv(a,k)\), with \(k = \ntimes(a,w)\). Since \(a \neq \zero\), by cancellation we have \(\next(\zero) = \ntimes(\nmindiv(a),w)\), so that \(\nmindiv(a) = \next(\zero)\), a contradiction. Thus \(\ndiv(a,\nmindiv(a))\), so we have \(a = \nmindiv(a)\) as needed.

Minimal divisors are prime.

Let \(a \in \nats\) with \(a \neq \zero\) and \(a \neq \next(\zero)\). Then \[\nisprime(\nmindiv(a)) = \btrue.\]

Let \(a \in \nats\) with \(a \neq \zero\) and \(a \neq \next(\zero)\), and let \(d = \nmindiv(a)\). Suppose now that \(d = \ntimes(u,v)\). Since \(d \neq \zero\), we have \(u \neq \zero\). If \(u = \next(\zero)\), we have \(v = d\). If \(u \neq \next(\zero)\), we have \(\ndiv(u,a)\) and thus \(\nleq(d,u)\); but \(\nleq(u,d)\), so that \(d = u\) by antisymmetry and thus \(v = \next(\zero)\). Thus \(\nisprime(\nmindiv(a))\) as claimed.

_test_prime_mindiv :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_prime_mindiv _ =
  testName "if leq(next(next(zero)),a) then prime(mindiv(a)) == true" $
  \a -> if leq (next (next zero)) a
    then eq (prime (mindiv a)) true
    else true

Primes interact with \(\ngcd\) as expected.

Let \(p,a \in \nats\) with \(\nisprime(p)\). Then \[\ngcd(a,p) = \left\{ \begin{array}{ll} p & \mathrm{if}\ \ndiv(p,a) \\ \next(\zero) & \mathrm{otherwise}. \end{array} \right.\]

Let \(d = \ngcd(a,p)\). Now \(\ndiv(d,p)\), so that either \(d = \next(\zero)\) or \(d = p\). If \(\ndiv(p,a) = \bfalse\), we thus have \(d = \next(\zero)\).

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

Testing

Suite:

_test_prime ::
  ( TypeName n, Natural n, Equal n, Arbitrary n, Show n
  ) => Int -> Int -> n -> IO ()
_test_prime size cases n = do
  testLabel1 "mindiv & prime" n

  let args = testArgs size cases

  runTest args (_test_mindiv_div n)
  runTest args (_test_mindiv_min n)
  runTest args (_test_prime_mindiv n)
  runTest args (_test_prime_gcd n)

Main:

main_prime :: IO ()
main_prime = do
  _test_prime 40 100 (zero :: Unary)