Single-element structures and type synonyms

Stream: mathlib4

[Wrenna Robson]

Could I ask what the current plans are (if any) for refactors to turn things that were once irreducible type syonyms into one-fieldstructures?

Mathlib.Algebra.Opposites has PreOpposite from which MulOppositeand AddOpposite are defined, but Additive and Multiplicative are very much still type synonyms, and I think from the comments around the necessity for PreOpposite that this is deliberate.

The situation in Order-land confuses me though. For one thing, we seem to have Mathlib.Order.TypeTags (in which WithBot and WithTop are defined). I am not sure what "type tags" is meant to mean here - in Mathlib.Algebra.Group.TypeTags.Basic it refers to Additive and Multiplicative, but unlike with WithBot and WithTop (which actively add an element by defining them both as synonyms of Option) Additive etc. are more what I would think of as a "tag" because they are equivalent to the original type.

Then we have Mathlib.Order.Synonym, which is where type synonyms are defined, apparantly. The documentation implies OrderDual, Lex and Colex are all found here. In fact OrderDual is defined in Mathlib.Order.Basic, I assume for some kind of dependency reason, but it is strange to me to do that there and not define it in Mathlib.Order.Defs, which doesn't to be fair currently exist. All of these I think are defined as type synonyms.

(There is also Mathlib.Algebra.Group.WithOne.Defs in which WithOne and WithZero are both defined - this is quite similar to WithBot and WithTop though.)

I'm asking about this not because I particularly want to push a solution (I do think single-element structures for everything feels most "right" to me but that may not actually be useful in practice), but more that I feel consious that the current situation is a diversity of approaches which are confusingly heterogenous. I would be quite prepared to put some hours in to helping out with or even leading part of any necessary refactor, but currently I don't think I understand what the current consensus is or even if there is one.

[Wrenna Robson]

(I may have missed some examples of this design pattern above - I would appreciate knowing about them as I don't want to miss part of the picture. But I think this is a good slice of the examples I commonly encounter.)

[Wrenna Robson]

It may be most appropriate to write this up as an issue in GitHub and seek consensus there rather than on a Zulip thread - I would also be happy to do that. In general I want to be a good-mannered and productive contributor to Mathlib - it's getting on for six years on and off of being in the Lean community now so I do feel I should "PR responsibly" for sure.

[Wrenna Robson]

Sometimes it feels a bit like I do things the wrong way and get told off without much guidance on how to improve which is why I've been more reticient to contribute to Mathlib in recent times: so I hope this post, at least, is considered productive.

[Junyan Xu]

Personally I don't like single-field structures. (When I see "single-element" I think of subsingletons.) I think they introduce artificial non-defeqs which complicate proofs (need to transport across isomorphism), and are not the right solution to defeq abuse; the solution should be some automation to flag decls whose type make use of non-reducible defeqs (just insert with_reducible and see if they still typecheck?).

[Wrenna Robson]

Yeah, I see that argument. I like the artifical non-defeqs though: I don't think you can separate "defeqs that are good" and "defeqs that are bad" cleanly, certainly.

[Wrenna Robson]

We do certainly use single field structures in at least a handful of instances though, so if we did come to the consensus they weren't the best way to handle it, there would still be stuff to change.

[Snir Broshi]

Doesn't the module system solve defeq abuse since you can remove the @[expose]?

[Wrenna Robson]

Quite possibly! That would be good.

[Violeta Hernández]

I like the idea of single-field structures in principle, but the def-eq (ab)use they inhibit is just far too convenient in my opinion. I recently wrote this file where half of the theorems are proven via OrderDual def-eq shenanigans.

[Violeta Hernández]

@Yaël Dillies who I believe had some strong opinions about this topic.

[Wrenna Robson]

Violeta Hernández said:

I like the idea of single-field structures in principle, but the def-eq (ab)use they inhibit is just far too convenient in my opinion. I recently wrote (this file)[https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/CompleteLattice/PiLex.html] where half of the theorems are proven via OrderDual def-eq shenanigans.

Yeah I mean I think I use it all the time. It's such a pain to work with the dual without it as well. But it does feel odd sometimes.

[Edward van de Meent]

i have to say the only reason that i know why OrderDual hasn't gone the way of the 1-field structure yet, is the fact that OrderDual (WithTop X) = WithBot (OrderDual X) is abused, and fixing these specific occurrences is more tedious than the usual fix of inserting toDual, ofDual, and congrArg in the right places

[Edward van de Meent]

(deleted)

[Edward van de Meent]

and even then, i believe nowadays the duplication should just be fixed by to_dual, no?

[Wrenna Robson]

I was looking at it yesterday (and being frustrated by the fact it's defined in Order. Basic)! I think it would be doable but it might be a little harder than you would think. Also we would probably want to change the definition of OrderDual.toDual and ofDual - currently these are defined as equivs but this isn't consistent with other places where there's a separate equiv function. Or we should change all the other places, idk.

[Violeta Hernández]

A lot of the duplication will be fixed by to_dual, yes. But I don't think it'll solve 100% of all our problems. For instance, I have no idea how I would be able to get it to work with docs#Lex and docs#Colex.