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.

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	✓	✓

DFinsupp has the nice property of matching the computation model of Pi (via Pi.single, Function.support, and the usual arithmetic). Algorithmically though it is inefficient as the preSupport set grows with each operation.

List of prior Zulip discussions

• 2019-08-14 timeout when working with ideal of polynomial ring: this thread mentions the main attempt to remove decidable_eq, but doesn't really justify the reason to.
• 2022-08-14 nonconstructive polynomials
• 2023-06-04 Making a computable version of MvPolynomial.monomial
• #5942 Add a DecidableEq instance for Polynomial

List of relevant PRS

• chore(data/mv_polynomial): use classical logic
• https://github.com/leanprover-community/mathlib/pull/1890