Ditch CompleteSemilatticeSup

Stream: mathlib4

[Violeta Hernández]

docs#CompleteSemilatticeInf and docs#CompleteSemilatticeSup are entirely equivalent to docs#CompleteLattice. The former contains the data for the infimum, and the latter contains the data from the maximum, so they're not strictly equivalent from the viewpoint of the typeclass system, but the other half can always be completed from docs#completeLatticeOfCompleteSemilatticeInf or docs#completeLatticeOfCompleteSemilatticeSup, so mathematically neither is stronger than the others.

I believe we should remove CompleteSemilatticeInf and CompleteSemilatticeSup entirely, turning them into two constructors for CompleteLattice. Any objections?

[Eric Wieser]

Is there an argument for keeping them to match the MinimalAxioms types?

[Junyan Xu]

Docstring says:

Note that we rarely use CompleteSemilatticeInf (in fact, any such object is always a CompleteLattice, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.

[Violeta Hernández]

Well, we do have some API stated using CompleteSemilatticeInf, see e.g. docs#sInf_le. My claim is that we should have none.

[Violeta Hernández]

Eric Wieser said:

Is there an argument for keeping them to match the MinimalAxioms types?

What's up with them? I don't really understand their design.

[Junyan Xu]

e.g. docs#sInf_le. My claim is that we should have none.

If we're not removing CompleteSemilatticeInf I don't think we should change the assumption; some automated tool might change it back ...

[Violeta Hernández]

No need for automated tools: #33740

[Yury G. Kudryashov]

Initially, I added one of them as a constructor for CompleteLattice, then @Kim Morrison added these typeclasses in !3#6797

[Eric Wieser]

Violeta Hernández said:

Eric Wieser said:

Is there an argument for keeping them to match the MinimalAxioms types?

What's up with them? I don't really understand their design.

I think it's just a way of making the custom constructor for the real typeclass more convenient, docs#Monoid.ofMinimalAxioms let's you use {} notation to name arguments

[Eric Wieser]

Oh nevermind, we don't have these for algebra, only for order

[Eric Wieser]

Then I agree that the design of these is fishy too

[Violeta Hernández]

Yeah, surely we could remove docs#Order.Frame.MinimalAxioms entirely and replace its functionality with a constructor for docs#Order.Frame, analogously to what docs#Ring.ofMinimalAxioms does currently.

[Yury G. Kudryashov]

I don't think that Order.Frame.MinimalAxioms should be a class.

[Yury G. Kudryashov]

If it's a "named args for a constructor" thing, then it should be a struct, and the constructor should be an abbrev.

[Violeta Hernández]

Order.Frame.MinimalAxioms is just a single axiom on top of CompleteLattice. I don't think it even needs to be a struct.

[Eric Wieser]

Yury G. Kudryashov said:

I don't think that Order.Frame.MinimalAxioms should be a class.

I think it's a class because it extends a class

[Eric Wieser]

I claim that structures extending classes are usually a bad design, even if nothing actually breaks

[Artie Khovanov]

I support this refactor

[Yury G. Kudryashov]

Let's wait for @Kim Morrison who turned a constructor into a class.

[Kim Morrison]

Sorry, it's been a long time. I don't have any attachment to my change.