# [Agda] divMod variant

Serge D. Mechveliani mechvel at botik.ru
Sun Sep 16 14:29:59 CEST 2012

People,
the archive  http://botik.ru/pub/local/Mechveliani/agdaNotes/ddivRem.zip
contains
* the implementation  DDivRem.agda  for division with remainder for
unary coded natural numbers,
* the test module  Main.agd,
* notes  notes.agda  and questions on this program

-- all this is for  Agda-2.3.0.1 + lib-0.6.

data DivMod : Nat -> Nat -> Set where
result : {divisor : Nat} (q : Nat) (r : Fin divisor) ->
DivMod (toNat r + q * divisor) divisor
of Standard
divRem  has the result type

record NatDivRem (dividend divisor : Nat) : Set where
field
quot  : Nat
rem   : Nat
proof : (rem < divisor) x (dividend == (quot * divisor + rem))

natDivRem : (dividend : Nat)     -> (divisor : Nat) ->
False (divisor =? 0) -> NatDivRem dividend divisor

(For this letter I denote  \bn ->  Nat,  \equiv ->  ==,   \=? ->  =? ).

It also builds the needed proofs.
In its internal loop, it processes the additional arguments for
* the counter for subtractions, in order to help the termination proof,
* the current proof for   m == (q * n' + r),  in order to provide an
incremental proof, to save the cost.

I shall be grateful to you if you look into (a quite small code in)
DDivRem.agda  and give notes.
The mark  debug'  in comments points at questionable places.

I tried  divRem m 5   for several values of  m  (see Main.agda).
I understand that
* probably,  Agda-2.3.0.1 + lib-0.6  does not at all aim at performance,
* unary coded naturals  is not an appropriate test for investigating
the performance points;
I think, say, sorting a long character list fits better.

Still consider the following.
1. The time cost in  divRem  looks like  O(m^2).
2. The version "-skipProofs" has the same timing.
Why does it look as  O(m^2) ?
A short comment in  notes.agda  argues for that it must be  O(m).

Thanks,

------
Sergei
`