finite or fintype

Stream: general

[Sebastien Gouezel]

There is a disagreement in #17553 between @Yury G. Kudryashov and @Eric Wieser, where Yury wants to replace fintype instances by finite instances (thereby making things less computable), while Eric would like to make things more computable. I think this is something we should sort out on Zulip. Personally, I would be really happy to get rid of all computability in mathlib, and even of the [decidable] typeclass, since I don't think this is a good mechanism for computation (algorithms implemented in CAS-like functions like norm_num seem to me much better suited for the job), I've seen it creating defeq issues a lot of times, and I haven't seen once a place where this really turned out to be useful. But this is maybe an extreme position :-). I'd be interested in hearing why some people think it is important/useful to get things computable, especially with concrete examples!

[Eric Wieser]

It's worth remembering that one of the ways that norm_num works is by transferring the information from a noncomputable type (such as real) into a computable type (such as rat), and then doing computation in the VM to get a normal form.

If we follow that pattern, it's reasonable to assume that it will be easier to build norm_num extensions for types if we have computable versions of them.

[Eric Wieser]

Thanks for raising this on Zulip; If someone is blocked by the change in #17553 then I'm fine with the noncomputable version going in in the medium term.

[Eric Wieser]

In the long term, I strongly feel that we're making things hard on ourselves by making finsupp noncomputable (whether polynomials are noncomputable is a related but independent concern). Changing that is already a herculean effort, and every change to make corners of the API more noncomputable makes that even harder

[Kyle Miller]

In this case, I guess a question is whether something like norm_num would ever want to compute with a finsupp, or if it would try to transfer to a much better representation (like a list of monomials).

[Eric Wieser]

Perhaps that's an argument in favor of finsupp being represented internally with a list of monomials instead

[Eric Wieser]

Perhaps it's not a particularly good argument, but; if finsupp and polynomial were computable than (X + C 2 : polynomial rat).degree = 1 would be true by refl (because all the decidability instances would reduce without getting stuck on a classical.dec_eq)

[Kyle Miller]

docs#finsupp is a closure (to_fun) along with a finset that is a support. The problem with closures is that they are not memoized by default, so you can easily have very inefficient finsupp terms.

[Eric Wieser]

Do you have a good reference to learn how closures are represented in the VM?

[Sebastien Gouezel]

From a complexity point of view, things will depend a lot on the shape of the underlying space. For instance, if you're working with polynomials, then you want to use the order structure to compute efficiently, while if you're working with the group algebra of the free group, say, then you would frame your computations very differently. I don't think there is a "one size fits all" algorithm here. That's something norm_num can do very well, using different algorithms depending on the shape of the input, while refl can't.

[Kyle Miller]

Eric Wieser said:

(because all the decidability instances would reduce without getting stuck on a classical.dec_eq)

I'm not sure that's a safe assumption, because they might depend on well-founded recursion, which can get stuck. You can still #eval of course.

I've thought about how it might be nice to have a super_refl that does something like refl but by (essentially) unfolding definitions using unfold rather than dunfold. I.e., allow rewrites. This is a bit of a non-sequitur, but it'd solve this well-founded recursion problem.

[Sebastien Gouezel]

Having (X + C 2 : polynomial rat).degree to compute by refl doesn't seem useful to me, because most often you're not working with rat but with a general abstract field, in which this won't compute.

[Eric Wieser]

Even if there's not a "one size fits all" algorithm, having an inefficient algorithm available everywhere would remove a lot of pain from the simple cases without having to write tactic code.

[Eric Wieser]

because most often you're not working with rat but with a general abstract field, in which this won't compute.

I agree; but lift or norm_num could presumably translate it into a polynomial over rat for the sake of computation, just like it does for numeric literals

[Kyle Miller]

Eric Wieser said:

Do you have a good reference to learn how closures are represented in the VM?

Not really, but the main point is that a closure is a bit of code that has to be re-evaluated every time, and there's nothing to cache the results. Inductive datatypes (like a list) are places where evaluated data can actually be stored and read again later. One way to deal with this problem with closures is to evaluate a table of all outputs for every input then create a new function that reads that (and then prove that the new function is equal to the old one).

[Eric Wieser]

I had something like your last sentence in mind too

[Kyle Miller]

I guess I'll mention one example of polynomials in Lean 4. I needed an efficient implementation, so this is hand-tuned for handling multivariable Laurent polynomials (this ring in particular is $\mathbb{Z}[t_0^{\pm 1}, t_1^{\pm 1}, t_2^{\pm 1},\dots]$). It uses lists of monomials sorted by exponents, since that way when you add polynomials you can merge and deal with entries with duplicate exponents. This is much more efficient than what you could get with a more generic finset type of representation, and I suspect I couldn't have finished my calculation without this optimization. I'm sure this is what Sebastien meant about using order properties.

[Sebastien Gouezel]

For now I have the impression that the discussion is pretty hypothetical, in the form: if finsupp were computable, then maybe it could help for some norm_num algorithms. @Mario Carneiro , do you have some thoughts on that?

[Kevin Buzzard]

Can someone remind us of the polynomial story? My memory was that they were initially computable and then they were switched to being noncomputable, and my memory was that this solved some problems but didn't break anything.

@Reid Barton had a problem with finsupp IIRC, in the sense that I think he once told me that in some sense it was some kind of half-way house between being computable and noncomputable and hence no good for anyone.

[Johan Commelin]

I think it's very good to have definitions that are optimized for reasoning as well as definitions that are optimized for computations. And they probably will overlap sometimes, but not very much.

[Eric Wieser]

Arguably what matters for reasoning is usually the API, not the definition itself

[Kevin Buzzard]

Making the API is much harder (for me, at least) if the definition is not optimised for reasoning.

[Kevin Buzzard]

Example: proving add_assoc for num vs proving it for nat.

[Reid Barton]

If the API mentions decidable_eq in the type of union or whatever, then it is the wrong API for reasoning about.

[Eric Wieser]

Are you advocating removing decidable_eq from docs#finset.union?

[Reid Barton]

The problem is no one seems to agree on what finset is for

[Kyle Miller]

I'd advocate for defining finite_set as a set with a set.finite proof, then letting finset be there for generic computation.

[Eric Wieser]

Reid Barton said:

If the API mentions decidable_eq in the type of union or whatever, then it is the wrong API for reasoning about.

Taking this to the extreme, this seems to also advocate having and prefering a classical version of docs#ite that avoids decidable arguments

[Reid Barton]

I am just saying that the API(s) for implementation(s) of finset designed for computation cannot be identical to the API for the one for reasoning, because they will have extra decidable_eq or linear_order or whatever hypotheses.

[Kyle Miller]

@Eric Wieser There's been at least one discussion on zulip (with Reid) with that suggestion for a classical ite

[Eric Wieser]

I don't fully see the argument for why a decidable_eq argument is a big deal for reasoning; most of the time you can just ignore it's there and Lean will handle it for you

[Reid Barton]

Didn't you design a whole linter to make sure that decidable_eq arguments in definitions/lemmas are properly generalized over, and such? It wouldn't even need to exist in an ideal world.

[Eric Wieser]

Arguably I only designed about 3/4 of it and never got back to the 1/4...

[Mario Carneiro]

Sebastien Gouezel said:

For now I have the impression that the discussion is pretty hypothetical, in the form: if finsupp were computable, then maybe it could help for some norm_num algorithms. Mario Carneiro , do you have some thoughts on that?

It's not used in norm_num, but one example of a tactic that does rely on kernel reduction in order to extract witnesses is fin_cases. This will use typeclass inference to infer a fintype instance on the target, then reduce it to get a list of elements to present as goals.

Also, of course there is the decide tactic (previously dec_trivial), which should not be discounted. I find 657 uses of dec_trivial in mathlib, which puts it up there with some of the most used heavy tactics like linarith. If we were to completely remove decidability, then we would basically lose this tactic entirely and would have to reinvent an evaluation framework to which norm_num is only an approximation.

However, I agree with the thrust of the argument. Kernel reduction has weird performance characteristics and generally requires custom implementations anyway, so I don't think we should assume that standardly defined mathlib notions will be optimal for this kind of computation. And in many cases, like fin_cases, I think it would be better served by a meta typeclass similar to norm_num extensions to handle synthesis of the elements of arbitrary types, written the way we want them to be (the one you get by kernel reduction is more or less forced to have the form [zero, zero.succ, zero.succ.succ] and so on).

[Scott Morrison]

And note the interval_cases (which is a thin wrapper on fin_cases) actually has to call norm_num internally to rewrite those horrible "numerals" back into literals.