conflicting simp-normal form: bot vs 0

Stream: mathlib4

[Floris van Doorn]

The following innocuous-looking code results in a maximum recursion depth being reached.

import Mathlib

example {R : Type*} [CommRing R] [IsDomain R] [ValuationRing R] (I : Ideal R) : I = ⊥ := by
  classical
  simp

The issue is that docs#Submodule.zero_eq_bot and docs#bot_eq_zero' have conflicting simp-normal forms, and docs#ValuationRing.instLinearOrderIdealOfDecidableLE is happy to provide the required linear-order instance (assuming some decidability instance, which is why classical is necessary).

This seems bad, and presumably a consistent simp-normal form should be chosen.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib3/pull/14553 added docs#bot_eq_zero' and there's a discussion in the PR about this design decision (and in particular about the disadvantage of it not being a simp lemma).

[Kevin Buzzard]

zero_eq_bot is back in the dark ages (2018) where we were allowed +500 line PRs: https://github.com/leanprover-community/mathlib3/pull/462 . Basically the simp attribute has been there forever.

[Floris van Doorn]

To what extent is ⊥ the preferred spelling of the zero ideal? Would it be feasible to change the simp-normal form to 0, so that it's consistent with the more general case of linear orders?

[Artie Khovanov]

The bottom submodule, subring, submodule etc is spelled ⊥ everywhere afaik. It would be a big refactor.
On the merits themselves, I'd support it, because it matches pen and paper notation.

[Floris van Doorn]

I guess one small downside of changing it, is that currently we consistently(?) use ⊥ for all minimal substructures, and after this change we use 0 for some and ⊥ for others...

[Floris van Doorn]

Another option would be to not have docs#ValuationRing.instLinearOrderIdealOfDecidableLE as an instance. The decidability of that instance already disables it most of the time (which is presumably why this hasn't been an issue that often so far)

This is quite far outside my area, so I'll let others decide what the best way to solve/work around this is

(cc @María Inés de Frutos Fernández @Filippo A. E. Nuccio @Adam Topaz to ping some of the people for whom this might be relevant)

[Violeta Hernández]

Floris van Doorn said:

To what extent is ⊥ the preferred spelling of the zero ideal? Would it be feasible to change the simp-normal form to 0, so that it's consistent with the more general case of linear orders?

At some point in the past I tried making a typeclass for stating ⊥ = 0 (before we had docs#CanonicallyOrderedAdd automatically providing this for docs#Ordinal) and I found that this was the one place in the library where we wanted the opposite simp normal form.

[Violeta Hernández]

On the other hand, it'd be kind of weird to write 0 for the bottom ideal and ⊤ for the top ideal. So if we are going to change something here I believe we should be consistent and also set ⊤ = 1 as a normal form.

[Kevin Buzzard]

I think that 1 is a confusing name for the top ideal in the sense that mathematicians could be confused by it. I'd be happy to consistently call the zero ideal bot even though it's often called zero in the literature. We use bot for plenty of other things which mathematicians would call zero.

[Patrick Massot]

I denote the top ideal by 1 in my algebra lectures since it is neutral for multiplication.

[Kevin Buzzard]

Yeah it's pretty clear what it must mean if you think about it -- it's the ideal generated by 1 just like 0 is the ideal generated by 0. I'm just saying that it's I think far less common to denote the top ideal of R by 1 when you can just denote it by R (on the blackboard).

[Patrick Massot]

To be honest I probably used R before getting infected.

[Filippo A. E. Nuccio]

Floris van Doorn said:

I guess one small downside of changing it, is that currently we consistently(?) use ⊥ for all minimal substructures, and after this change we use 0 for some and ⊥ for others...

I have always been happy with 0 = ⊥ being simp but thinking about it I'd be happy to revert it to 0; this would match our preference for 0 as the normal form of the bottom element for linear orders. So, we would end up using ⊥ for all minimal structures in general lattices, and 0 for all minimal structures in linear orders (like ideals).

[Patrick Massot]

One argument against this is that for ideals it would look weird to use 0 but not 1 while for most other cases the 1 would be meaningless.

[Filippo A. E. Nuccio]

Well, but 1 has no special meaning from the lattice point of view.

[Filippo A. E. Nuccio]

Or perhaps I don't see exactly your point, @Patrick Massot : are you suggesting that we make ⊤ = 1 a simp lemma (or rather: suggesting that if we make ⊥ = 0 simp, then we should also do the same for ⊤ = 1 and this looks weird?)

[Patrick Massot]

Precisely I say that if we want to be consistent within ideal theory then we should either use ⊥ and ⊤ or 0 and 1. But if we choose the second option then on a larger scale consistency would require to use 0 also for other submodules say, and there we would have 0 and ⊤ which looks inconsistent.

[Filippo A. E. Nuccio]

Athough I understand your point, I'm not sure that for consistency we need to mark ⊤ = 1 as a simp lemma. Since ideals are implemented as submodules, and the 1 notation only makes sense for ideals and not for submodules, I feel that the ⊤ = 1 equality is more of an accident that something to be recorded.

[Filippo A. E. Nuccio]

(and I promise I would never tell something of the sort to my students :smirk: )

[Patrick Massot]

I’m not sure I understand which one you wouldn’t tell students, is it ⊤ or 1?

[Filippo A. E. Nuccio]

I wouldn't tell students that the equality ⊤ = 1 is an accident (which is my argument for not marking it as simp although I would mark ⊥ = 0 as simp)

[Jireh Loreaux]

I claim that we should keep ⊥ as the simp normal form even for Ideal R, because the lattice structure is more frequently used than the semiring structure. It's possible that I'm showing my bias here as someone who doesn't work in algebra. :shrug:

[Filippo A. E. Nuccio]

I think that the semiring structure is seldom used (although all the time in algebraic number theory), but the monoid one is quite common.

[Riccardo Brasca]

Something to keep in mind is that, even in number theory part of mathlib, currently most of results about ideals are stated (I think) using ⊥ (probably exactly because it is the simp normal form).

[Riccardo Brasca]

Mathlib.NumberTheory.RamificationInertia.Basic for a random example

[Filippo A. E. Nuccio]

Well, it depends on what you call "the" simp normal form.

[Filippo A. E. Nuccio]

(As said, having worked extensively with this part of the library, I initially believed that ⊥ was actually better, but given that we use different conventions for linear orders or for arbitrary lattices, I'm beginning to doubt)

[Riccardo Brasca]

I don't have strong opinions, what I mean is that currently we have tons of declarations having the assumption I ≠ ⊥. If we decide we prefer 0 it would make sense to try to modify all these assumptions.

[Patrick Massot]

My favorite example is still https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/C09_Groups_and_Rings/solutions/Solutions_S02_Rings.lean#L36-L50 that really uses the semi-ring structure.

[Kevin Buzzard]

I think I'd also vote for bot as the simp normal form always. One could even argue to mathematicians that "0" is not the correct name for the zero ideal because it's actually {0}.

[Johan Commelin]

Kevin Buzzard said:

because it's actually {0}.

Also known as 1 :rofl:

[Edward van de Meent]

(deleted)

[Filippo A. E. Nuccio]

Kevin Buzzard said:

I think I'd also vote for bot as the simp normal form always. One could even argue to mathematicians that "0" is not the correct name for the zero ideal because it's actually {0}.

By "always" do you mean also in linear orders or only for ideals?

[Kevin Buzzard]

Oh I don't think I want simp to simplify 0 to bot in the naturals! I think I must mean "just de-simp bot_eq_zero'"

[Filippo A. E. Nuccio]

Yes, I imagined... :slight_smile: But then the naturals end up with a bot that does not simplify to 0.