[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
> `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
More information about the Agda
mailing list