[Merged by Bors] - refactor: optimize proofs with omega#11093
Closed
[Merged by Bors] - refactor: optimize proofs with omega#11093
Conversation
Member
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit d94f33d. Benchmark Metric Change
==================================================================================
+ ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplex instructions -15.3%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift instructions -16.8%
+ ~Mathlib.Algebra.Homology.HomotopyCategory.MappingCone instructions -21.6%
+ ~Mathlib.AlgebraicTopology.DoldKan.Faces instructions -46.9%
+ ~Mathlib.AlgebraicTopology.SimplexCategory instructions -26.1%
+ ~Mathlib.Computability.AkraBazzi.AkraBazzi instructions -6.5%
+ ~Mathlib.Order.RelSeries instructions -25.7% |
mattrobball
approved these changes
Mar 1, 2024
| (h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)) : | ||
| Homotopy f₁ f₂ := | ||
| (Cochain.equivHomotopy f₁ f₂).symm ⟨descCochain φ γ₁ γ₂ (by linarith), by | ||
| (Cochain.equivHomotopy f₁ f₂).symm ⟨descCochain φ γ₁ γ₂ (by norm_num), by |
Contributor
There was a problem hiding this comment.
One of these is not like the other.
Member
Author
There was a problem hiding this comment.
omega works here, but norm_num is even faster.
Contributor
|
bors delegate+ Once CI is green, please send it. Thanks! |
Contributor
|
✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with |
dwrensha
commented
Mar 2, 2024
| comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by linarith) (by linarith), | ||
| comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by linarith) (by linarith), | ||
| comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by linarith) (by linarith), assoc] | ||
| rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by omega), |
Member
Author
There was a problem hiding this comment.
I added the explicit term add_assoc here because omega seemed to be actually a bit slower than linarith, and writing the term like this was easy enough.
Member
Author
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 2, 2024
I ran [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) on all files under `Mathlib` to find all locations where `omega` succeeds. For each that was a `linarith` without an `only`, I tried replacing it with `omega`, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow `aesop`s along the way.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
kbuzzard
pushed a commit
that referenced
this pull request
Mar 12, 2024
I ran [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) on all files under `Mathlib` to find all locations where `omega` succeeds. For each that was a `linarith` without an `only`, I tried replacing it with `omega`, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow `aesop`s along the way.
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
I ran [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) on all files under `Mathlib` to find all locations where `omega` succeeds. For each that was a `linarith` without an `only`, I tried replacing it with `omega`, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow `aesop`s along the way.
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
I ran [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) on all files under `Mathlib` to find all locations where `omega` succeeds. For each that was a `linarith` without an `only`, I tried replacing it with `omega`, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow `aesop`s along the way.
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
I ran [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) on all files under `Mathlib` to find all locations where `omega` succeeds. For each that was a `linarith` without an `only`, I tried replacing it with `omega`, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slow `aesop`s along the way.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 14, 2024
Replaces 63 usages of `linarith` or `nlinarith` with `omega`. In all of these cases I have observed the new proof to be faster. I found these improvements by running [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) to try `omega` at every tactic step in mathlib. This is a continuation of the work from #11093.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
I ran tryAtEachStep on all files under
Mathlibto find all locations whereomegasucceeds. For each that was alinarithwithout anonly, I tried replacing it withomega, and I verified that elaboration time got smaller. (In almost all cases, there was a noticeable speedup.) I also replaced some slowaesops along the way.