Zulip Chat Archive

Stream: maths

Topic: coe_sort for finset


view this post on Zulip Enrico Borba (Jan 14 2020 at 04:56):

I'm trying to prove (in Lean) the statement that the cardinality of End(A)\text{End}(A) where AA is a finite set is equal to AA|A|^{|A|}. However, I'm having a hard time just stating it in Lean. What I tried was

theorem finset_endomorphism_cardinality {α : Type*} (s : finset α) :
    finset.card (↥s → ↥s) = (finset.card s) ^ (finset.card s) :=
  sorry

However, it doesn't seem that coe_sort exists for finset. I'm wondering: 1) what is a working way to state this now, 2) Is there a need for coe_sort in finset?

view this post on Zulip Bryan Gin-ge Chen (Jan 14 2020 at 05:21):

I think this is may be what you want:

import data.finset

theorem finset_endomorphism_cardinality {α : Type*} [decidable_eq α] (s : finset α) :
    finset.card (s.pi (λ _, s) ) = (finset.card s) ^ (finset.card s) :=
begin
  simp only [finset.card, finset.pi, multiset.card_pi,
    multiset.prod_repeat, multiset.map_const, nat.pow_eq_pow]
end

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 08:06):

Finite sets are a great example of where Lean proofs can look very different to what I write on the board. The book I used in my intro to proof course had a "multiplication principle" which said that if you had an nn-step process and you could do the $$i$$th step in aia_i ways (independent of what happened in the other steps) then clearly the number of ways you could complete the process was i=1nai\prod_{i=1}^na_i. No proof was offered and the result was taken as fundamental and used to compute things like the number of maps from a finite set AA to a finite set BB (building the function element by element). Had this stuff not been possible in Lean it would have been hard to stick with it, but there was this gigantic multiset and finset library in place which proved everything rigorously, and I learnt that looking through these files and just reading the statements of the lemmas could teach me a lot. Each one was trivial (most followed from the multiplication principle or even simple principles ;-) ) but it was good to see that they were there.

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:12):

@Enrico Borba Do you want finset or fintype? The difference can at first be confusing for mathematicians. But think of set as "subset" and type as "set".

view this post on Zulip Enrico Borba (Jan 14 2020 at 08:37):

I guess I want fintype since I’m looking to talk about functions with these finite sets as domains and images. What’s the distinction between finset and fintype?

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:38):

A fintype is a type with only finitely many terms (i.e. elements).
A finset is a finite subset of an arbitrary type.

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:39):

You can naturally talk about functions between types. But not (naturally) about functions between subsets.

view this post on Zulip Enrico Borba (Jan 14 2020 at 08:43):

This cleared some things up for me: https://github.com/leanprover-community/mathlib/blob/master/docs/theories/sets.md

view this post on Zulip Enrico Borba (Jan 14 2020 at 08:43):

I think I understand. Thank you

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:46):

If you use fintype, you'll probably have an easier time proving your theorem

view this post on Zulip Enrico Borba (Jan 14 2020 at 08:50):

Likely yes. I’m also trying to understand Lean’s type system while I learn these things. I didn’t realize it would implicitly coerce sets to types, which is why finsets caught me off guard a bit.

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 08:55):

Sets were a point of confusion for me for quite a while! A term of type set X is really a term, not a type, so you are limited in what you can do with it (e.g. you can't define a function from A : set X to a type, even though mathematicians would have no trouble doing this).

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 08:56):

The corresponding subtype contains precisely the same information, just packaged in a different way.

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 08:58):

That page in the docs you link to was written by Patrick and Chris. When I was learning, I didn't know enough about Lean to be able to write docs; now I understand a lot more stuff and tend not to write docs because I understand it and I don't know what docs people need! Do you have any doc requests?

view this post on Zulip Patrick Massot (Jan 14 2020 at 09:11):

I don't think I wrote any of that page, I think it's all from Chris.

view this post on Zulip Enrico Borba (Jan 15 2020 at 04:35):

I think this is may be what you want:

import data.finset

theorem finset_endomorphism_cardinality {α : Type*} [decidable_eq α] (s : finset α) :
    finset.card (s.pi (λ _, s) ) = (finset.card s) ^ (finset.card s) :=
begin
  simp only [finset.card, finset.pi, multiset.card_pi,
    multiset.prod_repeat, multiset.map_const, nat.pow_eq_pow]
end

@Bryan Gin-ge Chen How did you know which definitions to pass to simp? by simp * works, but I'd like a way to know which simplifications it applied so I can rewrite it as a simp only.

view this post on Zulip Bryan Gin-ge Chen (Jan 15 2020 at 04:38):

You can use squeeze_simp to give you a minimal set. It usually works, but it's not perfect. Sometimes there are extra / missing lemmas.

view this post on Zulip Enrico Borba (Jan 15 2020 at 05:33):

That's awesome! Thanks a ton.


Last updated: May 18 2021 at 08:14 UTC