Timeouts in ring_theory/dedekind_domain.lean:664:9

Stream: general

[Eric Wieser]

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]

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]

That was going to be my first guess :)

[Kevin Buzzard]

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]

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

[Sebastien Gouezel]

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]

I can reproduce here

[Sebastien Gouezel]

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

[Eric Wieser]

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

[Sebastien Gouezel]

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]

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

[Anne Baanen]

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]

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

[Anne Baanen]

Yes, sorry for the confusion.

[Eric Wieser]

Do you plan to PR both speedups @Anne Baanen?

[Anne Baanen]

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

[Anne Baanen]

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]

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]

#9232

[Eric Wieser]

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

[Yaël Dillies]

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

[Eric Wieser]

#9227 failed bors because of this timeout

[Eric Wieser]

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

[Sebastien Gouezel]

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

[Eric Wieser]

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]

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]

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