[Agda] Nat arithmetic properties

[Sergei Meshveliani]

On Fri, 2016-09-23 at 16:54 +0200, Ulf Norell 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?
> 

It is type-checked when '...' is replaced with `anything'.
But it is not difficult to replace it with a real proof.


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

Thank you for explanations.

------
Sergei