<div dir="ltr"><div class="gmail_extra">On Fri, Sep 23, 2016 at 2:18 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail-HOEnZb"><div class="gmail-h5"><br></div></div>
------------------------------<wbr>------------------------------<wbr>-<br>
_≤&#39;_ :  Rel â„• _<br>
m â‰¤&#39; n =  âˆƒ \k â†’ m + k â‰¡ n<br>
<br>
_≤&#39;?_ : Decidable _≤&#39;_<br>
m â‰¤&#39;? n =  case m âˆ¸ n<br>
  Â  Â  Â  Â  Â of \<br>
  Â  Â  Â  Â  Â { 0 â†’ let k = n âˆ¸ m<br>
<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â m+k≡n : m + k â‰¡ n<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â m+k≡n = ...<br>
<br>
  Â  Â  Â  Â  Â  Â  Â  Â in  yes (k , m+k≡n)<br>
<br>
  Â  Â  Â  Â  Â ; (suc d) â†’ let noDiff : âˆ€ {k} â†’ m + k â‰¢ n<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â noDiff = \ {k} â†’ ...<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â in<br>
  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â  Â no (\ k,prop â†’ noDiff (projâ‚‚ k,prop))<br>
  Â  Â  Â  Â  Â }<br>
------------------------------<wbr>------------------------------<wbr>--<br>
<br>
Has it chance to be fast?<br></blockquote><div><br></div><div>I suspect you&#39;re going to need a &#39;with&#39; rather than a &#39;case&#39;, did you actually get something like that to type check?</div><div><br></div><div>But assuming you work it out, yes, it will be fast as long as you&#39;re lazy in the proof object.</div><div><br></div><div>If you pattern match against proof it will need to be evaluated and the implementation of m+k≡n is slow (I assume). You can solve that us<font face="arial, helvetica, sans-serif">ing <span style="color:rgb(51,51,51);white-space:pre">Relation.Binary.PropositionalEquality.TrustMe</span>.</font></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">About equality:<br>
<br>
 _≟&#39;_ : Decidable _≡_<br>
 m â‰Ÿ&#39; n =  case ((suc m âˆ¸ suc n) , (suc n âˆ¸ suc m))<br>
  Â  Â  Â  Â  Â of \<br>
  Â  Â  Â  Â  Â { (0 , 0)  Â  Â â†’ yes (m∸n≡0,n∸m≡0→→m≡n _)<br>
  Â  Â  Â  Â  Â ; (suc d , _) â†’ no ...<br>
  Â  Â  Â  Â  Â ; ...<br>
  Â  Â  Â  Â  Â }<br>
<br>
Has it chance to be fast?</blockquote><div><br></div><div>Yes, with the same caveats as above. Even faster would be to use Agda.Builtin.Nat._==_ instead of two calls to minus.</div><div><br></div><div>I have -vprofile.interactive:10 in my Emacs &#39;Agda2 Program Args&#39; configuration parameter (M-x customize-group agda2) which makes the Emacs mode measure the time of C-c C-n (among other commands). Using that you can play around with different implementations and compare their performance.</div><div><br></div><div>For instance, using agda-prelude and &#39;open import Prelude&#39;, I get the following (using _ofType_ to resolved the overloaded literals):</div><div><br></div><div>C-c C-n 48329483209 == (48329483209 ofType Nat)</div><div>Time: 11ms</div><div>yes refl</div><div><br></div><div>C-c C-n compare 48329483209 (432847329 ofType Nat)<br></div><div>Time: 12ms<br></div></div>greater (diff 47896635879 refl)<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">/ Ulf</div></div>