[Agda] Nat arithmetic properties

[Ulf Norell]

On Fri, Sep 23, 2016 at 2:18 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> -------------------------------------------------------------
> _≤'_ :  Rel ℕ _
> m ≤' n =  ∃ \k → m + k ≡ n
>
> _≤'?_ : Decidable _≤'_
> m ≤'? n =  case m ∸ n
>            of \
>            { 0 → let k = n ∸ m
>
>                      m+k≡n : m + k ≡ n
>                      m+k≡n = ...
>
>                  in  yes (k , m+k≡n)
>
>            ; (suc d) → let noDiff : ∀ {k} → m + k ≢ n
>                            noDiff = \ {k} → ...
>                        in
>                        no (\ k,prop → noDiff (proj₂ k,prop))
>            }
> --------------------------------------------------------------
>
> Has it chance to be fast?
>

I suspect you're going to need a 'with' rather than a 'case', did you
actually get something like that to type check?

But assuming you work it out, yes, it will be fast as long as you're lazy
in the proof object.

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 using
Relation.Binary.PropositionalEquality.TrustMe.


> About equality:
>
>  _≟'_ : Decidable _≡_
>  m ≟' n =  case ((suc m ∸ suc n) , (suc n ∸ suc m))
>            of \
>            { (0 , 0)     → yes (m∸n≡0,n∸m≡0→→m≡n _)
>            ; (suc d , _) → no ...
>            ; ...
>            }
>
> Has it chance to be fast?


Yes, with the same caveats as above. Even faster would be to use
Agda.Builtin.Nat._==_ instead of two calls to minus.

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.

For instance, using agda-prelude and 'open import Prelude', I get the
following (using _ofType_ to resolved the overloaded literals):

C-c C-n 48329483209 == (48329483209 ofType Nat)
Time: 11ms
yes refl

C-c C-n compare 48329483209 (432847329 ofType Nat)
Time: 12ms
greater (diff 47896635879 refl)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160923/1e117694/attachment.html