Fintype (X → Y) from Fintype X and Fintype Y?

Stream: new members

[Yannick Seurin]

It does not seem possible to infer Fintype (X → Y) from Fintype X and Fintype Y but I'm struggling to see why and what extra assumptions I would need...

import Mathlib

variable (X Y : Type*) [Fintype X] [Fintype Y]

instance : Fintype (X × Y) := inferInstance -- works

instance : Fintype (Bool → Fin 5) := inferInstance -- works

instance : Fintype (X → Y) := inferInstance -- failed to synthesize Fintype (X → Y)

[Kenny Lau]

@Yannick Seurin you're looking for Pi.instFintype, and you need X to be discrete

[Kenny Lau]

but actually i don't see why you would need that...

[Yannick Seurin]

I'd like to define the uniform distribution on the space of functions from X to Y using PMF.uniformOfFintype

[Kenny Lau]

@Yannick Seurin well, do you care about making things computable, and why?

[Kenny Lau]

because classically you can just assume that every type is discrete

[Kenny Lau]

Kenny Lau said:

but actually i don't see why you would need that...

actually I think I see it now, let's say you have X = {a1, a2} and Y = {b1, b2}, now you want to build 4 functions X -> Y, so let's say the first function sends a1 to b1 and a2 to b2... oh wait, how do you decide if the given input is a1 or a2?

[Kenny Lau]

@Yannick Seurin but all this detail is unnecessary, we've decided long ago in mathlib that we don't care about computability, we would just classically assume everything is decidable and move on with our lives

[Yannick Seurin]

Hm, no I don't care about computability. Does that mean I can work with [Finite X] and [Finite Y]?

[Riccardo Brasca]

@Yannick Seurin if your goal is to do mathematics you may prefer to use Finite instead of Fintype

[Kenny Lau]

and Nat.card instead of Fintype.card

[Kenny Lau]

and put have := Classical.propDecidable everywhere

[Yannick Seurin]

I see thanks! (I'm still a bit confused about using Finset vs. Finite)

[Kenny Lau]

Finset X is the type of finite sets on X

[Kenny Lau]

Finite X is the prop saying that X is a finite type

[Kenny Lau]

so e.g. {5, 7, 10} : Finset Nat

[Kenny Lau]

and there's nothing in Finite Nat because that's not a true statement

[Yannick Seurin]

Sorry, I meant "I'm still a bit confused about using Fintype vs. Finite"

[Kenny Lau]

some functions in the library require Fintype because they were set up differently

[Kenny Lau]

but we're slowly getting rid of them and replacing them all with Finite

[Kenny Lau]

but if you do need to use one then you can either 1. assume Fintype anyway, or 2. make that instance classically using FIntype.ofFinite

[Yannick Seurin]

I'll go with Finite then! Thanks!

[Aaron Liu]

Kenny Lau said:

but actually i don't see why you would need that...

why not

[Aaron Liu]

Kenny Lau said:

but we're slowly getting rid of them and replacing them all with Finite

I would hope not

[Robert Maxton]

It's still nice to be able to prove things by exhaustive checking sometimes!