<div dir="ltr"><div class="gmail_extra">On Fri, Sep 23, 2016 at 2:18 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
_≤'_ : Rel ℕ _<br>
m ≤' n = ∃ \k → m + k ≡ n<br>
<br>
_≤'?_ : Decidable _≤'_<br>
m ≤'? 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're going to need a 'with' rather than a 'case', 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'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>
_≟'_ : Decidable _≡_<br>
m ≟' 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 'Agda2 Program Args' 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 'open import Prelude', 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>