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