-- Some isomorphisms between ℕ and ℕ×ℕ.

||| An isomorphism between ℕ and ℕ×ℕ, counting off "by squares", like this:
|||
||| 0 3 8
||| 1 2 7
||| 4 5 6
|||
||| and so on, where the first column contains the square numbers.
||| sqIso' is the inverse.

!!! ∀ n : Nat. sqIso (sqIso' n) == n

sqIso : ℕ×ℕ → ℕ
sqIso (x,y) =
  {? y^2 + x           if x <= y,
     (x+1)^2 .- 1 .- y   otherwise
  ?}

||| Inverse direction of the square isomorphism.

!!! ∀ p : Nat*Nat. sqIso' (sqIso p) == p

sqIso' : ℕ → ℕ×ℕ
sqIso' n =
  let r = sqrt n
  in  {? (n .- r^2, r)            if  n <= r^2 + r,
         (r, (r+1)^2 .- 1 .- n)    otherwise
      ?}

||| The classic "diagonal" isomorphism:
|||
||| 0 2 5
||| 1 4
||| 3
|||
||| where the first column contains the triangular numbers.

!!! ∀ n : Nat. diagIso (diagIso' n) == n
!!! ∀ p : Nat * Nat. diagIso' (diagIso p) == p

diagIso : ℕ×ℕ → ℕ
diagIso (x,y) = (x+y)*(x+y+1)//2 + x

diagIso' : ℕ → ℕ×ℕ
diagIso' n =
     let d = (sqrt(1 + 8n) .- 1)//2 : N
  in let t = d*(d+1)//2
  in (n .- t, d .- (n .- t))


||| Every POSITIVE n can be decomposed into a power of two times an
||| odd number, n = 2^x (2y + 1).  This creates an isomorphism n <->
||| (x,y).  This is actually an isomorphism between {n | n : ℕ, n > 0}
||| and ℕ×ℕ, but at the moment the disco type system doesn't let us
||| say that (and it likely never will).

-- We have to be careful not to call powerIsoPos' 0 because it gets stuck
-- in infinite recursion!  One way that would work is to write the
-- test as follows:

!!! forall n:Nat. powerIsoPos (powerIsoPos' (n+1)) == (n+1)

-- Alternatively, since 'implies' is lazy (i.e. "short-circuiting"),
-- we can write

!!! ∀ n : Nat. (n > 0) ==> powerIsoPos (powerIsoPos' n) == n

powerIsoPos : ℕ×ℕ → ℕ
powerIsoPos (x,y) = 2^x * (2y + 1)

powerIsoPos' : ℕ → ℕ×ℕ
powerIsoPos' n =
  {? (0, n//2)  if not (2 divides n),
     (x+1,y)    when powerIsoPos' (n//2) is (x,y)
  ?}

||| We can turn powerIsoPos into an isomorphism between all natural
||| numbers and ℕ×ℕ simply by adding and subtracting one.

!!! forall n:Nat. powerIso (powerIso' n) == n
!!! ∀ p : ℕ×ℕ. powerIso' (powerIso p) == p

powerIso : ℕ×ℕ → ℕ
powerIso(p) = powerIsoPos(p) .- 1

powerIso' : ℕ → ℕ×ℕ
powerIso'(n) = powerIsoPos'(n+1)


||| And finally, there is a very cool isomorphism called "Morton
||| Z-order" which takes a pair of natural numbers, expresses them in
||| binary, and interleaves their binary representations to form a
||| single natural number.  It ends up looking like this:
|||
||| 0 2 8  10
||| 1 3 9  11
||| 4 6 12 14
||| 5 7 13 15

!!! forall n:N. zOrder(zOrder'(n)) == n
!!! forall p:N*N. zOrder'(zOrder(p)) == p

zOrder : ℕ×ℕ → ℕ
zOrder(0,0) = 0
zOrder(2m,n) = 2 * zOrder(n,m)
zOrder(2m+1,n) = 2 * zOrder(n,m) + 1

zOrder' : ℕ → ℕ×ℕ
zOrder'(0)    = (0,0)
zOrder'(2n)   = {? (2y,x) when zOrder'(n) is (x,y) ?}
zOrder'(2n+1) = {? (2y+1,x) when zOrder'(n) is (x,y) ?}