## Stream: maths

### Topic: set.finite.fintype

#### Kevin Buzzard (Jan 28 2020 at 17:05):

import data.set.finite

open set

/- From data.set.finite:

noncomputable instance finite.fintype {s : set α} (h : finite s) : fintype s :=
classical.choice h

-/

example (α : Type*) (s : set α) (hs : finite s) : fintype s :=
by apply_instance
/-
tactic.mk_instance failed to generate instance for
fintype ↥s
state:
α : Type ?,
s : set α,
hs : finite s
⊢ fintype ↥s
-/

noncomputable example (α : Type*) (s : set α) (hs : finite s) : fintype s :=
by apply_instance -- same error

noncomputable theory
open_locale classical
local attribute [instance, priority 10000] set.finite.fintype

example (α : Type*) (s : set α) (hs : finite s) : fintype s :=
by apply_instance -- same error


The instance finite s -> fintype s -- I can't ever get it to fire. I just changed instance to def in mathlib and recompiled, and it seems to compile fine (I haven't finished yet but it's been running for a while). Should it be a def?

#### Yury G. Kudryashov (Jan 28 2020 at 17:15):

I think it should

#### Reid Barton (Jan 29 2020 at 00:06):

We could detect this with a linter, right? hs is not a type class argument (and finite is not even a class--does this matter?) and nothing depends on hs so there is no way it could ever be inferred, either.

#### Mario Carneiro (Jan 29 2020 at 00:09):

I like the idea of checking this with a linter. It can definitely be done

#### Mario Carneiro (Jan 29 2020 at 00:10):

it does matter that finite is not a class

#### Mario Carneiro (Jan 29 2020 at 00:13):

The simplest way to make the linter work is to create a replica of the instance type and try to prove it by apply_instance

#### Mario Carneiro (Jan 29 2020 at 00:15):

this might have false negatives for "transitivity" instances like foo A B -> foo B C -> foo A C (which should be discouraged)

Last updated: May 14 2021 at 19:21 UTC