[Agda] Nat arithmetic properties

[Ulf Norell]

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


This should read

If you pattern match against the 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.erase.

/ Ulf

On Fri, Sep 23, 2016 at 4:54 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/01c88877/attachment.html