Naturally Paired Up

It is Cantor's best-known results that there are exactly as many integers as there are fractions, although it seems to be more of the latter than of the former. There is a remarkably beautiful constructive proof of this, and I find no need to repeat the argument. It is somewhat complicated by having to take into account the fact that there is more than one way to write the same rational number q = m/n = (k·m)/(k·n) for any nonzero k. Stripped of this technicality, Cantor's diagonal argument is simple: make a tableau of pairs indexed by rows and columns, and read it by diagonals. This construction is straightforward to implement in a functional language:

let rec diag n =
  if n == 0 then (0, 0) else
  match diag (pred n) with
  | (x, 0) -> (0, succ x)
  | (x, y) -> (succ x, pred y)

This amounts to walking said diagonals and wrapping around upon hitting the edge. While this is not the most efficient diagonalization procedure one could devise, it has the virtue of being amenable to program inversion by simple inspection of the case analysis:

let rec undiag = function
| (0, 0) -> 0
| (0, y) -> succ (undiag (pred y, 0))
| (x, y) -> succ (undiag (pred x, succ y))

It is obvious both that diag is total on N and undiag is total on N×N. To prove that program inversion was correctly carried out, I will show that undiag ∘ diag = id, and diag ∘ undiag = id. The base case for the first theorem is trivial:

   undiag (diag 0)
= { Definition }
   undiag (0, 0)
= { Definition }
   0

The corresponding inductive step:

   undiag (diag n)
= { Definition with n ≠ 0 }
   undiag (match diag (pred n) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y))
= { Application over a conditional }
   match diag (pred n) with
   | (x, 0) -> undiag (0, succ x)
   | (x, y) -> undiag (succ x, pred y)
= { Definition of undiag, twice }
   match diag (pred n) with
   | (x, 0) -> succ (undiag (pred (succ x), 0))
   | (x, y) -> succ (undiag (pred (succ x), succ (pred y)))
= { Arithmetic, guard on y ≠ 0 }
   match diag (pred n) with
   | (x, 0) -> succ (undiag (x, 0))
   | (x, y) -> succ (undiag (x, y))
= { Identity guards }
   succ (undiag (diag (pred n)))
= { Inductive step }
   succ (pred n)
= { n ≠ 0 }
   n

The base case of the second identity is:

   diag (undiag (0, 0))
= { Definition }
   diag 0
= { Definition }
   (0, 0)

I will show the inductive step by case analysis. If on the first row:

   diag (undiag (0, y))
= { Definition with y ≠ 0 }
   diag (succ (undiag (pred y, 0)))
= { Definition of diag with n ≠ 0 }
   match (diag (pred (succ (undiag (pred y, 0))))) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Arithmetic }
   match (diag (undiag (pred y, 0))) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Inductive step }
   match (pred y, 0) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Guard }
   (0, succ (pred y))
= { y ≠ 0 }
   (0, y)

The second case is for a general pair:

   diag (undiag (x, y))
= { Definition with x ≠ 0 }
   diag (succ (undiag (pred x, succ y)))
= { Definition }
   match (diag (pred (succ (undiag (pred x, succ y))))) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Arithmetic }
   match (diag (undiag (pred x, succ y))) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Inductive step }
   match (pred x, succ y) with
   | (x, 0) -> (0, succ x)
   | (x, y) -> (succ x, pred y)
= { Guard }
   (succ (pred x), pred (succ y))
= { x ≠ 0 }
   (x, y)

The corollary is that, indeed, N is isomorphic to N×N, as witnessed by diag and undiag.

Now the latter has a well-known arithmetic expression that doesn't require primitive recursion over the naturals:

let undiag (x, y) =
  let k = x + y in
  let t = k * (k + 1) / 2 in
  t + x

The k-th diagonal contains the k+1 pairs whose components sum to k. This means that the first pair (0, k) on the diagonal has T.k = k·(k+1)/2 pairs preceding it. It is rather tedious to prove that this is in fact equal to the recursive version:

   undiag (0, 0)
=
   0
=
   (0 + 0) * (0 + 0 + 1) / 2 + 0

and

   undiag (0, y)
= { Definition }
   1 + undiag (y - 1, 0)
= { Induction }
   1 + (y - 1) * y / 2 + y - 1
= { Arithmetic }
   y * (y + 1) / 2
=
   (0 + y) * (0 + y + 1) / 2 + 0

and finally

   undiag (x, y)
= { Definition }
   1 + undiag (x - 1, y + 1)
= { Induction }
   1 + (x - 1 + y + 1) * (x - 1 + y + 1 + 1) / 2 + x - 1
= { Arithmetic }
   (x + y) * (x + y + 1) / 2 + x

In every case, I have aimed at arriving at the expansion of undiag x y = (x + y)·(x + y + 1)/2 + x. Now this is again amenable to inversion, albeit of a different nature:

let diag n =
  let k = truncate (floor (sqrt (0.25 +. 2. *. float n) -. 0.5)) in
  let t = n - k * (k + 1) / 2 in
  (t, k - t)

Regarded as a quadratic equation, k·(k+1)/2 - n = 0 for positive k = √(¼ + 2·n) - ½; the diagonal starts with the pair indexed by ⌊k⌋. Then, the offset is the corresponding remainder. Beyond the evidently correct arithmetic inversion, it is equationally immediate that this version of diag is equivalent to the primitive recursive one:

   diagR = diagA
≡ { undiag is total }
   undiagA ∘ diagR = undiagA ∘ diagA
≡ { undiagA = undiagR }
   undiagR ∘ diagR = id
≡
   true