Zulip Chat Archive

Stream: general

Topic: rationals that are actually integers


view this post on Zulip Johan Commelin (Aug 08 2018 at 17:48):

By some elaborate method I have defined a polynomial with coefficients in rat. Now there is a math theorem (which I hope to turn into a Lean theorem) that says that my polynomial actually has coefficients in int. But this is not at all clear from the definition. What is the best way to turn my polynomial into something with integral coefficients?
(For reference, my actual use case with mv_polynomials can be found here: https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L215)
Here is a baby case version of this phenomenon:
Define x=(74)/7x = {7 \choose 4}/7. A priori this is a rational number. But because 77 is prime, it turns out that xx is an integer. This can be turned into Lean, so that we have some x : rat. Now I could do define y := x.num. And then try to prove that (y : rat) = x.
Is this the best way to go about this problem? How would this scale to (mv_)polynomials?

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:49):

I guess you have to insert the maths somewhere. I think your question is asking how to insert the maths. Maybe the answer depends on the maths that needs to be inserted.

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:51):

Right. That might very well be true. In maths-maths there would be just one theorem. "Look, this polynomial actually has int coeffients." In Lean-maths I guess there will be 6 stupid ways, and 1 clever way...

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:52):

So maybe the clever way depends on the math that needs to be inserted. But so far I've usually seen that there is a CS-reason for choosing a particular method. And then the maths that needs to be inserted has to be pushed into the right form.

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:53):

At the end of the day you have some object defined over Q (e.g. a polynomial or something) and you need to prove that there's some object defined over Z which coerces into it. Now of course _if you know the theorem is true_, then for every q in Q you could let z be floor(q) or ceil(q) or numerator(q) or whatever. But you'll still have to prove that \u z = q, and my guess is that the best choice of z will depend on what your proof that q is actually an integer will be.

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:53):

What is the proof, by the way? I've not looked at the maths in your code yet...

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:54):

That is one argument. The other is that you later on want to use z.

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:54):

And that might be more important then getting a convenient form for the proof of \u z = q.

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:54):

There is no proof yet.

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:55):

The proof that I've seen (in Serre's "Local fields") is not trivial. It will need quite some extra work to formalise it.

view this post on Zulip Kevin Buzzard (Aug 08 2018 at 17:56):

My gut feeling is that the best strategy is to figure out what the maths strategy is first. I think that's a more important question than asking about the endgame.

view this post on Zulip Johan Commelin (Aug 08 2018 at 17:58):

Ok. Then I'll have to do a bit of homework first (-;

view this post on Zulip Simon Hudon (Aug 08 2018 at 20:11):

If I had to try, I would try to not step through the rationals. I would use integer division and prove that 7 divides (74)\binom{7}{4} for later consumption (i.e. if you need to multiply x by 7 and prove that it lands back on (74)\binom{7}{4}).

view this post on Zulip Simon Hudon (Aug 08 2018 at 20:12):

(do you use a \begin{array} ... for the choice operator?)

view this post on Zulip Kenny Lau (Aug 08 2018 at 20:13):

you mean \binom?

view this post on Zulip Simon Hudon (Aug 08 2018 at 20:14):

Yes indeed, thanks

view this post on Zulip Johan Commelin (Aug 09 2018 at 04:00):

Alternative: {7 \choose 4}.

view this post on Zulip Johan Commelin (Aug 09 2018 at 04:01):

About your suggestion: In the baby case I agree that it is possible to avoid the rationals. But with my polynomial, I don't see how to do this.

view this post on Zulip Simon Hudon (Aug 09 2018 at 04:42):

Can you show me why that isn't possible? I would have thought that using something like ↑(choose p q ÷ 7) wouldn't pose a problem in a context with rational numbers.

view this post on Zulip Johan Commelin (Aug 09 2018 at 05:31):

Simon, if you look at https://github.com/jcommelin/mathlib/blob/witt/algebra/witt_vector.lean#L215 you see that I take some polynomial Φ\Phi with integral coefficients, and I build another (sequence of) polynomial witt_structure_int \Phi with integer coefficients.

view this post on Zulip Johan Commelin (Aug 09 2018 at 05:31):

But the construction goes via the rationals.

view this post on Zulip Johan Commelin (Aug 09 2018 at 05:31):

I first define witt_structure_rat in terms of X_in_terms_of_W. And those latter polynomials have honest rational coefficients.

view this post on Zulip Johan Commelin (Aug 09 2018 at 05:32):

There might be an entirely different way of defining witt_structure_int, but I don't know this.


Last updated: May 13 2021 at 06:15 UTC