Exercise 5.13 (Scott 1981, PRG-19, Lecture V) — a one-one pairing `num : N × N →

N`

Prove the existence of a one-one function num : ℕ × ℕ → ℕ such that

• num(0, 0) = 0,
• num(n, m+1) = num(n+1, m) + 1,
• num(n+1, 0) = num(0, n) + 1.

Draw a picture (an infinite matrix) for the function and find a closed form for its values. Use the function to prove the isomorphism of the domains P N, P(N × N), P N × P N.

The picture

Reading n down the rows and m across the columns, the three recurrences walk the anti-diagonals n + m = const, climbing one step (+1) each move and jumping to the start of the next diagonal at the left edge:

        m=0   m=1   m=2   m=3
n=0      0     2     5     9
n=1      1     4     8
n=2      3     7
n=3      6

The closed form

On the anti-diagonal s = n + m the values run T(s), T(s)+1, …, T(s)+s where T(s) = s(s+1)/2 is the s-th triangular number; the offset within the diagonal is exactly m. Hence

num n m = (n + m) * (n + m + 1) / 2 + m

— the Cantor pairing function. We take this as the definition (num), verify Scott's three recurrences (num_zero_zero, num_succ_right, num_succ_left), and prove it is one-one (num_injective). In fact it is a bijection: we build a choice-free inverse unnum (iterate the diagonal walk nextCell from (0,0)) and package the bijection as numEquiv : ℕ × ℕ ≃ ℕ.

The domain isomorphisms

Following Exercise 4.17, the power-set domain P A is modelled by the complete lattice (Set A, ⊆). Order-isomorphisms of these domains are then induced by bijections of the index types (setCongr). Since ℕ × ℕ ≃ ℕ (via numEquiv) and ℕ ⊕ ℕ ≃ ℕ (Mathlib's Equiv.natSumNatEquivNat), all three domains are isomorphic:

P N ≅ P(N × N) (pnOrderIsoPNN), P N ≅ P N × P N (pnOrderIsoProd), P(N × N) ≅ P N × P N (pnnOrderIsoProd).

Everything (including numEquiv and the order-isomorphisms) is choice-free (#print axioms ⊆ {propext, Quot.sound}).

Triangular numbers

def Domain.Neighborhood.Exercise513.tri (k : ℕ) : ℕ

The k-th triangular number T(k) = k(k+1)/2.

Equations

• Domain.Neighborhood.Exercise513.tri k = k * (k + 1) / 2

theorem Domain.Neighborhood.Exercise513.two_dvd_mul_succ (k : ℕ) : 2 ∣ k * (k + 1)

k(k+1) is even (choice-free, by induction).

theorem Domain.Neighborhood.Exercise513.tri_mul_two (k : ℕ) : tri k * 2 = k * (k + 1)

The defining doubling identity 2·T(k) = k(k+1) — the division is exact because k(k+1) is even.

theorem Domain.Neighborhood.Exercise513.tri_succ (k : ℕ) : tri (k + 1) = tri k + (k + 1)

The triangular recurrence T(k+1) = T(k) + (k+1).

theorem Domain.Neighborhood.Exercise513.tri_le_succ (k : ℕ) : tri k ≤ tri (k + 1)

theorem Domain.Neighborhood.Exercise513.tri_mono {a b : ℕ} (h : a ≤ b) : tri a ≤ tri b

T is monotone (proved by hand on ≤ to stay choice-free).

The pairing function num

def Domain.Neighborhood.Exercise513.num (n m : ℕ) : ℕ

The pairing function num n m = (n+m)(n+m+1)/2 + m (Cantor's diagonal enumeration).

Equations

• Domain.Neighborhood.Exercise513.num n m = Domain.Neighborhood.Exercise513.tri (n + m) + m

def Domain.Neighborhood.Exercise513.numP (p : ℕ × ℕ) : ℕ

Its uncurried form, the actual N × N → N of the exercise.

Equations

• Domain.Neighborhood.Exercise513.numP p = Domain.Neighborhood.Exercise513.num p.1 p.2

theorem Domain.Neighborhood.Exercise513.num_zero_zero : num 0 0 = 0

theorem Domain.Neighborhood.Exercise513.num_succ_right (n m : ℕ) : num n (m + 1) = num (n + 1) m + 1

theorem Domain.Neighborhood.Exercise513.num_succ_left (n : ℕ) : num (n + 1) 0 = num 0 n + 1

theorem Domain.Neighborhood.Exercise513.num_lt_tri_succ (n m : ℕ) : num n m < tri (n + m + 1)

The value num n m sits in the half-open diagonal block [T(n+m), T(n+m+1)): the upper bound.

theorem Domain.Neighborhood.Exercise513.num_injective : Function.Injective numP

The function is one-one. The diagonal s = n+m is recovered as the unique s with T(s) ≤ num n m < T(s+1); then m is the offset and n = s - m.

The inverse: walking the diagonals

def Domain.Neighborhood.Exercise513.nextCell : ℕ × ℕ → ℕ × ℕ

One step of the diagonal walk: the cell holding num c + 1. Moving up-right within a diagonal, or to the start of the next diagonal at the top edge.

Equations

• Domain.Neighborhood.Exercise513.nextCell (n.succ, m) = (n, m + 1)
• Domain.Neighborhood.Exercise513.nextCell (0, m) = (m + 1, 0)

theorem Domain.Neighborhood.Exercise513.numP_nextCell (c : ℕ × ℕ) : numP (nextCell c) = numP c + 1

def Domain.Neighborhood.Exercise513.unnum : ℕ → ℕ × ℕ

The inverse unnum v = nextCellᵛ (0, 0).

Equations

• Domain.Neighborhood.Exercise513.unnum 0 = (0, 0)
• Domain.Neighborhood.Exercise513.unnum v.succ = Domain.Neighborhood.Exercise513.nextCell (Domain.Neighborhood.Exercise513.unnum v)

theorem Domain.Neighborhood.Exercise513.numP_unnum (v : ℕ) : numP (unnum v) = v

theorem Domain.Neighborhood.Exercise513.unnum_numP (c : ℕ × ℕ) : unnum (numP c) = c

def Domain.Neighborhood.Exercise513.numEquiv : ℕ × ℕ ≃ ℕ

Exercise 5.13. The pairing function packaged as a bijection ℕ × ℕ ≃ ℕ (choice-free, via the explicit inverse unnum).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.Exercise513.numEquiv_apply (p : ℕ × ℕ) : numEquiv p = num p.1 p.2

The domain isomorphisms

The power-set domain P A is the complete lattice (Set A, ⊆) (Exercise 4.17). A bijection of index types lifts to an order-isomorphism of power-set domains.

def Domain.Neighborhood.Exercise513.setCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : Set α ≃o Set β

A bijection α ≃ β induces an order-isomorphism P α ≅ P β of power-set domains, by direct image.

Equations

• Domain.Neighborhood.Exercise513.setCongr e = { toFun := fun (S : Set α) => ⇑e '' S, invFun := fun (T : Set β) => ⇑e.symm '' T, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Domain.Neighborhood.Exercise513.pnOrderIsoPNN : Set ℕ ≃o Set (ℕ × ℕ)

P N ≅ P(N × N) — induced by the pairing bijection numEquiv.

Equations

• Domain.Neighborhood.Exercise513.pnOrderIsoPNN = Domain.Neighborhood.Exercise513.setCongr Domain.Neighborhood.Exercise513.numEquiv.symm

def Domain.Neighborhood.Exercise513.pnOrderIsoProd : Set ℕ ≃o Set ℕ × Set ℕ

P N ≅ P N × P N — N ≅ N ⊕ N together with P(A ⊕ B) ≅ P A × P B (Set.sumEquiv).

Equations

• Domain.Neighborhood.Exercise513.pnOrderIsoProd = (Domain.Neighborhood.Exercise513.setCongr Equiv.natSumNatEquivNat.symm).trans Set.sumEquiv

def Domain.Neighborhood.Exercise513.pnnOrderIsoProd : Set (ℕ × ℕ) ≃o Set ℕ × Set ℕ

P(N × N) ≅ P N × P N — by composing the two isomorphisms above.

Equations

• Domain.Neighborhood.Exercise513.pnnOrderIsoProd = Domain.Neighborhood.Exercise513.pnOrderIsoPNN.symm.trans Domain.Neighborhood.Exercise513.pnOrderIsoProd