[Merged by Bors] - perf: replace many instances of 'linarith' with 'omega'#19951
[Merged by Bors] - perf: replace many instances of 'linarith' with 'omega'#19951
Conversation
PR summary 47605f6eb5Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
!bench |
|
Here are the benchmark results for commit 9bf532e. |
grunweg
left a comment
There was a problem hiding this comment.
Thanks a lot for this change, would review again! I double-check against the benchmarking output that all changed files really got faster (some very substantially so).
If you find more of these, I'll be happy to review that PR also.
maintainer merge
| mul_comm (2 : K), add_sub_cancel, neg_neg, add_sub, Nat.cast_inj, | ||
| eq_sub_iff_add_eq, ← Nat.cast_add, ← sub_eq_neg_add, sub_eq_iff_eq_add] at this | ||
| linarith [this, hn] | ||
| omega |
There was a problem hiding this comment.
This change seems to be within noise, but it's shorter - I'll take it.
There was a problem hiding this comment.
Actually: perhaps this change didn't get benchmarked yet --- that would explain things.
| exact (cs.length_mul_simple w i).resolve_right (by omega) | ||
| · intro _ | ||
| linarith | ||
| omega |
There was a problem hiding this comment.
This file even sped up by 25%, nice!
| obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp' | ||
| by_cases hp' : 1 ≤ p.natDegree; swap | ||
| · obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by nlinarith) | ||
| · obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by omega) |
There was a problem hiding this comment.
This change speeds up the file by 8%, nice!
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Thanks 🎉 bors merge |
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.
|
Pull request successfully merged into master. Build succeeded: |
|
I maybe should have also mentioned:
|
Replaces 63 usages of
linarithornlinarithwithomega. In all of these cases I have observed the new proof to be faster.I found these improvements by running tryAtEachStep to try
omegaat every tactic step in mathlib.This is a continuation of the work from #11093.