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