Zulip Chat Archive

Stream: general

Topic: mu2


view this post on Zulip Kenny Lau (Oct 10 2018 at 10:33):

mu2 is the inductive type with two terms: 1 and -1. It is closed under negation, multiplication, and power. This type casts to int as well as zmodp, and is injective as long as p is an odd prime. It can also be cast to the units of ang ring. This type can be used in defining the sign of a permutation, as well as for proving quadratic reciprocity. Without this type, we would need 1000 auxiliary lemmas in the form of (? = 1 or ? = -1). Are these reasons good enough to define this type?

view this post on Zulip Chris Hughes (Oct 10 2018 at 10:34):

It's already there and called units int

view this post on Zulip Kenny Lau (Oct 10 2018 at 10:34):

Then why didn’t you use it in your QR proof?

view this post on Zulip Kenny Lau (Oct 10 2018 at 10:34):

you used cases 4 times consecutively and produced 16 goals

view this post on Zulip Chris Hughes (Oct 10 2018 at 10:35):

I should have used it to define legendre sym?

view this post on Zulip Kenny Lau (Oct 10 2018 at 10:36):

legendre symbol can be 0, so don’t replace it with another definition. Instead, define another partial legendre symbol and prove that they are equal

view this post on Zulip Kenny Lau (Oct 10 2018 at 10:37):

do you have a better idea?

view this post on Zulip Chris Hughes (Oct 10 2018 at 10:40):

I don't see what problem this solves.

view this post on Zulip Johan Commelin (Oct 10 2018 at 10:42):

The legende_symbol takes values in with_zero (units int)

view this post on Zulip Chris Hughes (Oct 10 2018 at 11:46):

I don't see what problem this solves.

That said, I didn't give this issue that much thought, and it may well be better to change it. It will probably be changed if anyone wants to generalize stuff, and do the Jacobi symbol.

view this post on Zulip Johan Commelin (Oct 10 2018 at 11:52):

@Kenny Lau def μ₂ := bool. Does that work?

view this post on Zulip Chris Hughes (Oct 10 2018 at 11:55):

Why would you define it again when there's already units int?

view this post on Zulip Johan Commelin (Oct 10 2018 at 12:06):

Because inductive types are pretty to work with?

view this post on Zulip Chris Hughes (Oct 10 2018 at 12:33):

You can always define a units_int.rec_on, that looks exactly like what mu2.rec_on would look like. mu2.rec_on wouldn't even be that nice, because it would split it into the cases mu2.one and mu2.neg_one, not has_one.one and has_neg.neg has_one.one

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:27):

These are interesting questions. They are pure implementation issues so as a mathematician with 30 years of experience I find that I have nothing to say. I guess one thing I don't understand is why it even matters. You make a random implementation decision and then you prove all the lemmas you need for your interface, and then who cares how the type is defined. Right? [I'm assuming not]

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:31):

I don't suggest using with_zero (units int), it doesn't interact with other numeric types well enough, I think

view this post on Zulip Mario Carneiro (Oct 10 2018 at 20:31):

I would just use int and prove that it has absolute value <= 1, or it is a unit if not zero, or something like that

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:41):

Just use X [has_one X] [has_mul X] [has_neg X]


Last updated: May 13 2021 at 04:21 UTC