[Agda] Nat arithmetic properties

[Sergei Meshveliani]

On Wed, 2016-09-21 at 12:52 +0200, Ulf Norell wrote:
> 
> 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.
> 

Being not able to provably verify the type checker 
(and also MAlonzo, GHC, linker, and hardware) does not mean that one
needs to assume/postulate the properties of all the upper levels. The
more levels are verified the better

(by the way, one can imagine a provably verified type checker, provably
verified Agda interpreter ... -- may such have sense?).

Adding proofs to efficient programs for a generic fraction arithmetic,
polynomial arithmetic, etc, allows it to preserve performance.
As to natural numbers, the provable part can cover without performance
loss everything besides macrodigits.

Namely, suppose that we represent Natural as  Nat' = List Macrodigit,
map Macrodigit to Int of Haskell and make arithmetic operations on
Macrodigits built-in, postulate several properties of the Macrodidit
arithmetic, program in Agda arithmetical operations on Nat' by
processing lists of macrodigits, add the proofs for the properties (like
say +-comm) for Nat'.  
With this approach the arithmetic in Nat  a) will be fast enough, 
b) the postulated part will be restricted to operations on Macrodigit,
so that the programs will be more verified.

Has this approach sense?

Regards,

------
Sergei