FinEnum

Stream: general

[Shreyas Srinivas]

Love this. Since you are writing about discrete mathematics, I was wondering if the book could guide users on how to move between Finsets and finite maps. When it is advisable to use Fintype, FinEnum, and just Fin n and so on.

[Eric Wieser]

(I think docs#FinEnum is probably not currently that useful for anything, and could be redesigned from scratch)

[Shreyas Srinivas]

Well, I used it in finite graphs.

[Shreyas Srinivas]

It was easy to extract an ordering of neighbours from a Finset.

[Shreyas Srinivas]

See : https://github.com/Shreyas4991/DGAlgorithms/blob/cb167b1911aca1a4158e9d1069804306ebd98a7d/DGAlgorithms/Models/Fingraph.lean#L132

[Shreyas Srinivas]

Fintype only gives you a Finset. Not great when you want to write a computation iterating over it, which can be the case for a lot of proofs in discrete math.

[Bhavik Mehta]

Shreyas Srinivas said:

Fintype only gives you a Finset. Not great when you want to write a computation iterating over it, which can be the case for a lot of proofs in discrete math.

With regards to discrete maths, it is absolutely true that FinEnum is pretty useless, a Finset is indeed plenty when you want to have a proof with iteration. The difference happens only when you want to work with a finset together with a specific ordering, which is a rare (non-existent?) situation in discrete mathematics.

[Shreyas Srinivas]

Well. Here is an easy example: round robin algorithm for finding EF 1 allocations of indivisible goods

[Shreyas Srinivas]

You start by allocating goods ( to say two agents) in some order determined by their valuation functions

[Shreyas Srinivas]

This is used to prove the existence of EF1 allocations

[Bhavik Mehta]

I think this discussion is not on topic any more, but - just going off the wikipedia description - the way this is typically done in mathlib is picking an ordering of the elements (wikipedia's step 1: "Number the people arbitrarily from 1 to n") by taking a list representative of the given finset, and running step 2 with a list fold. This immediately gives you the existence of EF1 allocations that you ask for.

[Shreyas Srinivas]

How is the ordering of the elements chosen? FinEnum gives one directly.

[Shreyas Srinivas]

Anyway, this is the kind of confusion that beginners like me tend to have

[Bhavik Mehta]

Shreyas Srinivas said:

Anyway, this is the kind of confusion that beginners like me tend to have

Right, I think this is a great example of why mentioning FinEnum increases the confusion! Let's continue the EF1 discussion elsewhere

[Shreyas Srinivas]

Can some selection messages be moved to a different thread? EF1 is just one example. I am thinking of all the problems whose solutions are some dynamic programming style recurrence.

[Yaël Dillies]

Yes, somehow file#Combinatorics/Enumerative/DoubleCounting is a stupidly easy but very crucial file

[Patrick Massot]

Shreyas, this is probably a nice example but not relevant to MIL which is about mathematics.

[Jeremy Avigad]

@Shreyas Srinivas For verifying combinatorial computation, you want to choose efficient representations and use the mathematical objects as ideal references to state and prove correctness. I agree that Finset and Fintype are not good for computation! As Patrick says, that's out of scope for MIL, though it is a good topic for lots of papers and tutorial.

[Notification Bot]

25 messages were moved here from #general > Finset vs Finite by Kim Morrison.

[Kim Morrison]

I have moved messages here, to try to increase the signal to noise ratio of the other thread.

(Avoiding the need for this in the first place may have been helpful!)

[Shreyas Srinivas]

@Kim Morrison : Apologies, I didn't want to side track that discussion. My primary goal was to bring up the kind of confusion that beginners face with finite types. Also, there is such a huge overlap between discrete mathematics and theoretical CS (especially complexity and algorithms theory) that I didnt quite see these topics as "not math". In fact the example I picked comes from social choice theory where mathematicians (Nash, Gale, Shapley, Steinhaus etc) have contributed a lot.

[Shreyas Srinivas]

@Jeremy Avigad : I am not trying to write efficient combinatorial procedures. Just prove things. Some proofs are just most elegantly described as recursive procedures upon which we do induction. I recall that this is also sometimes true in pure mathematics from Halmos' proof of the Steinitz lemma in his FDVS book. In such cases there is a "choose some ordering of elements" step, and my point is FinEnum does that for free.

[Eric Wieser]

Shreyas Srinivas said:

Fintype only gives you a Finset. Not great when you want to write a computation iterating over it, which can be the case for a lot of proofs in discrete math.

My claim is not that "FinEnum is a useless idea", but rather "FinEnum is a poorly-executed idea". The API works in terms of bijections with Fin, but every instance goes back and forth with lists, making many things O(n) which should be O(1)