# [Agda] Proof seemingly takes far too long to check?

mechvel at scico.botik.ru mechvel at scico.botik.ru
Fri Apr 15 14:49:02 CEST 2022

```depsterr,

this is not precisely an answer to your question, but something like
relating to it.
The statement

a-b≡-b-a : ∀ (a b : ℚ) → a - b ≡ - (b - a)

is a special case for  a ∙ b⁻¹ ≈ (b ∙ a⁻¹)⁻¹
for an arbitrary Group.
So, I use standard items
Group, Algebra.Properties.Group, its lemmas ⁻¹-involutive,
⁻¹-anti-homo-∙,
and the instance  +-0-group  for the additive group of ℚ (Rational):

---------------------------------------------------------
open import Algebra using (Op₂; Group)
import      Algebra.Properties.Group as GroupProps
open import Data.Rational.Properties as ℚprops
open import Level
open import Relation.Binary.Reasoning.MultiSetoid

open Group ℚprops.+-0-group using (_≈_; sym; ∙-congʳ; setoid)
renaming (Carrier to ℚ; _∙_ to _+_; _⁻¹ to
-_)
open GroupProps ℚprops.+-0-group using (⁻¹-involutive; ⁻¹-anti-homo-∙)

_-_ :  Op₂ ℚ
x - y =  x + (- y)

a-b≈-[b-a] :  ∀ (a b : ℚ) → a - b ≈ - (b - a)
a-b≈-[b-a] a b =
sym
(begin⟨ setoid ⟩
- (b - a)       ≈⟨ ⁻¹-anti-homo-∙ b (- a) ⟩
(- (- a)) - b   ≈⟨ ∙-congʳ {(- b)} (⁻¹-involutive a) ⟩
a - b
∎)
---------------------------------------------------------------

\$ agda \$agdaLibOpt --safe --without-K +RTS -M2G -RTS QExample.agda

type-checks it fast (Agda 2.6.2.2).

I do not know why your code is type-checked heavily.

Only there is a point on type-checking standard library.
For example, if the library has been type-checked under another keys,
then, I fear, the above command will cause re-type-checking a large
piece
of stdlib
(will it ?).

And next time, only the given module will be type-checked.
Let people correct me if I am wrong.

Regards,

------
Sergei

On 2022-04-15 13:45, depsterr wrote:
> `--sage` should be `--safe` in the options, my apologies.
>
> -------- Original Message --------
> On Apr 15, 2022, 12:29, depsterr < depsterr at protonmail.com> wrote:
> Hi all, I've run into something quite unusual.
> I've been trying to construct the reals and prove that their equality
> is an equivalence relation, however during the proof of symmetry I've
> ran into an issue. My proof type checks but the addition of one of the
> lemmas/helpers has forced me to set the agda heap size to 16GB and
> wait 37 minutes for it to typecheck.
> The culprit is the following:
> a-b≡-b-a : ∀ (a b : ℚ) → a - b ≡ - (b - a)
> a-b≡-b-a a b =
> begin
> a - b
> ≡⟨⟩
> a + - b
> ≡˘⟨ ⁻¹-involutive (a + - b) ⟩
> - (- (a + - b))
> ≡⟨ cong -_ (neg-distrib-+ a (- b)) ⟩
> - (- a + - (- b))
> ≡⟨ cong (λ c → - (- a + c) ) (⁻¹-involutive b) ⟩
> - (- a + b)
> ≡⟨ cong -_ (+-comm (- a) b) ⟩
> - (b + - a)
> ≡⟨⟩
> - (b - a)
> ∎
> It seems that it's the usage of ⁻¹-involutive which slows it down,
> as it took no longer than 30 seconds before it was added (if you
> replace it with holes, for instance).
> I'm not quite sure if this should be considered a bug or if I'm doing
> something wrong, certainly something this trivial shouldn't take so
> long?
> I'm using agda built from source with `cabal install
> -foptimise-heavily` from commit