Finite or Fintype?

Stream: mathlib4

[Kevin Buzzard]

I no longer understand mathlib's policy about stating theorems involving finite types. I've written this in FLT:

variable {R : Type*} [τR : TopologicalSpace R] [Semiring R] [TopologicalSemiring R]

variable {ι : Type*} [Finite ι] {A : ι → Type*} [∀ i, AddCommMonoid (A i)]
  [∀ i, Module R (A i)] [∀ i, TopologicalSpace (A i)]
  [∀ i, IsModuleTopology R (A i)]

instance pi : IsModuleTopology R (∀ i, A i) := by

"The product topology for a finite product of modules with the module topology, is the module topology". But when I PR this to mathlib am I supposed to be using [Finite ι] or [Fintype ι]? What is the rule? I know that Thomas Browning has been going through finite group theory changing Fintypes to Finites but don't really understand why (I have a preference for Finite because it's Prop-valued so you can't get into a pickle with two instances, but it's only a mild one because I understand how to avoid these problems nowadays).

[Riccardo Brasca]

I think Finite is perfectly fine here. Going from Fintype to Finite is possible (without any choice) so this shouldn't harm anything, and in my opinion is closer to the mathematical notion.

[Eric Wieser]

If IsModuleTopology is prop-valued then Finite is certainly the right choice here

[Kevin Buzzard]

Yes it's Prop-valued (yay for the Is naming convention). I'm well aware of how to move between Fintype and Finite so my response to Riccardo is "yes but going from Finite to Fintype is also possible", and my response to Eric is "why?"

[Sébastien Gouëzel]

If you have a Fintype instance, then typeclass inference will also find a Finite instance. If you have a Finite instance, then typeclass inference won't find a Fintype instance, since there is additional data to be produced. So, if you assume Finite in your lemma, it will apply in more situations.

[Kevin Buzzard]

Then why were we using Fintype in 2017? Why do we use Fintype at all?

[Riccardo Brasca]

Exactly, it is possible via a choice, in particular it won't be computable.

[Riccardo Brasca]

If you have a Fintype you can use decide (or whatever) to check all the cases, one by one.

[Kevin Buzzard]

I know that, and this is exactly what means that I don't understand why I'm supposed to be using "Finite". You were saying "oh look, with Finite there is an advantage" and now you're saying "oh look, with Fintype there is a different advantage"

[Kevin Buzzard]

And because I'm now proficient at moving between them it's got to the point where I don't even care which one I use, so I'm trying to establish what the mathlib convention is and why.

[Riccardo Brasca]

I think Fintype is similar to "Kuratowski finite", and Finite is "Dedekind Finite" (wiki)

[Riccardo Brasca]

for you those are completely the same because you don't care about computability

[Yaël Dillies]

Long story short, use Finite unless your statement needs Fintype

[Eric Wieser]

I'd go a little further than that, the norm on docs#PiLp is defined with Fintype (which IMO is correct) not because the statement needs Fintype, but because the data within the definition (and the lemma expanding that definition) does.

[Michael Rothgang]

Yaël Dillies said:

Long story short, use Finite unless your statement needs Fintype

#10235 adds a linter (AIUI, porting an analogous mathlib3 linter) for this.

It's waiting on somebody (e.g. me) finding the time to make the linter fast enough to land. If that's urgent for you, let me know and I prioritise my mathlib time there.

[Kyle Miller]

Kevin Buzzard said:

Then why were we using Fintype in 2017? Why do we use Fintype at all?

A strong reason for this is that we didn't have Finite until 2022 :-) mathlib3#14373

The port caused a little bit of a disruption to the "finite-ification" of mathlib, but I'm happy to see that it's been progressing.

Kevin Buzzard said:

I have a preference for Finite because it's Prop-valued so you can't get into a pickle with two instances, but it's only a mild one because I understand how to avoid these problems nowadays

Yes, this was one of the motivations for Finite. Even though the issues are surmountable, when proving theorems it's purely wasted effort.

Another motivation is that people were tempted to add noncomputable Fintype instances, which defeats the purpose of Fintype, which is that it's supposed to be computable. Now those can safely be Finite instances instead.

A last main motivation is that moving to Finite tends to mean you can avoid needing any Decidable instances, which also add friction to doing math.

Re "yes but going from Finite to Fintype is also possible": this is exactly like making use of classical decidable instances. It works, but it can cause the usual sorts of problems where you have the 'wrong' instance somewhere. It's easier to stick with Finite and not worry about it.

[Kevin Buzzard]

My takeaway from this is "going forward, use Finite". So should I also be moving away from Finset.sum?

[Kyle Miller]

I'm not sure what the current status is there.

Something I've wanted to see is a FiniteSet type that's bundles a Set and a Set.Finite proof, and then have all the theory be developed for that, and perhaps we could use a FiniteSet.sum. This would be the type you need to comfortably work with the lattice of finite sets, free from any complications from Fintype or DecidableEq.

At least there's ∑' (tsum), which works right now. For infinite domains the fact it deals with convergence could be regarded as a 'junk value' when things do happen to converge.

[Kyle Miller]

There's something to be said for definitions that don't unnecessarily require additional hypotheses (like finiteness), since there's less chance for DTT hell. A definition like that is docs#Nat.card, which doesn't require that the type be finite, eliminating large classes of "motive not type correct" errors.

[Daniel Weber]

There's also docs#finsum

[Violeta Hernández]

Fintype is useful for computational applications, such as using fin_cases. There's otherwise very little reason to use it.