mu2

Stream: general

[Kenny Lau]

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]

It's already there and called units int

[Kenny Lau]

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

[Kenny Lau]

you used cases 4 times consecutively and produced 16 goals

[Chris Hughes]

I should have used it to define legendre sym?

[Kenny Lau]

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]

do you have a better idea?

[Chris Hughes]

I don't see what problem this solves.

[Johan Commelin]

The legende_symbol takes values in with_zero (units int)

[Chris Hughes]

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]

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

[Chris Hughes]

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

[Johan Commelin]

Because inductive types are pretty to work with?

[Chris Hughes]

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]

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]

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

[Mario Carneiro]

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]

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