Zulip Chat Archive

Stream: new members

Topic: iterate over a multiset/finset


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 07 2020 at 02:11):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 07 2020 at 02:13):

what are you trying to do?

view this post on Zulip 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)

view this post on Zulip Jack J Garzella (May 07 2020 at 02:15):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Reid Barton (May 07 2020 at 02:56):

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

view this post on Zulip Kenny Lau (May 07 2020 at 02:59):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 07 2020 at 03:05):

firstly the roots do not exist

view this post on Zulip Jack J Garzella (May 07 2020 at 03:07):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 07 2020 at 03:10):

it would be very hard to make this a computable function

view this post on Zulip Kenny Lau (May 07 2020 at 03:10):

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

view this post on Zulip Kenny Lau (May 07 2020 at 03:10):

which you can prove using induction on the degree

view this post on Zulip 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 )

view this post on Zulip 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 )

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 07 2020 at 03:14):

what trick?

view this post on Zulip Mario Carneiro (May 07 2020 at 03:15):

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

view this post on Zulip Kenny Lau (May 07 2020 at 03:16):

what on earth

view this post on Zulip Kenny Lau (May 07 2020 at 03:16):

how about #xyp

view this post on Zulip Kenny Lau (May 07 2020 at 03:16):

why can't you capture the empty string?

view this post on Zulip Reid Barton (May 07 2020 at 03:17):

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

view this post on Zulip Kenny Lau (May 07 2020 at 03:17):

like ^xy()$

view this post on Zulip Mario Carneiro (May 07 2020 at 03:17):

@reid that was my thought as well

view this post on Zulip Mario Carneiro (May 07 2020 at 03:18):

I don't follow your solution @kenny

view this post on Zulip Kenny Lau (May 07 2020 at 03:19):

well you said you need to have one capture group

view this post on Zulip Kenny Lau (May 07 2020 at 03:19):

so you can just have it capture the empty string

view this post on Zulip Mario Carneiro (May 07 2020 at 03:19):

I think I tried that, 1 sec

view this post on Zulip Mario Carneiro (May 07 2020 at 03:21):

can't be empty

view this post on Zulip Kenny Lau (May 07 2020 at 03:21):

great

view this post on Zulip Kenny Lau (May 07 2020 at 03:21):

how about something like (.{0})

view this post on Zulip Mario Carneiro (May 07 2020 at 03:21):

there is only a small set of allowed characters

view this post on Zulip Kenny Lau (May 07 2020 at 03:22):

but it is a regex

view this post on Zulip Mario Carneiro (May 07 2020 at 03:22):

#xy

view this post on Zulip Kenny Lau (May 07 2020 at 03:23):

how does that work?

view this post on Zulip Kenny Lau (May 07 2020 at 03:23):

oh

view this post on Zulip Johan Commelin (May 07 2020 at 03:30):

Kenny, you are officially a regex hacker (-;


Last updated: May 11 2021 at 00:31 UTC