normed_comm_ring

Stream: general

[Yury G. Kudryashov]

It seems that Lean fails to unify two ways to get ring from normed_comm_ring: normed_comm_ring → comm_ring → ring and normed_comm_ring → normed_ring → ring, see https://github.com/leanprover-community/mathlib/runs/1244482591

[Heather Macbeth]

I'm surprised this wasn't already an issue for two paths from normed_field to ring?

[Yury G. Kudryashov]

While I can use some workaround here (e.g., redo everything in terms of polynomial.eval₂ to drop the commutativity assumption), I wonder if there is some way to actually fix this problem.

[Yury G. Kudryashov]

normed_field extends field using new structure cmd, so it just has to_field. What paths are you talking about?

[Yury G. Kudryashov]

I think that in the case of normed_comm_ring, Lean fails to unify two paths because of some mix of new and old structures.

[Heather Macbeth]

Oh, I see. I don't really know about the old/new structure distinction (past the fact that it exists), it's not possible to use new structures for normed_comm_ring?

[Yury G. Kudryashov]

normed_comm_ring is a new structure but it's impossible to make a new structure extend two structures with competing fields.

[Yury G. Kudryashov]

Because new structure stores to_* fields instead of unpacking all the extended structures.

[Yury G. Kudryashov]

And I don't want to redo the whole algebraic hierarchy based on the new structure cmd right now.

[Yury G. Kudryashov]

And without Lean 4 support for cyclic inheritance.

[Eric Wieser]

Can you just make normed_comm_ring an old structure?

[Yury G. Kudryashov]

This would require making lots of other typeclasses old structures too.

[Yury G. Kudryashov]

And there are no old structures in Lean 4, so I don't think that migrating in this direction is a good idea.

[Patrick Massot]

We will have the option to put back the old structure command. But it won't be there by default.

[Eric Wieser]

old_structure_cmd seems pretty core to the entire algebraic heirarchy - I don't think it's unreasonable to keep using it when building further on top of that.