Why is `Polynomial` noncomputable?

Stream: mathlib4

[Jihoon Hyun]

In Mathlib.Data.Polynomial.Basic, the structure Polynomial is defined in a noncomputable section. Is there any reason for not applying noncomputable for noncomputable types only? Any other building blocks of Polynomial doesn't seem to be noncomputable.

[Anne Baanen]

The reason is that we decided not to care about computability of polynomials when they were defined. Now there is a lot more reason to care about computability but it's going to be a lot of work to do so nicely. See e.g. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Polynomial.20uncomputable

[Anne Baanen]

Here is a wiki page with even more information: https://github.com/leanprover-community/mathlib4/wiki/Computation-models-for-polynomials-and-finitely-supported-functions

[Eric Wieser]

Please add this Zulip thread to the list of Zulip topics on that page :)

[Eric Wieser]

(having a record of this being asked for is helpful in justifying the change in future, if it is ever made)

[Jihoon Hyun]

While staring at the wiki page, I couldn't figure out how de-classified Finsupp, DFinsupp, and DFinsupp' achieve f i (aka p.coeff i) without DecidableEq ι. How can it compute f j if f = single i 1 and i = j but doesn't have DecideableEq ι property?

[Jihoon Hyun]

I'd also like to share my idea of computable Finsupp. Let ι be a type which we can choose one element (if not empty) without classical choose, for example zero. Also let Finsupp ι R contain f which is a finite set of functions from ι to ι, which is likely to be computable. This will require the same restriction as the quotient of inductive type method for operations listed in the table, while not being inductive.

[Eric Wieser]

Jihoon Hyun said:

While staring at the wiki page, I couldn't figure out how de-classified Finsupp, DFinsupp, and DFinsupp' achieve f i (aka p.coeff i) without DecidableEq ι. How can it compute f j if f = single i 1 and i = j but doesn't have DecideableEq ι property?

Because the DecidableEq obligation appeands at f = single i 1 not at f i

[Eric Wieser]

I don't really understand your suggestion (I think it has at least one typo, because you don't mention R in your definition)

[Jihoon Hyun]

Eric Wieser 말함:

Jihoon Hyun said:

While staring at the wiki page, I couldn't figure out how de-classified Finsupp, DFinsupp, and DFinsupp' achieve f i (aka p.coeff i) without DecidableEq ι. How can it compute f j if f = single i 1 and i = j but doesn't have DecideableEq ι property?

Because the DecidableEq obligation appeands at f = single i 1 not at f i

Thank you for the explanation! Then it seems like the deterministic equality checking of index is not an issue when working on f i, right? Why is this the case?

[Jihoon Hyun]

Eric Wieser 말함:

I don't really understand your suggestion (I think it has at least one typo, because you don't mention R in your definition)

I meant that single i r or + in the table doesn't require DecidableEq for both types, while f i requires DecidableEq ι and support needs both DecidableEq ι and DecidableEq R, just like the 'quotient of inductive type'.

I'll explain more about the method. Each element F of Finsupp ι R of mine will hold functions from ι to ι, which denotes an index f 0 for each f in F . single i r is constructible by choosing a singleton set F which contains a function f which maps 0 to i, along with r. + can be lazily operated without comparison on ι. If we don't need to deterministically check for equality as stated above, then it seems like the DecidabeEq ι can also be cancelled out, but for support operation we still need both DecidableEq constraints.

[Junyan Xu]

It's hard to understand your idea by words. I wrote down some possible implementations of Finsupp here (in Lean 3). Can you take a look and how your approach differ, preferably with some actual code?

[Junyan Xu]

If you want to compute with polynomials, there is the polynomial tactic as well as a new approach of mine that works for polynomials over types with decidable equality and computable arithmetic operations, like ℕ, ℤ, and ℚ.

[Jihoon Hyun]

It seems like my idea was not that good after all. I tried creating an equivalence relation on ι -> ι, then noticed that there is a bijection between the created equivalence classes and ι itself, which implies that what I have thought was actually similar to that of DFinsupp.