## Stream: new members

### Topic: iterate over a multiset/finset

#### Jack J Garzella (May 07 2020 at 02:08):

If I want to take a multiset (or a finset or a set for that matter), and I wish to match on this in a similar way to a list, i.e.

match my_multiset with
| [] := sorry
| (a :: b) := sorry


how would I go about doing this?

#### Mario Carneiro (May 07 2020 at 02:11):

in short, you can't, at least not using match

#### Mario Carneiro (May 07 2020 at 02:12):

You can write custom recursion principles, but they don't interact with match which is reserved for pattern matching on inductive types

#### Mario Carneiro (May 07 2020 at 02:13):

what are you trying to do?

#### Jack J Garzella (May 07 2020 at 02:15):

What I'm trying to do is implement an algorithm that performs a specified action for each element in a multiset (really it's underlying set)

#### Jack J Garzella (May 07 2020 at 02:15):

In this case, adjoining all of the roots of a polynomial to a field

#### Jack J Garzella (May 07 2020 at 02:16):

Given one element, I know what to do, but I don't know how to get elements out of the multiset I have

#### Mario Carneiro (May 07 2020 at 02:18):

You can use multiset.fold, but keep in mind that the operation you fold must be commutative

#### Jack J Garzella (May 07 2020 at 02:48):

Ok, but there is no way to convert a finset to a list containing the elements in that finset? (say I don't care about the order)

#### Reid Barton (May 07 2020 at 02:56):

Well you might not care about the order, but somebody else might care.

#### Kenny Lau (May 07 2020 at 02:59):

you can, but not computably (at least in general)

#### Jack J Garzella (May 07 2020 at 03:04):

Kenny Lau said:

you can, but not computably (at least in general)

So, if I were to decide I'm willing to give up on computation, how would I go about it?

#### Kenny Lau (May 07 2020 at 03:05):

in your case, "adjoin all the roots of a polynomial to a field" does not literally mean, extract the roots of said polynomial as a multiset of some unspecified type, and then do this operation of adjoining each one of them to a field

#### Kenny Lau (May 07 2020 at 03:05):

firstly the roots do not exist

#### Jack J Garzella (May 07 2020 at 03:07):

Yes, my multiset is really of the irreducible factors of my polynomial

#### Jack J Garzella (May 07 2020 at 03:09):

My "operation" is adjoining a single root of one irreducible factor, and then recomputing the irreducibles over the new field

#### Kenny Lau (May 07 2020 at 03:10):

it would be very hard to make this a computable function

#### Kenny Lau (May 07 2020 at 03:10):

instead you can prove the statement that splitting field exists for any polynomial over any field

#### Kenny Lau (May 07 2020 at 03:10):

which you can prove using induction on the degree

#### Kenny Lau (May 07 2020 at 03:10):

(I'm a bit surprised that field_theory.splitting_field does not contain this statement @Chris Hughes )

#### Kenny Lau (May 07 2020 at 03:12):

so let's say this is an XY-problem (do we need a new link like #mwe but for #xy? @Mario Carneiro )

#### Mario Carneiro (May 07 2020 at 03:14):

the link for XY-problem contains neither of the letters x nor y so I can't use same trick as for #mwe

what trick?

#### Mario Carneiro (May 07 2020 at 03:15):

https://leanprover.zulipchat.com/#narrow/stream/236604-Zulip-meta/topic/.23mwe.20bot/near/195720265

what on earth

#### Kenny Lau (May 07 2020 at 03:16):

why can't you capture the empty string?

#### Reid Barton (May 07 2020 at 03:17):

https://en.wikipedia.org/wiki/XY_problem#x

#### Kenny Lau (May 07 2020 at 03:17):

like ^xy()\$

#### Mario Carneiro (May 07 2020 at 03:17):

@reid that was my thought as well

#### Kenny Lau (May 07 2020 at 03:19):

well you said you need to have one capture group

#### Kenny Lau (May 07 2020 at 03:19):

so you can just have it capture the empty string

#### Mario Carneiro (May 07 2020 at 03:19):

I think I tried that, 1 sec

can't be empty

great

#### Kenny Lau (May 07 2020 at 03:21):

how about something like (.{0})

#### Mario Carneiro (May 07 2020 at 03:21):

there is only a small set of allowed characters

#### Kenny Lau (May 07 2020 at 03:22):

but it is a regex

#xy

#### Kenny Lau (May 07 2020 at 03:23):

how does that work?

oh

#### Johan Commelin (May 07 2020 at 03:30):

Kenny, you are officially a regex hacker (-;

Last updated: May 11 2021 at 00:31 UTC