Minimal axioms for Group, CommRing etc

Stream: maths

[Chris Hughes]

One of the things I'm surprised we don't have currently, is custom constructors for Group, CommRing and Field etc, that only ask for the minimal proof requirements. Is there something I'm missing for why we don't already have this, or should I start making a PR with a bunch of these things?

[Yaël Dillies]

I agree we should have these, although some thought needs to go into what minimal sets of axioms we care about, since there are so many different ones.

[Chris Hughes]

We can have different constructors for the many different ones. I don't see a problem with that.

[Chris Hughes]

I'll start working on it.

[Eric Wieser]

Are you advocating removing the unnecessary data fields (pow, nsmul, natCast etc) too?

[Eric Wieser]

What would be the purpose of such constructors? My general feeling is that they would act as footguns, and in mathlib review we'd just tell people not to use them anyway. I can see they might be useful pedagogically though.

[Chris Hughes]

I think for those, I would advocate a similar approach to the current approach, which is they're filled in by an optParam or whatever it's called.

[Chris Hughes]

Why would we tell people not to use them?

[Chris Hughes]

I think I'm talking mainly about unnecessary proof obligations anyway

[Chris Hughes]

Yaël Dillies said:

I agree we should have these, although some thought needs to go into what minimal sets of axioms we care about, since there are so many different ones.

I could do something weird like asking for (∀ a, a + 0 = a) ∨ (∀ a, 0 + a = a)

[Eric Wieser]

The usual pattern I see is

1. Contributor shows [Ring A] : Ring (MyFoo A)
2. A reviewer comments "isn't [Monoid A] : Monoid (MyFoo A) also true"
3. The Ring instance proof is now mostly just copying the Monoid fields

While the "easy" constructor for Ring might be used in step 1, there'd be no point using it in step 3 since it wouldn't save any work, and would increase the chance of diamonds. The refactor from 1 to 3 is easier if the "easy" constructor never existing, as now the "redudnant" fields cannot just be copied and pasted.

[Patrick Massot]

I agree in principle, although I think that in practice the redundant fields cost very little extra work. And all those simplifications work only for rich structures. In mathlib we often first assume very little assumptions and get a monoid, then add some more assumptions and upgrade to group etc. In that case you don't gain anything because the redundant fields are redundant only for groups, not for monoids.

[Chris Hughes]

I agree that that pattern is common, but I certainly don't think it's the only thing that ever happens. There are some groups that are just groups with some variant being a monoid first.

[Patrick Massot]

And I just saw Eric's message that has some overlap with mine.

[Eric Wieser]

Patrick, I think your explanation was better :)

[Chris Hughes]

For reference, the motivation for me is I'm doing ModelTheory and I'm proving that a Model for the theory of fields is a field. Now I could go and define the Theory of Semirings and so on first, but I'm not sure this is a good idea at this stage for Model Theory, because it's fairly new and untested, and also not an easy thing to get right, so it might require a lot of refactors and building a lot of code about the Model Theory of Semirings that will be unused for a long time seems like not such a good idea.

[Patrick Massot]

Note I was trying to explain why those constructor are less useful than they would appear to be, but I'm not against having them anyway.

[Eric Wieser]

Note in mathlib3 we actually dropped the add_zero and zero_add fields of Ring. They were added back (accidentally?) during the ad-hoc port.

[Chris Hughes]

!4#6173 for a first PR just for groups.

[Julian Külshammer]

If you take seriously the "minimal" part, you should also PR to the Counterexamples folder, examples of things that satisfy all axioms but one (for each axiom).

[Kevin Buzzard]

I certainly made things like the constructor for a group using only the axioms I was taught as an undergraduate (mul_assoc, one_mul and one of the inverse axioms; the one which doesn't make a * b := b and a^-1 := 1 into a group). But I never PRed them because this was before the time that Chris finally got it into my head that PRing was important. I was surprised to find that they didn't seem to come up so much as I would have expected but perhaps the earlier responses on the chat explain this. Also, typically proofs of one_mul and mul_one are easy anyway so it's not too much trouble supplying both.

[Yury G. Kudryashov]

E.g., for cardinals we prove one of mul_add/add_mul using the other one.