[ add ] a 'better' division with remainder for `Data.Integer.Base`

[jamesmckinna]

The gymnastics associated with the three constructors of ℤ exhaust me... especially when the signed representation seems to streamline the definition of division with remainder, as follows:

module _ (i : ℤ) (d : ℕ) .{{_ : ℕ.NonZero d}} where

  infixl 7 _/ℕ_ _%ℕ_

  divℕmod : ℤ × ℕ
  divℕmod with s ◂ n ← signAbs i with q ← n ℕ./ d with r ← n ℕ.% d with s
  ... | Sign.+ = + q ,  r
  ... | Sign.- with r
  ...   | ℕ.zero      = - (+ q) , 0
  ...   | r@(ℕ.suc _) = -[1+ q ] , d ℕ.∸ r

  _/ℕ_ : ℤ
  _/ℕ_ = proj₁ divℕmod
  _%ℕ_ : ℕ
  _%ℕ_ = proj₂ divℕmod

Any reason why doing it this way would be a bad/worse idea than the current version?

UPDATED:

• tidied up the block
• followup question: could we make divℕmod a fully-fledged view which enforces the spec? (modulo importing the properties from Nat... so we'd have to move these operations out of Base.. but maybe that's OK?)
• see also [ question ] Status of BUILTIN pragmas: possibility of redefining 'basic' Data representations? agda#8208 ... could we have a 'better' primitive Int representation? If only Agda permitted it?

Similarly, for Nat, we can fold fuse the helper functions together, and obtain

div-mod-helper : (m n j : ℕ) → ℕ × ℕ → ℕ × ℕ
div-mod-helper m  zero    _      p = p
div-mod-helper m (suc n)  zero   (k , _) = div-mod-helper m n m (suc k , 0)
div-mod-helper m (suc n) (suc j) (k , l) = div-mod-helper m n j (k , suc l)

module _ (dividend divisor : ℕ) .{{_ : NonZero divisor}} where

  infixl 7 _/_ _%_

  div-mod : ℕ × ℕ
  div-mod = div-mod-helper n dividend n (0 , 0)
    where n = pred divisor

  _/_ = proj₁ div-mod
  _%_ = proj₂ div-mod

NB. Issue #2644 may require further rethinking of such definitions!

[JacquesCarette]

What the most ergonomic construction of ℤ is unknown to me. All the versions that I've seen develop dark corners or are ridiculously tedious to work with. Probably because we're asking too much out of a single representation and ought to use views some more...

The high-powered reason seems to be that "The free Abelian Group on a single generator does not have a direct inductive representation". And the various representations that leverage the free monoid on a single generator are a pain.

I'm definitely a big fan of that div-mod-helper as expressing a significant recursion pattern.

[jamesmckinna]

I'm definitely a big fan of that div-mod-helper as expressing a significant recursion pattern.

And it can (perhaps) be slightly optimised with a bit more plumbing, as:

  div-mod : ℕ × ℕ
  div-mod = go dividend d (0 , 0)
    where
    d = pred divisor
    go : (m n : ℕ) → ℕ × ℕ → ℕ × ℕ
    go zero    _       p       = p
    go (suc m) zero    (j , _) = go m d (suc j , 0)
    go (suc m) (suc n) (j , k) = go m n (j , suc k)

but perhaps with additional cost in its proof of correctness? (but we only have to do this once, as in Agda.Builtin.Nat for the informal proof, and Data.Nat.DivMod.Core for the details, ... and that's already an indigestible mess to begin with!)

UPDATED: and hence for the OP

...
  divℕmod : ℤ × ℕ
  divℕmod with s ◂ n ← signAbs i with q , r ← n ℕ.div-mod d with s
  ... | Sign.+ = + q ,  r
  ... | Sign.- with r
  ...   | r@ℕ.zero    = - (+ q) , r
  ...   | r@(ℕ.suc _) = -[1+ q ] , d ℕ.∸ r

  ...

etc.

[jamesmckinna]

What the most ergonomic construction of ℤ is unknown to me. All the versions that I've seen develop dark corners or are ridiculously tedious to work with. Probably because we're asking too much out of a single representation and ought to use views some more...

Well, hence my suggestion to use the SignAbs view in this instance... but also #2879 as a perhaps slightly better version of ℤ, which doesn't rely so much on the semantic understanding of the negsuc constructor... or rather: makes that semantics explicit via ℕ.NonZero.

The high-powered reason seems to be that "The free Abelian Group on a single generator does not have a direct inductive representation". And the various representations that leverage the free monoid on a single generator are a pain.

Indeed. The one reason I would consider adopting higher inductive(-recursive) definitions would be to capture the 'inductive-modulo' character of bread-and-butter concepts such as FreeAbGrp(𝟙)... but I wonder if we shouldn't, at least, develop ℤ via the 'INT' construction (on ℕ) as another view.

[JacquesCarette]

In div-mod: make that go a private global, having it in a where clause will mean that proving anything about div-mod will be very hard.

And yes, the INT construction is most likely a much better completion - especially when you are lazy about normalizing.

[jamesmckinna]

In div-mod: make that go a private global, having it in a where clause will mean that proving anything about div-mod will be very hard.

I think that a local module Div-Mod where before go should help with that...