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

[depsterr]

`--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 `505464961f07f0991263708fd8cbf5f7ad12f53f` on master.
My standard library is version 1.7.1
I am using flags `--sage --without-K`
The full agda file can be found here https://githug.xyz/depsterr/constructive-analysis-in-agda/src/commit/345d7d11c12cc446764f7c1a9fe0afa0920632fb/src/Chapter2.agda
Hope to gain some insight into this, Cheers!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220415/554f22e9/attachment.html>