<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="font-size:12.8px">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</span><font face="arial, helvetica, sans-serif" style="font-size:12.8px">ing <span style="color:rgb(51,51,51);white-space:pre-wrap">Relation.Binary.<wbr>PropositionalEquality.TrustMe</span>.</font></blockquote><div><br></div><div>This should read</div><div><br></div><div><span style="font-size:12.8px">If you pattern match against the proof it will need to be evaluated and the implementation of m+k≡n is slow (I assume). You can solve that us</span><font face="arial, helvetica, sans-serif" style="font-size:12.8px">ing <span style="color:rgb(51,51,51);white-space:pre-wrap">Relation.Binary.<wbr>PropositionalEquality.TrustMe.erase</span>.</font></div><div><font face="arial, helvetica, sans-serif" style="font-size:12.8px"><br></font></div><div><font face="arial, helvetica, sans-serif" style="font-size:12.8px">/ Ulf</font></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Sep 23, 2016 at 4:54 PM, Ulf Norell <span dir="ltr">&lt;<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><span class=""><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></span><div class="gmail_extra"><div class="gmail_quote"><span class=""><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div><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></span><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-wrap">Relation.Binary.<wbr>PropositionalEquality.TrustMe</span>.</font></div><span class=""><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></span><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)<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div class="gmail_extra"><br></div><div class="gmail_extra">/ Ulf</div></font></span></div>
</blockquote></div><br></div>