[Agda] simple example
Nils Anders Danielsson
nad at chalmers.se
Wed Aug 15 16:33:29 CEST 2012
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
More information about the Agda
mailing list