Missing Finite instance?

Stream: mathlib4

[Ching-Tsun Chou]

There is an instance instInfiniteOption for infinite Option types. But there does not seem to be a corresponding Finite Option instance, like the following:

instance instFiniteOption {X : Type*} [Finite X] : Finite (Option X) := by
  apply Finite.of_finite_univ
  apply finite_option.mpr
  exact toFinite {x | some x ∈ univ}

Shouldn't something like the above be added to mathlib?

[Kyle Miller]

Yes, that is definitely missing.

One of the usual ways to derive these is using the Fintype instance like

instance {X : Type*} [Finite X] : Finite (Option X) :=
  have := Fintype.ofFinite X
  Finite.of_fintype _

but if your version lets it appear earlier that's fine too.

[Ching-Tsun Chou]

Should instFiniteOption be added to mathlib?

[Kyle Miller]

By "it's missing", I mean "mathlib should have it", not "it's intentionally excluded", to be clear.

The instance should not be given an explicit name.

[Ching-Tsun Chou]

I can't find such an instance in mathlib.

[Kyle Miller]

"Mathlib ought to have it" — please contribute it

[Kyle Miller]

The code suggestion was how the contribution could look. For style, we like to use the autogenerated name, hence the suggestion to not give it an explicit name.

When I said it's definitely missing, that's after verifying that the instance does not exist. I used this code:

import Mathlib

variable {X : Type*} [Finite X]
#synth Finite (Option X)

[Ching-Tsun Chou]

Which mathlib file should the instance be added to?

[Ruben Van de Velde]

import Mathlib

instance {X : Type*} [Finite X] : Finite (Option X) :=
  have := Fintype.ofFinite X
  Finite.of_fintype _
#min_imports -- import Mathlib.Data.Fintype.Option

vs

import Mathlib
open Set
instance instFiniteOption {X : Type*} [Finite X] : Finite (Option X) := by
  apply Finite.of_finite_univ
  apply finite_option.mpr
  exact toFinite {x | some x ∈ univ}
#min_imports -- import Mathlib.Data.Set.Finite.Basic

So you should add Kyle's proof to Mathlib.Data.Fintype.Option

[Ching-Tsun Chou]

PR: https://github.com/leanprover-community/mathlib4/pull/28783

[Ching-Tsun Chou]

By the way, thanks for all the comments!

[Junyan Xu]

Wait, Mathlib.Data.Fintype.Option is heavier with 370 imports compared to Mathlib.Data.Set.Finite.Basic's 312 imports.
(You can check this by

import Mathlib.Data.Set.Finite.Basic
#trans_imports "Mathlib."

)

[Ruben Van de Velde]

Hm, I thought I checked and Mathlib.Data.Set.Finite.Basic imported Mathlib.Data.Fintype.Option, but it doesn't seem so anymore. Still, the Option file seems more topical

[Junyan Xu]

I also observed that docs#nonempty_fintype saves a few (dozen?) imports over Fintype.ofFinite. The latter should probably be moved into the same file as the former.

[Kyle Miller]

@Junyan Xu Please feel free to make these basic instances not depend on Fintype/Finset/etc.

The Option instance can be created using much more basic imports, e.g.

import Mathlib

instance {X : Type*} [inst : Finite X] : Finite (Option X) := by
  obtain ⟨f⟩ := inst
  exact ⟨(Equiv.optionCongr f).trans finSuccEquivLast.symm⟩
#min_imports
/-
import Mathlib.Data.Finite.Defs
import Mathlib.Logic.Equiv.Fin.Basic
-/

[Kyle Miller]

(I didn't check if optionCongr or finSuccEquivLast are actually in more basic modules, but in principle they could be.)