ring vs Ring

Stream: mathlib4

[Eric Wieser]

Why do these have different base classes but no porting note? docs4#Ring is

class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

but docs#ring is

class ring (α : Type u) extends add_comm_group_with_one α, monoid α, distrib α

(i.e., skips the zero_mul and mul_zero fields)

[Mario Carneiro]

Narrowed it down to https://github.com/leanprover-community/mathlib4/pull/655/commits/1dbb7fcf2664393981b552effcc1286909082dea by @Ruben Van de Velde ; my guess is that it was copied from the adhoc version

[Chris Hughes]

I think you can get commutativity as well so it could extend add_group instead of add_comm_group. a + b = - a + a + a + b + b - b = - a + (1 + 1) * a + (1 + 1) * b - b =- a + (1 + 1) * (a + b) - b =-a + 1 * (a + b) + 1 * (a + b) - b = b + a

[Eric Wieser]

Right, but you're describing a refactor. I'm asking "why did we refactor in the port?".

[Eric Wieser]

Because now we have these extra zero_mul and mul_zero fields to fill in which mathlib3 provides no proof of

[Ruben Van de Velde]

I don't recall. I'll try to take a look tonight what might have happened

[Eric Wieser]

A reasonable option would be to backport the refactor; I could believe that the new-style structures in Lean4 make the new spelling advantageous

[Yaël Dillies]

That goes against our philosophy not to clutter structures with redundant fields. How does the new spelling make it advantageous? At any rate I wouldn't easily deem it reasonable.

[Eric Wieser]

With new-style structures It means that ring.to_semiring is a projection and doesn't expand to an application of semiring.mk, which is supposedly the whole reason new-style structures all a thing at all

[Ruben Van de Velde]

I started aligning to mathlib3 in mathlib4#1768, but hitting some timeouts I don't have time to diagnose. If anyone feels like looking into them, please go ahead

[Yaël Dillies]

With your explanation, Eric, I think the reasonable solution is to not align. Deep down, this difference is introduced by the way new structures work and backporting will be unpractical because of the lack of structure eta.

[Eric Wieser]

Backporting will be easy, it's just a case of writing the mul_zero and zero_mul proofs

[Yaël Dillies]

Better: Write a constructor to avoid writing them.

[Eric Wieser]

Then you lose the nice {} syntax

[Yaël Dillies]

Then revive #17826 to fill the fields automagically.

[Eric Wieser]

My argument is:

• If we do nothing, people will fill these fields in during porting. This won't be reviewed as thoroughly as in a mathlib3 PR, and we won't be able to estimate the overall impact of the change.
• If we fill those fields in in mathlib3, then we make the porting job easier
• Doing clever tactic stuff is unlikely to translate well to Lean4 anyway

[Yaël Dillies]

But in that case the clever tactic stuff is very lightweight and will be translated to Lean 4 before we merge it.