New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(ring_theory/dedekind_domain): speed up dedekind_domain.lean
#9232
Conversation
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-Authored-By: Kevin Buzzard <k.buzzard@imperial.ac.uk>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors d+
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
The queue is empty but the PR builders are busy, so let's just throw this over to nael and hope bors r+ |
…9232) @eric-wieser [noticed that `dedekind_domain.lean`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeouts.20in.20ring_theory.2Fdedekind_domain.2Elean.3A664.3A9) was compiling slowly and on the verge of a timeout. @kbuzzard, @sgouezel and I reworked some definitions to make everything elaborate much faster: `is_dedekind_domain_inv_iff`, `mul_inv_cancel_of_le_one` and `ideal.unique_factorization_monoid` went from over 10 seconds on my machine to less than 3 seconds. No other declaration in that file now takes over 2 seconds on my machine. Apart from the three declarations getting new proofs, I also made the following changes: * The operations on `localization` (`has_add`, `has_mul`, `has_one`, `has_zero`, `has_neg` and `localization.inv`) are now `@[irreducible]` * `fraction_ring.field` copies its field from `localization.comm_ring` for faster unification (less relevant after the previous change) * Added `fractional_ideal.map_mem_map` and `fractional_ideal.map_injective` to simplify the proof of `is_dedekind_domain_inv_iff`.
Build failed: |
Well that at least got us an answer quickly! |
This should ensure the API for `localization` is contained within `mk`/`mk_eq_mk_iff`/`rec`, no more `quotient` defs escaping
This halves the elaboration time of `matrix.mul_vec_eq_zero_iff`
I'm going to re-request a review since a lot changed since the previous one. |
Thanks 🎉 bors merge |
…9232) @eric-wieser [noticed that `dedekind_domain.lean`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeouts.20in.20ring_theory.2Fdedekind_domain.2Elean.3A664.3A9) was compiling slowly and on the verge of a timeout. @kbuzzard, @sgouezel and I reworked some definitions to make everything elaborate much faster: `is_dedekind_domain_inv_iff`, `mul_inv_cancel_of_le_one` and `ideal.unique_factorization_monoid` went from over 10 seconds on my machine to less than 3 seconds. No other declaration in that file now takes over 2 seconds on my machine. Apart from the three declarations getting new proofs, I also made the following changes: * The operations on `localization` (`has_add`, `has_mul`, `has_one`, `has_zero`, `has_neg`, `npow` and `localization.inv`) are now `@[irreducible]` * `fraction_ring.field` copies its field from `localization.comm_ring` for faster unification (less relevant after the previous change) * Added `fractional_ideal.map_mem_map` and `fractional_ideal.map_injective` to simplify the proof of `is_dedekind_domain_inv_iff`. * Split the proof of `matrix.exists_mul_vec_eq_zero_iff` into two parts to speed it up Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
dedekind_domain.lean
dedekind_domain.lean
@eric-wieser noticed that
dedekind_domain.lean
was compiling slowly and on the verge of a timeout. @kbuzzard, @sgouezel and I reworked some definitions to make everything elaborate much faster:is_dedekind_domain_inv_iff
,mul_inv_cancel_of_le_one
andideal.unique_factorization_monoid
went from over 10 seconds on my machine to less than 3 seconds. No other declaration in that file now takes over 2 seconds on my machine.Apart from the three declarations getting new proofs, I also made the following changes:
localization
(has_add
,has_mul
,has_one
,has_zero
,has_neg
,npow
andlocalization.inv
) are now@[irreducible]
fraction_ring.field
copies its field fromlocalization.comm_ring
for faster unification (less relevant after the previous change)fractional_ideal.map_mem_map
andfractional_ideal.map_injective
to simplify the proof ofis_dedekind_domain_inv_iff
.matrix.exists_mul_vec_eq_zero_iff
into two parts to speed it up