Could Fintype.ofFinite be made an instance inside Classical?

Stream: mathlib4

[Terence Tao]

I understand why we don't make docs#Fintype.ofFinite an instance by default, as it makes Fintype noncomputable. But perhaps it would be safe to make such an instance after one opens Classical? I found it annoying that I could not write down ∑ x, f x when the type X of x had only a finite instance [Finite X] and not a Fintype instance [Fintype X]; having typeclass inference supply this when working in a classical setting in which I do not care about computation would be convenient.

[Aaron Liu]

If this happens, it should be a low priority instance like how docs#Classical.propDecidable is (priority := low).

[Yaël Dillies]

This is a priori a bad idea as it would let you write lemmas that are syntactically under general, but actually this is exactly the situation Decidable already enjoys. At any rate, it should be lower priority.

[Kevin Buzzard]

On the other hand it's in general quite annoying when you have to randomly add decidable instances in situations where you are never going to compute anything, I'm finding this situation in group homology right now and it's difficult to explain to mathematicians

[Kenny Lau]

But then on the other hand we want a sum to be computable when it's on a fintype so that we can easily reduce a sum on a concrete type like Fin 37, I think?

[Aaron Liu]

This is looking just like the situation with Decidable to me

[Kyle Miller]

Terence Tao said:

But perhaps it would be safe to make such an instance after one opens Classical?

I think there's no reason not to do this. I've suggested adding it to the classical tactic, but an obstruction now is that this is a core Lean tactic.

However, we shouldn't ever make Fintype.ofFinite a global instance. This would poison the computability of Fintype, whose raison d'être is to be computable. This should be some pressure to make things more Finite (I'd like a future where sums all use Finite and there's an easy way to reflect sums to Finset.sum to compute them when needed.)

[Eric Wieser]

Kyle Miller said:

I think there's no reason not to do this. I've suggested adding it to the classical tactic, but an obstruction now is that this is a core Lean tactic.

I guess lean4#7948 would resolve this, if I could get it to build.

Is the problem that there is no builtin_macro_rules?

[Eric Wieser]

Kyle Miller said:

I'd like a future where sums all use Finite and there's an easy way to reflect sums to Finset.sum to compute them when needed.)

What scares me most about this is that everything implemented in terms of such summations (docs#dotProduct, docs#Matrix.instRing, docs#DirectSum.toAddMonoid, etc) has to somehow opt into this reflection too, and the boilerplate to do this is surely far greater than the cost of Finite.toFinite inside proofs

[Kyle Miller]

Yeah, that's a valid concern. I think some research is needed here, it's not a 'let's "just" do this' situation.

[Eric Wieser]

I think we could "just do this" for the titular suggestion though

[Eric Wieser]

Do you think you could adopt lean4#7948? I assume there's some bootstrapping / builtin_ thing I'm missing.

[Matt Diamond]

is this something that docs#finsum was supposed to help with?