[Merged by Bors] - chore(data/int/gcd): streamline imports #16811
Conversation
This file contains 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
hrmacbeth
added
awaiting-review
|
Given that this doesn't seem to be API lemmas, would it make more sense to put in the |
|
I can even put it in the main I'm also avoiding referencing that PR by hyperlink, for the same reason :) |
|
Surely referencing a PR doesn't reset its position on the PR queue? |
|
I don't know, but I'd rather not risk it :) |
|
Let me try to reference my PR #16804 |
|
Tough luck, it's not on the queue. #15289 is however. EDIT: Indeed it doesn't move it. |
|
Oh sorry, github default is actually descending numeric order if I'm not logged in; |
|
#16588 is now merged, but I decided to move the |
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
## Historical background This tackles a problem that we have had for six years (#2697 for its move to mathlib, before it was in core): `ordered_semiring` assumes that addition and multiplication are strictly monotone. This led to weirdness within the algebraic order hierarchy: * `ennreal`/`ereal`/`enat` needed custom lemmas (`∞ + 0 = ∞ = ∞ + 1`, `1 * ∞ = ∞ = 2 * ∞`). * A `canonically_ordered_comm_semiring` was not an `ordered_comm_semiring`! ## What this PR does This PR solves the problem minimally by renaming `ordered_(comm_)semiring` to `strict_ordered_(comm_)semiring` and adding a new class `ordered_(comm_)semiring` that doesn't assume strict monotonicity of addition and multiplication but only monotonicity: ``` class ordered_semiring (α : Type*) extends semiring α, ordered_add_comm_monoid α := (zero_le_one : (0 : α) ≤ 1) (mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b) (mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c) class ordered_comm_semiring (α : Type*) extends ordered_semiring α, comm_semiring α class ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α := (zero_le_one : 0 ≤ (1 : α)) (mul_nonneg : ∀ a b : α, 0 ≤ a → 0 ≤ b → 0 ≤ a * b) class ordered_comm_ring (α : Type u) extends ordered_ring α, comm_ring α class strict_ordered_semiring (α : Type*) extends semiring α, ordered_cancel_add_comm_monoid α := (zero_le_one : (0 : α) ≤ 1) (mul_lt_mul_of_pos_left : ∀ a b c : α, a < b → 0 < c → c * a < c * b) (mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c) class strict_ordered_comm_semiring (α : Type*) extends strict_ordered_semiring α, comm_semiring α class strict_ordered_ring (α : Type u) extends ring α, ordered_add_comm_group α := (zero_le_one : 0 ≤ (1 : α)) (mul_pos : ∀ a b : α, 0 < a → 0 < b → 0 < a * b) class strict_ordered_comm_ring (α : Type*) extends strict_ordered_ring α, comm_ring α ``` ## Whatever happened to the `decidable` lemmas? Scrolling through the diff, you will see that only one lemma in the `decidable` namespace out of many survives this PR. Those lemmas were originally meant to avoid using choice in the proof of `nat` and `int` lemmas. The need for decidability originated from the proofs of `mul_le_mul_of_nonneg_left`/`mul_le_mul_of_nonneg_right`. ``` protected lemma decidable.mul_le_mul_of_nonneg_left [@decidable_rel α (≤)] (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b := begin by_cases ba : b ≤ a, { simp [ba.antisymm h₁] }, by_cases c0 : c ≤ 0, { simp [c0.antisymm h₂] }, exact (mul_lt_mul_of_pos_left (h₁.lt_of_not_le ba) (h₂.lt_of_not_le c0)).le, end ``` Now that these are fields to `ordered_semiring`, they are already choice-free. Instead, choice is now used in showing that an `ordered_cancel_semiring` is an `ordered_semiring`. ``` @[priority 100] -- see Note [lower instance priority] instance ordered_cancel_semiring.to_ordered_semiring : ordered_semiring α := { mul_le_mul_of_nonneg_left := λ a b c hab hc, begin obtain rfl | hab := hab.eq_or_lt, { refl }, obtain rfl | hc := hc.eq_or_lt, { simp }, { exact (mul_lt_mul_of_pos_left hab hc).le } end, mul_le_mul_of_nonneg_right := λ a b c hab hc, begin obtain rfl | hab := hab.eq_or_lt, { refl }, obtain rfl | hc := hc.eq_or_lt, { simp }, { exact (mul_lt_mul_of_pos_right hab hc).le } end, ..‹ordered_cancel_semiring α› } ``` It seems unreasonable to make that instance depend on `@decidable_rel α (≤)` even though it's only needed for the proofs. ## Other changes To have some lemmas in the generality of the new `ordered_semiring`, I needed a few new lemmas: * `bit0_mono` * `bit0_strict_mono` It was also simpler to golf `analysis.special_functions.stirling` using `positivity` rather than fixing it so I introduce the following (simple) `positivity` extensions: * `positivity_succ` * `positivity_factorial` * `positivity_asc_factorial`
…degeneracy (#16779) In this PR, it is shown that the Čech nerve of a split epimorphism has an extra degeneracy. It is also shown that if two augmented simplicial objects are isomorphic, then an extra degeneracy for one of these transports as an extra degeneracy for the other.
…6844) Squeeze simps and replace a slow `convert` by `eq.subst` with explicit motive (maybe `convert` was unfolding the instances?). From >20s to 4s on my machine.
hrmacbeth
removed
the
awaiting-review
github-actions
bot
removed
the
awaiting-CI
hrmacbeth
added
the
awaiting-review
|
bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Oct 10, 2022
The file on gcds of integers is fundamentally very elementary, but it contained two lemmas about prime numbers, and `data.nat.prime` seems to import everything (modules! half the order library!). Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
eric-wieser
added
the
hacktoberfest-accepted
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
The file on gcds of integers is fundamentally very elementary, but it contained two lemmas about prime numbers, and
data.nat.primeseems to import everything (modules! half the order library!).