set.finite.fintype

Stream: maths

[Kevin Buzzard]

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]

I think it should

[Reid Barton]

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]

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

[Mario Carneiro]

it does matter that finite is not a class

[Mario Carneiro]

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]

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

[Nicolás Ojeda Bär]

I don't underestand the following error (something to do with universes?). Any ideas?

import data.set.finite

universe u

def foo (α : Type u) (s : set α) (hs : set.finite s) : ℕ :=
fintype.card (set.finite.fintype hs)
/-
type mismatch at application
  fintype.card hs.fintype
term
  hs.fintype
has type
  fintype ↥s : Type u
but is expected to have type
  Type ? : Type (?+1)
-/

[Kevin Buzzard]

hs is a proof that a set is finite. fintype.card wants the type itself, not a proof that it is finite.

[Kevin Buzzard]

The function you're looking for already exists and is called something like nat.card

[Eric Wieser]

docs#nat.card is about types not sets, but that doesn't really matter.

[Oliver Nash]

I guess this might be illustrative:

noncomputable def foo (α : Type u) (s : set α) (hs : set.finite s) : ℕ :=
@fintype.card _ hs.fintype

[Kevin Buzzard]

So welcome to type theory. If X is a type then the type of subsets of X is called set X and a term S : set X is a term not a type. In particular you can't in theory talk about x : S to mean "x is in S", you need to do x : X and then hxS : x ∈ S.

[Kevin Buzzard]

fintype is a typeclass on types meaning "this type is finite". set.finite is a function on terms meaning "this set is finite". That weird ↥ arrow in your error message is an automatically inserted coercion meaning "I know it's a term, but I'm promoting it to a type because that's the only way to make this make sense".

[Kevin Buzzard]

Note also Oliver's trick of hs.fintype being notation for set.finite.fintype hs because hs has type set.finite ... -- this trick is called dot notation. I'm just mentioning these things because I know you're just starting in Lean -- sorry if you figured them all out already!

[Oliver Nash]

Conscious that @Nicolás Ojeda Bär is newish I'd like to offer reassurance that things get easier and formalisation quickly becomes huge fun. At the beginning it can feel annoying that there seem to be obstacles everywhere but in time the problems evaporate.

[Nicolás Ojeda Bär]

Thanks for the explanations @Kevin Buzzard , they are useful!

Kevin Buzzard said:

hs is a proof that a set is finite. fintype.card wants the type itself, not a proof that it is finite.

But I am passing a type, right? That's what set.finite.fintype is supposed to produce... However it only works if I the noncomputable annotation (with the explicit _ placeholder), as suggested by Oliver:

Oliver Nash said:

noncomputable def foo (α : Type u) (s : set α) (hs : set.finite s) : ℕ :=
@fintype.card _ hs.fintype

Is there a simple explanation why it doesn't typecheck if I don't add the noncomputable annotation (and the explicit _) ?

[Yaël Dillies]

Totally agree with Oliver. Yesterday I rewrote some of Henry Swanson's derangements PR and I really surprised myself by knowing how to deal with all the subtyping and coercions mess to actually get to the point. I really thought "No way 2021 May's Yaël could have done that".

[Yaël Dillies]

Noncomputability is inherited from set.finite.fintype

[Oliver Nash]

@Nicolás Ojeda Bär Consider this:

import data.set.finite

universe u

#check fintype.card -- Output: fintype.card : Π (α : Type u_1) [_inst_1 : fintype α], ℕ

This says that fintype.card is a function taking two arguments, called α and _inst_1 above. The second one is optional but by prefixing fintype.card with an @ sign I opted to provide it manually. I then left out the first argument (indicated by _) since its value can be inferred from the type of the second argument.

[Yaël Dillies]

set.finite means "There exists a finset whose elements are the same as my set, but I don't know which" (roughly) while fintype means "Here's a finset and a proof that it contains all the stuff in my type"

[Yaël Dillies]

That's the difference between knowing there exists an object that satisfies some conditions and actually having such an object.

[Eric Wieser]

The noncomputability of docs#set.finite.fintype is deliberate : if you want computable finiteness, use [fintype ↥s] instead of (h : s.finite)

[Oliver Nash]

(deleted)

[Kevin Buzzard]

Nicolás Ojeda Bär said:

But I am passing a type, right? That's what set.finite.fintype is supposed to produce...

set.finite.fintype hs is a proof that the type ↥s is finite, so it's a term not a type.

[Oliver Nash]

Passing the type would look like this:

noncomputable def foo (α : Type u) (s : set α) (hs : set.finite s) : ℕ :=
fintype.card ↥s

[Oliver Nash]

But that fails because it cannot find the typeclass (i.e., the optional argument hs.fintype) which needs to be built from hs.

[Kevin Buzzard]

There's also the added confusion that fintype was written with constructive mathematics in mind, so a term of type fintype X is not even a proof, it's actually data (but it's still a term, not a type).

[Nicolás Ojeda Bär]

Oliver Nash said:

(But that fails because it cannot find the typeclass, which needs to be built from hs.)

Thanks, that clears up (one of) my confusions, I had gotten the implicit argument to fintype.card mixed up.

[Kevin Buzzard]

There are two times where Lean will automatically fill in function inputs for you -- the {} system, where Lean figures out any inputs to functions marked with squiggly brackets using unification, and the [] system, where Lean figures out these inputs by looking at a big database called "the current contents of the typeclass system"

[Oliver Nash]

Right, so there are three types of arguments:

1. Explicit, for which we use round brackets ()
2. Typeclass, for which we use square brackets []
3. Implicit, for which we use curly brackets {}

[Kevin Buzzard]

You can override both systems with this @ trick, which means that you have to input all inputs manually (but then you can skip some and hope that Lean can figure them out)

[Nicolás Ojeda Bär]

Kevin Buzzard said:

There's also the added confusion that fintype was written with constructive mathematics in mind, so a term of type fintype X is not even a proof, it's actually data (but it's still a term, not a type).

Yes, I was indeed mixed up in my previous comment about it being a type, I see it now. Thanks!

[Yaël Dillies]

And semi-implicit ⦃⦄ :wink:

[Yaël Dillies]

I don't know if that's the official name for it.

[Kevin Buzzard]

I think those are being removed in Lean 4, so it's best not to talk about them ;-)

[Yaël Dillies]

Oh nooo, I liked them. But apparently I was the only one.

[David Renshaw]

It looks to me like they've been recently added to Lean4 : https://github.com/leanprover/lean4/commit/4cd7e359dfbfd56cca7f4a70d502ed159a61aa3e

[Yakov Pechersky]

The def everyone wants here is finset.card, and the value is (hs : set.finite).to_finset.card

[Yakov Pechersky]

docs#set.finite.to_finset

[Kevin Buzzard]

https://xkcd.com/927/

[Kevin Buzzard]

I am not sure that mathematicians ever want finset or fintype, we're just conditioned to use them by the constructivists.