Zulip Chat Archive

Stream: general

Topic: Timeouts in ring_theory/dedekind_domain.lean:664:9


Eric Wieser (Sep 16 2021 at 12:57):

It seems this is right on the cusp of a timeout. Both #9226 and #9220 are failing due to this.

https://github.com/leanprover-community/mathlib/blob/b7593841620449def9435f0b9f3a1002afecff53/src/ring_theory/dedekind_domain.lean#L664-L680

Any ideas, @Anne Baanen?

Kevin Buzzard (Sep 16 2021 at 13:07):

Changing

      { use mt ideal.is_unit_iff.mpr hirr.not_unit,

to

      { refine ⟨⟨mt ideal.is_unit_iff.mpr hirr.not_unit, _⟩⟩,

on line 669 seems to shave over 1 second off elaboration time on my machine, so that's some kind of sticking plaster

Anne Baanen (Sep 16 2021 at 13:09):

That was going to be my first guess :)

Kevin Buzzard (Sep 16 2021 at 13:12):

I didn't know use could go into binders like that. The goal is a structure with one field, and use gives a term of the field's type.

Kevin Buzzard (Sep 16 2021 at 13:13):

The actual issue seems to be the simp only, to my mild surprise

Sebastien Gouezel (Sep 16 2021 at 13:14):

instance ideal.unique_factorization_monoid :
  unique_factorization_monoid (ideal A) :=
{ irreducible_iff_prime := λ P,
    λ hirr, hirr.ne_zero, hirr.not_unit, λ I J, begin
      have : P.is_maximal,
      { refine ⟨⟨mt ideal.is_unit_iff.mpr hirr.not_unit, _⟩⟩,
        intros J hJ,
        obtain J_ne, H, hunit, P_eq := ideal.dvd_not_unit_iff_lt.mpr hJ,
        exact ideal.is_unit_iff.mp ((hirr.is_unit_or_is_unit P_eq).resolve_right hunit) },
      rw [ideal.dvd_iff_le, ideal.dvd_iff_le, ideal.dvd_iff_le],
      simp only [has_le.le, preorder.le, partial_order.le],
      contrapose!,
      rintros ⟨⟨x, x_mem, x_not_mem⟩, y, y_mem, y_not_mem⟩⟩,
      exact x * y, ideal.mul_mem_mul x_mem y_mem,
             mt this.is_prime.mem_or_mem (not_or x_not_mem y_not_mem)⟩,
    end⟩,
    prime.irreducible⟩,
  .. ideal.wf_dvd_monoid }

is much faster on my computer.

Kevin Buzzard (Sep 16 2021 at 13:15):

I can reproduce here

Sebastien Gouezel (Sep 16 2021 at 13:16):

Btw, the simp only line is a clear sign of a missing API.

Eric Wieser (Sep 16 2021 at 13:16):

I think it's just lost api, its docs#set_like.le_def

Sebastien Gouezel (Sep 16 2021 at 13:18):

Ah, great, thanks! Then it could even be

instance ideal.unique_factorization_monoid :
  unique_factorization_monoid (ideal A) :=
{ irreducible_iff_prime := λ P,
    λ hirr, hirr.ne_zero, hirr.not_unit, λ I J, begin
      have : P.is_maximal,
      { refine ⟨⟨mt ideal.is_unit_iff.mpr hirr.not_unit, _⟩⟩,
        intros J hJ,
        obtain J_ne, H, hunit, P_eq := ideal.dvd_not_unit_iff_lt.mpr hJ,
        exact ideal.is_unit_iff.mp ((hirr.is_unit_or_is_unit P_eq).resolve_right hunit) },
      rw [ideal.dvd_iff_le, ideal.dvd_iff_le, ideal.dvd_iff_le,
          set_like.le_def, set_like.le_def, set_like.le_def],
      contrapose!,
      rintros ⟨⟨x, x_mem, x_not_mem⟩, y, y_mem, y_not_mem⟩⟩,
      exact x * y, ideal.mul_mem_mul x_mem y_mem,
             mt this.is_prime.mem_or_mem (not_or x_not_mem y_not_mem)⟩,
    end⟩,
    prime.irreducible⟩,
  .. ideal.wf_dvd_monoid }

Kevin Buzzard (Sep 16 2021 at 13:19):

We're now down from 7 seconds to 3 on my machine so probably this will solve the issues.

Anne Baanen (Sep 16 2021 at 13:23):

Another interesting find: changing the first line of is_dedekind_domain_inv_iff from set h : fraction_ring A ≃ₐ[A] K := fraction_ring.alg_equiv A K, toset h := fraction_ring.alg_equiv A K,, saves about a second on my machine.

Eric Wieser (Sep 16 2021 at 13:24):

I assume it doesn't change the speed of the lemma I started with, and just speeds up its own lemma?

Anne Baanen (Sep 16 2021 at 13:25):

Yes, sorry for the confusion.

Eric Wieser (Sep 16 2021 at 13:36):

Do you plan to PR both speedups @Anne Baanen?

Anne Baanen (Sep 16 2021 at 13:37):

Sure, I'm seeing if I can speed up _inv_iff some more

Anne Baanen (Sep 16 2021 at 13:50):

Looks like the main source of slowness is unifying the comm_ring instance deriving from docs#fraction_ring.field with docs#localization.comm_ring

Anne Baanen (Sep 16 2021 at 14:56):

Ok, I went through dedekind_domain.lean and now we have 3 declarations (docs#is_dedekind_domain_inv_iff, docs#mul_inv_cancel_of_le_one and docs#ideal.unique_factorization_monoid) that went from >10 seconds on my machine to about 3 seconds now. Thank you @Kevin Buzzard and @Sebastien Gouezel for the speedup! All the other declarations in the file are less than 2 seconds.

Anne Baanen (Sep 16 2021 at 14:59):

#9232

Eric Wieser (Sep 16 2021 at 15:55):

Looks like CI is unhappy; I'm wary of the irreducible attributes, those frequently cause more harm than good on instances

Yaël Dillies (Sep 17 2021 at 08:46):

And it timed out me a build again! I'm really looking forward to that speedup :smile:

Eric Wieser (Sep 17 2021 at 08:56):

#9227 failed bors because of this timeout

Eric Wieser (Sep 17 2021 at 08:59):

I've created #9243 to stop the bleeding, since #9232 has fallen afoul of its own ambition

Sebastien Gouezel (Sep 17 2021 at 09:02):

I've just borsed it (this one is too important to wait for CI :-)

Eric Wieser (Sep 17 2021 at 09:04):

No doubt we will need the rest of @Anne Baanen's speedups sooner rather than later, but this will buy us some time

Anne Baanen (Sep 17 2021 at 09:05):

Yeah, turns out that docs#localization mixes a lot of its instances between docs#con.comm_monoid and docs#localization.comm_monoid, so it will take a bit to untangle :grimacing:

Anne Baanen (Sep 17 2021 at 11:08):

Okay, I think I put all the quot behind the irreducible barrier on localization, let's see if anything else tries to escape...


Last updated: Dec 20 2023 at 11:08 UTC