-
Notifications
You must be signed in to change notification settings - Fork 360
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(*): golf using omega
#20231
Conversation
PR summary 45f718bf46
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Data.FP.Basic | 512 | 416 | -96 (-18.75%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Data.FP.Basic |
-96 |
Declarations diff
No 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 script/declarations_diff.sh
contains some details about this script.
Decrease in tech debt: (relative, absolute) = (4.00, 0.00)
Current number | Change | Type |
---|---|---|
4837 | -4 | porting notes |
Current commit 45f718bf46
Reference commit 3874e58afc
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relative
value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolute
value is therelative
value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
!bench |
Here are the benchmark results for commit 45f718b. |
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.
Let me label a few places that got slightly slower (found by sorting the benchmarking output by the "absolute change" column). Probably, most of these are still worth it - but this should be a conscious decision.
cases' hi₁₂ with hi₁₂ hi₁₂ | ||
· exact hi₁₂ ▸ h₂ | ||
· exact hi₁₂ ▸ h₁ | ||
obtain rfl | rfl : i₁ = i ∨ i₂ = i := by omega |
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.
This file got a bit slower.
clear h₁ h₂ h₁' h₂' | ||
-- Porting note: Originally `decide!` | ||
revert i₁ i₂ i₃; decide | ||
have h3 : ∀ i : Fin 3, i = i₁ ∨ i = i₂ ∨ i = i₃ := by omega |
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.
This also got a bit slower.
@@ -194,9 +194,7 @@ theorem normalize : PythagoreanTriple (x / Int.gcd x y) (y / Int.gcd x y) (z / I | |||
theorem isClassified_of_isPrimitiveClassified (hp : h.IsPrimitiveClassified) : h.IsClassified := by | |||
obtain ⟨m, n, H⟩ := hp | |||
use 1, m, n |
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.
As did this file (not sure which line).
revert this hp3 hp1 | ||
generalize p % 4 = m | ||
intros; interval_cases m <;> simp_all -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11043): was `decide!` | ||
have hp41 : p % 4 = 1 := by omega |
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.
This file got about 5% slower (but this is a nice golf, so perhaps worth it).
simp only [Nat.one_ne_zero, if_false, ite_eq_left_iff, (by omega : (-1 : ℤ) ≠ 1), imp_false, | ||
not_not, Ne, reduceCtorEq] | ||
exact ⟨fun h ↦ ne_of_eq_of_ne h (by omega), (Nat.odd_mod_four_iff.mp h₁).resolve_right⟩ | ||
omega |
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.
This file also got a bit slower.
· have : n - 1 - (ν - 1) = n - ν := by | ||
rw [gt_iff_lt, ← Nat.succ_le_iff] at h'' | ||
rw [← tsub_add_eq_tsub_tsub, add_comm, tsub_add_cancel_of_le h''] | ||
· have : n - 1 - (ν - 1) = n - ν := by omega |
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.
Also very slightly slower - but the automation is probably worth it.
Taking a step back: thanks for proposing these golfs! They are much nicer to read, and mostly quite a bit faster. |
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.
The total build instructions only increases by 0.006%, which amounts to 1038*.006%~0.06 seconds wall-clock time, so I wouldn't worry about the slowdown. Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded: |
omega
omega
Found by https://github.com/dwrensha/tryAtEachStep