Zulip Chat Archive

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)

Nicolás Ojeda Bär (Aug 16 2021 at 11:16):

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 (Aug 16 2021 at 11:17):

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

Kevin Buzzard (Aug 16 2021 at 11:17):

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

Eric Wieser (Aug 16 2021 at 11:18):

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

Oliver Nash (Aug 16 2021 at 11:19):

I guess this might be illustrative:

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

Kevin Buzzard (Aug 16 2021 at 11:21):

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 (Aug 16 2021 at 11:23):

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 (Aug 16 2021 at 11:25):

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 (Aug 16 2021 at 11:27):

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 (Aug 16 2021 at 11:29):

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 (Aug 16 2021 at 11:29):

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 (Aug 16 2021 at 11:30):

Noncomputability is inherited from set.finite.fintype

Oliver Nash (Aug 16 2021 at 11:31):

@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 (Aug 16 2021 at 11:31):

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 (Aug 16 2021 at 11:32):

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

Eric Wieser (Aug 16 2021 at 11:33):

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

Oliver Nash (Aug 16 2021 at 11:33):

(deleted)

Kevin Buzzard (Aug 16 2021 at 11:34):

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 (Aug 16 2021 at 11:35):

Passing the type would look like this:

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

Oliver Nash (Aug 16 2021 at 11:36):

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 (Aug 16 2021 at 11:36):

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 (Aug 16 2021 at 11:38):

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 (Aug 16 2021 at 11:40):

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 (Aug 16 2021 at 11:41):

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 (Aug 16 2021 at 11:41):

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 (Aug 16 2021 at 11:41):

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 (Aug 16 2021 at 11:42):

And semi-implicit ⦃⦄ :wink:

Yaël Dillies (Aug 16 2021 at 11:42):

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

Kevin Buzzard (Aug 16 2021 at 11:42):

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

Yaël Dillies (Aug 16 2021 at 11:43):

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

David Renshaw (Aug 16 2021 at 12:03):

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

Yakov Pechersky (Aug 16 2021 at 13:52):

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

Yakov Pechersky (Aug 16 2021 at 13:53):

docs#set.finite.to_finset

Kevin Buzzard (Aug 16 2021 at 14:58):

https://xkcd.com/927/

Kevin Buzzard (Aug 16 2021 at 14:59):

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


Last updated: Dec 20 2023 at 11:08 UTC