chore(algebra/to_interval_mod): refactor add_comm_group.modeq to have a simpler definition
#18941
Conversation
…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>
eric-wieser
added
the
awaiting-review
| lemma not_modeq_iff_ne_mod_zmultiples : | ||
| ¬a ≡ b [PMOD p] ↔ (b : α ⧸ add_subgroup.zmultiples p) ≠ a := | ||
| modeq_iff_eq_mod_zmultiples.not |
There was a problem hiding this comment.
I wouldn't mind if you remove this lemma.
| Equivalently (as shown further down the file), `b` does not lie in the open interval `(a, a + p)` | ||
| 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 modeq (p a b : α) : Prop := ∃ z : ℤ, b = a + z • p |
There was a problem hiding this comment.
This definition is probably easiest to use, but would be a departure from nat.modeq, int.modeq, and smodeq which are defined to be equality after the mod (%) operation or equality in the quotient. Is this what @YaelDillies plan to use as the general definition?
There was a problem hiding this comment.
People have complained in the past that int.modeq was defined using % and that nat.modeq wasn't defined in terms of int.modeq. My plan of action is to
- define
add_comm_group.modeq. Easy - drop
int.modeqin favour of it. Probably easy, just have to realign some names and fix a few proofs (most proofs don't use the definition ofint.modeqbecause it is terrible) - redefine
nat.modeqin terms of it. Easy. - replace
add_comm_group.modeqwith notation aroundsmodeq. Potentially hard becauseadd_comm_group.modeqis the special case ofsmodeqwhere the submodule is generated by a single element.
It's likely we can only do step 1 before the port. Also note that if we go through all those steps, the definition of int.modeq will change twice, and hopefully that's okay because as said above almost no proof relies on the defeq because of how useless it is.
Note however that my new definition of add_comm_group.modeq isn't quite the same as the one Eric has here. I instead have
def modeq (p a b : α) : Prop := ∃ z : ℤ, b - a = z • p
which is defeq to p | b - a when p a b : ℤ. You can see my progress on the branch eric-wieser/redef-Imodeq.
There was a problem hiding this comment.
This sounds like a good plan, and your add_comm_group.modeq is also defeq to the proposed new smodeq definition applied to zmultiples, so maybe step 4 won't be hard once we adopt the new smodeq.
For future reference, let me note that smodeq (and add_comm_group.modeq) could be generalized further from add_comm_group to add_group with exactly the same definition, and then it would mean that two elements lie in the same right_coset (to express that two elements lie in the same left coset, we may say their inverses lie in the same right coset), and it could also be to_additive'd from the multiplicative version.
There was a problem hiding this comment.
Oh indeed! Then if @eric-wieser agrees, I suggest we merge eric-wieser/redef-Imodeq into this PR.
There was a problem hiding this comment.
It sounds like you both have stronger opinions on this than me. I propose we either:
- Merge this PR as is, and let @YaelDillies create a follow up from the branch above
- Abandon this PR and let @YaelDillies do the whole thing directly from the branch above
- Abandon this PR and refrain from doing anything until mathlib4
There was a problem hiding this comment.
I'm happy to go with 2 if you're tired of leading the charge.
There was a problem hiding this comment.
@eric-wieser @YaelDillies Does that mean that this PR should now be closed?
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
…dd_comm_group.modeq
|
Subsumed by #18958 |
This redefines it as
∃ z : ℤ, b = a + z • pinstead of∀ z : ℤ, b - z • p ∉ set.Ioo a (a + p)(as requested by @alreadydone), which needs less in the way of typeclass assumptionsadd_comm_group.modeq#18955