<div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hi Sergei,<div> No the standard library doesn't currently have a fast compare. Feel free to open a PR to adjust the implementation.</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Mar 28, 2019 at 1:38 AM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear standard library developers,<br>
<br>
The comparison  Nat.<-cmp  is `exponentially' slow.<br>
<br>
As lib-0.18-candidate  has fast  _≡ᵇ_ and _<ᵇ_, <br>
and as _≟_ is also fast on Nat (when the proof is not inspected),<br>
this gives a hope for making <-cmp fast in a similar sense.<br>
<br>
The below  compareFast  implements the goal by using that _∸_ is<br>
expressed via built-in.<br>
<br>
I wonder of whether standard library supports a simpler solution. <br>
If it does not, then maybe it could incorporate a similar thing. <br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
--------------------------------------------------------------<br>
compareFast :  (m n : ℕ) → Tri (m < n) (m ≡ n) (m > n)<br>
--<br>
-- _≟_ and _∸_ are via built-in.<br>
<br>
compareFast m n =  aux (m ≟ n) (m ∸ n) (n ∸ m) refl refl <br>
  where<br>
  aux :  Dec (m ≡ n) → (d d' : ℕ) → m ∸ n ≡ d → n ∸ m ≡ d' →<br>
                               Tri (m < n) (m ≡ n) (m > n)<br>
<br>
  aux (yes m≡n) _ _ _ _ =  tri≈ (<-irrefl m≡n) m≡n m≯n<br>
                           where<br>
                           m≯n = <-irrefl (sym m≡n)<br>
<br>
  aux (no m≢n) 0 _ m∸n≡0 _ =  tri< m<n m≢n (<-asym m<n) <br>
                              where<br>
                              m≤n =  m∸n≡0⇒m≤n m∸n≡0<br>
                              m<n =  ≤,≢⇒< m≤n m≢n<br>
<br>
  aux (no m≢n) (suc _) 0 _ n∸m≡0 =  <br>
                           tri> (<-asym n<m) m≢n n<m<br>
                           where<br>
                           n≤m  =  m∸n≡0⇒m≤n n∸m≡0<br>
                           n≢m =  m≢n ∘ sym<br>
                           n<m  =  ≤,≢⇒< n≤m n≢m<br>
<br>
  aux _ (suc d₁) (suc d₂) m∸n≡1+d₁ n∸m≡1+d₂ =  <br>
                          contradiction n<m (<-asym m<n)<br>
      where<br>
      m∸n≢0 = \m-n≡0 → let 1+d₁≡0 = trans (sym m∸n≡1+d₁) m-n≡0<br>
                       in  suc≢0 1+d₁≡0<br>
<br>
      n∸m≢0 = \n-m≡0 → let 1+d₂≡0 = trans (sym n∸m≡1+d₂) n-m≡0<br>
                       in  suc≢0 1+d₂≡0<br>
<br>
      n<m = m∸n≢0⇒n<m {m} {n} m∸n≢0<br>
      m<n = m∸n≢0⇒n<m n∸m≢0<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</div></div>