## Stream: general

### Topic: mu2

#### 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?

#### Chris Hughes (Oct 10 2018 at 10:34):

It's already there and called units int

#### Kenny Lau (Oct 10 2018 at 10:34):

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

#### Kenny Lau (Oct 10 2018 at 10:34):

you used cases 4 times consecutively and produced 16 goals

#### Chris Hughes (Oct 10 2018 at 10:35):

I should have used it to define legendre sym?

#### 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

#### Kenny Lau (Oct 10 2018 at 10:37):

do you have a better idea?

#### Chris Hughes (Oct 10 2018 at 10:40):

I don't see what problem this solves.

#### Johan Commelin (Oct 10 2018 at 10:42):

The legende_symbol takes values in with_zero (units int)

#### 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.

#### Johan Commelin (Oct 10 2018 at 11:52):

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

#### Chris Hughes (Oct 10 2018 at 11:55):

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

#### Johan Commelin (Oct 10 2018 at 12:06):

Because inductive types are pretty to work with?

#### 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

#### 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]

#### 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

#### 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

#### 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