||| Division of natural numbers, by iterated subtraction using well-founded ||| recursion module Data.Nat.DivMod.IteratedSubtraction import Data.Fin import Data.So import Control.WellFounded %default total %access public ||| A strict less-than relation on `Nat`. ||| ||| @ n the smaller number ||| @ m the larger number data LT' : (n,m : Nat) -> Type where ||| n < 1 + n LTSucc : LT' n (S n) ||| n < m implies that n < m + 1 LTStep : LT' n m -> LT' n (S m) %name LT' lt, lt' ||| Nothing is strictly less than zero instance Uninhabited (LT' n 0) where uninhabited LTSucc impossible ||| Zero is less than any non-zero number. LTZeroLeast : LT' Z (S n) LTZeroLeast {n = Z} = LTSucc LTZeroLeast {n = S n} = LTStep LTZeroLeast ||| If n < m, then 1 + n < 1 + m ltSuccSucc : LT' n m -> LT' (S n) (S m) ltSuccSucc LTSucc = LTSucc ltSuccSucc (LTStep lt) = LTStep \$ ltSuccSucc lt ||| If n + 1 < m, then n < m lteToLt' : LTE (S n) m -> LT' n m lteToLt' {n = Z} (LTESucc x) = LTZeroLeast lteToLt' {n = S k} (LTESucc x) = ltSuccSucc \$ lteToLt' x ||| Convert from LT' to LTE ltToLTE : LT' n m -> LTE (S n) m ltToLTE LTSucc = lteRefl ltToLTE (LTStep lt) = lteSuccRight \$ ltToLTE lt ||| Subtraction gives a result that is actually smaller. minusLT' : (x,y : Nat) -> x - y `LT'` S x minusLT' Z y = LTSucc minusLT' (S k) Z = LTSucc minusLT' (S k) (S j) = LTStep (minusLT' k j) ||| Strict less-than is well-founded, with the cascade stopping at ||| zero (because there's nothing less than zero). This can't be done ||| for LTE, because that one doesn't stop at zero (because `LTE 0 0` ||| is inhabited). instance WellFounded LT' where wellFounded x = Access (acc x) where ||| Show accessibility by induction on the structure of the LT' witness acc : (x, y : Nat) -> LT' y x -> Accessible LT' y -- Zero is vacuously accessible: there's nothing smaller to check acc Z y lt = absurd lt -- If the element being accessed is one smaller, we're done acc (S y) y LTSucc = Access (acc y) -- If the element is more than one smaller, we need to go further acc (S k) y (LTStep smaller) = acc k y smaller ||| The result of division on natural numbers. ||| ||| @ dividend the dividend ||| @ divisor the divisor data DivMod : (dividend, divisor : Nat) -> Type where ||| The result of division, with a quotient and a remainder. ||| ||| @ dividend the dividend ||| @ divisor the divisor ||| @ quotient the quotient ||| @ remainder the remainder (bounded by the divisor) ||| @ ok the fact that this is, in fact, a result of division DivModRes : {dividend, divisor : Nat} -> (quotient : Nat) -> (remainder : Fin divisor) -> (ok : dividend = finToNat remainder + quotient * divisor) -> DivMod dividend divisor ||| Any natural number can be a `Fin` where the bound is itself plus some difference. private toFin : (x : Nat) -> (diff : Nat) -> Fin (plus x (S diff)) toFin Z diff = FZ toFin (S k) diff = FS \$ toFin k diff ||| Converting to a `Fin` and back to `Nat` preserves the input. This is a correctness proof for `toFin`. private toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x toFinAndBack Z diff = Refl toFinAndBack (S k) diff = cong (toFinAndBack k diff) ||| The accessibilty predicate used for division. private accPlusLT' : LT' (S j) (S (plus k (S j))) accPlusLT' {j = Z} {k = Z} = LTSucc accPlusLT' {j = Z} {k = S k} = LTStep (accPlusLT' {j = Z} {k = k}) accPlusLT' {j = S j} {k = k} = rewrite sym \$ plusSuccRightSucc k (S j) in ltSuccSucc accPlusLT' ||| Division and modulus on `Nat`, inspired by the definition in the ||| Agda standard library. ||| ||| This uses well-founded recursion on `LT'`. ||| ||| @ dividend the dividend ||| @ divisor the divisor ||| @ nonzero division by zero is nonsense total -- yay! divMod : (dividend, divisor : Nat) -> {auto nonzero : So (not (decAsBool (decEq divisor Z)))} -> DivMod dividend divisor divMod _ Z {nonzero} = absurd nonzero divMod Z (S k) = DivModRes 0 FZ Refl divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero where ||| The goal passed to the accessibility eliminator. ||| ||| This is responsible for generating the goal in the ||| well-founded fixed point. ||| ||| @ dividend the dividend to recurse over P : (dividend : Nat) -> Type P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor ||| Well-founded recursion needs a recursion operator. ||| ||| @ dividend the dividend we are recursing over ||| @ rec the recursive call provided by the well-founded induction operator stepDiv : (dividend : Nat) -> (rec : (d' : Nat) -> LT' d' dividend -> P d') -> P dividend -- We need not consider division by zero stepDiv dividend rec Z nonzero = absurd nonzero -- Dividing zero by anyting else gives 0, with 0 remainder stepDiv Z rec (S k) nonzero = DivModRes 0 0 Refl -- To divide two non-zero values, we must know which is larger stepDiv (S j) rec (S k) nonzero with (cmp j k) -- n / n = 1 remainder 0 stepDiv (S j) rec (S j) nonzero | CmpEQ = DivModRes 1 0 (sym \$ cong (plusZeroRightNeutral j)) -- if n < m, then m = n + r, and the quotient is 0 with remainder r stepDiv (S j) rec (S (plus j (S diff))) nonzero | CmpLT diff = DivModRes 0 (toFin (S j) diff) \$ rewrite toFinAndBack j diff in sym \$ cong (plusZeroRightNeutral j) -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder stepDiv (S (plus k (S diff))) rec (S k) nonzero | CmpGT diff = let res = rec (S diff) accPlusLT' (S k) Oh in case res of DivModRes quotient remainder ok => DivModRes (S quotient) remainder \$ rewrite plusAssociative (finToNat remainder) (S k) (mult quotient (S k)) in rewrite plusCommutative (finToNat remainder) (S k) in rewrite sym \$ plusAssociative (S k) (finToNat remainder) (mult quotient (S k)) in rewrite ok in Refl