[Agda] simple example

[Nils Anders Danielsson]

On 2012-08-15 07:08, Serge D. Mechveliani wrote:
> 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?

The case "rem (suc _) zero _ = ..." is type-correct. Agda doesn't try to
figure out that a type-correct case may in fact be impossible.

> 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?

You may want to have a look at Data.Nat.DivMod in the standard library
(but I think I've seen less complicated implementations).

> May be, one needs to provide a proof for   n Б┬╦ k < n  ?
>                                             (\.-  for subtraction)

No, that wouldn't help. n ∸ k is not /structurally/ smaller than suc n.

> 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 ?

Data.Nat.decTotalOrder contains a proof showing that _≤_ is total.

-- 
/NAD