Zulip Chat Archive

Stream: new members

Topic: Recurse on `finset`

Marcus Rossel (Jan 12 2021 at 14:27):

Is there some way to define a function recursively over a finset, where each "iteration" has access to one element of the set?
First I thought this shouldn't be possible, since choosing an element from a set isn't really possible. But then again there's classical.choice.

I want to do something for each element in a finset and so far my approach has been to sort the set into a list first, which requires some kind of order on the elements though.

So far I've only found finset.strong_induction_on, which doesn't suit my case (I think).

Alex J. Best (Jan 12 2021 at 14:37):

Maybe docs#finset.induction_on'

Logan Murphy (Jan 12 2021 at 14:37):

I haven't done a ton of this kind of stuff with finset, but maybe you can do the recursion on the underlying multiset (lists up to permutation) and then provide a proof that your function doesn't introduce duplicates

Marcus Rossel (Jan 12 2021 at 14:40):

Perhaps I should clarify my exact use case:
I have some object o : O and p : finset P. For each x ∈ p I need to update something about o by using p. I happen to know that the order in which the xs are chosen doesn't matter.

Reid Barton (Jan 12 2021 at 14:49):

It might help to know more about O and P

Reid Barton (Jan 12 2021 at 14:49):

for example, if O = P = nat and "update something about o using p" means "add p to o" then this is finset.sum

Reid Barton (Jan 12 2021 at 14:50):

more generally, if P acts on O through a commutative monoid of operations then again you can express it directly as a kind of fold/product

Marcus Rossel (Jan 12 2021 at 14:54):

@Reid Barton Thanks! finset.fold is what I was looking for.

Last updated: Dec 20 2023 at 11:08 UTC