Finsupp noncomputability

Stream: new members

[Robert Spencer]

I am trying to work with Finsupp over a DecidableEq target. However, many of my definitions end up being noncomputable because docs#Finsupp.single is. I'd like to have as much of my (very finite) theory to be as computable as possible, since I don't see a good reason for it not to be, and I enjoy being able to #eval on occasion.

I've been getting round this by just using functions from my finite base set to the target, but then when I want to talk about docs#Module.Basis I have to restate a lot of my work. It would be nicer if I could just define the basis and work with it, but docs#Module.Basis.instFunLike is not computable for this reason.

Have others come across this? What is the recommended way to think about functions from finite types (functions or Finsupps?) Am I asking too much for a computable theory (e.g. I have my own computable version of docs#Finsupp.equivFunOnFinite)?

On a more technical level, this feels like function specialisation: if we have DecidableEq M then we can use a computable version of Finsupp.single but if not, we could fall back. However, I vaguely know that this is a whole can of confusion and debugging troubles in other languages. Does lean4 do it?

[Robin Arnez]

Well, there's also docs#DFinsupp which does have computable API.

[Filippo A. E. Nuccio]

@Riccardo Brasca

[Riccardo Brasca]

I've recently though about this exact same problem, improving Finsupp.single and I come up to the conclusion that in principle is doable, but it may be very annoying and I stopped as at the end it was not exactly what I needed. Something that I don't understand is why Finsupp and DFinsupp have different designs, but maybe it is just beacuse of historical reasons.

[Riccardo Brasca]

The easiest thing to do is probably just to use DFinsupp.

[Robert Spencer]

Hmm. I think the ripple effect to Module.Basis means there isn't much of a point for me

[Robert Spencer]

When you say it was annoying, what was the reason for that? Lots of downstream updates needed? Presumably some applications don't want to enforce DecidableEq

[Riccardo Brasca]

Yes, that's the point. noncomputable stuff is so embedded into mathlib that it is basically impossible to get something computable unless it is very very basic.

[Riccardo Brasca]

We cannot assume DefidableEq M in Finsupp.single as this is used for polynomials (for example), and we surely want polynomials over the reals. We can of course have two versions, but it's a nightmare to maintain a parallel library if you need things that are quite advanced in the library.

[Riccardo Brasca]

What we, as human beings, do is to use DecidableEqif this is available for obvious reasons, and ignore it (i.e. we use choice and in our brain we know that we moved in the world where we can prove things but not evaluating stuff). I guess we just don't know how to teach a computer to do that yet

[Robert Spencer]

Yeah, that makes sense, but is unfortunate. I think I was hoping that there was a way to override definitions, such as "use this one if we have decidability, otherwise fall back to this noncomputable theory" as you describe us doing manually. However, I also see that having two definitions (one for computable and one for noncomputable theory) would be a nightmare.

Is the implicit conclusion that the mathlib ecosystem is comfortable with things being needlessly noncomputable?

(aside, do I misunderstand docs#Real.decidableEq? I also thought it was undecidable)

[Robert Spencer]

(link, because the docs go 404)

[Riccardo Brasca]

Ah sorry, I didn't realize we have that. Anyway it comes from

open scoped Classical in
noncomputable instance linearOrder : LinearOrder ℝ :=
  Lattice.toLinearOrder ℝ

so using choice under the hood and in practice it cannot be used.

[Riccardo Brasca]

This can work in practice, add DecidableEq (using choice) on all concrete types that don't have it. Anyway you can just try to open a PR improving Finsupp.single and see what happens. I didn't spend a lot of time with it because the first file broke quite badly, but maybe the rest is OK.

[Yaël Dillies]

Note that #25273 is a prerequisite to unifying Finsupp and DFinsupp painlessly. I am actively working on it

[Riccardo Brasca]

I was pinging you asking exactly this, but you were faster :)

[Snir Broshi]

Is it possible to make "leaf" definitions of the API computable, e.g. docs#Finsupp.zipWith ?

[Riccardo Brasca]

Snir Broshi said:

Is it possible to make "leaf" definitions of the API computable, e.g. docs#Finsupp.zipWith ?

If you want to make something computable you need to find the source of noncomputability, so you should more go in the opposite direction. Something else that can be done is to replace a noncomputable def X with a computable X' and prove that X = X', but this works only if defining X' is possible without using all the machinery used in X (maybe because we want X' in a more specific situation).

[Robert Spencer]

Ok, I'll have a go in my little project (amusingly, a different type of MonoidAlgebra to #25273) at seeing how bad it would be to improve Finsupp.single.

However, I'm not even sure what "improve" means in this case, since we want both theories. Would it look like having both X and X'?

[Riccardo Brasca]

I mean to make the current Finsupp.single computable. If you look at DFinsupp.single you see that one has to assume that the source has decidable equality, but not the target. But if @Yaël Dillies is already doing that in making all the Finsupp API a special case of the DFinsupp API maybe it's better to just wait

[Eric Wieser]

There is work which can be done now, which is to switch basis to use DFinsupp instead of Finsupp; I have a stale PR somewhere that attempts this

[Robert Spencer]

If finsupp becomes a special case of dfinsupp, then presumably its ok to leave the basis definition as-is? Am I reading it wrong that we'd want to define basis as something like M ≃ₗ[R] Π₀ ι, R?

[Riccardo Brasca]

Morally Finsupp is a special case of DFinsupp, so there is no need to have two separate APIs (we can always specialize theorems to the Finsupp case) and the most natural thing to do is to make everything for Finsupp and adding specialized version only when something goes wrong (sometimes Lean struggles to understand how to specialize a dependent version of something to the non-dependent version). @Yaël Dillies do you plan to work on this after the monoid algebra thing?

What Eric is suggesting is to start removing uses of Finsupp and replacing them with DFinsupp.

Both approaches look reasonable to me, and they can also be done in parallel.

[Robert Spencer]

I see. So we'll write the definition of a basis in terms of a dependent finite support where there is actually no dependency?

[Riccardo Brasca]

Yes, letting β in DFinsupp be the constant function fun _ ↦ M should give exactly Finsupp. The PR mentioned by @Eric Wieser is I think #25170.

[Robert Spencer]

Great. Makes sense, thanks

[Riccardo Brasca]

If you believe the script Claude wrote for me the following is the graph of noncomputable declarations Module.Basis.instFunLike depends on.
graphviz.jpeg

[Riccardo Brasca]

In particular it seems making Finsupp.single computable is not enough.

[Violeta Hernández]

to be clear, is the eventual goal to phase out Finsupp in favor of DFinsupp? I recall this document about all the different possible approaches to Finsupp computability, I'm not sure if we ever concluded DFinsupp was the "correct" one.

[Riccardo Brasca]

I think there is no eventual goal, this discussion started like 2 hours ago :)

[Violeta Hernández]

Yaël has clearly been thinking about this for like a year at this point, that wider discussion is what I'm asking about