Binary search division

bdiv.hs

ultraDiv ∷ Integer → Integer → (Integer, Integer)
-- pre: 1 <= d <= n
-- post: a*d + b == n
--    && (A) x > d . (a*x > n)
--         where
--           (a, b) = ultraDiv n d
ultraDiv n d = bDiv n d 1 n
  where
    -- pre: same as ultraDiv
    --   && d * lower <= n && d * upper > n
    -- post: same as ultraDiv
    -- invariant: lower <= middle < upper
    --         && (A) x in [0, lower] . (x * d <= n)
    --         && (A) x in (upper..]  . (x * d > n)
    -- variant: upper-lower
    bDiv n d lower upper
       | lower ≡ upper-1  = (lower, n - d*lower)
       | middle*d > n     = bDiv n d lower middle
       | otherwise        = bDiv n d middle upper
      where
        middle = (upper + lower) `div` 2

ultraDiv2 ∷ Integer → Integer → (Integer, Integer)
-- pre: 1 <= d <= n
-- post: a*d + b == n
--    && (A) x > d . (a * x > n)
--         where
--           (a, b) = ultraDiv2 n d
ultraDiv2 n d = bDiv n d 1 n
    where
      -- pre: same as ultraDiv2
      --   && d * lower <= n && d * (lower+i) >= n
      -- post: same as ultraDiv2
      -- invariant: lower <= lower+i
      --         && (A) x in [0, lower]  . (x * d <= n)
      --         && (A) x in [lower+i..] . (x * d >= n)
      -- variant: i
      bDiv n d lower i
          | i ≡ 0            = (lower, n - d*lower)
          | (lower+i)*d ≤ n  = bDiv n d (lower+i) (i `div` 2)
          | otherwise        = bDiv n d lower (i `div` 2)