[Agda] _divMod_

[Andreas Abel]

Hello Serge,

On 03.09.12 8:02 PM, Serge D. Mechveliani wrote:
> People,
> I have a question on  Nat.DivMod  of Standard library
>                                       (of Agda-2.3.0.1, lib-0.6):
> need to study how to use _divMod_.
> Nat.DivMod  has an example of such usage: the function  _mod_.
> I copy the  _mod_  definition from  Nat.DivMod  to my module  Main.agda
> with changing the identifiers as
>                    _mod_ -> mod2,  \?= -> eq?,  \nequiv 0 -> p
> (see the _mod_ code in  Nat/DivMod.agda):
> ----------------
> mod2 : (dividend divisor : Nat) {p : False (divisor eq? 0)} -> Fin divisor
> mod2 m n {p} with _divMod_ m n {p}
> .(toNat r + q * n) mod n | result q r = r

It seems that you forgot to rename _mod_ to mod2 in the last line.

> The report is:  "Missing with-clauses for function mod2".
>
> (1) Nat.DivMod.agda  is compiled, and  Main.agda  is not:
>      can you explain this effect?
>
> I thought, probably, the last line applies a _view_, similar as the
> User Guide explains in Section `3.1 Views'.
> At the moment, I do not understand `views'. But I look into the Guide
> example of Parity and `parity' in this section, and just try to mimic
> it. I change the implementation to
> --------------
> mod2 m n {p} with _divMod_ m n {p}
> mod2 .(toNat r + q * n) n | result q r = r
> --------------
> (the second line has two arguments before `|', instead of the three
> arguments in Nat/DivMod).
> I do not know of _what_ this computes, but at least it is compiled.
> I wonder what all this story may be about.
>
> (2) Why it is chosen a name  _divMod_  having two underscores?
>      It is not declared as infix.

If you define mixfix operators like

  _divMod_ : ...
  _divMod_ = ...

then you can use them by filling terms for the underscores, like

   m divMod n

or you use it prefix

   _divMod_ m n

Only in prefix usage you can supply hidden arguments.

> (3) My beginner's attempt of  divMod  might be like this:
>
>    record MyDivMod (dividend divisor : Б└∙) : Set
>           where
>           field
>             quot  : Б└∙
>             rem   : Fin divisor
>             proof : (dividend  Б┴║  quot * divisor + (toБ└∙ rem))
>
>    myDivMod : (n : Б└∙) -> (m : Б└∙) -> False (m Б┴÷ 0) -> MyDivMod n m
>    myDivMod n m p = ...
>
> Will this approach work?

The termination checker might complain, depending on your definition of 
myDivMod...

> May be  _divMod_  is better, this needs studying;
> and so far, I only try to  apply _divMod_.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/