A finite set has finitely many endofunctions?

Stream: new members

[Agnishom Chattopadhyay]

I have a finite set qq and I want to prove that the functions qq → qq are also a finite set.

Something like this:

instance finiteness_of_endofunctions {qq : Type} [fintype qq] : fintype (qq → qq) := sorry

How do I do that?

[Chris Hughes]

by apply_instance

There's already a fintype for pi types.

[Chris Hughes]

You need decidable_eq qq as well as it turns out

[Agnishom Chattopadhyay]

Like this? instance finiteness_of_endofunctions {qq : Type} [fintype qq] [decidable_eq qq] : fintype (qq → qq) := pi.fintype

[Agnishom Chattopadhyay]

Why do I need the decidable_eq?

[Reid Barton]

I imagine it's because each of the finitely many functions qq -> qq needs to be able to determine which element of the input it is looking at.

[Reid Barton]

fintype without decidable_eq is sort of a strange beast.

[Agnishom Chattopadhyay]

Well, I suppose that is reasonable

[Agnishom Chattopadhyay]

But now, if I do add decidable_eq on qq, for the purpose of what I am doing, I would also have to endow qq -> qq with decidable_eq.

instance decidable_eq_endofunctions {qq : Type} [fintype qq] [decidable_eq qq] : decidable_eq (qq → qq) :=  sorry

Library search suggests using classical.dec_eq (qq → qq)

Any chance I can avoid going classical?

[Chris Hughes]

by apply_instance does work there.

[Mario Carneiro]

You shouldn't have to write these instances; instance search will find these in use cases even without your instance declaration

[Agnishom Chattopadhyay]

I thought so too, but it did not seem to be working

[Mario Carneiro]

it should work with the decidable_eq instance in the context

[Yury G. Kudryashov]

I think that we should stop pretending that we care about constructive math (as opposed to computable defs). In particular, I'd stop requiring decidable P whenever we only use this assumption to prove a proposition.

[Kevin Buzzard]

There will always be people who want to use lean to do things which are quite a long way from maths, I guess. I just switch classical on and don't think any more about it :-)

[Chris Hughes]

The trouble is that switching classical on doesn't always mean you don't have to think about it.

[Agnishom Chattopadhyay]

it should work with the decidable_eq instance in the context

I thought so too.

Please take a look at line 38 of this. I'd want a lot of this painful instances to be automatic, but they are not, for some reason