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, r$
such that
$a = qb + r$.
The number
$q$
is the **quotient**
$a /_n b$,
and the number
$r$
is the **remainder**
$a \% b$.

record DivMod (a b : Nat) : Type where constructor divmod field 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 $a$ is smaller than $1+a$ β that we have already computed numbers $q', r'$ with $a = q'b + r'$. Since the ordering on $\mathbb{N}$ is trichotomous, we can proceed by cases on whether $(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' < b$,
i.e.,
$1 + r'$
*can* serve as a remainder for the division of
$(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$

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' = 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'$
and
$r = 0$,
which works out because
($0 < 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'$. Itβs impossible because, by the definition of division, we have $r' < b$, meaning $(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 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/0$
and
$x \% 0$.
The canonical choice is to yield
$0$
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 Ξ± 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 Ξ²