Zulip Chat Archive

Stream: mathlib4

Topic: ring vs Ring


Eric Wieser (Jan 22 2023 at 15:44):

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 (Jan 22 2023 at 15:54):

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 (Jan 22 2023 at 16:01):

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 (Jan 22 2023 at 16:05):

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

Eric Wieser (Jan 22 2023 at 16:06):

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 (Jan 22 2023 at 16:11):

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

Eric Wieser (Jan 22 2023 at 17:42):

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 (Jan 22 2023 at 17:52):

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 (Jan 22 2023 at 18:08):

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 (Jan 22 2023 at 19:53):

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 (Jan 22 2023 at 20:00):

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 (Jan 22 2023 at 20:21):

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

Yaël Dillies (Jan 22 2023 at 20:25):

Better: Write a constructor to avoid writing them.

Eric Wieser (Jan 22 2023 at 20:28):

Then you lose the nice {} syntax

Yaël Dillies (Jan 22 2023 at 20:32):

Then revive #17826 to fill the fields automagically.

Eric Wieser (Jan 22 2023 at 20:42):

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 (Jan 22 2023 at 20:46):

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


Last updated: Dec 20 2023 at 11:08 UTC