deprecated sub{monoid,group} predicates

Stream: mathlib4

[Johan Commelin]

Jeremy Tan said:

I would have expected #16836 to have been merged by now

Cross-posting a message that I just posted on the PR page:

There's a lot of discussion that happened about these files. I think it is very good that we do something:

• remove them, or
• undeprecate them.

Historically, the structures in these files were classes. And there was consensus that this was not a good design, and hence they were deprecated. Back in the mathlib3 era, Kevin refactored mathlib to make the deprecated classes into structures: https://github.com/leanprover-community/mathlib3/commit/f961b28041ad901e12ff55653c93a640000da4d5#diff-9dfe378e58a7961147b1d523be114d4c149665a6b9cee973d330bfc5057cc710. It is worth taking a moment to look at Kevin's commit message. In particular, he reaches the conclusion that there isn't much harm in deleting these files.

However, we should also consider some past zulip discussions (there might be more):

• https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Submonoids.20containing.20the.20base.2Fcentral.20ring/near/218724723
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deprecated.20is_sub*/near/210452380
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deprecated.20is_sub*/near/210400716

I personally lean towards: undeprecate, move to some appropriate place in the mathlib directory structure, but do not give these a central role in the algebraic APIs.

I think we should have 1 more final zulip discussion about this.

[Violeta Hernández]

If we're talking about uses of IsGroup and friends, I've got one myself. In the proof that nimbers are algebraically closed, you have to reason about certain intervals Iio x of nimbers being closed under addition / multiplication / inverses, and what that entails for x.

[Violeta Hernández]

That being said, the current proof draft just makes these into predicates for Nimber, and it seems to be cleaner. We can even exclude some hypotheses that aren't really needed for the proof, such as 0 being in a group and 1 being in a field.

[Yaël Dillies]

My two cents here is that even if we want these predicates, we should rewrite the API from scratch. The purpose of the files as they currently are is purely archival. So many things have changed since they were written and they have changed so little that I think we should just trash them. To give you an idea, this kind of file would take me one or two hours to write at most, so I don't think we are saving any time by keeping them around.

[Johan Commelin]

I think we are saving one or two hours of Yael-time per file. So we're talking about a full Yael-day. We don't have those in abundant supply...

[Johan Commelin]

Unless you think the current API is really terrible. But from glossing over the files, I think they're not that bad.

[Antoine Chambert-Loir]

And even if yael commits himself to be available 24/7 for writing stuff like this upon request, mathlib should build on something more sustainable.

[Kim Morrison]

I'm inclined to scrap these. They date from before the port, and ever since then have been unused in Mathlib, and sitting in a folder named Deprecated.

[Kim Morrison]

Are there actual users?

[Jeremy Tan]

Not that I know of

[Johan Commelin]

Nope, but that's a bit self-reinforcing.

[Johan Commelin]

It's in a folder named Deprecated. So nobody will use it.

[Jeremy Tan]

Yaël Dillies said:

My two cents here is that even if we want these predicates, we should rewrite the API from scratch. The purpose of the files as they currently are is purely archival. So many things have changed since they were written and they have changed so little that I think we should just trash them. To give you an idea, this kind of file would take me one or two hours to write at most, so I don't think we are saving any time by keeping them around.

You could substitute me in this paragraph if you doubled the times mentioned

[Kim Morrison]

Is anyone proposing that we keep this material in the Deprecated folder?

[Kim Morrison]

Does anyone with a use case want to rewrite them and move them out of Deprecated?

[Kim Morrison]

I think unless there is a specific yes on one of those questions from someone who wants to take ownership, then we should delete.

[Kim Morrison]

Just leaving material in Deprecated for years is not a plan.

[Johan Commelin]

Is it also an option to move them out of Deprecated as is, without rewriting? Because I would happily answer that question with "yes"

[Kim Morrison]

I guess it is. I'm skeptical about (re)introducing multiple ways to talk about the same thing (usual reason, API cost) without stronger evidence that it is really useful.

What if we did something like move it out of Deprecated, but with a module doc that says "Please use this if it is really actually useful to you (maybe some hints about how to determine that). If we find that it is still unused in 6 months, however, we'll deprecate."

[Jeremy Tan]

If some PR really needed this it would have moved the material out of Deprecated itself, but no PR has done so. Thus I believe we have no need to wait any longer to straight-up delete the files

[Kevin Buzzard]

The examples which Johan posted -- it seemed to be that there were easy workarounds given what we have. For example Reid's subsets X n of a group, indexed by the naturals, and his proof by induction that they were all subgroups, could be replaced by defining subgroups G n recursively where G n = X n was rfl.

[Eric Wieser]

Kim Morrison said:

I guess it is. I'm skeptical about (re)introducing multiple ways to talk about the same thing (usual reason, API cost) without stronger evidence that it is really useful.

I think there's a way of doing this with no API cost. If we change to

structure Submonoid where
   carrier : Set M
   isSubmonoid : IsSubmonoid M

then

theorem IsSubmonoid.inter ...
instance : Inf (Submonoid M) := ...

isn't really duplication, since the first theorem would be used to prove the second.

[Kim Morrison]

@Johan Commelin, thoughts here? I remain at "no one is using these, no one is writing a PR to revamp these and start using them, they've been deprecated for a long time ===> delete".

[Johan Commelin]

Yeah, fine. Let's just delete.

[Kim Morrison]

Done.

[Michael Rothgang]

Two tests are failing.

[Kevin Buzzard]

Which PR are we talking about? Several searches have come up with nothing.

[Michael Rothgang]

#16836

[Kevin Buzzard]

Oh! I was expecting a recent one; i had not understood that this was a discussion about an old PR. OK well I guess we just broke some people's projects! But I'm definitely in favour of removing these files. As I said in my PR message when I deprecated them, I was expecting to run into what seemed to be genuine use cases but I never did, really.

[Damiano Testa]

It does not exactly apply to this PR, but there was a recent discussion about how to deprecate an entire file in favour of other files.

[Damiano Testa]

It was more in the context of splitting/renaming files, but if the deprecatedModule machinery were available, it could probably also be repurposed to mitigate the effect of these removals