[Agda] Nat arithmetic properties

[Ulf Norell]

On Wed, Sep 21, 2016 at 11:51 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Ulf Norell wrote recently
>
> > [..]
> > natural number operations (_+_, _*_ etc) are compiled to the
> > corresponding Haskell Integer operations.
>
> But this means that the properties of these operations on Nat become
> postulated.
> Do they?
>
> For example, the commutativity property  +-comm  of
> Data.Nat.Properties.Simple
> is proved in this module for Nat represented in unary system and for the
> algorithm for _+_
> given in Data.Nat.
> Now as _+_ is compiled to  +-via-Haskell-Integer,  the proof for +-comm
> is not a proof for
> +-via-Haskell-Integer.
>
> Can somebody explain, please?
>

Operationally, the proof of +-comm carries no bits of information, and so
can be erased
at runtime.

If you're concerned about correctness, there is indeed an implicit
assumption that the Haskell
Integer arithmetic functions are semantically equivalent to the unary
natural number functions
defined in Agda (and so that the proof of +comm for unary numbers implies
+comm for Haskell
Integers). I feel pretty confident that this is the case. Certainly more
confident than I am in there
being no inconsistency bugs in the type checker, for instance.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160921/14e96abe/attachment.html