<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 21, 2016 at 11:51 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Ulf Norell wrote recently<br>
<br>
> [..]<br>
> natural number operations (_+_, _*_ etc) are compiled to the<br>
> corresponding Haskell Integer operations.<br><br>
But this means that the properties of these operations on Nat become postulated.<br>
Do they?<br>
<br>
For example, the commutativity property +-comm of Data.Nat.Properties.Simple<br>
is proved in this module for Nat represented in unary system and for the algorithm for _+_<br>
given in Data.Nat.<br>
Now as _+_ is compiled to +-via-Haskell-Integer, the proof for +-comm is not a proof for<br>
+-via-Haskell-Integer.<br>
<br>
Can somebody explain, please?<br></blockquote><div><br></div><div>Operationally, the proof of +-comm carries no bits of information, and so can be erased</div><div>at runtime.</div><div><br></div><div>If you're concerned about correctness, there is indeed an implicit assumption that the Haskell</div><div>Integer arithmetic functions are semantically equivalent to the unary natural number functions</div><div>defined in Agda (and so that the proof of +comm for unary numbers implies +comm for Haskell</div><div>Integers). I feel pretty confident that this is the case. Certainly more confident than I am in there</div><div>being no inconsistency bugs in the type checker, for instance.</div><div><br></div><div>/ Ulf</div></div></div></div>