Learning Number Theory and Haskell: More QuickCheck and Divisors

This is part two of my series Learning Number Theory and Haskell. Last time, we implemented a division algorithm according to an exact specification from Jones Elementary Number Theory. We used the QuickCheck testing library to make ourselves fairly confident that the code was actually correct (in other words, behaved according to certain expectations).

More QuickCheck

Since QuickCheck may be feeling pretty new right now, let’s play around with it for a bit. Exercises 1.1 and 1.2 of the Jones text give some interesting theorems about the remainders of perfect squares. We will verify these theorems with a hundred or so random test cases each. (Note that I’ve now stopped using the jonesQuot and jonesRem functions defined earlier. It was nice to be able to reproduce that behavior, but it’s nicer to become skilled at using the standard library functions instead of inventing our own replacements. We’ll just be careful about negative numbers from here on.)

Prelude> :qc \\n -> (n^2 `rem` 4) `elem` [0, 1]
+++ OK, passed 100 tests.
Prelude> :qc \\n -> (n^2 `rem` 3) `elem` [0, 1]
+++ OK, passed 100 tests.
Prelude> :qc \\n -> (n^2 `rem` 5) `elem` [0, 1, 4]
+++ OK, passed 100 tests.
Prelude> :qc \\n -> (n^2 `rem` 6) `elem` [0, 1, 3, 4]
+++ OK, passed 100 tests.

Yep, they all check out. Of course, you should still write proofs because, as you’re probably quite familiar by now, QuickCheck is suitable for contradicting things or providing evidence in favor, but not for proving things.

Generalizing the Proof Method

I was interested in this concept, so I extended it to arbitrary divisors with a simple Haskell program that generalizes the method of the proofs in the text. If you’re following along to learn Haskell, this makes use of two shorthands for creating lists. The innermost list [0 .. d - 1] is an arithmetic sequence, and hopefully it’s fairly obvious what that does. The outer list is built using a list comprehension. The vertical bar should still be read as “such that”, and in this context, <- is read as “element of”. So the outermost list is the list of all (n^2) `rem` d such that n is an element of [0 .. d - 1]. These techniques make a lot of mathematical code in Haskell very concise, and keep it closer to math syntax. Finally, nub just removes the duplicates from a list. You can :edit NumTheory.hs again, and add the following:

import Data.List (nub) -- Add this at the top of the file, by the other import

squareRems d = nub $ [(n^2) `rem` d | n <- [0 .. d - 1] ]

We can check this, but we’ll need to be careful about negative values of the divisor since I used rem instead of jonesRem.

Prelude> :l NumTheory
[1 of 1] Compiling NumTheory        ( NumTheory.hs, interpreted )
Ok, modules loaded: NumTheory.
*NumTheory> :qc \\n d -> (d > 0) ==> ((n^2) `rem` d) `elem` squareRems d
+++ OK, passed 100 tests.

This algorithm can be supported by a proof that is not given in the text. The theorem is that the remainder of a² when divided by d is equal to the remainder of some k², where 0 <= k < d. This is proven by writing a as qd + r by the division algorithm. The a² = q²d² + 2qdr + r². In turn, r² can be written as pd + s by the division algorithm. Then a² = q²d² + 2qdr + pd + s, which in turn is equal to d(q²d + 2qr + p) + s. Thus, a² gives a remainder of s, but so does r², and we know that 0 <= r < d. It should, therefore, be no surprise that the QuickCheck test succeeds.

Divisors

The next set of theorems from the text deal with divisors.  If we’d like to verify these theorems using QuickCheck, we need a way to decide if one number divides another one or not. Following Jones, we’ll say (b | a), read as “b divides a,” iff there is some integer q such that a = qb. Recall that for any pair of numbers a and b, with b not equal to 0, there is a unique pair of integers (q, r) such that a = qb + r and 0 <= r < b. In the special case that b is not zero, it’s clear that b | a iff r = 0 for the unique values of q and r given by the division algorithm.

b `divides` a = a `rem` b == 0

This leaves out the possibility that b = 0. The function above will fail if that occurs, because rem a b is undefined when b = 0. So we go back to the definition, which is that b divides a iff there is a q so that a = qb. If b = 0, that equation becomes a = 0b, which is only true if a = 0. Adding that as a special case, the function looks like this:

0 `divides` a  = a == 0
b `divides` a  = a `rem` b == 0

(This is a definition by pattern matching, which is one of the nicest syntax aspects of the Haskell language. The order is significant here, as the second version of the function will match all possible parameters that aren’t matched beforehand.)

I’ve convinced myself that the function is correct, but it’s time for some good old QuickCheck. The text gives a few corner cases explicitly at the top of page 4, so we can test them.

*NumTheory> :qc \\n -> n `divides` 0
+++ OK, passed 100 tests.
*NumTheory> :qc \\n -> 1 `divides` n
+++ OK, passed 100 tests.
*NumTheory> :qc \\n -> n `divides` n
+++ OK, passed 100 tests.

Excellent! Now we’d like to test the general case so we can be really sure that divides is correct… but how? All we have is that b divides a iff for some q, a = qb. We need to know something more about q than it merely being an integer to make this work. A convenient property is given in exercise 1.3 (d) from the Jones text. If a satisfactory q exists, it must divide a itself, so it is between –a and a. The case not covered by this reasoning is when a = 0, but then q = 0 will definitely do the trick! Let’s write a test.

*NumTheory> :qc \\a b -> (b `divides` a) == any (\\q -> a == q * b) [(- abs a) .. abs a]
+++ OK, passed 100 tests.

Here, I build a list of all possible values for q, and then use the built-in any function to see if any of them work. Notice that the first parameter to any is another function, which I’ve written using the anonymous lambda syntax. This is far too slow to be used for an implementation, but it works fine as a test.

Testing a Property of Divisors

Let us now make use of our new function. Exercise 1.4 of the text asks whether it is the case that if a | b and c | d, then (a + c) | (b + d). If you’re following along with me in the text, which I hope you are, you should convince yourself of the answer ahead of time by more mundane means. QuickCheck easily gives the answer.

(Here’s a comprehension quiz. The mere fact that QuickCheck can provide a definite answer should tell you what the answer is. Why?)

*NumTheory> :qc \\a b c d -> ((a `divides` b) && (c `divides` d)) ==> (a + c) `divides` (b + d)
*** Failed! Falsifiable (after 5 tests and 7 shrinks):
1
1
1
0

So not only do we get an answer (no, the conjecture is false!), but we get a counter-example. If a = 1, b = 1, c = 1, and d = 0, then it is true that a | b because b = (-2)a and c | d because d = (-1)c, but it is not true that (a + c) | (b + d).  a + c is 2, and b + d is 1, and clearly there is no integer q such that 1 = 2q.