feat(Algebra/Order/Floor): Weaken assumptions on theorems about FloorRing#37964
feat(Algebra/Order/Floor): Weaken assumptions on theorems about FloorRing#37964mortarsanjaya wants to merge 20 commits intoleanprover-community:masterfrom
FloorRing#37964Conversation
This reverts commit 676181f.
In particular, we can remove `IsOrderedRing` in some of the lemmas.
These lemmas will be used to weaken/remove the `IsOrderedRing` and `IsStrictOrderedRing` assumptions from the lemmas on `FloorSemiring` and `FloorRing`.
These cannot be weakened further; the instances are false without at least `IsOrderedAddMonoid`.
The lemmas in `Floor/Semiring` have their `IsOrderedRing`/`IsStrictOrderedRing` assumptions weakened, most of which can be done immediately or with minimal modification. For the lemmas `mul_cast_floor_div_cancel` and `floor_add_natCast`, we need to change their proof.
Most of these require at most minor modifications, mainly applying the `FloorRing` analogue of `Nat.cast_le` and its variants. The proof golfs are also primarily intended to make it so that the corresponding lemmas require less instances. One big exception is `mul_cast_floor_div_cancel_of_pos`, which requires writing the multiplication as `zsmul`, and it also requires an extra import `Mathlib.Algebra.Order.Group.Basic`.
Again, the main goal is to weaken assumptions on the corresponding lemmas. But in doing that we obtained a shorter proof.
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 663c249650
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Order.Floor.Ring | 647 | 648 | +1 (+0.15%) |
| Mathlib.Algebra.Order.Round | 648 | 649 | +1 (+0.15%) |
| Mathlib.Data.Rat.Floor | 654 | 655 | +1 (+0.15%) |
| Mathlib.Algebra.ContinuedFractions.Computation.Approximations | 808 | 809 | +1 (+0.12%) |
| Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat | 811 | 812 | +1 (+0.12%) |
Import changes for all files
| Files | Import difference |
|---|---|
10 filesMathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Algebra.Order.Floor.Ring Mathlib.Algebra.Order.Round Mathlib.Data.Int.CardIntervalMod Mathlib.Data.NNRat.Floor Mathlib.Data.Rat.Floor Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv |
1 |
Declarations diff
+ ceil_nonpos
+ floor_lt_zero
+ intCast_le_iff
+ intCast_lt_iff
+ intCast_mono
+ intCast_strictMono
++ instance : CharZero α := ⟨natCast_strictMono.injective⟩
++ instance : ZeroLEOneClass α := ⟨by simpa only [Nat.cast_one] using natCast_nonneg 1⟩
++ natCast_le_iff
++ natCast_lt_iff
++ natCast_mono
++ natCast_nonneg
++ natCast_pos
++ natCast_strictMono
-- instance : NeZero (1 : α)
-- instance : Nontrivial α := NeZero.nontrivial 1
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
These theorems now give a warning saying that `IsStrictOrderedRing` is not required for them.
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
No need for the "strict"ness.
1 participant
This PR weakens as much assumptions as possible on theorems about
FloorSemiringandFloorRing. Mainly,IsOrderedRingandIsStrictOrderedRingare weakened to justIsOrderedAddMonoidor removed completely from the assumptions on the theorems.Most theorems can be generalized as is or only requires a minor modification of replacing lemmas about casting naturals/integers preserving order (the likes of
Nat.cast_le,Int.cast_lt, etc.) with the corresponding version forFloorRing. Some other lemmas require modification in the proofs, but these changes shorten the proofs. The new proof of the theoremInt.mul_cast_floor_div_cancel_of_posrequires an extra import.The assumption
IsOrderedAddMonoidis required on lemmas that involve comparison + addition, andIsOrderedRingis required only on lemmas that involve comparison + multiplication of two non-integer elements.Nat.castis strictly monotone inFloorSemiringandFloorRing#37714