This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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

• Finsupp
• Polynomial
• MvPolynomial
• Basis

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.
• DFinsupp': A version of DFinsupp that stores a Finset that is a superset.
• 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 table outlines the computational behavior that ι →₀ R could have under these strategies.

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

Recall that Polynomials are ℕ →₀ R with ι = ℕ, so DecidableEq ι is not at all a burden here. MvPolynomials are (σ →₀ ℕ) →₀ R with ι = σ →₀ ℕ, so DecidableEq ι amounts to DecidableEq σ.

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.

Alternatives to computational models

TODO: describe norm_num-style computation.

List of prior Zulip discussions

• 2019-02-24 free_comm_ring: "I agree that mv_polynomial should have decidable_eq removed, but this isn't the only way to achieve that". This talks about the quotient approach a little.
• 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
• 2023-09-21 Computable degree-bound polynomials
• 2023-12-09 Removing classicality from single and update for #evaling fun₀ notation
• 2024-02-10 Using typeclass inference to synthesize computable representations
• 2024-02-20 Why is Polynomial noncomputable?
• 2024-04-26 rfl for finite sets (of Polynomials)

List of relevant PRS

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

I want computable polynomials today!

Wish granted:

import Mathlib

open scoped DirectSum

abbrev CPolynomial (R) [Semiring R] := ⨁ i : ℕ, R
abbrev CPolynomial.X {R} [Semiring R] : CPolynomial R := .single 1 1

unsafe instance {R} [Semiring R] [Repr R] : Repr (CPolynomial R) where
  reprPrec x prec := 
    let l := x.support'.unquot.1.sort (· ≤ ·)
    Std.Format.joinSep (l.map fun
      | 0 => repr (x 0)
      | 1 => f!"{repr (x 1)}*X"
      | i => f!"{repr (x i)}*X^{i}") f!" + "

open CPolynomial

#eval (3*X^2 + 1 : CPolynomial Int)

example :
    ∀ p ∈ ({3*X^2, 2*X^3, 3*X + 1} : Finset (CPolynomial Int)), p ≠ 0 := by
  decide

No, I meant multivariate polynomials

import Mathlib

open scoped DirectSum

abbrev CMvPolynomial (σ R) [DecidableEq σ] [Semiring R] := ⨁ i : (Π₀ i : σ, ℕ), R
abbrev CMvPolynomial.X {σ R} [DecidableEq σ] [Semiring R] (i : σ) : CMvPolynomial σ R := .single (.single i 1) 1

unsafe instance {R} [Semiring R] [DecidableEq σ] [LinearOrder σ] [DecidableLT σ] [Repr σ] [Repr R] : Repr (CMvPolynomial σ R) where
  reprPrec x prec := 
    let l := x.support'.unquot.1.unquot.mergeSort (toLex · < toLex ·)
    Std.Format.joinSep (l.dedup.map fun s =>
        let mon := Std.Format.joinSep (s.support'.unquot.1.sort (· ≤ ·) |>.dedup.map fun i =>
          match s i with
          | 0 => f!""
          | 1 => f!"*(X {repr i})"
          | _ => f!"*(X {repr i})^{s i}") f!""
        f!"{repr (x s)}{mon}") f!" + "

open CMvPolynomial

#eval (3*(X 0)^2 + 1*X 1 : CMvPolynomial (Fin 3) Int)

example :
    ∀ p ∈ ({3*X 0^2, 2*X 1^3, 3*X 2 + 1} : Finset (CMvPolynomial (Fin 3) Int)), p ≠ 0 := by
  decide