<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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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>
&gt; [..]<br>
&gt; natural number operations (_+_, _*_ etc) are compiled to the<br>
&gt; 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&#39;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>