Finite Option

Stream: mathlib4

[Thomas Vigouroux]

Hi, I needed to have Finite (Option T) at some point in a proof, and I ended up writing a proof of that. Is it interesting to have that in lean4 ? I am willing to open a PR

[Yaël Dillies]

docs#Finite is in Mathlib. Are you sure you are in the right stream?

[Thomas Vigouroux]

Woops probably not indeed

[Thomas Vigouroux]

I can't change stream though, do you want me to close this one and open another in #mathlib4 ?

[Notification Bot]

This topic was moved here from #lean4 > Finite Option by Floris van Doorn.

[Thomas Vigouroux]

Thanks !

[Floris van Doorn]

docs#instFintypeOption is probably what you want?

[Floris van Doorn]

Oh, you meant actually the Finite version of that. yeah, that would be useful. Please open a PR.

[Thomas Vigouroux]

Hmmm, for some reason I could not find it...

[Thomas Vigouroux]

Then my question is settled :wink:, thanks !

[Notification Bot]

Thomas Vigouroux has marked this topic as resolved.

[Floris van Doorn]

I think it is still useful to add a finite instance as well. This now fails:

import Mathlib

variable (T : Type*) [Finite T]
#synth Finite (Option T)

[Thomas Vigouroux]

As you wish
I think that my proof of Finite (Option T) is a bit long though

[Floris van Doorn]

You should be reusing the existing Fintype instance. Or use docs#finSuccEquiv + docs#Equiv.optionCongr .
But this works:

import Mathlib

instance (T : Type*) [Finite T] : Finite (Option T) :=
  have := Fintype.ofFinite T
  inferInstance

#min_imports -- Mathlib.Data.Fintype.Option

Please PR this!

[Notification Bot]

Thomas Vigouroux has marked this topic as unresolved.

[Thomas Vigouroux]

Will do !

[Thomas Vigouroux]

Will do !

[Kevin Buzzard]

@Thomas Vigouroux that's one reason why we don't encourage resolving topics -- it can break stuff :-) But the option is there and can't be switched off so basically it seems to be a hopeless cause.

[Thomas Vigouroux]

Sorry about that !

[Notification Bot]

Yaël Dillies has marked this topic as unresolved.