Sergei Meshveliani

2018-02-10 13:45:07 UTC

Dear all,

I need to type-check a program that uses a certain large global constant

a.

And the function test2 below is type-checked much longer than test1,

It takes too long.

This is Agda 2.5.3.

Can people, please, explain the effect?

--------------------------------------------------------------

open import Function using (_∘_; _$_)

open import Relation.Binary.PropositionalEquality using (_≡_; cong)

open import Data.Nat using (ℕ; suc; _+_; _∸_)

open import Data.Nat.Properties using (+-comm)

a : ℕ

a = 12345

test1 : ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a

test1 n = cong (_∸ a) (+-comm a n)

test2 : ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)

test2 n = cong (suc ∘ (_∸ a)) (+-comm a n)

-- cong suc (test1 n)

---------------------------------------------------------------

The interactive type-checker highlights the expression

cong (suc ∘ (_∸ a)) (+-comm a n)

and hangs for a long time.

Also test2 type-checks fast if it is implemented as

cong suc (test1 n).

I can type-check the whole program with, say, a = 7.

But for a good run-time performance `a' needs to be large

(and it relies on that the run-time arithmetic is built-in).

Thanks,

------

Sergei

I need to type-check a program that uses a certain large global constant

a.

And the function test2 below is type-checked much longer than test1,

It takes too long.

This is Agda 2.5.3.

Can people, please, explain the effect?

--------------------------------------------------------------

open import Function using (_∘_; _$_)

open import Relation.Binary.PropositionalEquality using (_≡_; cong)

open import Data.Nat using (ℕ; suc; _+_; _∸_)

open import Data.Nat.Properties using (+-comm)

a : ℕ

a = 12345

test1 : ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a

test1 n = cong (_∸ a) (+-comm a n)

test2 : ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)

test2 n = cong (suc ∘ (_∸ a)) (+-comm a n)

-- cong suc (test1 n)

---------------------------------------------------------------

The interactive type-checker highlights the expression

cong (suc ∘ (_∸ a)) (+-comm a n)

and hangs for a long time.

Also test2 type-checks fast if it is implemented as

cong suc (test1 n).

I can type-check the whole program with, say, a = 7.

But for a good run-time performance `a' needs to be large

(and it relies on that the run-time arithmetic is built-in).

Thanks,

------

Sergei