[Agda] Nat arithmetic properties

[Sergei Meshveliani]

On Thu, 2016-09-22 at 22:20 +0200, Ulf Norell wrote:
> On Thu, Sep 22, 2016 at 10:08 PM, Sergei
> Meshveliani <mechvel at botik.ru> wrote:
>         Another reason for necessity of n-ary provable arithmetic:
>         
>           _≤?_  of Data.Nat.decTotalOrder  is slow.
>         
>         Probably this is because it is not built-in
>         (and how can it? assuming that the result may contain a proof
>         made of
>         many certain constructors).
>  
> You should use the _≤″_ ordering [1] instead. It has constant size
> representation
> of inequality proofs.
> 
> 
> / Ulf
> 
> 
> [1]
> https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda#L72
> 


Thank you.
I consider now its analogue:

-------------------------------------------------------------
_≤'_ :  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?

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?

Further, there are needed  DecTotalOrder and StrictTotalOrder  for _≤'_.
For example, sorting a list relies on DecTotalOrder.

Regards,

------
Sergei