open import 1Lab.Prelude

open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Nat.Order
open import Data.Dec.Base
open import Data.Nat.Base
open import Data.Sum.Base

module Data.Nat.DivMod where

Natural divisionπŸ”—

This module implements the basics of the theory of division (not divisibility, see there) for the natural numbers. In particular, we define what it means to divide in the naturals (the type DivMod), and implement a division procedure that works for positive denominators.

The result of division isn’t a single number, but rather a pair of numbers q,rq, r such that a=qb+ra = qb + r. The number qq is the quotient a/nba /_n b, and the number rr is the remainder a%ba \% b.

record DivMod (a b : Nat) : Type where
  constructor divmod

    quot : Nat
    rem  : Nat
    .quotient : a ≑ quot * b + rem
    .smaller  : rem < b

The easy case is to divide zero by anything, in which case the result is zero with remainder zero. The more interesting case comes when we have some successor, and we want to divide it.

divide-pos : βˆ€ a b β†’ .⦃ _ : Positive b ⦄ β†’ DivMod a b
divide-pos zero (suc b) = divmod 0 0 refl (s≀s 0≀x)

It suffices to assume β€” since aa is smaller than 1+a1+a β€” that we have already computed numbers qβ€²,rβ€²q', r' with a=qβ€²b+rβ€²a = q'b + r'. Since the ordering on N{\mathbb{N}} is trichotomous, we can proceed by cases on whether (1+rβ€²)<b(1 + r') < b.

divide-pos (suc a) b with divide-pos a b
divide-pos (suc a) b | divmod qβ€² rβ€² p s with ≀-split (suc rβ€²) b

First, suppose that 1+rβ€²<b1 + r' < b, i.e., 1+rβ€²1 + r' can serve as a remainder for the division of (1+a)/b(1 + a) / b. In that case, we have our divisor! It remains to show, by a slightly annoying computation, that

(1+a)=qβ€²b+1+r (1 + a) = q'b + 1 + r

divide-pos (suc a) b | divmod qβ€² rβ€² p s | inl rβ€²+1<b =
  divmod qβ€² (suc rβ€²) (ap suc p βˆ™ sym (+-sucr (qβ€² * b) rβ€²)) rβ€²+1<b

The other case β€” that in which 1+rβ€²=b1 + r' = b β€” is more interesting. Then, rather than incrementing the remainder, our remainder has β€œoverflown”, and we have to increment the quotient instead. We take, in this case, q=1+qβ€²q = 1 + q' and r=0r = 0, which works out because (0<b0 < b and) of some arithmetic. See for yourself:

divide-pos (suc a) (suc bβ€²) | divmod qβ€² rβ€² p s | inr (inr rβ€²+1=b) =
  divmod (suc qβ€²) 0
    ( suc a                           β‰‘βŸ¨ ap suc p βŸ©β‰‘
      suc (qβ€² * (suc bβ€²) + rβ€²)        β‰‘Λ˜βŸ¨ ap (Ξ» e β†’ suc (qβ€² * e + rβ€²)) rβ€²+1=b βŸ©β‰‘Λ˜
      suc (qβ€² * (suc rβ€²) + rβ€²)        β‰‘βŸ¨ nat! βŸ©β‰‘
      suc (rβ€² + qβ€² * (suc rβ€²) + zero) β‰‘βŸ¨ ap (Ξ» e β†’ e + qβ€² * e + 0) rβ€²+1=b βŸ©β‰‘
      (suc bβ€²) + qβ€² * (suc bβ€²) + 0    ∎ )
    (s≀s 0≀x)

Note that we actually have one more case to consider – or rather, discard – that in which b<1+rβ€²b < 1 + r'. It’s impossible because, by the definition of division, we have rβ€²<br' < b, meaning (1+rβ€²)≀b(1 + r') \le b.

divide-pos (suc a) (suc bβ€²) | divmod qβ€² rβ€² p s | inr (inl b<rβ€²+1) =
  absurd $ <-not-equal b<rβ€²+1
    (≀-antisym (≀-sucr (≀-peel b<rβ€²+1)) (recover (≀-dec _ _) s))

As a finishing touch, we define short operators to produce the result of applying divide-pos to a pair of numbers. Note that the procedure above only works when the denominator is nonzero, so we have a degree of freedom when defining x/0x/0 and x%0x \% 0. The canonical choice is to yield 00 in both cases.

_%_ : Nat β†’ Nat β†’ Nat
a % zero = zero
a % suc b = divide-pos a (suc b) .DivMod.rem

_/β‚™_ : Nat β†’ Nat β†’ Nat
a /β‚™ zero = zero
a /β‚™ suc b = divide-pos a (suc b) .DivMod.quot

is-divmod : βˆ€ x y β†’ .⦃ _ : Positive y ⦄ β†’ x ≑ (x /β‚™ y) * y + x % y
is-divmod x (suc y) with divide-pos x (suc y)
... | divmod q r Ξ± Ξ² = recover (Discrete-Nat _ _) Ξ±

x%y<y : βˆ€ x y β†’ .⦃ _ : Positive y ⦄ β†’ (x % y) < y
x%y<y x (suc y) with divide-pos x (suc y)
... | divmod q r Ξ± Ξ² = recover (≀-dec _ _) Ξ²