Stating theorems in terms of degree vs natDegree

Stream: mathlib4

[Thomas Browning]

Many theorems about polynomials can be stated equally well in terms of degree or natDegree (e.g., a theorem with assumption deg ≤ 1. In #32103, @Anne Baanen suggested that both version be kept (https://github.com/leanprover-community/mathlib4/pull/32103#discussion_r2569201618), but on #34656, @Violeta Hernández rightfully points out that keeping around two versions of every such lemma is a lot of duplication (https://github.com/leanprover-community/mathlib4/pull/34656#discussion_r2750133092).

Is there a preferred option, or should both be kept?

[Thomas Browning]

/poll Here's an informal poll to gague opinion:
Keep degree variant
Keep natDegree variant
Keep both

[Thomas Browning]

If we do decide to keep both, then there's the further question of what to do about lemmas that lean one way or the other. E.g., a deg = 0 hypothesis is best stated in terms of natDegree for maximum generality.

[Violeta Hernández]

degree carries more useful information than natDegree does. Saying that natDegree p = n really means that either the degree of p is n, or n = 0 and p is the zero polynomial. So I believe we should prefer degree everywhere, unless we legitimately need a natural number in order to state a theorem (as in docs#Polynomial.leadingCoeff_comp, to give an example).

[Snir Broshi]

Thomas Browning said:

E.g., a deg = 0 hypothesis is best stated in terms of natDegree for maximum generality.

For this specific question I guess p.degree ≤ 0 is a good replacement for p.natDegree = 0, no need to use natDegree here

[Kevin Buzzard]

I think it's naive to say "we should prefer degree everywhere". I've seen plenty of situations where natDegree made life easier (that's why it's there in the first place!) and I think that having two versions of every lemma makes our formalizing lives easier. We have two definitions and we should have lots of API for both, simply because we should have lots of API for every definition we have, that's a basic principle which mathlib has been built on from the start.

[Violeta Hernández]

I'm not arguing against natDegree here. But I do believe that instead of having N many theorems which only differ in a single hypothesis e.g. 0 < p.degree vs 0 < p.natDegree, we should choose one and use docs#Polynomial.natDegree_pos_iff_degree_pos when we have the other hypothesis.

[Kevin Buzzard]

I think that saying "we should remove API from a definition" is a retrograde step. More API makes formalisation easier. "We should remove a theorem and make the user figure out how to prove it themselves (remark: I know how to do this exercise myself)" is something which I think you'll find it very hard to sell.

[Violeta Hernández]

If discoverability is a problem, we could take the more extreme approach of making 0 < p.degree the simp-normal form of 0 < p.natDegree. Then the user only needs to type by simpa.

[Kevin Buzzard]

I think that this also will cause problems. If you are doing a calculation in nats with p.natDegree embedded in the term (which definitely happens), then you don't want 0 < p.natDegree normalised to something else not mentioning natDegree because this will break things like linarith.

I feel like that your argument "it's code duplication so it's bad" can be applied to essentially any declaration which is easily built from an older definition, followed by API for the new declaration which is built from the old one. But that's the mathlib way.

[Yury G. Kudryashov]

Note that the vote above is not binding, because it's a responsibility of the maintainers team to make decisions like this. If someone will want to start a big refactor based on the vote, then the maintainers team should agree on this first.

[Yury G. Kudryashov]

E.g., we have Set.encard and Set.ncard which is just (Set.encard s).toNat. Moreover, they're just (Cardinal.mk s).toENat/(Cardinal.mk s).toNat, but we have APIs for these definitions anyway.

[Violeta Hernández]

Again, I'm not arguing for removing natDegree or its API. I'm arguing that, if we have some condition in a larger theorem that can be equivalently stated using degree or natDegree, then we should just choose one, rather than having both variants.

[Violeta Hernández]

I believe there's precedent for this. For instance, we generally prefer to state theorems about non-zero naturals using n ≠ 0 rather than 0 < n.

[Yury G. Kudryashov]

How large is the theorem?

[Yury G. Kudryashov]

One difference between degree/natDegree and your example is that the terms live in different types.

[Violeta Hernández]

The theorem that sparked this discussion is docs#Polynomial.exists_irreducible_of_degree_pos.

[Thomas Browning]

Violeta Hernández said:

I believe there's precedent for this. For instance, we generally prefer to state theorems about non-zero naturals using n ≠ 0 rather than 0 < n.

In this case, you can get from 0 < n to n ≠ 0 by appending .ne', but converting between degree and natDegree is a little more painful.

[Violeta Hernández]

Converting from degree to natDegree is easier than converting from natDegree to degree, in my experience. So I think the same reasoning applies.

[Violeta Hernández]

The value of degree entirely characterizes the value of natDegree, but not the other way around.

[Yury G. Kudryashov]

Same applies to Set.encard vs Set.ncard. Of course, one difference is that ENat.toNat is not a monotone map.

[Violeta Hernández]

Well, if we had multiple theorems in Mathlib that were duplicated except one had a hypothesis s.encard = 1 but the other had s.ncard = 1, I'd probably be making a thread about that as well.

[Riccardo Brasca]

In my opinion duplication in basic theorem is fine, but I agree that having both Polynomial.exists_irreducible_of_degree_pos and Polynomial.exists_irreducible_of_natDegree_pos is strange.

[Riccardo Brasca]

Is it unreasonable to add a couple of lemma to grind (or some other tactic) to make it able to prove 0 < p.degree having 0 < p.natDegree and similar stuff?

[Anne Baanen]

Perhaps even a custom @[grind] set (enabled by default) so we can write theorem (hf : 0 < f.degree := by assumption_mod_unbot) or similar?

[Kevin Buzzard]

It's a shame that we can't have dot notation as a slick way of switching from one to the other (like we do to switch between n \not= 0 and 0<n in nat)

[Violeta Hernández]

We already have a compute_degree tactic, maybe we could beef it up so it can do conversions like these?

[Thomas Browning]

Kevin Buzzard said:

It's a shame that we can't have dot notation as a slick way of switching from one to the other (like we do to switch between n \not= 0 and 0<n in nat)

In theory you could define LT.lt.degree_pos and LT.lt.natDegree_pos in the root namespace :slight_smile:

[Artie Khovanov]

In my experience the natDegree versions are much more useful. In fact, I was planning to PR a bunch of them in from my project! It's very annoying to constantly rewrite between degree and natDegree. The issue is that there isn't a clear normal form.

[Violeta Hernández]

I agree that the rewrite is annoying, and for that same reason I wanted to PR more lemmas on degree...

I'd rather just decide on one or another rather than be playing tug of war.

[Artie Khovanov]

I get the point that moving from degree to natDegree is easier than the other way around. So maybe: natDegree in assumptions, degree in conclusions? Where it makes sense, of course: sometimes you have to use degree in both.

[Kevin Buzzard]

What's wrong with "lots of API for both"? It just seems to me like the simplest solution, easiest for other people to use etc.

[Artie Khovanov]

From my POV, it's annoying to maintain and entails a lot of duplication. Also sometimes people won't add one or the other version, so you have to go from natDegree to degree a lot. However I worry the alternative is too restrictive.

[Artie Khovanov]

The advantage of writing everything using natDegree is that it's easy to chain facts with lia. Working with WithBot is pain. Same reason we use finrank, fincard, etc.

[Artie Khovanov]

I have the following lemmas in my project; they are very convenient.

-- Mathlib.Algebra.Polynomial.Degree.Definitions
theorem Polynomial.degree_eq_one_iff_natDegree_eq_one
    {R : Type*} [Semiring R] {p : Polynomial R} :
    p.degree = 1 ↔ p.natDegree = 1 :=
  degree_eq_iff_natDegree_eq_of_pos (Nat.zero_lt_one)

-- Mathlib.Algebra.Polynomial.Degree.Definitions
theorem Polynomial.degree_eq_iff_natDegree_eq_of_atLeastTwo
    {R : Type*} [Semiring R] {p : Polynomial R} {n : ℕ} [Nat.AtLeastTwo n] :
    p.degree = n ↔ p.natDegree = n :=
  degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_neZero n)

[Violeta Hernández]

Artie Khovanov said:

The advantage of writing everything using natDegree is that it's easy to chain facts with lia. Working with WithBot is pain. Same reason we use finrank, fincard, etc.

Perhaps that points to a lack of API/automation, rather than something to be swept under the rug.

Artie Khovanov said:

I have the following lemmas in my project; they are very convenient.

Case in point, huh

[Artie Khovanov]

Violeta Hernández said:

Perhaps that points to a lack of API/automation, rather than something to be swept under the rug.

Maybe, but these are pretty stable patterns by now. I would lean towards natDegree everywhere unless necessary, acknowledging it's the more annoying direction to transfer in.

[Kevin Buzzard]

Artie Khovanov said:

From my POV, it's annoying to maintain and entails a lot of duplication.

Yup. But it makes users happier, because the exact lemma they want is just there.

[Violeta Hernández]

What I argue is that if we had a canonical way of writing this down, then the users would be happy, because the canonical form would just be there, rather than them having to hope someone remembered to add both variants.

[Kevin Buzzard]

What I am concerned about is that the amount of times degree and natDegree are used in general is going to be a lot more than the amount of times that you have the specific hypothesis h : 0 < f.degree or h : 0 < f.natDegree. My experience with using these types is that for a typical argument (which may be long) one choice of degree function is often better than the other, so you make that choice (perhaps even in the statement of the result) at the beginning and then run the entire argument through with that choice, and then prove the other variant in 2 lines by reducing one choice of degree to the other. This idea that for some specific arguments we want the library to force you to use one of the choices sounds to me like it is going to degrade that user experience, and the way to keep/enhance that experience is code duplication.

[Jireh Loreaux]

I have no dog in this fight as this isn't my end of the library, but I suspect we indeed want some small tactic. However, I'm also not terribly opposed to living with the duplication; but that duplication is also easier to maintain with attributes that autogenerate the other version (using this small tactic).

In short, I think there is some useful automation missing, regardless of which approach we eventually decide upon.

[Violeta Hernández]

I can agree with the centrist position. It's definitely too soon to do any major refactoring one way or the other.

As for the PR #34656 that started this. Can we at least agree on removing docs#Polynomial.exists_irreducible_of_natDegree_ne_zero in favor of docs#Polynomial.exists_irreducible_of_natDegree_pos ? Converting n ≠ 0 to 0 < n for n : ℕ is entirely trivial.

[Snir Broshi]

Is something like this possible?

@[to_unbot] -- magic ✨
theorem Splits.comp_of_degree_le_one {f g : R[X]} (hf : f.Splits) (hg : g.degree ≤ 1) :
    (f.comp g).Splits := ...

That won't work for everything, e.g. a statement with a degree = 0 hypothesis can't be translated to natDegree = 0, but maybe the translation macro can try calling grind to translate?

[Snir Broshi]

Violeta Hernández said:

Can we at least agree on removing docs#Polynomial.exists_irreducible_of_natDegree_ne_zero in favor of docs#Polynomial.exists_irreducible_of_natDegree_pos ?

I prefer the other way around, n ≠ 0 everywhere. I also remember seeing a PR that replaced a bunch of 0 < n with n ≠ 0, but idk how to find it.
Edit: #33131 #29988 #27647

[Aaron Liu]

We prefer n ≠ 0 in hypotheses and 0 < n in conclusions of theorems

[Snir Broshi]

There's also the ≠ 0 vs NeZero duplication :sweat_smile:
docs#ArithmeticFunction.carmichael_eq_exponent vs docs#ArithmeticFunction.carmichael_eq_exponent'

[Violeta Hernández]

Oh yeah sorry, we should do this the other way around. Deprecate docs#Polynomial.exists_irreducible_of_natDegree_pos in favor of docs#Polynomial.exists_irreducible_of_natDegree_ne_zero.

[Kevin Buzzard]

The "n ≠ 0 in hypotheses and 0 < n in conclusions" rule was made before the dot-notation theorems needed to make it trivial to convert between them were added, and nowadays I am not entirely clear about the logic of this rule.

[Edward van de Meent]

(how does one convert from n ≠ 0 to 0 < n using dot notation?)

[Violeta Hernández]

I wouldn't be opposed to adding NE.ne.pos as an alias for the converse of docs#pos_iff_ne_zero

[Violeta Hernández]

works for ordinals works for me

[Edward van de Meent]

you mean docs#NE.ne.pos ? i don't think that would work with dot notation though?

[Violeta Hernández]

This is news to me

[Aaron Liu]

that should probably be Ne.pos

[Aaron Liu]

since the declaration is called docs#Ne

[Edward van de Meent]

indeed, Ne is not a notation class like LT and the like

[Violeta Hernández]

Yikes, I hope someone gets fired for that blunder
(It was me, I added this a year ago...)

[Edward van de Meent]

i suppose i personally was surprised by the fact there's a nontrivial set of classes which allows one to conclude this implication

[Violeta Hernández]

I've been wishing for a ⊥ = 0 typeclass for a long time, but yeah canonically ordered addition is the next best thing