## Exercise 3.23

divN ∷ Nat -> Nat -> Nat as an instance of unfoldN or unfoldN'.

We'll assume that division by zero causes an exception to be raised.
It's possible to return a Maybe value, but this is a needless
complication, since there's never any useful information to be had
from a divide-by-zero.

We have a further issue, though--we'll need to make use of subN, which
returns a Maybe value.

To express this as an unfold, we interpret integer division as repeated
subtraction of the divisor b from the dividend a, terminating when the
dividend is zero.  That is, we will unfold on a, which means reversing
the order of the arguments.

Using the universal property of unfoldN, we have

    divN b = unfoldN p f

    iff

    divN b x = if p x then Zero else Succ (divN b (f x))

Since we need to use subN, x ∷ Maybe Nat.

Using a = bq + r and ignoring r, we know that q = Zero when a = Zero
or a < b.  So we define

    p ∷ Maybe Nat -> Bool
    p (Just Zero)     = True    -- unneeded, see below
    p (Just (Succ a)) = lessN (Succ a) b

But we've excluded the (undefined) case b = Zero, so, if a = Zero, then
we can conclude a < b.  So the first case can be dropped.

We have:

    divN b (Just Zero) = Zero

For the case p x = False, we have a ≥ b.  So:

    divN b a = Succ (divN b (subN a b)),  (*)

that is, the quotient of a and b is one plus the quotient of (a - b)
and b.

      divN b (Just (Succ a)) = if p (Just (Succ a))
                                 then Zero
                                 else Succ (divN b (f (Just (Succ a))))

    ≡   { p (Just (Succ a)) = False, ITE }

      divN b (Just (Succ a)) = Succ (divN b (f (Just (Succ a))))

    ≡   { (*) }

      Succ (divN b (subN (fromJust (Just (Succ a))) b))
        = Succ (divN b (f (Just (Succ a))))

    ≡   { abstraction }

      Succ (divN b ((λma → subN (fromJust ma) b) (Just (Succ a))))
        = Succ (divN b (f (Just (Succ a))))

    ≡   { generalizing (Just (Succ a)) to mx }

      Succ (divN b ((λma → subN (fromJust ma) b) mx)) = Succ (divN b (f mx))

which gives us a solution for f.

    f ∷ Maybe Nat -> Maybe Nat
    f Nothing  = Nothing  -- can't happen
    f (Just a) = subN a b

where b is in the enclosing function's scope.

So the final definition (using an as-pattern for clarity) is:

    divN a b@(Succ x) = unfoldN p f (Just a)
      where
        p (Just m) = lessN m b
        f (Just c) = subN c b