DivMod.agda 3.1 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102
  1. module DivMod where
  2. -- From examples/simple-lib
  3. open import Lib.Vec
  4. open import Lib.Nat
  5. open import Lib.Id
  6. open import Lib.Logic
  7. open import Lib.Fin
  8. -- Certified implementation of division and modulo
  9. module Direct where
  10. data DivMod : Nat -> Nat -> Set where
  11. dm : forall {b} q (r : Fin b) -> DivMod (toNat r + q * b) b
  12. getQ : forall {a b} -> DivMod a b -> Nat
  13. getQ (dm q _) = q
  14. getR : forall {a b} -> DivMod a b -> Nat
  15. getR (dm _ r) = toNat r
  16. divModˢ : (a b : Nat) -> DivMod a (suc b)
  17. divModˢ zero b = dm 0 zero
  18. divModˢ (suc a) b with divModˢ a b
  19. divModˢ (suc ._) b | dm q r with maxView r
  20. divModˢ (suc ._) b | dm q .(fromNat b) | theMax
  21. with toNat (fromNat b) | lem-toNat-fromNat b
  22. ... | .b | refl = dm {suc b} (suc q) zero
  23. divModˢ (suc ._) b | dm q .(weaken i) | notMax i
  24. with toNat (weaken i) | lem-toNat-weaken i
  25. ... | .(toNat i) | refl = dm q (suc i)
  26. divMod : (a b : Nat){nz : NonZero b} -> DivMod a b
  27. divMod a zero {}
  28. divMod a (suc b) = divModˢ a b
  29. -- Let's try the inductive version. Less obvious that this one is correct.
  30. module Inductive where
  31. data DivMod : Nat -> Nat -> Set where
  32. dmZ : forall {b} (i : Fin b) -> DivMod (toNat i) b
  33. dmS : forall {a b} -> DivMod a b -> DivMod (b + a) b
  34. getQ : forall {a b} -> DivMod a b -> Nat
  35. getQ (dmZ _) = 0
  36. getQ (dmS d) = suc (getQ d)
  37. getR : forall {a b} -> DivMod a b -> Nat
  38. getR (dmZ r) = toNat r
  39. getR (dmS d) = getR d
  40. data BoundView (n : Nat) : Nat -> Set where
  41. below : (i : Fin n) -> BoundView n (toNat i)
  42. above : forall a -> BoundView n (n + a)
  43. boundView : (a b : Nat) -> BoundView a b
  44. boundView zero b = above b
  45. boundView (suc a) zero = below zero
  46. boundView (suc a) (suc b) with boundView a b
  47. boundView (suc a) (suc .(toNat i)) | below i = below (suc i)
  48. boundView (suc a) (suc .(a + k)) | above k = above k
  49. infix 4 _≤_
  50. data _≤_ : Nat -> Nat -> Set where
  51. leqZ : forall {n} -> zero ≤ n
  52. leqS : forall {n m} -> n ≤ m -> suc n ≤ suc m
  53. ≤-suc : forall {a b} -> a ≤ b -> a ≤ suc b
  54. ≤-suc leqZ = leqZ
  55. ≤-suc (leqS p) = leqS (≤-suc p)
  56. plus-≤ : forall a {b c} -> a + b ≤ c -> b ≤ c
  57. plus-≤ zero p = p
  58. plus-≤ (suc a) (leqS p) = ≤-suc (plus-≤ a p)
  59. ≤-refl : forall {a} -> a ≤ a
  60. ≤-refl {zero} = leqZ
  61. ≤-refl {suc n} = leqS ≤-refl
  62. -- Recursion over a bound on a (needed for termination).
  63. divModˢ : forall {size} a b -> a ≤ size -> DivMod a (suc b)
  64. divModˢ a b prf with boundView (suc b) a
  65. divModˢ .(toNat r) b _ | below r = dmZ r
  66. divModˢ .(suc b + k) b (leqS prf) | above k = dmS (divModˢ k b (plus-≤ b prf))
  67. divMod : forall a b {nz : NonZero b} -> DivMod a b
  68. divMod a zero {}
  69. divMod a (suc b) = divModˢ a b ≤-refl
  70. -- We ought to prove that the inductive version behaves the same as the
  71. -- direct version... but that's more work than we're willing to spend.
  72. open Inductive
  73. _div_ : (a b : Nat){nz : NonZero b} -> Nat
  74. _div_ a b {nz} = getQ (divMod a b {nz})
  75. _mod_ : (a b : Nat){nz : NonZero b} -> Nat
  76. _mod_ a b {nz} = getR (divMod a b {nz})