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 such that . The number is the quotient , and the number is the remainder .
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 is smaller than β that we have already computed numbers with . Since the ordering on is trichotomous, we can proceed by cases on whether .
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 , i.e., can serve as a remainder for the division of . In that case, we have our divisor! It remains to show, by a slightly annoying computation, that
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 β 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, and , which works out because ( 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 . Itβs impossible because, by the definition of division, we have , meaning .
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 and . The canonical choice is to yield 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 _ _) Ξ²