Refactor polynomials and finsupp

[urkud]

Drawbacks of the current implementation:

1. We have no proof of (P * Q) A = P A * Q A if P, Q are polynomials, and A is a matrix. At least, not in data/polynomial.
2. While finsupp pretends to be a function, actually it is a monoid algebra.
   For f g : α →?? β with anything in place of ?? I'd expect f * g to be the pointwise multiplication.
3. Polynomial addition / multiplication is slow.
4. It's hard to define new types of pseudo-polynomials. E.g., in ODE people need to work with ∑ e^{λ_k t} P_k(t).

Proposed changes

Mathematically visible

• Possibly (not necessarily) implement finsupp on top of dfinsupp.
• Redefine has_mul on finsupp to the pointwise multiplication.
• Define monoid_algebra R M := finsupp M R with multiplication from the old finsupp.
• Define aeval for non-commutative algebras (e.g., endomorphisms of a vector space).
• Drop eval₂ or redefine it in terms of aeval with an ad-hoc of_hom algebra structure .

Improving computation

It might make sense to turn finsupp or monoid_algebra into a structure that takes some optional arguments (and propositions stating that they are equal to default implementations), and uses them to speed up computation. Currently I don't know what arguments would make sense.

Another approach is to have Based on comments below, those who want fast computation should write a custom structure that works fast for their use case, and define a ring_equiv between monoid_algebra R (multiplicative nat) and this structure.

[ChrisHughes24]

All of these changes seem like good ideas to me.

With regards to computation speed, I'm usually not in favour of sacrificing ease of proof for faster computation. There's no such thing as the fastest implementation of polynomials over an arbitrary ring, and preserving computability often requires decidable_eq assumptions which can be annoying especially when they are so rarely actually used to compute. As long as there is no loss of ease of proof then there's no objection to a faster implementation, it can be useful to have a moderately fast version for a few computations in proofs.

[urkud]

I guess, we shouldn't try to improve computation speed now. Probably it's better to wait for #408 / #1868, then use different implementation for proofs and computations.

[kbuzzard]

Just to expand on something which probably most people already know about computation speed: as Chris says, there's no right decision for an implementation if "you want speed". I've used (unverified) computer algebra systems in the past for manipulating large matrices, and even though they might pretend there is one constructor for a matrix, there have been flags which the user can set when constructing a matrix; e.g. flag=default does one thing, and flag=sparse does another; algorithms for manipulating the matrices depend on how they're flagged, and the idea is that the power user who cares about speed is supposed to know the flags and choose appropriately. I guess @urkud is envisaging an analogous situation here, where we reason about polynomials as efficiently as we can, and if people actually want to use them to do calculations then perhaps other more efficient implementations can be written later (e.g. after Lean 4) and then glued to our inefficient-for-calculations-but-efficient-for-reasoning implementations. It's like nat v num. Sorry to spell out something which is already blindingly obvious to the CS people. Sparse polynomials are a thing, and I see little point in sweating on an attempt at a speedy implementation when it's clear that you can't please all the people all the time.

[urkud]

@kbuzzard Updated main description.

[semorrison]

There's just been some brief discussion on Zulip. I think the consensus there is:

• the pointwise structure on finsupp is not particularly useful, as it's not unital (perhaps we can return to this if someone gets interested in non-unital rings...)
• we should change the current definition of the convolution multiplication, so that it requires a multiplicative monoid, rather than the current additive one
• this will allow us to define group rings/algebras (in fact, we'll already have them)
• we'll need to change polynomial to finsupp (multiplicative nat)
• and similarly for mv_polynomial

[jcommelin]

Still, defining a wrapper type monoid_algebra seems useful. If only for readability.

[urkud]

* the pointwise structure on `finsupp` is not particularly useful, as it's not unital (perhaps we can return to this if someone gets interested in non-unital rings...)

Then I'd rename finsupp to something else, e.g., monoid_algebra.

[semorrison]

I'm working on this now. I've added add_monoid_algebra (for polynomial like things) and monoid_algebra (for group ring like things), both of which are definitionally equal to finsupp.

finsupp doesn't get given any multiplication at all, and these ones receive appropriate variations of the convolution product.

It mostly seems to work, so I'll PR soon.

[semorrison]

@urkud, it's possible that the "refactor" parts of this issue are now done. (I think we decided not to switch to dfinsupp for now.)

Shall we close this and make separate ones for:

• (P * Q) A = P A * Q A
• define aeval for noncommutative algebras
• drop aeval₂