-
Notifications
You must be signed in to change notification settings - Fork 316
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
feat: add a FloorSemiring instance to NNRat #13548
Open
eric-wieser
wants to merge
22
commits into
master
Choose a base branch
from
eric-wieser/nnrat-floor
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+159
−3
Open
Changes from all commits
Commits
Show all changes
22 commits
Select commit
Hold shift + click to select a range
46361cf
feat: add lemmas for NNRat
eric-wieser 987cddc
more
eric-wieser 1d468be
whitespace
eric-wieser d00d944
feat: add a FloorSemiring instance to nnrat
eric-wieser e4a084e
fix
eric-wieser 41f1de7
whitespace
eric-wieser 7e41bc7
Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f…
eric-wieser 422a5d5
working
eric-wieser 42db170
Merge branch 'master' into eric-wieser/nnrat-floor
eric-wieser 8c3eb6e
Update Floor.lean
eric-wieser 900b41f
add import
eric-wieser 8e1768d
add lemmas
eric-wieser fbed638
more silly lemmas
eric-wieser 0c0206f
shake
eric-wieser 97859f6
grammar fix
eric-wieser 0459227
Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f…
eric-wieser a5f49e8
more lemmas
eric-wieser a62409e
Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f…
eric-wieser b7d6be9
sorry-free
eric-wieser e30bc10
fix deprecation
eric-wieser eaa6533
add @[simp]
eric-wieser 6d6f59b
Merge remote-tracking branch 'origin/master' into eric-wieser/nnrat-f…
eric-wieser File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,90 @@ | ||
/- | ||
Copyright (c) 2024 Eric Wieser. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Eric Wieser | ||
-/ | ||
import Mathlib.Data.Rat.Floor | ||
|
||
/-! | ||
# Floor Function for Non-negative Rational Numbers | ||
|
||
## Summary | ||
|
||
We define the `FloorSemiring` instance on `ℚ≥0`, and relate its operators to `NNRat.cast`. | ||
|
||
Note that we cannot talk about `Int.fract`, which currently only works for rings. | ||
|
||
## Tags | ||
|
||
nnrat, rationals, ℚ≥0, floor | ||
-/ | ||
|
||
namespace NNRat | ||
|
||
instance : FloorSemiring ℚ≥0 where | ||
floor q := ⌊q.val⌋₊ | ||
ceil q := ⌈q.val⌉₊ | ||
floor_of_neg h := by simpa using h.trans zero_lt_one | ||
gc_floor {a n} h := by rw [← NNRat.coe_le_coe, Nat.le_floor_iff] <;> norm_cast | ||
gc_ceil {a b} := by rw [← NNRat.coe_le_coe, Nat.ceil_le]; norm_cast | ||
|
||
@[simp, norm_cast] | ||
theorem floor_coe (q : ℚ≥0) : ⌊(q : ℚ)⌋₊ = ⌊q⌋₊ := rfl | ||
YaelDillies marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
||
@[simp, norm_cast] | ||
theorem ceil_coe (q : ℚ≥0) : ⌈(q : ℚ)⌉₊ = ⌈q⌉₊ := rfl | ||
|
||
@[simp, norm_cast] | ||
theorem coe_floor (q : ℚ≥0) : ↑⌊q⌋₊ = ⌊(q : ℚ)⌋ := Int.ofNat_floor_eq_floor q.coe_nonneg | ||
|
||
@[simp, norm_cast] | ||
theorem coe_ceil (q : ℚ≥0) : ↑⌈q⌉₊ = ⌈(q : ℚ)⌉ := Int.ofNat_ceil_eq_ceil q.coe_nonneg | ||
|
||
protected theorem floor_def (q : ℚ≥0) : ⌊q⌋₊ = q.num / q.den := by | ||
rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def, Int.ofNat_ediv, den_coe, num_coe] | ||
|
||
section Semifield | ||
|
||
variable {K} [LinearOrderedSemifield K] [FloorSemiring K] | ||
|
||
@[simp, norm_cast] | ||
theorem floor_cast (x : ℚ≥0) : ⌊(x : K)⌋₊ = ⌊x⌋₊ := | ||
(Nat.floor_eq_iff x.cast_nonneg).2 (mod_cast (Nat.floor_eq_iff x.cast_nonneg).1 (Eq.refl ⌊x⌋₊)) | ||
|
||
@[simp, norm_cast] | ||
theorem ceil_cast (x : ℚ≥0) : ⌈(x : K)⌉₊ = ⌈x⌉₊ := by | ||
eric-wieser marked this conversation as resolved.
Show resolved
Hide resolved
|
||
obtain rfl | hx := eq_or_ne x 0 | ||
· simp | ||
· refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊)) <;> simpa | ||
|
||
end Semifield | ||
|
||
section Field | ||
|
||
variable {K} [LinearOrderedField K] [FloorRing K] | ||
|
||
@[simp, norm_cast] | ||
theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋ := by | ||
rw [Int.floor_eq_iff (α := K), ← coe_floor] | ||
norm_cast | ||
norm_cast | ||
rw [Nat.cast_add_one, ← Nat.floor_eq_iff (zero_le _)] | ||
|
||
@[simp, norm_cast] | ||
theorem intCeil_cast (x : ℚ≥0) : ⌈(x : K)⌉ = ⌈(x : ℚ)⌉ := by | ||
rw [Int.ceil_eq_iff, ← coe_ceil, sub_lt_iff_lt_add] | ||
constructor | ||
· have := NNRat.cast_strictMono (K := K) <| Nat.ceil_lt_add_one <| zero_le x | ||
rw [NNRat.cast_add, NNRat.cast_one] at this | ||
refine Eq.trans_lt ?_ this | ||
norm_cast | ||
· rw [Int.cast_natCast, NNRat.cast_le_natCast] | ||
exact Nat.le_ceil _ | ||
|
||
end Field | ||
|
||
@[norm_cast] | ||
theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊ = n / d := | ||
Rat.natFloor_natCast_div_natCast n d | ||
|
||
end NNRat |
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
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
Oops, something went wrong.
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.
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.
Doesn't that mean we are missing
Nat.fract
with the obvious definition?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.
Yeah, but adding new definitions seems out of scope for a PR that adds new instances.