Field.toSemifield

Stream: mathlib4

[Matthew Ballard]

Currently we have

instance (priority := 100) Field.toSemifield : Semifield K :=
  { ‹Field K›, (inferInstance : Semiring K) with }

which is defeq to

instance (priority := 100) Field.toSemifield : Semifield K :=
  { ‹Field K› with }

What is the intention with throwing in the Semiring instance?

[Eric Wieser]

This was needed until we refactored Ring

[Eric Wieser]

(previously it was missing some axioms that were "obvious")

[Matthew Ballard]

And never got switched?

[Eric Wieser]

I don't think the refactor of ring was deliberate, it was an accident due to an ad-hoc port

[Eric Wieser]

But downstream file wouldn't ever complain if you provided an extra with term like that, so everything was left in

[Matthew Ballard]

They suffer in silence

[Matthew Ballard]

#6686

[Sebastien Gouezel]

You are still using with there. Is it worth building something neater manually, or do you expect that the changes you are trying in core will eventually get something nice automatically?

[Matthew Ballard]

I expect this to be no-op in current mathlib.

For future changes to core, that is not up to me. But the current elaboration of structures using with is a bit of a performance footgun with no benefit I can see at the moment. I don’t think mathlib can tweak its way around it.

One possible heuristic: if a user provides a structure instance that occurs as a parent (or parent of parent…), then they mean for that to used, at least if they have not explicitly specified a field.

I’m trying that out with some other minor tweaks to structure elaboration in #6539. But the problem I ran into was that this current pattern explicitly inserted the extra Semiring for both of these reducing performance in contexts with DivisionRing orField were present.

[Matthew Ballard]

For comparison, #6539 vs #6319. The latter has hand-rolled constructions for one file.

I need to find time to sit down and carefully look at the difference but at a quick glance you get most of the benefits in the global change with the benefit of not touching the existing code.