@@ -0,0 +1,60 @@
1+||| Euclidean division using primitive recursion/induction.
2+module Data.Nat.DivMod
3+
4+%default total
5+
6+||| The result of euclidean division of natural numbers
7+|||
8+||| @ dividend the dividend
9+||| @ divisor the divisor
10+data DivMod : (dividend, divisor : Nat) -> Type where
11+ ||| The result of division. The order of operations and operands in the
12+ ||| result type was picked to not require any explicit proofs.
13+ |||
14+ ||| @ quotient the quotient
15+ ||| @ remainder the remainder
16+ ||| @ divisor the divisor
17+ ||| @ remainderSmall proof that the remainder is in the range
18+ ||| `[0 .. divisor - 1]`
19+ MkDivMod : (quotient, remainder : Nat) ->
20+ (remainderSmall : remainder `LT` divisor) ->
21+ DivMod (remainder + quotient * divisor) divisor
22+
23+||| The base case, dividing zero by a successor.
24+|||
25+||| @ n the predecessor of the divisor
26+ZDivModSn : Z `DivMod` S n
27+ZDivModSn = MkDivMod 0 0 (LTESucc LTEZero)
28+
29+||| Given a number less than or equal to a bound, is it equal, or less?
30+|||
31+||| @ m the lesser or equal number
32+||| @ n the greater or equal number
33+||| @ mLten proof that `m` is less than or equal to `n`
34+stepLT : (mLten : m `LTE` n) -> Either (m = n) (m `LT` n)
35+stepLT {m = Z} {n = Z} LTEZero = Left Refl
36+stepLT {m = Z} {n = (S n)} LTEZero = Right (LTESucc LTEZero)
37+stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) with (stepLT mLten)
38+ stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Left mEqn) = Left $ cong mEqn
39+ stepLT {m = (S m)} {n = (S n)} (LTESucc mLten) | (Right mLtn) = Right $ LTESucc mLtn
40+
41+||| The inductive step, taking a division of `m` to a division of `S m`
42+|||
43+||| @ m the dividend in the inductive hypothesis
44+||| @ n the divisor
45+||| @ hyp the inductive hypothesis
46+SmDivModn : (hyp : m `DivMod` n) -> (S m) `DivMod` n
47+SmDivModn (MkDivMod q r rLtn) with (stepLT rLtn)
48+ SmDivModn (MkDivMod q r rLtn) | (Left Refl) = MkDivMod (S q) 0 (LTESucc LTEZero)
49+ SmDivModn (MkDivMod q r rLtn) | (Right srLtn) = MkDivMod q (S r) srLtn
50+
51+||| Euclidean division. Note that this takes the predecessor of the divisor to
52+||| avoid division by zero.
53+|||
54+||| @ dividend the dividend
55+||| @ predDivisor the predecessor of the desired divisor
56+divMod : (dividend, predDivisor : Nat) -> dividend `DivMod` S predDivisor
57+divMod Z n = ZDivModSn
58+divMod (S m) n = SmDivModn (m `divMod` n)
59+
60+