<div dir="ltr"><div><div><div>I did mean `n`, which is a free variable of the term <span class="gmail-im">`(a + n) ∸ a</span>`. Built-in arithmetic<br></div>can only do its thing if all arguments to the built-in function are constants, but in this<br></div>case `n` is an argument to the function and its value is not fixed at type checking time.<br><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 12, 2018 at 4:57 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, 2018-02-12 at 08:18 +0100, Ulf Norell wrote:<br>
> I haven't looked at what the type checker is doing in detail that<br>
> makes test2 so extremely slow, but note that built-in arithmetic does<br>
> not kick in for open terms. In your example `(a + n) ∸ a` contains a<br>
> free variable `n`, if the type checker has to evaluate it (which I<br>
> suspect it does for test2, but not test1) it will use the non-built-in<br>
> recursive definitions for `_+_` and `_∸_`.<br>
<br>
<br>
</span>Did you mean `a' being free there rather than `n' ?<br>
<br>
As to `a', it is a constant, it is substituted with 12345, at some<br>
stage. I do not know of whether this occurrence is qualified as free.<br>
<span class=""><br>
> I would advise abstracting over `a` whenever you can.<br>
<br>
</span>Thank you for your note. I shall think about this.<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
> On Sat, Feb 10, 2018 at 2:45 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
>         Dear all,<br>
><br>
>         I need to type-check a program that uses a certain large<br>
>         global constant a.<br>
>         And the function  test2  below is type-checked much longer<br>
>         than  test1, It takes too long.<br>
>         This is  Agda 2.5.3.<br>
><br>
>         Can people, please, explain the effect?<br>
><br>
>         ------------------------------<wbr>------------------------------<wbr>--<br>
>         open import Function using (_∘_; _$_)<br>
>         open import Relation.Binary.<wbr>PropositionalEquality using (_≡_;<br>
>         cong)<br>
>         open import Data.Nat            using (ℕ; suc; _+_; _∸_)<br>
>         open import Data.Nat.Properties using (+-comm)<br>
><br>
>         a : ℕ<br>
>         a = 12345<br>
><br>
>         test1 :  ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a<br>
>         test1 n =  cong (_∸ a) (+-comm a n)<br>
><br>
>         test2 :  ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)<br>
>         test2 n =  cong (suc ∘ (_∸ a)) (+-comm a n)<br>
><br>
>                    -- cong suc (test1 n)<br>
>         ------------------------------<wbr>------------------------------<wbr>---<br>
><br>
>         The interactive type-checker highlights the expression<br>
>                              cong (suc ∘ (_∸ a)) (+-comm a n)<br>
><br>
>         and hangs for a long time.<br>
><br>
>         Also  test2  type-checks fast if it is implemented as<br>
>         cong suc (test1 n).<br>
><br>
>         I can type-check the whole program with, say,  a = 7.<br>
>         But for a good run-time performance `a' needs to be large<br>
>         (and it relies on that the run-time arithmetic is built-in).<br>
><br>
>         Thanks,<br>
><br>
>         ------<br>
>         Sergei<br>
><br>
>         ______________________________<wbr>_________________<br>
>         Agda mailing list<br>
>         <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>         <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
<br>
<br>
</div></div></blockquote></div><br></div>