||| Euclidean division using primitive recursion/induction. module Data.Nat.DivMod %default total %access public export ||| The result of euclidean division of natural numbers ||| ||| @ dividend the dividend ||| @ divisor the divisor data DivMod : (dividend, divisor : Nat) -> Type where ||| The result of division. The order of operations and operands in the ||| result type was picked to not require any explicit proofs. ||| ||| @ quotient the quotient ||| @ remainder the remainder ||| @ divisor the divisor ||| @ remainderSmall proof that the remainder is in the range ||| `[0 .. divisor - 1]` MkDivMod : (quotient, remainder : Nat) -> (remainderSmall : remainder `LT` divisor) -> DivMod (remainder + quotient * divisor) divisor ||| The base case, dividing zero by a successor. ||| ||| @ n the predecessor of the divisor ZDivModSn : Z `DivMod` S n ZDivModSn = MkDivMod 0 0 (LTESucc LTEZero) ||| Given a number less than or equal to a bound, is it equal, or less? ||| ||| @ m the lesser or equal number ||| @ n the greater or equal number ||| @ mLten proof that `m` is less than or equal to `n` stepLT : (mLten : m `LTE` n) -> Either (m = n) (m `LT` n) stepLT {m = Z} {n = Z} LTEZero = Left Refl stepLT {m = Z} {n = (S n)} LTEZero = Right (LTESucc LTEZero) stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) with (stepLT mLten) stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Left mEqn) = Left \$ cong mEqn stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Right mLtn) = Right \$ LTESucc mLtn ||| The inductive step, taking a division of `m` to a division of `S m` ||| ||| @ m the dividend in the inductive hypothesis ||| @ n the divisor ||| @ hyp the inductive hypothesis SmDivModn : (hyp : m `DivMod` n) -> (S m) `DivMod` n SmDivModn (MkDivMod q r rLtn) with (stepLT rLtn) SmDivModn (MkDivMod q r rLtn) | (Left Refl) = MkDivMod (S q) 0 (LTESucc LTEZero) SmDivModn (MkDivMod q r rLtn) | (Right srLtn) = MkDivMod q (S r) srLtn ||| Euclidean division. Note that this takes the predecessor of the divisor to ||| avoid division by zero. ||| ||| @ dividend the dividend ||| @ predDivisor the predecessor of the desired divisor divMod : (dividend, predDivisor : Nat) -> dividend `DivMod` S predDivisor divMod Z n = ZDivModSn divMod (S m) n = SmDivModn (m `divMod` n)