Coherent approach to one-field structures.

Stream: mathlib4

[Wrenna Robson]

Lately I've been seeing (and participated in myself) a few efforts towards turning some semireducible type synonyms into one-element structures, to avoid defeq abuse and the like.

The use case for this basically is when you have some type T and want to define a one-field structure, that field having the type T, in order to represent "T, in a new context" - you want to attach a different set of instances, normally.

It occurs to me that when you make such a type you often then have a lot of boilerplate work that you need to do establishing the API for this pseudo-type synonym. In an ideal world this would always be the same API, or at least consistent between them.

I'm no metaprogrammer, but surely something could be done in the vein of simps in order to auto-generate all the necessary API for these types. Perhaps this is even already possibly with tools like deriving, but that generates instances, rather than associated to/of functions or the like.

What do people think? Is there any usefulness in creating an automated "one-field structure API maker"? What are the pitfalls and problems?

[Kyle Miller]

Could you expand on what boilerplate you would expect to be generated?

[Wrenna Robson]

At minimum I guess the relevant maps to/from the wrapper to the original type, and the related Equiv.

[Wrenna Robson]

I'd also like to be able to say "import this, this and this instances unchanged", kind of thing.

[Eric Wieser]

A common requirement is "copy across all the additive structure, but let me define a new multiplication"

[Wrenna Robson]

Right.

[Wrenna Robson]

And obviously that's case by case so you need to have a system for that.

[Eric Wieser]

Having a "transport this instance and everything under it" approach would be close to what we need

[Eric Wieser]

So transporting AddCommGroup also creates the required [AddSemigroup X] : AddSemigroup (Wrapper X) instance

[Wrenna Robson]

I noticed by the way, there's good machinery for using an Equiv to transport the algebra hierarchy but that doesn't seem to exist as much for the order hierarchy.

[Eric Wieser]

You could also see this happening as part of typeclass search by having an IsAddWrapper Wrapper "tag" typeclass, though that probably runs into quantifier issues, and maybe has more of a runtime cost.

[Eric Wieser]

Wrenna Robson said:

I noticed by the way, there's good machinery for using an Equiv to transport the algebra hierarchy but that doesn't seem to exist as much for the order hierarchy.

I contend that this machinery is in fact not particularly good, and is merely extant

[Eric Wieser]

The "good" machinery is the docs#Function.Injective.group family

[Wrenna Robson]

OK, that's fair. Yael is currently improving it a little by making it all not be in one file at least.

[Eric Wieser]

Yes, I hope to find time to finish reviewing that PR on the next few days

[Wrenna Robson]

Still, I couldn't find a docs#Function.injective.completeSemilatticeInf, for instance.

[Yaël Dillies]

Why care about docs#CompleteSemilatticeInf ?

[Wrenna Robson]

Yes that's a fair question.

[Wrenna Robson]

I was in a weird case where I had two order-isomorphic structures and it was easy to prove one was a CompleteSemilatticeInf and one was a CompleteSemilatticeSup. And I wanted to say "these are both complete lattices, and the "hard" instances arise by transporting over the easy ones from the other structure via the order isomorphism".

[Wrenna Robson]

That feels like a pretty rare case:)

[Wrenna Robson]

I'm never sure if it's ever correct to use CompleteSemilatticeInf though.

[Wrenna Robson]

I would like to be able to transport a min or max using an order isomorphism though! And if that exists I couldn't find it.