Computable/decidable Finsupp?

Stream: mathlib4

[lyphyser]

Currently Finsupp is unnecessarily marked noncomputable and uses classical instead of DecidableEq in the core definitions (but with DecidableEq also sprinkled around other parts).

This creates the problem that things do not reduce as they get stuck on Classical.decEq and it isn't possible to use Finsupp in programs despite the fact that it's obviously a perfectly computable notion.

Is there any plan to fix it? Would contributions be welcome?

I started doing it but unfortunately a lot of things depend on it so it's a significant amount of work and churn.

[Eric Wieser]

Using docs#DFinsupp will avoid the issue

[Kyle Miller]

lyphyser said:

it isn't possible to use Finsupp in programs despite the fact that it's obviously a perfectly computable notion.

They are also not a very good data structure for programs, since Finsupp operations never memoize the underlying functions, leading to giant closures and surprising negative performance. DFinsupp has similar issues.

If the goal is computation, I would suggest making/finding appropriate basic data structures. Then, if you need to prove anything, create the function from this structure to Finsupp and prove the supporting lemmas to carry operations over.

[lyphyser]

thanks! I completely missed DFinsupp, just assumed it was the same but dependent

[lyphyser]

They are also not a very good data structure for programs, since Finsupp operations never memoize the underlying functions, leading to giant closures and surprising negative performance. DFinsupp has similar issues.

Indeed, although my goal right now is only reducibility and being able to produce a computable function, but probably not running it, so DFinsupp seems perfect for now.

More in general, I think this might perhaps be solvable though by redefining Finsupp/DFinsupp to be a custom function-like type plus an RBMap overriding it with specific values; this way (D)Finsupp.update would work efficiently by updating the RBMap and the function-like type could just be an empty function where all operations are trivial if it's constructed from Finsupp.single/etc.; but unlike just using RBMap this would allow to still specify arbitrary functions with huge but finite support and use them seamlessly along with the single/update RBMap ones.

[Eric Wieser]

Kyle Miller said:

They are also not a very good data structure for programs, since Finsupp operations never memoize the underlying functions, leading to giant closures and surprising negative performance. DFinsupp has similar issues.

If all you do with DFinsupp in a program is evaluate the function and sum over the support, then it is a fine data structure. It's some of the operations on that structure that are inefficient, notably addition.

[Eric Wieser]

I think using RBMap is troublesome for mathlib as this requires the indices to be ordered

[Eric Wieser]

Maybe we can make this palatable with some Indexing I typeclass which carries DecidableEq I and Trunc (LinearOrder I) or similar

[Kyle Miller]

lyphyser said:

redefining Finsupp/DFinsupp

I think for math purposes, Finsupp/DFinsupp are fine as they are, and I would like to see development going in the direction of making new computational versions of the types that have reasonable efficiency and creating bridges to the mathematical types.

The alternative to unnecessary noncomputability is the math library seeing unnecessary decidability. It'd be better to not have to make compromises on this point and instead have separate types.

[Yury G. Kudryashov]

It would be nice to have some to_computable tactic (or what should it be?) that takes a definition and tries to replace noncomputable bits with computable, searching for missing [Decidable..] etc instances for the types in question. So that we should be able to redefine Finsupp without anything computable (i.e., no Finsets, just Set.Finite toFun.support), then lift specific Finsupps needed for, e.g., Nat.factorization to something computable. Not sure how can it work and if it's actually possible.

[Alex Meiburg]

I just found myself hitting the same issue. I've got some rather long definitions (involving Nat.find, Encodable.encode, etc.) and I would like to be able to just native_decide/decide it. But I can't, because there's Finsupp.instAdd in there.

Is there a reason explicitly to not let Finsupp be noncomputable? Is there a real worry that someone will write code that uses it, expects performance, and suffers for it?

[Eric Wieser]

@Alex Meiburg,can you use docs#DFinsupp ?

[Eric Wieser]

Is there a reason explicitly to not let Finsupp be noncomputable?

My personal opinion is no, but very pragmatically it is extraordinarily hard to make this change across all of Mathlib at once

[Alex Meiburg]

Eric Wieser said:

can you use docs#DFinsupp ?

I'll try that and see. :) If it works (or maybe even it it doesn't!) it would be good to add some comment to this effect in Finsupp/Defs.lean, next to where it says "This file is a noncomputable theory and uses classical logic throughout.".

[Eric Wieser]

If you want to pursue this, I think a good stepping stone would be to switch Basis to use DFinsupp

[Eric Wieser]

#17881 has a nice example of where computable dfinsupp is handy

[Tristan Figueroa-Reid]

I just ran into this myself with in #28075 (thanks for pointing this out @Oliver Nash!). Based on the conversation above, it seems that I'm not the only one who naturally thought that Finsupp would be a good type for computation.

DFinsupp works for me as well, but it doesn't have as much theory and utility functions built on top of it as Finsupp has, and it feels clunky to work with dependent types when I just don't need them. I do think that it would be worthwhile to have Finsupp be computable when its not that inconvenient.

[Eric Wieser]

I think in the short term we should build the API for DFinsupp that's missing

[Fabrizio Montesi]

FWIW, I found it very surprising that DFinsupp and Finsupp are so different (decidability vs classical approach). The D-naming suggests the latter is just the non-dependent version of the former.

[Johan Commelin]

Yeah... turns out the d also stands for "decidable" :see_no_evil: :oops:

[Yaël Dillies]

@Fabrizio Montesi, there are plans to change this. But it takes time and effort to coordinate such changes. I am personally currently doing as many "obviously good" changes in that direction, before attacking the ones that the community has historically been wary about

[Fabrizio Montesi]

Yaël Dillies said:

Fabrizio Montesi, there are plans to change this. But it takes time and effort to coordinate such changes. I am personally currently doing as many "obviously good" changes in that direction, before attacking the ones that the community has historically been wary about

Thanks for the note!
(I appreciate the complexity of such changes, these things take time. :))