[Agda] Fwd: fastCompare for Nat

[Matthew Daggitt]

Hi Sergei,
 No the standard library doesn't currently have a fast compare. Feel free
to open a PR to adjust the implementation.
Matthew

On Thu, Mar 28, 2019 at 1:38 AM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear standard library developers,
>
> The comparison  Nat.<-cmp  is `exponentially' slow.
>
> As lib-0.18-candidate  has fast  _≡ᵇ_ and _<ᵇ_,
> and as _≟_ is also fast on Nat (when the proof is not inspected),
> this gives a hope for making <-cmp fast in a similar sense.
>
> The below  compareFast  implements the goal by using that _∸_ is
> expressed via built-in.
>
> I wonder of whether standard library supports a simpler solution.
> If it does not, then maybe it could incorporate a similar thing.
>
> Thanks,
>
> ------
> Sergei
>
>
> --------------------------------------------------------------
> compareFast :  (m n : ℕ) → Tri (m < n) (m ≡ n) (m > n)
> --
> -- _≟_ and _∸_ are via built-in.
>
> compareFast m n =  aux (m ≟ n) (m ∸ n) (n ∸ m) refl refl
>   where
>   aux :  Dec (m ≡ n) → (d d' : ℕ) → m ∸ n ≡ d → n ∸ m ≡ d' →
>                                Tri (m < n) (m ≡ n) (m > n)
>
>   aux (yes m≡n) _ _ _ _ =  tri≈ (<-irrefl m≡n) m≡n m≯n
>                            where
>                            m≯n = <-irrefl (sym m≡n)
>
>   aux (no m≢n) 0 _ m∸n≡0 _ =  tri< m<n m≢n (<-asym m<n)
>                               where
>                               m≤n =  m∸n≡0⇒m≤n m∸n≡0
>                               m<n =  ≤,≢⇒< m≤n m≢n
>
>   aux (no m≢n) (suc _) 0 _ n∸m≡0 =
>                            tri> (<-asym n<m) m≢n n<m
>                            where
>                            n≤m  =  m∸n≡0⇒m≤n n∸m≡0
>                            n≢m =  m≢n ∘ sym
>                            n<m  =  ≤,≢⇒< n≤m n≢m
>
>   aux _ (suc d₁) (suc d₂) m∸n≡1+d₁ n∸m≡1+d₂ =
>                           contradiction n<m (<-asym m<n)
>       where
>       m∸n≢0 = \m-n≡0 → let 1+d₁≡0 = trans (sym m∸n≡1+d₁) m-n≡0
>                        in  suc≢0 1+d₁≡0
>
>       n∸m≢0 = \n-m≡0 → let 1+d₂≡0 = trans (sym n∸m≡1+d₂) n-m≡0
>                        in  suc≢0 1+d₂≡0
>
>       n<m = m∸n≢0⇒n<m {m} {n} m∸n≢0
>       m<n = m∸n≢0⇒n<m n∸m≢0
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190328/728da0a7/attachment.html>