rationals that are actually integers

Stream: general

[Johan Commelin]

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 = {7 \choose 4}/7$. A priori this is a rational number. But because $7$ is prime, it turns out that $x$ 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?

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Johan Commelin]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

There is no proof yet.

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Kenny Lau]

you mean \binom?

[Simon Hudon]

Yes indeed, thanks

[Johan Commelin]

Alternative: {7 \choose 4}.

[Johan Commelin]

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.

[Simon Hudon]

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.

[Johan Commelin]

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.

[Johan Commelin]

But the construction goes via the rationals.

[Johan Commelin]

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

[Johan Commelin]

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