Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

[Andreas Abel]

There are two issues with these built-ins:

1. I think they are unnecessary complicated due to the use of an 
accumulator argument to make them tail-recursive.  If internally we 
compute with the Haskell primitive, tail recursion does not give us 
anything besides complication.  I might be wrong here, so please 
contradict if it is the case.

2. They have an initial value m for a running parameter j, and the 
current proof of false exploits that that the running parameter j is 
initialized to a value above m, which violates an unspoken precondition 
of the functions.

If we are to keep these primitives, we need to extend their semantics to 
a j > m.  That should be easy.

But we should also consider removing the accumulator.  That would also 
simplify proofs about them.

Cheers,
Andreas

On 23.04.12 3:04 PM, Ulf Norell wrote:
>
> On Mon, Apr 23, 2012 at 10:28 AM, Nils Anders Danielsson
> <nad at chalmers.se <mailto:nad at chalmers.se>> wrote:
>
>     On 2012-04-23 09:07, Andreas Abel wrote:
>
>         Mmh, the easiest fix is: trash the builtin NATDIVSUCAUX. I do
>         not know what it is for. The only use I found for it was in
>
>           example/lib/Data/Nat.agda
>
>         with the definition you have given below.
>
>
>     See http://code.google.com/p/agda/__issues/detail?id=172
>     <http://code.google.com/p/agda/issues/detail?id=172> for some context.
>
> The purpose is to give you fast (=running on Haskell integers) div and
> mod on nats
> at compile time.
>
>     By the way, I'm not surprised that people manage to wreak havoc by using
>     BUILTINs, in many cases the sanity checking for BUILTINs is less than
>     optimal. I think the idea is that you should only use BUILTINs (and
>     postulates, and the FFI) if you know what you are doing.
>
>
> The sanity checking for BUILTINs is supposed to disallow incorrect
> definitions,
> if it doesn't it's a bug that should be fixed. The FFI and postulates
> obviously let
> you "prove" whatever you want, but BUILTINs shouldn't.
>
> / Ulf

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