[Agda] built-in divMod

[Ulf Norell]

agda-prelude has efficient certified divMod (though not gmp-efficient of
course), without
postulating any properties. See

https://github.com/UlfNorell/agda-prelude/blob/master/src/Numeric/Nat/DivMod.agda

/ Ulf

On Wed, Mar 20, 2019 at 7:34 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear standard library developers,
>
> As I understand,
> (1) the certified Nat arithmetic is exponentially slow, due to unary
>     representation,
> (2) due to this, it is added a non-certified built-in arithmetic for
>     Nat, including the predicates _≡ᵇ_; _<ᵇ_ returning a Boolean result.
>
> But is there a fast built-in  divMod  for Nat ?
>
> For I do not see, how (2) can help with fast GCD, and hence with a fast
> _rational_ number arithmetic over Nat and Integer.
>
> In scientific computation rational numbers are used as widely as
> Integer, strongly needed.
>
> On the other hand, a fast divMod will allow us to program in Agda a fast
> gcd   and fast rational arithmetic over Nat (Integer)
> (if I am not missing something, for this is difficult to make sure
> without trying to write the code).
>
> This (divMod a b b\=0)  can, say, return  (quot , rem) : Nat x Nat,
> and the proofs for
>                T (a ≡ᵇ a * quot + rem),   T (rem <ᵇ b)
>
> can be postulated in the library.
> As many non-certified things for Nat are already included, why do not
> add built-in  divMod ?  I hope this will be the last one.
> Probably it is somewhere in the  gmp  library (used in GHC ?).
>
> Am I missing something?
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190320/6944226f/attachment.html>