Zulip Chat Archive

Stream: maths

Topic: set.finite.fintype


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jan 28 2020 at 17:15):

I think it should

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 29 2020 at 00:09):

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

view this post on Zulip Mario Carneiro (Jan 29 2020 at 00:10):

it does matter that finite is not a class

view this post on Zulip 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

view this post on Zulip 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