[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` #18912

eric-wieser · 2023-05-02T00:00:54Z

This replaces mem_Ioo_mod hp a b with ¬add_comm_group.modeq p a b.
This is more consistent with int.modeq, nat.modeq, and smodeq.

There's still some duplication here, but at least these four ideas are now conceptually aligned.

This remove any lemmas of the form ¬modeq p a b ↔ _ ≠ _ as these are now trivial consequences of the modeq p a b ↔ _ = _ versions,

depends on: [Merged by Bors] - chore(algebra/order/to_interval_mod): Reorder arguments #18908

src/algebra/order/to_interval_mod.lean

mathlib-dependent-issues-bot · 2023-05-02T01:53:54Z

This PR/issue depends on:

~~[Merged by Bors] - chore(algebra/order/to_interval_mod): Reorder arguments #18908~~
By Dependent Issues (🤖). Happy coding!

alreadydone

Not sure why there are merge conflicts now ...

src/algebra/order/to_interval_mod.lean

alreadydone · 2023-05-02T05:15:45Z

src/algebra/order/to_interval_mod.lean

+/-- `Imodeq p a b` means that `b` does not lie in the open interval `(a, a + p)` modulo `p`.
+Equivalently (as shown below), `b` is congruent to `a` modulo `p`, or `to_Ico_mod hp a` disagrees
+with `to_Ioc_mod hp a` at `b`, or `to_Ico_div hp a` disagrees with `to_Ioc_div hp a` at `b`. -/
+def Imodeq (p a b : α) : Prop := ∀ z : ℤ, b - z • p ∉ set.Ioo a (a + p)


Calling this definition Imodeq sounds weird to me. If you want to unify with smodeq in the future, wouldn't you take the RHS of Imodeq_iff_eq_mod_zmultiples as the definition?

This PR looks good to me apart from this issue.

If you want to unify with smodeq in the future, wouldn't you take the RHS of Imodeq_iff_eq_mod_zmultiples as the definition?

Yes, absolutely; I just figured that was a much larger refactor than I wanted to make, as it flips the order of all the proofs below. ~~If you want to do this in a follow-up, I'm happy to review; but we could also just leave it till after the port.~~ I can do this as a follow-up, but it's orthogonal to #17743

Another possible name would be archimedean.modeq?

Or add_comm_group.modeq

What I meant is that I think Imodeq is an acceptable name for (a : α ⧸ add_subgroup.zmultiples p) = b (and add_comm_group.modeq is reasonable too), but the name for the current definition should be something like not_mem_Ioo in order to be descriptive. However, if you plan to replace the definition by (a : α ⧸ add_subgroup.zmultiples p) = b in the future, then I think we should keep the current name, but we should also add the replacement as a TODO item in the docstring.

FYI I am currently writing the API for

def modeq (p a b : α) : Prop := ∃ z : ℤ, b - a = z • p

…m_Ioo_mod` This replaces `mem_Ioo_mod hp a b` with `¬Imodeq p a b`, where `Imodeq` stands for `interval mod equal`. This is more consistent with `int.modeq`, `nat.modeq`, and `smodeq`. There's still some duplication here, but at least these four ideas are now conceptually aligned. This remove any lemmas of the form `¬Imodeq p a b ↔ _ ≠ _` as these are now trivial consequences of the `Imodeq p a b ↔ _ = _` versions,

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

YaelDillies

Let's move forward with this.

maintainer merge

github-actions · 2023-05-02T16:33:49Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

semorrison · 2023-05-02T22:46:47Z

bors merge

…m_Ioo_mod` (#18912) This replaces `mem_Ioo_mod hp a b` with `¬add_comm_group.modeq p a b`. This is more consistent with `int.modeq`, `nat.modeq`, and `smodeq`. There's still some duplication here, but at least these four ideas are now conceptually aligned. This remove any lemmas of the form `¬modeq p a b ↔ _ ≠ _` as these are now trivial consequences of the `modeq p a b ↔ _ = _` versions,

bors · 2023-05-03T06:27:41Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

eric-wieser requested a review from alreadydone May 2, 2023 00:01

github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label May 2, 2023

YaelDillies reviewed May 2, 2023

View reviewed changes

src/algebra/order/to_interval_mod.lean Outdated Show resolved Hide resolved

mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label May 2, 2023

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 2, 2023

alreadydone reviewed May 2, 2023

View reviewed changes

eric-wieser force-pushed the eric-wieser/flip-mem_Ioo_mod branch from 79bdb72 to 5c94437 Compare May 2, 2023 08:07

eric-wieser and others added 3 commits May 2, 2023 09:09

Apply suggestions from code review

2dd56db

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

golf

9d73bd0

blank line

0b3e1cc

eric-wieser mentioned this pull request May 2, 2023

[Merged by Bors] - feat(algebra/order/to_interval_mod): add circular_order instance for add_circle #17743

Closed

7 tasks

rename

f7fe457

YaelDillies added t-algebra Algebra (groups, rings, fields etc) and removed modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. labels May 2, 2023

YaelDillies approved these changes May 2, 2023

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 2, 2023

bors bot changed the title ~~refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod~~ [Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod May 3, 2023

bors bot closed this May 3, 2023

bors bot deleted the eric-wieser/flip-mem_Ioo_mod branch May 3, 2023 06:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` #18912

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` #18912

eric-wieser commented May 2, 2023 •

edited

Loading

mathlib-dependent-issues-bot commented May 2, 2023

alreadydone left a comment

alreadydone May 2, 2023 •

edited

Loading

eric-wieser May 2, 2023 •

edited

Loading

eric-wieser May 2, 2023 •

edited

Loading

eric-wieser May 2, 2023

alreadydone May 2, 2023 •

edited

Loading

YaelDillies May 2, 2023

YaelDillies left a comment

github-actions bot commented May 2, 2023

semorrison commented May 2, 2023

bors bot commented May 3, 2023

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod #18912

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of mem_Ioo_mod #18912

Conversation

eric-wieser commented May 2, 2023 • edited Loading

mathlib-dependent-issues-bot commented May 2, 2023

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone May 2, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser May 2, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser May 2, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser May 2, 2023

Choose a reason for hiding this comment

alreadydone May 2, 2023 • edited Loading

Choose a reason for hiding this comment

YaelDillies May 2, 2023

Choose a reason for hiding this comment

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented May 2, 2023

semorrison commented May 2, 2023

bors bot commented May 3, 2023

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` #18912

[Merged by Bors] - refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` #18912

eric-wieser commented May 2, 2023 •

edited

Loading

alreadydone May 2, 2023 •

edited

Loading

eric-wieser May 2, 2023 •

edited

Loading

eric-wieser May 2, 2023 •

edited

Loading

alreadydone May 2, 2023 •

edited

Loading