Adding Polynomial.fromRoots?

Stream: mathlib4

[metakuntyyy]

I just checked that the Multiset prod paradigm is used somewhat regularly. Does it make sense to introduce a separate definition and rewrite existing theorems using the new definition?

import Mathlib

namespace Polynomial

noncomputable def fromRootMultiset {R: Type*} [CommRing R] (s: Multiset R) : R[X] :=
  (Multiset.map (fun (a : R) => X - C a) s).prod

[Ruben Van de Velde]

Loogle says the pattern occurs 27 times in mathlib; didn't check if there's any false positives

[metakuntyyy]

Is that enough occurences to introduce a new definition?

[metakuntyyy]

Opened #32005. Feedback welcome.

[metakuntyyy]

Does anyone know how I can remove the simp rule I defined from aesop? My build's crashing:

Error: error: Mathlib/Algebra/Polynomial/Factors.lean:215:2: aesop: error in norm simp: Tactic simp failed with a nested error:

[Junyan Xu]

Maybe ofRootMultiset is in better agreement with mathlib convention.

[metakuntyyy]

How can I remove a specific theorem from the simp set for a whole file?

[Ruben Van de Velde]

Is it attribute [-simp] foo?

[metakuntyyy]

Build succeeded, lint failed. I think I did something off, how do I resolve this?

Run cd pr-branch
+ cd pr-branch
+ env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib

Build progress [starting at 19/22]

✔ [19/22] Built Batteries.Data.Array.Basic:c.o (294ms)

✔ [20/22] Built runLinter (856ms)

✔ [21/22] Built runLinter:c.o (561ms)

✔ [22/22] Built runLinter:exe (478ms)

Running linter on specified module: Mathlib
-- Found 2 errors in 276466 declarations (plus 199085 automatically generated ones) in Mathlib with 15 linters

/- The `simpNF` linter reports:

SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.

see note [simp-normal form] for tips how to debug this.

https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Algebra.Polynomial.BigOperators

Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Algebra/Polynomial/BigOperators.lean:272:1: error: @Polynomial.natDegree_multiset_prod_X_sub_C_eq_card Left-hand side simplifies from

(Multiset.map (fun x => Polynomial.X - Polynomial.C x) s).prod.natDegree

to

(Polynomial.fromRootMultiset s).natDegree

using

simp only [*, @Polynomial.fromRootMultiset_eq_map_prod]

Try to change the left-hand side to the simplified term!
-- Mathlib.Algebra.Polynomial.Roots

Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Algebra/Polynomial/Roots.lean:292:1: error: @Polynomial.roots_multiset_prod_X_sub_C simp can prove this:

by simp only [*, @Polynomial.fromRootMultiset_eq_map_prod, @Polynomial.roots_fromRootMultiset]

One of the lemmas above could be a duplicate.

If that's not the case try reordering lemmas or adding @[priority].

Error: Process completed with exit code 1.

[Weiyi Wang]

Because you added @[simp] theorem fromRootMultiset_eq_map_prod, (Multiset.map (fun (a : R) => X - C a) s).prod is no longer a simp-normal form, so any other simp lemma with this in LHS needs to also change to the new simp-normal form fromRootMultiset s

If you don't want to do too much refactor now, perhaps remove @[simp] from fromRootMultiset_eq_map_prod?

[Weiyi Wang]

All the breaking that requires simp [-fromRootMultiset_eq_map_prod] to fix is effectively for the same reason

[Weiyi Wang]

I suspect that there are reasons against this change, though. Let's say I am new to mathlib, and I'd like to loogle Polynomial.natDegree_multiset_prod_X_sub_C_eq_card by guessing its statement. I might search for Multiset.prod, Polynomial.natDegree. It can find the theorem now, but it won't if we switch over to fromRootMultiset that hides the Multiset.prod

[Riccardo Brasca]

I am not totally conviced this is a good idea, I have the impression it just adds an abstraction layer that may be harmful. If in a file this is used a lot it can of course be a notation, and this is most likely a good ideam but a global definition I don't know.

[metakuntyyy]

I think there are quite a lot of good points made. I'm not sure if my idea is good as I never did any such refactor.

Here's my rationale, what I'm working on and why I think a separate definition is warranted.
During my search I needed to prove injectivity of the map that takes a multiset to a polynomial that has as roots this multiset. My first ideas were to find theorems in Polynomial.Roots as I knew that roots gives me a multiset. I could find that roots goes from Polynomials to Multisets but I couldn't find the canonical map that goes from Multiset to Polynomials.

I did however find https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Roots.html#Polynomial.roots_multiset_prod_X_sub_C which is exactly the thing that I needed (modulo it being in a more explicit form).

Now I don't know how to do this refactor, or even if this refactor is good. I don't know the intricacies between simp normal forms. Now when I think about it it makes sense to put this definition in Polynomial.Basic so that it's well documented along other constructions.

What would a local definition look like. In Polynomial.Roots there are 7 occurences. There are 3 more occurences in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/BigOperators.html

I assume there are more occurences in other files.

[Jovan Gerbscheid]

I think to see that this refactor is worthwile, we should replace all occurrences of the pattern (s.map fun a : R => X - C a).prod with Polynomial.ofRootMultiset s and see if it makes the theorems/proofs nicer or not. This will also get rid of the simpNF linter warning, because the simp lemmas will now use Polynomial.ofRootMultiset instead of (s.map fun a : R => X - C a).prod.

[Oliver Nash]

I agree with Jovan here: in order to decide about #32005 we would need to see the proposed refactor in conjunction.

[Oliver Nash]

One way I could see this tipping into useful territory is if the fact that this is a multiplicative morphism comes up enough. This could be expressed as:

def ofMultiset : Multiplicative (Multiset R) →* R[X] where
  toFun s := (s.toAdd.map (fun a ↦ X - C a)).prod
  map_one' := by simp
  map_mul' s y := by simp

but probably it is better to avoid Multiplicative, keep ofMultiset as a raw function, and just have simp lemmas for the map_one and map_mul properties (stated as sending 0 to 1, and + to *).

[Kevin Buzzard]

Note that we have docs#AddChar although I never really know if we should be using it.

[Michael Stoll]

It is used quite a bit by now:

> git grep AddChar | wc -l
387

(and most of it is not from the file that defines docs#AddChar ...)

[metakuntyyy]

Ok, I've completed the refactor ofMultiset #32005.

Does anyone know how to best resolve the linter issues here https://github.com/leanprover-community/mathlib4/actions/runs/19849515472/job/56873327397?

[Jovan Gerbscheid]

I think the linter warning explains itself: ofMultiset_apply is a simp lemma, and it seems you don't want it to be a simp lemma. So don't use @[simps].

[Ruben Van de Velde]

Or @[simps -simp] or whatever the syntax is

[Yaël Dillies]

@[simps -isSimp]

[metakuntyyy]

Ah I see. I have taken the simps annotation from the suggestion from @Oliver Nash . I have resolved the issue by reverting the two previous theorems so that they can keep the simp.

I am surprised how smooth the refactor was. I guess everything is nice if you are refactoring modulo defeq.

[Oliver Nash]

Good work. Glancing briefly now, it looks like using the new definition everywhere mostly creates some extra indirection, and proofs mostly get a bit more awkward. IMHO the new definition is worth adding because it captures the docs#AddChar issue but at the moment using it everywhere doesn't look so attractive.

[metakuntyyy]

I think I have to refactor this due to the simpnf linting issue. I think I can reduce some of those indirections.

[metakuntyyy]

Oliver Nash said:

Good work. Glancing briefly now, it looks like using the new definition everywhere mostly creates some extra indirection, and proofs mostly get a bit more awkward. IMHO the new definition is worth adding because it captures the docs#AddChar issue but at the moment using it everywhere doesn't look so attractive.

I force pushed so I can't reopen the old PR. However I opened #32496 with just the definition and it being AddChar.