Zulip Chat Archive

Stream: maths

Topic: integral rational numbers


view this post on Zulip Johan Commelin (Jun 03 2019 at 07:47):

I want to write a lemma that says that a rational number is an integer if all its p-adic valuations are nonnegative. What is the correct mathlib-idiomatic way to express this? I currently have

lemma integral_of_padic_val_ge_zero (r : ) (h :  p, nat.prime p  padic_val_rat p r  0) :
  (r.num : ) = r :=

view this post on Zulip Johan Commelin (Jun 03 2019 at 07:48):

The conclusion becomes int.cast r.num = r. Is that a good way, or should we use something else?

view this post on Zulip Reid Barton (Jun 03 2019 at 08:45):

There are so many ways one could write this, perhaps it's worth adding a dedicated one is_int

view this post on Zulip Reid Barton (Jun 03 2019 at 08:46):

In general it could be defined as being in the image of int.cast

view this post on Zulip Johan Commelin (Jun 03 2019 at 08:51):

Yeah... that's part of what I'm after with this question

view this post on Zulip Kevin Buzzard (Jun 03 2019 at 08:52):

I have felt for around a year now that for every "troublesome-to-a-mathematician" inclusion (e.g. like int in real) there could be a typeclass on the bigger type (e.g. complex.is_int), or even two typeclasses (the one which stores the int and the one which just says one exists). I have raised this suggestion before. One disadvantage pointed out to me was that now you get a "new int" (in fact several), i.e. {q : rat // is_int q}, which apparently is somehow bad.

view this post on Zulip Johan Commelin (Jun 03 2019 at 08:52):

But maybe using r.num instead of some chosen preimage should make things more computable?

view this post on Zulip Kevin Buzzard (Jun 03 2019 at 08:52):

One advantage was that you remove all the cast headaches; type class inferences shows is_int z -> is_rat z for example.

view this post on Zulip Johan Commelin (Jun 03 2019 at 08:54):

you get a "new int" (in fact several), i.e. {q : rat // is_int q}, which apparently is somehow bad.

Very bad :joy: after all... they aren't equal. Only canonically isomorphic :tears:

view this post on Zulip Kevin Buzzard (Jun 03 2019 at 08:55):

Yeah exactly. In some sense that's what makes it bad! You don't want canonically isomorphic stuff, you want stuff which is one of the standard type theory equals :-/

view this post on Zulip Kevin Buzzard (Jun 03 2019 at 08:56):

In fact perhaps the reason the CS guys tell us it's bad is precisely because we don't have the transfer tactic which will enable us to port all the stuff we want from one type to the canonically isomorphic one.

view this post on Zulip Kevin Buzzard (Jun 03 2019 at 08:57):

[right, as Patrick says, back to mowing the lawn...]


Last updated: May 06 2021 at 18:20 UTC