# [Agda] simple example

Serge D. Mechveliani mechvel at botik.ru
Wed Aug 15 13:08:30 CEST 2012

```People,

The function  rem  needs to evaluate the remainder of division of
natural numbers  n by m  by repeatedly subtracting  m  from the current
remainder.
The restriction  IsPositive m  is also processed.
The cost optimizations are ignored.
It uses Standard Library 0.6.
Math symbols used:  \bn, \.-

---------------------------------------------------------
module MyLib where
open import IO.Primitive
open import Data.Bool as Bool
open import Data.Nat as Nat hiding (less)
open import Prelude using (toCostring)

less : Б└∙ -> Б└∙ -> Bool              -- \bn for Nat
less zero    zero    = false
less zero    (suc _) = true
less (suc _) zero    = false
less (suc n) (suc m) = less n m

IsPositive : Б└∙ -> Set
IsPositive zero    = T false
IsPositive (suc _) = T true

rem : Б└∙ -> (m : Б└∙) -> IsPositive m -> Б└∙
rem zero    _       _ =  zero
rem (suc n) (suc k) p =  if less n k then  suc n
else              rem (n Б┬╦ k) (suc k) p
-- \.-  for subtraction on Nat
rem _       zero  ()  -- unaccessible

main : IO Unit
main = putStrLn (toCostring "done")
---------------------------------------------------------

1. If I skip the last sentence in  rem,  the compiler reports

... Missing cases:  rem (suc _) zero _  ...

Why cannot it derive from  `IsPositive m'  the fact that  m = zero
is not possible?

2. For the initial program, the compiler reports

Termination checking failed for the following functions:  rem
Problematic calls:          rem (n Б┬╦ k) (suc k) p
-- \.-  for subtraction

How to fix this?
May be, one needs to provide a proof for   n Б┬╦ k < n  ?
(\.-  for subtraction)
(if so, in what form can it be provided?).
May be, Standard library already has such a proof, and it can be
somehow imported?

3. It is natural to rely on the library.
What and how need I to use here from Standard Library 0.6 instead
of the above definitions for  less  and  IsPositive ?

Thank you in advance for explanation,

------
Sergei

```