@@ -0,0 +1,165 @@
1+||| Extra utilities for working with Nats
2+module Data.Nat
3+
4+import Data.Fin
5+import Data.So
6+
7+import Control.WellFounded
8+
9+%default total
10+
11+||| A strict less-than relation on `Nat`.
12+|||
13+||| @ n the smaller number
14+||| @ m the larger number
15+data LT' : (n,m : Nat) -> Type where
16+ ||| n < 1 + n
17+ LTSucc : LT' n (S n)
18+ ||| n < m implies that n < m + 1
19+ LTStep : LT' n m -> LT' n (S m)
20+
21+%name LT' lt, lt'
22+
23+||| Nothing is strictly less than zero
24+instance Uninhabited (LT' n 0) where
25+ uninhabited LTSucc impossible
26+
27+||| Zero is less than any non-zero number.
28+LTZeroLeast : LT' Z (S n)
29+LTZeroLeast {n = Z} = LTSucc
30+LTZeroLeast {n = S n} = LTStep LTZeroLeast
31+
32+||| If n < m, then 1 + n < 1 + m
33+ltSuccSucc : LT' n m -> LT' (S n) (S m)
34+ltSuccSucc LTSucc = LTSucc
35+ltSuccSucc (LTStep lt) = LTStep $ ltSuccSucc lt
36+
37+||| If n + 1 < m, then n < m
38+lteToLt' : LTE (S n) m -> LT' n m
39+lteToLt' {n = Z} (LTESucc x) = LTZeroLeast
40+lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x
41+
42+||| Convert from LT' to LTE
43+ltToLTE : LT' n m -> LTE (S n) m
44+ltToLTE LTSucc = lteRefl
45+ltToLTE (LTStep lt) = lteSuccRight $ ltToLTE lt
46+
47+||| Subtraction gives a result that is actually smaller.
48+minusLT' : (x,y : Nat) -> x - y `LT'` S x
49+minusLT' Z y = LTSucc
50+minusLT' (S k) Z = LTSucc
51+minusLT' (S k) (S j) = LTStep (minusLT' k j)
52+
53+||| Strict less-than is well-founded, with the cascade stopping at
54+||| zero (because there's nothing less than zero). This can't be done
55+||| for LTE, because that one doesn't stop at zero (because `LTE 0 0`
56+||| is inhabited).
57+instance WellFounded LT' where
58+ wellFounded x = Access (acc x)
59+ where
60+ ||| Show accessibility by induction on the structure of the LT' witness
61+ acc : (x, y : Nat) -> LT' y x -> Accessible LT' y
62+ -- Zero is vacuously accessible: there's nothing smaller to check
63+ acc Z y lt = absurd lt
64+ -- If the element being accessed is one smaller, we're done
65+ acc (S y) y LTSucc = Access (acc y)
66+ -- If the element is more than one smaller, we need to go further
67+ acc (S k) y (LTStep smaller) = acc k y smaller
68+
69+||| The result of division on natural numbers.
70+|||
71+||| @ dividend the dividend
72+||| @ divisor the divisor
73+data DivMod : (dividend, divisor : Nat) -> Type where
74+ ||| The result of division, with a quotient and a remainder.
75+ |||
76+ ||| @ dividend the dividend
77+ ||| @ divisor the divisor
78+ ||| @ quotient the quotient
79+ ||| @ remainder the remainder (bounded by the divisor)
80+ ||| @ ok the fact that this is, in fact, a result of division
81+ DivModRes : {dividend, divisor : Nat} ->
82+ (quotient : Nat) -> (remainder : Fin divisor) ->
83+ (ok : dividend = finToNat remainder + quotient * divisor) ->
84+ DivMod dividend divisor
85+
86+
87+||| Any natural number can be a `Fin` where the bound is itself plus some difference.
88+private
89+toFin : (x : Nat) -> (diff : Nat) -> Fin (plus x (S diff))
90+toFin Z diff = FZ
91+toFin (S k) diff = FS $ toFin k diff
92+
93+||| Converting to a `Fin` and back to `Nat` preserves the input. This is a correctness proof for `toFin`.
94+private
95+toFinAndBack : (x : Nat) -> (diff : Nat) -> finToNat (toFin x diff) = x
96+toFinAndBack Z diff = Refl
97+toFinAndBack (S k) diff = cong (toFinAndBack k diff)
98+
99+
100+||| The accessibilty predicate used for division.
101+private
102+accPlusLT' : LT' (S j) (S (plus k (S j)))
103+accPlusLT' {j = Z} {k = Z} = LTSucc
104+accPlusLT' {j = Z} {k = S k} = LTStep (accPlusLT' {j = Z} {k = k})
105+accPlusLT' {j = S j} {k = k} = rewrite sym $ plusSuccRightSucc k (S j) in
106+ ltSuccSucc accPlusLT'
107+
108+
109+||| Division and modulus on `Nat`, inspired by the definition in the
110+||| Agda standard library.
111+|||
112+||| This uses well-founded recursion on `LT'`.
113+|||
114+||| @ dividend the dividend
115+||| @ divisor the divisor
116+||| @ nonzero division by zero is nonsense
117+total -- yay!
118+divMod : (dividend, divisor : Nat) ->
119+ {auto nonzero : So (not (decAsBool (decEq divisor Z)))} ->
120+ DivMod dividend divisor
121+divMod _ Z {nonzero} = absurd nonzero
122+divMod Z (S k) = DivModRes 0 FZ Refl
123+divMod (S j) (S k) {nonzero} = wfInd {P=P} stepDiv (S j) (S k) nonzero
124+ where
125+ ||| The goal passed to the accessibility eliminator.
126+ |||
127+ ||| This is responsible for generating the goal in the
128+ ||| well-founded fixed point.
129+ |||
130+ ||| @ dividend the dividend to recurse over
131+ P : (dividend : Nat) -> Type
132+ P dividend = (divisor : Nat) -> (nonzero : So (not (decAsBool (decEq divisor Z)))) -> DivMod dividend divisor
133+
134+
135+ ||| Well-founded recursion needs a recursion operator.
136+ |||
137+ ||| @ dividend the dividend we are recursing over
138+ ||| @ rec the recursive call provided by the well-founded induction operator
139+ stepDiv : (dividend : Nat) -> (rec : (d' : Nat) -> LT' d' dividend -> P d') -> P dividend
140+ -- We need not consider division by zero
141+ stepDiv dividend rec Z nonzero = absurd nonzero
142+ -- Dividing zero by anyting else gives 0, with 0 remainder
143+ stepDiv Z rec (S k) nonzero = DivModRes 0 0 Refl
144+ -- To divide two non-zero values, we must know which is larger
145+ stepDiv (S j) rec (S k) nonzero with (cmp j k)
146+ -- n / n = 1 remainder 0
147+ stepDiv (S j) rec (S j) nonzero | CmpEQ =
148+ DivModRes 1 0 (sym $ cong (plusZeroRightNeutral j))
149+ -- if n < m, then m = n + r, and the quotient is 0 with remainder r
150+ stepDiv (S j) rec (S (plus j (S diff))) nonzero | CmpLT diff =
151+ DivModRes 0 (toFin (S j) diff) $
152+ rewrite toFinAndBack j diff
153+ in sym $ cong (plusZeroRightNeutral j)
154+ -- if n > m, then n = m + d, and the quotient is 1 + ((n - m) / m) with the same remainder
155+ stepDiv (S (plus k (S diff))) rec (S k) nonzero | CmpGT diff =
156+ let res = rec (S diff) accPlusLT' (S k) Oh
157+ in case res of
158+ DivModRes quotient remainder ok =>
159+ DivModRes (S quotient) remainder $
160+ rewrite plusAssociative (finToNat remainder) (S k) (mult quotient (S k)) in
161+ rewrite plusCommutative (finToNat remainder) (S k) in
162+ rewrite sym $ plusAssociative (S k) (finToNat remainder) (mult quotient (S k)) in
163+ rewrite ok in Refl
164+
165+