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

[depsterr]

Thank you! I knew it should be able to generalize, but was far too tired. It appears however that this was not the source of the issue. The issue was with my use of rewrite here

  ∣a-b∣≡∣b-a∣ : ∀ (a b : ℚ) → ∣ a - b ∣ ≡ ∣ b - a ∣
  ∣a-b∣≡∣b-a∣ a b rewrite a-b≡-b-a a b = ∣-p∣≡∣p∣ (b - a)

I am impressed it managed to solve it eventually. Doing the reasoning in place of the computer here solves the issue

  ∣a-b∣≡∣b-a∣ : ∀ (a b : ℚ) → ∣ a - b ∣ ≡ ∣ b - a ∣
  ∣a-b∣≡∣b-a∣ a b =
      begin
        ∣ a - b ∣
      ≡⟨ cong ∣_∣ (a-b≈-[b-a] a b) ⟩
        ∣ - (b - a) ∣
      ≡⟨ ∣-p∣≡∣p∣ (b - a) ⟩
        ∣ b - a ∣
      ∎

Thanks very much for your help, and sorry for taking your time !

------- Original Message -------
On Friday, April 15th, 2022 at 14:49, <mechvel at scico.botik.ru> wrote:


>
>
> 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