Coprime To

Posted on 2017-04-11 by nbloomf
Tags: arithmetic-made-difficult, literate-haskell

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 CoprimeTo
  ( coprime, _test_coprime, main_coprime
  ) where

import Testing
import Booleans
import And
import NaturalNumbers
import Times
import DivisionAlgorithm
import Divides
import GreatestCommonDivisor

Today we’ll take a break from reasoning about \(\ngcd\) to name a special relationship among natural numbers: coprimality. Recall that two integers are called coprime if their greatest common divisor is 1. This definition does not require recursion.

We define \(\ncoprime : \nats \times \nats \rightarrow \bool\) by \[\ncoprime(a,b) = \beq(\ngcd(a,b),\next(\zero)).\]

In Haskell:

Simple though it is, coprimality has some nice properties. We only need these two for now. The first result is known as Euclid’s Lemma.

Let \(a,b,c \in \nats\) such that \(\ncoprime(a,b)\) and \(\ndiv(a,\ntimes(b,c))\). Then \(\ndiv(a,c)\).

Since \(\next(\zero) = \ngcd(a,b)\), we have \[\begin{eqnarray*} & & c \\ & \href{/posts/arithmetic-made-difficult/Times.html#thm-times-one-left} = & \ntimes(\next(\zero),c) \\ & = & \ntimes(\ngcd(a,b),c) \\ & \href{/posts/arithmetic-made-difficult/GreatestCommonDivisor.html#thm-gcd-times} = & \ngcd(\ntimes(a,c),\ntimes(b,c)) \end{eqnarray*}\] But now \(\ndiv(a,\ntimes(a,c))\) and \(\ndiv(a,\ntimes(b,c))\), so that \(\ndiv(a,c)\) by the universal property of \(\ngcd\).

The second result doesn’t have a name as far as I know, but is still handy. The quotients of nonzero \(a\) and \(b\) by their (nonzero) greatest common divisor are coprime.

Let \(a,b,u,v \in \nats\) such that \(a,b \neq \zero\), \[a = \ntimes(u,\ngcd(a,b))\] and \[b = \ntimes(v,\ngcd(a,b)).\] Then \(\ncoprime(u,v)\).

Let \(k = \ngcd(u,v)\), and say \(u = \ntimes(s,k)\) and \(v = \ntimes(t,k)\). Now \[\begin{eqnarray*} & & a \\ & = & \ntimes(u,\ngcd(a,b)) \\ & = & \ntimes(s,\ntimes(k,\ngcd(a,b))) \end{eqnarray*}\] and \[\begin{eqnarray*} & & b \\ & = & \ntimes(v,\ngcd(a,b)) \\ & = & \ntimes(t,\ntimes(k,\ngcd(a,b))). \end{eqnarray*}\] In particular, \(\ntimes(k,\ngcd(a,b))\) is a common divisor of \(a\) and \(b\), and thus we have \[\ndiv(\ntimes(k,\ngcd(a,b)),\ngcd(a,b)).\] Note that \(\ngcd(a,b) \neq \zero\), so we have \(\ndiv(k,\next(\zero))\). Thus \(k = \next(\zero)\), and we have \(\ncoprime(u,v)\) as claimed.

Testing

Suite:

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

  let args = testArgs size cases

  runTest args (_test_coprime_euclids_lemma n)
  runTest args (_test_coprime_gcd_quo n)

Main:

main_coprime :: IO ()
main_coprime = do
  _test_coprime 20 100 (zero :: Unary)