## Exercise 3.24

Define logN ∷ Nat -> Nat -> Nat as an instance of unfoldN.

We want to compute logN b n = log to the base b of n, rounded down to
the nearest natural.  We can compute this by successive divisions of
n by b, using the fact that log b n = m iff n / (b ^ m) = 1.

    log b Zero              = Zero     -- round down
    log b (Succ Zero)       = Zero
    log b n@(Succ (Succ m)) = Succ (log b (divN n b))

This means that we will be unfolding on n.  Using the universal
property of unfoldN, we have:

    logN b = unfoldN p f

    iff

    logN b n = if p n then Zero else Succ (logN b (f n))

Using the recursive equations above, we define:

    p Zero            = True
    p (Succ Zero)     = True
    p (Succ (Succ n)) = False

When p is false, we reason:

      logN b n = Succ (logN b (f n))

    ≡   { n > 1, log.3 }

      Succ (logN b (divN n b)) = Succ (logN b (f n))

    ≡   { abstraction }

      Succ (logN b ((λm -> divN m b) n)) = Succ (logN b (f n))

which gives us a solution for f.

    logN b = unfoldN p f
      where
        p Zero            = True
        p (Succ Zero)     = True
        p (Succ (Succ n)) = False
        f m = divN m b