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

[mechvel at scico.botik.ru]

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
> `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!
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda