[Agda] built-in divMod

[Sergei Meshveliani]

(I have forgotten to copy it to the list)

> 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


Hi, Ulf.

As I recall, my DoCon-A-2.* uses fast divMod of your Agda Prelude, 
(about two year old matter), by caring only of the signature, 
without understanding the method, nor the implementation.

And my current question is about a way to continue Standard, by a single
minimal step related to divMod only, 
while Agda Prelude by Ulf Norell announced that is is totally diversed
from  standard.

What built-ins is used in your Agda Prelude for efficient divMod ?
Can you explain in simple words, what is the mathematical method?
(it is difficult to understand the method just from the bare code).

Suppose we have to find  divMod a b.
I do not know, is it by finding (maximal n such that (times n b <= a))
by the binary method?
b, b1 = b+b;  b2 = b1+b1, ..., where _+_ and (compare b(i) a) are fast
(built-in) -- is this the method?
   
If it has O(log a) fast additions, then it is all right, then this
divMod can be programmed in Agda and put to Standard. This will be still
better than adding one more built-in.
I thought of this for the first time. 

--
SM