Removing classicality from `Finsupp.single` and `Finsupp....

Stream: mathlib4

[Thomas Murrills]

I noticed that as-is you can’t #eval code involving finitely supported functions defined using the nice fun₀ notation—which is counterintuitive, as all of the data is finite.

The issue is just that we use classicality to get decidable equality on the domain and codomain types. Would it be reasonable to demand DecidableEq instances in single and update, and then turn on classicality when necessary to supply those instances?

(Or is this not how it works? I’m making some assumptions; I haven’t worked much with classicality in mathlib.)

[Eric Wieser]

I already have an open PR attempting to do this

[Damiano Testa]

I had the impression that DFinsupp is the decidable one though, right?

[Eric Wieser]

But in the short term, the answer is "use DFinsupp"

[Eric Wieser]

Yes, but that's not what the D is supposed to mean

[Damiano Testa]

Although, as far as I understand D is for dependent.

[Damiano Testa]

Eric, we seem to have crossed messages!

[Eric Wieser]

See also https://github.com/leanprover-community/mathlib4/wiki/Computation-models-for-polynomials-and-finitely-supported-functions

[Thomas Murrills]

Would using DFinsupp require changing my types everywhere? If so I might just hand-roll decidable versions of single and update and override the macro in the meantime; it’s just scratch work, and I don’t plan on PRing anything in the short term. :)

[Eric Wieser]

Yes, it not only means adjusting your types but also defining a dfinsupp version of the syntax!

[Eric Wieser]

Though it would be cool to have a dfinsupp version anyway

[Eric Wieser]

Especially if we can use one syntax, and have it use the expected type to disambiguate

[Eric Wieser]

Eric Wieser said:

I already have an open PR attempting to do this

#6317, though it does not pass CI

[Eric Wieser]

Ah, this doesn't really solve the problem, as it still remains non-computable

[Eric Wieser]

(because it only adds DecidableEq ι not DecidableEq α)

[Thomas Murrills]

But it’s halfway there! :)

[Eric Wieser]

It has the merit of doing the half of the refactor that is shared between your proposal and replacing finsupp with an alias for dfinsupp

[Eric Wieser]

Where the second halves of those refsctors diverge

[Eric Wieser]

(also, please could you add this thread to the list of threads on the wiki page I link above?)

[Thomas Murrills]

(Done—had to run right as that message came in :P)