Computation models for polynomials and finitely supported functions

Today, MvPolynomial and Polynomial are both implemented in terms of Finsupp. As a result, all of:

• Finsupp
• Polynomial
• MvPolynomial

are largely noncomputable.

Possible designs for a more computable Finsupp

Possible designs include:

• De-classicalized Finsupp: promote any Classical.decEq terms to typeclass parameters. As a reminder, this stores the exact Finset of non-zero values.
• DFinsupp: we already have a working model here. This stores a Multiset that is a superset of all the non-zero values
• Quotient of generators: an approach similar to FreeAlgebra. This could represent 1 + 3x^2 as add (monomial 0 1) (monomial 2 3) and quotient by algebraic rules (which is what FreeAlgebra does)

The following outlines the computational behavior that ι →₀ R could have under these strategies

Operation	De-classicalized Finsupp	DFinsupp	Quotient of inductive type
f i (aka p.coeff i)	✓	✓	DecidableEq ι
single i r (aka X)	DecidableEq ι DecidableEq R	DecidableEq ι	✓
support	✓	DecidableEq R	DecidableEq ι DecidableEq R
+	DecidableEq ι DecidableEq R	✓	✓

List of prior Zulip discussions

• #5942 Add a DecidableEq instance for Polynomial