[Merged by Bors] - feat: order lemmas for NNRat by eric-wieser · Pull Request #13547 · leanprover-community/mathlib4

eric-wieser · 2024-06-06T00:12:35Z

This copies the API for order lemmas on Rat

Mathlib/Data/Rat/Cast/Order.lean

YaelDillies · 2024-06-06T08:09:26Z

Mathlib/Data/Rat/Cast/Order.lean

+@[simp]
+theorem preimage_cast_Icc (a b : ℚ≥0) : (↑) ⁻¹' Icc (a : K) b = Icc a b :=
+  castOrderEmbedding.preimage_Icc ..
+
+@[simp]
+theorem preimage_cast_Ico (a b : ℚ≥0) : (↑) ⁻¹' Ico (a : K) b = Ico a b :=
+  castOrderEmbedding.preimage_Ico ..
+
+@[simp]
+theorem preimage_cast_Ioc (a b : ℚ≥0) : (↑) ⁻¹' Ioc (a : K) b = Ioc a b :=
+  castOrderEmbedding.preimage_Ioc a b
+
+@[simp]
+theorem preimage_cast_Ioo (a b : ℚ≥0) : (↑) ⁻¹' Ioo (a : K) b = Ioo a b :=
+  castOrderEmbedding.preimage_Ioo a b
+
+@[simp]
+theorem preimage_cast_Ici (a : ℚ≥0) : (↑) ⁻¹' Ici (a : K) = Ici a :=
+  castOrderEmbedding.preimage_Ici a
+
+@[simp]
+theorem preimage_cast_Iic (a : ℚ≥0) : (↑) ⁻¹' Iic (a : K) = Iic a :=
+  castOrderEmbedding.preimage_Iic a
+
+@[simp]
+theorem preimage_cast_Ioi (a : ℚ≥0) : (↑) ⁻¹' Ioi (a : K) = Ioi a :=
+  castOrderEmbedding.preimage_Ioi a
+
+@[simp]
+theorem preimage_cast_Iio (a : ℚ≥0) : (↑) ⁻¹' Iio (a : K) = Iio a :=
+  castOrderEmbedding.preimage_Iio a
+
+@[simp]
+theorem preimage_cast_uIcc (a b : ℚ≥0) : (↑) ⁻¹' uIcc (a : K) b = uIcc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIcc a b
+
+@[simp]
+theorem preimage_cast_uIoc (a b : ℚ≥0) : (↑) ⁻¹' uIoc (a : K) b = uIoc a b :=
+  (castOrderEmbedding (K := K)).preimage_uIoc a b


Can we have the corresponding image lemmas for NNRat -> Rat?

I'd claim "out of scope" here too; this PR just duplicates the existing Rat API, rather than adding new API.

YaelDillies · 2024-06-06T08:09:55Z

Mathlib/Data/Rat/Cast/Order.lean

+@[simp]
+theorem cast_lt_zero {n : ℚ≥0} : (n : K) < 0 ↔ n < 0 := by
+  norm_cast


This looks useless

I'd argue that unless the linter complains, it's not!

No but like there's no point blindly copying lemmas from one type to the other if they don't make sense for the new type. Both sides of your iff are always false, so you might as well replace it by Not LHS

Ah, I guess the linter doesn't tell me when the RHS is further simplified.

I've added your suggest but kept my original (without simp), because without this lemma norm_cast leaves some casts around.

Uh okay interesting

YaelDillies · 2024-06-06T08:10:12Z

Mathlib/Data/Rat/Cast/Order.lean

+  norm_cast
+
+@[simp, norm_cast]
+theorem cast_min {a b : ℚ≥0} : (↑(min a b) : K) = min (a : K) (b : K) :=


Suggested change

theorem cast_min {a b : ℚ≥0} : (↑(min a b) : K) = min (a : K) (b : K) :=

theorem cast_min (a b : ℚ≥0) : (↑(min a b) : K) = min (a : K) (b : K) :=

and below

This is consistent with the Rat versions of the lemmas; I'd prefer to declare this out of scope too.

I have opened #13644 to make your changes inconsistent with the Rat versions of the lemmas

I'd appreciate it if you could push the corresponding changes to this PR once that lands; but it can wait till after your final exam!

(or preferably, delegate this one first so that I can move on to the floorsemiring instance)

Sure, I guess that's fixable later

maintainer merge

Mathlib/Data/Rat/Cast/Order.lean

github-actions · 2024-06-08T09:23:34Z

PR summary

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Rat.Cast.Order	477	479	+2 (+0.42%)

Declarations diff

+ castOrderEmbedding
+ cast_le
+ cast_lt
+ cast_lt_zero
+ cast_max
+ cast_min
+ cast_mono
+ cast_nonpos
+ cast_pos
+ cast_strictMono
+ evalNNRatCast
+ le_def
+ lt_def
+ not_cast_lt_zero
+ preimage_cast_Icc
+ preimage_cast_Ici
+ preimage_cast_Ico
+ preimage_cast_Iic
+ preimage_cast_Iio
+ preimage_cast_Ioc
+ preimage_cast_Ioi
+ preimage_cast_Ioo
+ preimage_cast_uIcc
+ preimage_cast_uIoc

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

sgouezel · 2024-06-09T07:15:09Z

bors r+

This copies the API for order lemmas on `Rat`

mathlib-bors · 2024-06-09T08:11:59Z

Pull request successfully merged into master.

Build succeeded:

This copies the API for order lemmas on `Rat`

eric-wieser added 3 commits June 5, 2024 23:56

feat: add lemmas for NNRat

46361cf

more

987cddc

whitespace

1d468be

eric-wieser added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-order Order theory labels Jun 6, 2024

eric-wieser requested a review from YaelDillies June 6, 2024 00:12

eric-wieser mentioned this pull request Jun 6, 2024

[Merged by Bors] - feat: add a FloorSemiring instance to NNRat #13548

Closed

1 task

YaelDillies reviewed Jun 6, 2024

View reviewed changes

Mathlib/Data/Rat/Cast/Order.lean Show resolved Hide resolved

YaelDillies reviewed Jun 6, 2024

View reviewed changes

Mathlib/Data/Rat/Cast/Order.lean Show resolved Hide resolved

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 6, 2024

fix

eb81eda

eric-wieser added 2 commits June 8, 2024 09:46

tests

edf37aa

silence linter

7a163d9

eric-wieser added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 8, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 8, 2024

tidy

41def3a

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 9, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jun 9, 2024

feat: order lemmas for NNRat (#13547)

4810c69

This copies the API for order lemmas on `Rat`

mathlib-bors bot changed the title ~~feat: order lemmas for NNRat~~ [Merged by Bors] - feat: order lemmas for NNRat Jun 9, 2024

mathlib-bors bot closed this Jun 9, 2024

mathlib-bors bot deleted the eric-wieser/nnrat-lemmas branch June 9, 2024 08:12

AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024

feat: order lemmas for NNRat (#13547)

73bc871

This copies the API for order lemmas on `Rat`

YaelDillies mentioned this pull request Aug 27, 2024

[Merged by Bors] - feat: When NNRat.cast is less/greater than 1 #16137

Closed

	theorem cast_min {a b : ℚ≥0} : (↑(min a b) : K) = min (a : K) (b : K) :=
	theorem cast_min (a b : ℚ≥0) : (↑(min a b) : K) = min (a : K) (b : K) :=

Conversation

eric-wieser commented Jun 6, 2024

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jun 8, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary

Import changes

Declarations diff

Uh oh!

sgouezel commented Jun 9, 2024

Uh oh!

mathlib-bors bot commented Jun 9, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions bot commented Jun 8, 2024 •

edited

Loading