<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>