<div dir="ltr"><div dir="ltr"><div>agda-prelude has efficient certified divMod (though not gmp-efficient of course), without</div><div>postulating any properties. See</div><div><br></div><div><a href="https://github.com/UlfNorell/agda-prelude/blob/master/src/Numeric/Nat/DivMod.agda">https://github.com/UlfNorell/agda-prelude/blob/master/src/Numeric/Nat/DivMod.agda</a></div><div><br></div><div>/ Ulf<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 20, 2019 at 7:34 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear standard library developers,<br>
<br>
As I understand, <br>
(1) the certified Nat arithmetic is exponentially slow, due to unary <br>
    representation,<br>
(2) due to this, it is added a non-certified built-in arithmetic for <br>
    Nat, including the predicates _≡ᵇ_; _<ᵇ_ returning a Boolean result.<br>
<br>
But is there a fast built-in  divMod  for Nat ?<br>
<br>
For I do not see, how (2) can help with fast GCD, and hence with a fast<br>
_rational_ number arithmetic over Nat and Integer.<br>
<br>
In scientific computation rational numbers are used as widely as<br>
Integer, strongly needed. <br>
<br>
On the other hand, a fast divMod will allow us to program in Agda a fast<br>
gcd   and fast rational arithmetic over Nat (Integer) <br>
(if I am not missing something, for this is difficult to make sure<br>
without trying to write the code).<br>
<br>
This (divMod a b b\=0)  can, say, return  (quot , rem) : Nat x Nat,<br>
and the proofs for <br>
               T (a ≡ᵇ a * quot + rem),   T (rem <ᵇ b)  <br>
<br>
can be postulated in the library.<br>
As many non-certified things for Nat are already included, why do not<br>
add built-in  divMod ?  I hope this will be the last one.<br>
Probably it is somewhere in the  gmp  library (used in GHC ?).  <br>
<br>
Am I missing something?<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>