Zulip Chat Archive

Stream: new members

Topic: A finite set has finitely many endofunctions?


view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 16:22):

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?

view this post on Zulip Chris Hughes (Jan 12 2020 at 16:24):

by apply_instance

There's already a fintype for pi types.

view this post on Zulip Chris Hughes (Jan 12 2020 at 16:25):

You need decidable_eq qq as well as it turns out

view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 16:28):

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

view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 16:28):

Why do I need the decidable_eq?

view this post on Zulip Reid Barton (Jan 12 2020 at 17:07):

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.

view this post on Zulip Reid Barton (Jan 12 2020 at 17:09):

fintype without decidable_eq is sort of a strange beast.

view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 18:27):

Well, I suppose that is reasonable

view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 18:31):

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?

view this post on Zulip Chris Hughes (Jan 12 2020 at 18:34):

by apply_instance does work there.

view this post on Zulip Mario Carneiro (Jan 12 2020 at 20:28):

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

view this post on Zulip Agnishom Chattopadhyay (Jan 12 2020 at 20:44):

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

view this post on Zulip Mario Carneiro (Jan 12 2020 at 20:52):

it should work with the decidable_eq instance in the context

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

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.

view this post on Zulip Kevin Buzzard (Jan 13 2020 at 07:25):

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 :-)

view this post on Zulip Chris Hughes (Jan 13 2020 at 07:52):

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

view this post on Zulip Agnishom Chattopadhyay (Jan 14 2020 at 13:41):

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


Last updated: May 09 2021 at 20:11 UTC