0 | ||| Division theorem for (type-level) natural number division
  1 | module Data.Nat.Division
  2 |
  3 | import Syntax.WithProof
  4 | import Syntax.PreorderReasoning
  5 | import Syntax.PreorderReasoning.Generic
  6 | import Data.Nat
  7 | import Data.Nat.Equational
  8 | import Data.Nat.Order.Strict
  9 | import Data.Nat.Order.Properties
 10 | import Decidable.Order.Strict
 11 |
 12 | import Data.Nat.Properties
 13 |
 14 | %default total
 15 |
 16 | -- Division theorem --------------------
 17 |
 18 | ||| Show that, if we have enough fuel, we have enough fuel for the
 19 | ||| recursive call in `div'` and `mod'`.
 20 | fuelLemma : (numer, predDenom , fuel : Nat)
 21 |           -> (enoughFuel : numer `LTE` (S fuel))
 22 |           -> (numer `minus` (S predDenom)) `LTE` fuel
 23 | fuelLemma Z predDenom fuel enoughFuel = LTEZero
 24 | fuelLemma (S numer) (S denom) fuel enoughFuel =
 25 |   fuelLemma numer denom fuel $ lteSuccLeft enoughFuel
 26 | fuelLemma (S numer) Z  fuel enoughFuel =
 27 |   rewrite minusZeroRight numer in fromLteSucc enoughFuel
 28 |
 29 | -- equivalence between the duplicate definitions in Data.Nar  ---
 30 |
 31 | -- Internally, we use the two component definitions of divmod'
 32 | div'' : (fuel, numer, denom : Nat) -> Nat
 33 | div'' fuel numer denom = fst (divmod' fuel numer denom)
 34 |
 35 | mod'' : (fuel, numer, denom : Nat) -> Nat
 36 | mod'' fuel numer denom = snd (divmod' fuel numer denom)
 37 |
 38 |
 39 | divmod'_eq_div'_mod' : (fuel, numer, denom : Nat)
 40 |             -> (divmod' fuel numer denom) = (div' fuel numer denom, mod' fuel numer denom)
 41 | divmod'_eq_div'_mod'   0       numer denom = Refl
 42 | divmod'_eq_div'_mod'  (S fuel) numer denom with (Data.Nat.lte numer denom)
 43 |  divmod'_eq_div'_mod' (S fuel) numer denom | True  = Refl
 44 |  divmod'_eq_div'_mod' (S fuel) numer denom | False =
 45 |    rewrite divmod'_eq_div'_mod' fuel (numer `minus` (S denom)) denom in
 46 |    Refl
 47 |
 48 | div''_eq_div' : (fuel, numer, denom : Nat)
 49 |             -> div'' fuel numer denom = div' fuel numer denom
 50 | div''_eq_div' fuel numer denom = cong fst $
 51 |                                        divmod'_eq_div'_mod' fuel numer denom
 52 |
 53 | mod''_eq_mod' : (fuel, numer, denom : Nat)
 54 |             -> mod'' fuel numer denom = mod' fuel numer denom
 55 | mod''_eq_mod' fuel numer denom = cong snd $
 56 |                                        divmod'_eq_div'_mod' fuel numer denom
 57 |
 58 | export
 59 | divmodNatNZeqDivMod : (numer, denom : Nat) -> (0 prf1, prf2, prf3 : NonZero denom)
 60 |             -> (divmodNatNZ numer denom prf1) = (divNatNZ numer denom prf2, modNatNZ numer denom prf3)
 61 | divmodNatNZeqDivMod numer (S denom) prf1 prf2 prf3 = divmod'_eq_div'_mod' numer numer denom
 62 |
 63 | export
 64 | fstDivmodNatNZeqDiv : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
 65 |             -> (fst $ divmodNatNZ numer denom prf1) = divNatNZ numer denom prf2
 66 | fstDivmodNatNZeqDiv numer denom prf1 prf2 =
 67 |   rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
 68 |   Refl
 69 |
 70 | export
 71 | sndDivmodNatNZeqMod : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
 72 |             -> (snd $ divmodNatNZ numer denom prf1) = modNatNZ numer denom prf2
 73 | sndDivmodNatNZeqMod numer denom prf1 prf2 =
 74 |   rewrite divmodNatNZeqDivMod numer denom prf1 prf2 prf2 in
 75 |   Refl
 76 |
 77 |
 78 | -----------------------------------------------------------------------------
 79 | bound_mod'' : (fuel, numer, predDenom : Nat) -> (numer `LTE` fuel)
 80 |            -> (mod'' fuel numer predDenom) `LTE` predDenom
 81 | bound_mod'' 0        0     predDenom LTEZero = LTEZero
 82 | bound_mod'' (S fuel) numer predDenom enough  = case @@(Data.Nat.lte numer predDenom) of
 83 |   (True  ** numer_lte_predn)  => rewrite numer_lte_predn in
 84 |                                  Properties.lteIsLTE _ _ numer_lte_predn
 85 |   (False ** numer_gte_n    )  => rewrite numer_gte_n in
 86 |                                  bound_mod'' fuel (numer `minus` (S predDenom)) predDenom
 87 |                                                   (fuelLemma numer predDenom fuel enough)
 88 |
 89 | export
 90 | boundModNatNZ : (numer, denom : Nat) -> (0 denom_nz : NonZero denom)
 91 |               -> (modNatNZ numer denom denom_nz) `LT` denom
 92 | boundModNatNZ numer (S predDenom) denom_nz =
 93 |   LTESucc $
 94 |     rewrite sym $ mod''_eq_mod' numer numer predDenom in
 95 |       bound_mod'' numer numer predDenom $ reflexive
 96 | divisionTheorem' : (numer, predDenom : Nat)
 97 |                 -> (fuel : Nat) -> (enough : numer `LTE` fuel)
 98 |                 -> numer = (mod'' fuel numer predDenom) + (div'' fuel numer predDenom) * (S predDenom)
 99 |
100 | divisionTheorem'  0     predDenom  0       LTEZero = Refl
101 | divisionTheorem'  numer predDenom (S fuel) enough with (@@(Data.Nat.lte numer predDenom))
102 |  divisionTheorem' numer predDenom (S fuel) enough | (True ** prf)
103 |    = rewrite prf in
104 |      rewrite plusZeroRightNeutral numer in Refl
105 |  divisionTheorem' numer predDenom (S fuel) enough | (False ** prf)
106 |    = rewrite prf in
107 |      let denom  : Nat
108 |          denom = S predDenom
109 |          numer' : Nat
110 |          numer' = numer `minus` denom
111 |          denom_lte_numer : denom `LTE` numer
112 |          denom_lte_numer = Properties.notlteIsLT numer predDenom prf
113 |          enough' : numer' `LTE` fuel
114 |          enough' = fuelLemma numer predDenom fuel enough
115 |
116 |          inductionHypothesis : (numer'
117 |                              = (mod'' fuel numer' predDenom) +  (div'' fuel numer' predDenom) * denom)
118 |          inductionHypothesis = divisionTheorem' numer' predDenom fuel enough'
119 |      in sym $ Calc $
120 |      |~ (mod'' fuel numer' predDenom) + (denom + (div'' fuel numer' predDenom) * denom)
121 |      ~~ (mod'' fuel numer' predDenom) + ((div'' fuel numer' predDenom) * denom + denom)
122 |                ...(cong ((mod'' fuel numer' predDenom) +) $ plusCommutative
123 |                                                             denom
124 |                                                             ((div'' fuel numer' predDenom) * denom))
125 |      ~~((mod'' fuel numer' predDenom) +  (div'' fuel numer' predDenom) * denom) + denom
126 |                ...(plusAssociative
127 |                      (mod'' fuel numer' predDenom)
128 |                      ((div'' fuel numer' predDenom) * denom)
129 |                      denom)
130 |      ~~ numer' + denom ...(cong (+ denom) $ sym inductionHypothesis)
131 |      ~~ numer ...(plusMinusLte denom numer denom_lte_numer)
132 |
133 |
134 |
135 | export
136 | DivisionTheoremDivMod : (numer, denom : Nat)  -> (0 prf : NonZero denom)
137 |                -> numer = snd ( divmodNatNZ numer denom prf)
138 |                        + (fst $ divmodNatNZ numer denom prf)*denom
139 | DivisionTheoremDivMod numer (S predDenom) prf
140 |   = divisionTheorem' numer predDenom numer reflexive
141 |
142 | export
143 | DivisionTheorem : (numer, denom : Nat) -> (0 prf1, prf2 : NonZero denom)
144 |                -> numer = (modNatNZ numer denom prf1) + (divNatNZ numer denom prf2)*denom
145 | DivisionTheorem numer denom prf1 prf2
146 |   = rewrite sym $ fstDivmodNatNZeqDiv numer denom prf1 prf2 in
147 |     rewrite sym $ sndDivmodNatNZeqMod numer denom prf1 prf1 in
148 |     DivisionTheoremDivMod numer denom prf1
149 |
150 |
151 |
152 | divmodZeroZero : (denom, fuel : Nat)
153 |            -> divmod' fuel 0 denom = (0,0)
154 | divmodZeroZero denom  0       = Refl
155 | divmodZeroZero denom (S fuel) = Refl
156 |
157 | modZeroZero : (denom, fuel : Nat)
158 |            -> mod'' fuel 0 denom = 0
159 | modZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl
160 |
161 | divZeroZero : (denom, fuel : Nat)
162 |            -> div'' fuel 0 denom = 0
163 | divZeroZero denom fuel = rewrite divmodZeroZero denom fuel in Refl
164 |
165 |
166 | divmodFuelLemma : (numer, denom, fuel1, fuel2 : Nat)
167 |             -> (enough1 : fuel1 `GTE` numer)
168 |             -> (enough2 : fuel2 `GTE` numer)
169 |             -> divmod' fuel1 numer denom = divmod' fuel2 numer denom
170 | divmodFuelLemma  0 denom 0 fuel2 LTEZero enough2 = rewrite divmodZeroZero denom fuel2 in
171 |                                                 Refl
172 | divmodFuelLemma  0 denom (S fuel1) 0 enough1 LTEZero = Refl
173 | divmodFuelLemma  numer denom (S fuel1) (S fuel2) enough1 enough2 with (@@(Data.Nat.lte numer denom))
174 |  divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (True  ** prf)  =
175 |    rewrite prf in Refl
176 |  divmodFuelLemma numer denom (S fuel1) (S fuel2) enough1 enough2 | (False ** prf) =
177 |    rewrite prf in
178 |    rewrite divmodFuelLemma (numer `minus` (S denom)) denom fuel1 fuel2
179 |              (fuelLemma numer denom fuel1 enough1)
180 |              (fuelLemma numer denom fuel2 enough2) in
181 |    Refl
182 |
183 |
184 | multiplicationLemma : (q, predn, r : Nat) -> q * (S predn) + r `LTE` 0 -> (q = 0, r = 0)
185 | multiplicationLemma q predn r bound =
186 |   let r_eq_z : (r = 0)
187 |       r_eq_z = zeroPlusRightZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
188 |       qn_eq_z : (q * (S predn) = 0)
189 |       qn_eq_z = zeroPlusLeftZero (q * (S predn)) r (sym $ lteZeroIsZero bound)
190 |       q_eq_z : q = 0
191 |       q_eq_z = case zeroMultEitherZero q (S predn) qn_eq_z of
192 |         Left  q_eq_0 => q_eq_0
193 |         Right spred_eq_z impossible
194 |   in (q_eq_z, r_eq_z)
195 |
196 | multiplesModuloZero : (fuel, predn, k : Nat)
197 |        -> (enough : fuel `GTE` k * (S predn) )
198 |        -> mod' fuel (k * (S predn)) predn = 0
199 | multiplesModuloZero 0        predn k enough =
200 |   let (k_eq_z, _) = multiplicationLemma k predn 0 $
201 |                     rewrite plusZeroRightNeutral (k * (S predn)) in
202 |                     enough
203 |   in rewrite k_eq_z in
204 |   Refl
205 | multiplesModuloZero  (S fuel) predn 0 enough = Refl
206 | multiplesModuloZero  (S fuel) predn (S k) enough =
207 |   let n : Nat
208 |       n = S predn
209 |       n_lte_skn : n `LTE` (1 + k)*n
210 |       n_lte_skn = CalcWith {leq = LTE} $
211 |         |~ n
212 |         ~~ n  + 0     ...(sym $ plusZeroRightNeutral n)
213 |         ~~ (1 + 0)*n ...(Refl)
214 |         <~ (1 + k)*n   ...(multLteMonotoneLeft (1+0) (1+k) n $
215 |                            plusLteMonotoneLeft 1 0 k LTEZero)
216 |   in case @@(Data.Nat.lte ((1 + k)*n) predn) of
217 |     (True  ** skn_lte_predn) => absurd $ irreflexive {rel = Data.Nat.LT}
218 |                                        $ CalcWith {leq = LTE} $
219 |       |~ 1 + predn
220 |       ~~ n         ...(Refl)
221 |       ~~ n + 0     ...(sym $ plusZeroRightNeutral n)
222 |       ~~ (1 + 0)*n ...(Refl)
223 |       <~ (1 + k)*n ...(multLteMonotoneLeft (1+0) (1+k) n $
224 |                        LTESucc LTEZero)
225 |       <~ predn     ...(Properties.lteIsLTE _ _ skn_lte_predn)
226 |     (False ** prf) =>
227 |       rewrite prf in
228 |       let skn_minus_n_eq_kn : ((1 + k)*n `minus` n = k*n)
229 |           skn_minus_n_eq_kn = Calc $
230 |             |~ ((1+k)*n `minus` n)
231 |             ~~ ((1+k)*n `minus` (n + 0)) ...(cong ((1+k)*n `minus`) $ sym $ plusZeroRightNeutral n)
232 |             ~~ (n + k*n `minus` (n + 0)) ...(Refl)
233 |             ~~ (k*n `minus` 0)           ...(plusMinusLeftCancel n (k*n) 0)
234 |             ~~ k*n                       ...(minusZeroRight (k*n))
235 |       in rewrite skn_minus_n_eq_kn in
236 |       multiplesModuloZero fuel predn k $
237 |       (rewrite sym $ skn_minus_n_eq_kn in
238 |        fuelLemma ((1 + k)*n) predn fuel enough)
239 |
240 | -- We also want to show uniqueness of this decomposition
241 | -- This is, of course, quite horrible, but I want this theorem in the stdlib
242 | addMultipleMod': (fuel1, fuel2, predn, a, b : Nat) -> (enough1 : fuel1 `GTE` b * (S predn) + a)
243 |                                            -> (enough2 : fuel2 `GTE` a)
244 |        -> mod'' fuel1 (b * (S predn) + a) predn = mod'' fuel2 a predn
245 | addMultipleMod' 0         fuel2 predn a b enough1 enough2
246 |   = let (b_eq_z, a_eq_z) = multiplicationLemma b predn a enough1
247 |     in rewrite a_eq_z in
248 |        rewrite b_eq_z in
249 |        rewrite modZeroZero predn fuel2 in
250 |        Refl
251 | addMultipleMod' fuel1@(S _) fuel2 predn a 0 enough1 enough2 =
252 |   rewrite divmodFuelLemma a predn fuel1 fuel2 enough1 enough2 in
253 |   Refl
254 | addMultipleMod' (S fuel1) fuel2 predn a (S k) enough1 enough2 =
255 |   let n : Nat
256 |       n = S predn
257 |       lhsarg_geq_predn : ((1 + k)*n + a) `GT` predn
258 |       lhsarg_geq_predn = CalcWith {leq = LTE} $
259 |         |~ n
260 |         ~~ (1+0)*n     ...(sym $ plusZeroRightNeutral n)
261 |         <~ (1+k)*n     ...(multLteMonotoneLeft 1 (1+k) n $
262 |                            LTESucc LTEZero)
263 |         <~ (1+k)*n + a ...(lteAddRight $ (1+k)*n)
264 |       prf1 : lte ((1 + k)*n + a) predn = False
265 |       prf1 = GTIsnotlte ((1 + k)*n + a) predn lhsarg_geq_predn
266 |       argsimplify : (((1 + k) *n + a ) `minus` n = k*n + a)
267 |       argsimplify = Calc $
268 |         |~ (((1+k)*n + a) `minus` n)
269 |         ~~ (((n + k*n) + a) `minus` n)       ...(Refl)
270 |         ~~ ((n + (k*n + a)) `minus` (n + 0)) ...(cong2 minus
271 |                                                    (sym $ plusAssociative n (k*n) a)
272 |                                                    (sym $ plusZeroRightNeutral n))
273 |         ~~ ((k*n + a) `minus` 0)             ...(plusMinusLeftCancel n (k*n + a) 0)
274 |         ~~ k*n + a                           ...(minusZeroRight (k*n + a))
275 |   in rewrite prf1 in
276 |      rewrite argsimplify in
277 |      addMultipleMod' fuel1 fuel2 predn a k
278 |        (rewrite sym argsimplify in
279 |         fuelLemma ((1+k)*n + a) predn fuel1 enough1)
280 |        enough2
281 |
282 | addMultipleMod : (a, b, n : Nat) -> (0 n_neq_z1, n_neq_z2 : NonZero n)
283 |               -> snd (divmodNatNZ (a*n + b) n n_neq_z1) = snd (divmodNatNZ b n n_neq_z2)
284 | addMultipleMod a b n@(S predn) n_neq_z1  n_neq_z2 =
285 |   addMultipleMod' (a*n + b) b predn b a reflexive reflexive
286 |
287 | modBelowDenom : (r, n : Nat) -> (0 n_neq_z : NonZero n)
288 |              -> (r `LT` n)
289 |              -> snd (divmodNatNZ r n n_neq_z)  = r
290 | modBelowDenom 0 (S predn) n_neq_0 (LTESucc r_lte_predn) = Refl
291 | modBelowDenom r@(S _) (S predn) n_neq_0 (LTESucc r_lte_predn) =
292 |   rewrite LteIslte r predn r_lte_predn in
293 |   Refl
294 |
295 | modInjective : (r1, r2, n : Nat) -> (0 n_neq_z1, n_neq_z2 : NonZero n)
296 |              -> (r1 `LT` n)
297 |              -> (r2 `LT` n)
298 |              -> snd (divmodNatNZ r1 n n_neq_z1)  = snd (divmodNatNZ r2 n n_neq_z2)
299 |              -> r1 = r2
300 | modInjective r1 r2 n n_neq_z1 n_neq_z2 r1_lt_n r2_lt_n ri_mod_eq = Calc $
301 |   |~ r1
302 |   ~~ snd (divmodNatNZ r1 n n_neq_z1) ...(sym $ modBelowDenom r1 n n_neq_z1 r1_lt_n)
303 |   ~~ snd (divmodNatNZ r2 n n_neq_z2) ...(ri_mod_eq)
304 |   ~~ r2                              ...(      modBelowDenom r2 n n_neq_z2 r2_lt_n)
305 |
306 |
307 | step1 : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
308 |      -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
309 |      -> snd (divmodNatNZ numer denom denom_nz) = r
310 | step1 x n n_nz q r r_lt_n x_eq_qnpr = Calc $
311 |   |~ snd(divmodNatNZ x         n n_nz)
312 |   ~~ snd(divmodNatNZ (q*n + r) n n_nz) ...(cong (\u => snd $ divmodNatNZ u n n_nz) $ x_eq_qnpr)
313 |   ~~ snd(divmodNatNZ r         n n_nz) ...(addMultipleMod q r n n_nz n_nz)
314 |   ~~ r                                 ...(modBelowDenom r n n_nz r_lt_n)
315 |
316 | step2 : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
317 |      -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
318 |      -> fst (divmodNatNZ numer denom denom_nz) = q
319 | step2 x n n_nz q r r_lt_n x_eq_qnr =
320 |   let mod_eq_r : (snd (divmodNatNZ x n n_nz) = r)
321 |       mod_eq_r = step1 x n n_nz q r r_lt_n x_eq_qnr
322 |
323 |       two_decompositions : (fst $ divmodNatNZ x n n_nz) * n + r = q * n + r
324 |       two_decompositions = Calc $
325 |         |~ (fst $ divmodNatNZ x n n_nz) * n + r
326 |         ~~ (fst $ divmodNatNZ x n n_nz) * n + (snd $ divmodNatNZ x n n_nz)
327 |                                                        ...(cong (\ u =>
328 |                                                                 (fst $ divmodNatNZ x n n_nz)* n + u)
329 |                                                                 $ sym mod_eq_r)
330 |         ~~ snd(divmodNatNZ x n n_nz) + fst (divmodNatNZ x n n_nz) * n
331 |                                                        ...(plusCommutative _ _)
332 |         ~~ x                                           ...(sym $ DivisionTheoremDivMod x n n_nz)
333 |         ~~ q*n + r                                     ...(x_eq_qnr)
334 |
335 |   in multRightCancel  (fst $ divmodNatNZ x n n_nz) q n n_nz
336 |    $ plusRightCancel ((fst $ divmodNatNZ x n n_nz)* n) (q*n) r
337 |    $ two_decompositions
338 |
339 | export
340 | DivisionTheoremUniquenessDivMod : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
341 |      -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
342 |      -> divmodNatNZ numer denom denom_nz = (q, r)
343 | DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf =
344 |   rewrite sym $ step1 numer denom denom_nz q r x prf in
345 |   rewrite sym $ step2 numer denom denom_nz q r x prf in
346 |   pair_eta _  -- Should idris be able to see this automatically? Maybe only with homogeneous equality?
347 |   where
348 |     -- Should this go elsewhere?
349 |     ||| extensionality law for simple pairs
350 |     pair_eta : (x : (a,b)) -> x = (fst x, snd x)
351 |     pair_eta (x,y) = Refl
352 |
353 | export
354 | DivisionTheoremUniqueness : (numer : Nat) -> (denom : Nat) -> (0 denom_nz : NonZero denom)
355 |      -> (q, r : Nat) -> (r `LT` denom) -> (numer = q * denom + r)
356 |      -> (divNatNZ numer denom denom_nz = q, modNatNZ numer denom denom_nz = r)
357 | DivisionTheoremUniqueness numer denom denom_nz q r x prf =
358 |   rewrite sym $ fstDivmodNatNZeqDiv numer denom denom_nz denom_nz in
359 |   rewrite sym $ sndDivmodNatNZeqMod numer denom denom_nz denom_nz in
360 |   rewrite DivisionTheoremUniquenessDivMod numer denom denom_nz q r x prf in
361 |   (Refl, Refl)
362 |
363 | export
364 | modDividendMinusDivMultDivider : (0 numer, denom : Nat) -> {auto 0 denom_nz : NonZero denom} ->
365 |   modNatNZ numer denom denom_nz = numer `minus` divNatNZ numer denom denom_nz * denom
366 | modDividendMinusDivMultDivider numer denom = Calc $
367 |   |~ (modNatNZ numer denom denom_nz)
368 |   ~~ (divNatNZ numer denom denom_nz * denom + modNatNZ numer denom denom_nz `minus` divNatNZ numer denom denom_nz * denom)
369 |             ...(sym $ minusPlus $ divNatNZ numer denom denom_nz * denom)
370 |   ~~ (modNatNZ numer denom denom_nz + divNatNZ numer denom denom_nz * denom `minus` divNatNZ numer denom denom_nz * denom)
371 |             ...(rewrite plusCommutative (divNatNZ numer denom denom_nz * denom) (modNatNZ numer denom denom_nz)
372 |                 in Refl)
373 |   ~~ (numer `minus` divNatNZ numer denom denom_nz * denom)
374 |             ...(sym $ cong (`minus` (divNatNZ numer denom denom_nz * denom))
375 |                            (DivisionTheorem numer denom denom_nz denom_nz))
376 |