iterate over a multiset/finset

Stream: new members

[Jack J Garzella]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

what are you trying to do?

[Jack J Garzella]

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]

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

[Jack J Garzella]

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]

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

[Jack J Garzella]

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]

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

[Kenny Lau]

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

[Jack J Garzella]

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]

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]

firstly the roots do not exist

[Jack J Garzella]

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

[Jack J Garzella]

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

[Kenny Lau]

it would be very hard to make this a computable function

[Kenny Lau]

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

[Kenny Lau]

which you can prove using induction on the degree

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

what trick?

[Mario Carneiro]

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

[Kenny Lau]

what on earth

[Kenny Lau]

how about #xyp

[Kenny Lau]

why can't you capture the empty string?

[Reid Barton]

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

[Kenny Lau]

like ^xy()$

[Mario Carneiro]

@reid that was my thought as well

[Mario Carneiro]

I don't follow your solution @kenny

[Kenny Lau]

well you said you need to have one capture group

[Kenny Lau]

so you can just have it capture the empty string

[Mario Carneiro]

I think I tried that, 1 sec

[Mario Carneiro]

can't be empty

[Kenny Lau]

great

[Kenny Lau]

how about something like (.{0})

[Mario Carneiro]

there is only a small set of allowed characters

[Kenny Lau]

but it is a regex

[Mario Carneiro]

#xy

[Kenny Lau]

how does that work?

[Kenny Lau]

oh

[Johan Commelin]

Kenny, you are officially a regex hacker (-;