questions about `Rat.isInt`

Stream: mathlib4

[Matthew Pocock]

I was reading through the Rat source, and noticed that it defines isInt but then seems to not use it much of anywhere. Is this to avoid needing to constantly unfold the definition? Could this be "fixed" by marking it as simp? While playing about, I also proved the following trivial things that I couldn't see in the library but which I may have overlooked. Are they worth adding, potentially as simp rules? Not sure if I've followed the naming convention or style guide.

/--!
Some theorems describing cases where ℚ corresponds to ℤ.
-/

theorem isInt_ofInt (i : ℤ) : (Rat.ofInt i).isInt = true := by
    simp only [Rat.isInt, Rat.ofInt]

theorem floor_eq_self_if_isInt (a : ℚ) : a.isInt → a.floor = a := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.floor, Int.cast_ite]
    intro ha1
    simp [ha1, ← den_eq_one_iff a]

theorem ceil_eq_self_if_isInt (a : ℚ) : a.isInt → a.ceil = a := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.ceil, Int.cast_ite, Int.cast_add, Int.cast_one]
    intro ha1
    simp [ha1, ← den_eq_one_iff a]

theorem sum_isInt (a b : ℚ) : a.isInt → b.isInt → (a + b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.add_def]
    intro ha hb
    simp only [hb, Nat.cast_one, mul_one, ha]
    simp [Rat.normalize]

theorem sub_isInt (a b : ℚ) : a.isInt → b.isInt → (a - b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.sub_def]
    intro ha hb
    simp only [hb, Nat.cast_one, mul_one, ha]
    simp [Rat.normalize]

theorem mul_isInt (a b : ℚ) : a.isInt → b.isInt → (a * b).isInt := by
    simp only [Rat.isInt, Nat.beq_eq_true_eq, Rat.mul_def]
    intro ha hb
    simp only [ha, hb, mul_one]
    simp [Rat.normalize]

[Johan Commelin]

It seems to be used in the internals of the norm_num tactic.

[Johan Commelin]

• Your first lemma could be a simp lemma. The others not really.
• I would prove all these lemmas in the isInt namespace and call them something like floor_eq, ceil_eq, add, sub, mul, so that the resulting names become isInt.add, etc... Then they can be used with dot-notation, which is really useful.
• The arguments a and b should be implicit in all statements.

[Matthew Pocock]

Johan Commelin said:

• I would prove all these lemmas in the isInt namespace and call them something like floor_eq, ceil_eq, add, sub, mul, so that the resulting names become isInt.add, etc... Then they can be used with dot-notation, which is really useful.

Would this mean creating a file isInt.lean within the rat directory? Shall I put together a pull request?

[Ruben Van de Velde]

What's the goal here? Will this make norm_num more powerful?

[Thomas Murrills]

The .isInt from norm_num is actually a different .isInt: it’s Result.isInt, and can be distinguished by the fact that it takes several arguments (most of them Exprs). This one is Rat.isInt, and afaik is not used by…anything outside of core, yet? I couldn’t find any references for it beyond Lean.Meta.Tactic.LinearArith

[Ruben Van de Velde]

Looks like it's defined in Std and not used there at all?

[Thomas Murrills]

Interestingly, there’s a copy of the definition at Std.Data.Rat.Basic, with the only difference being that this one is @[inline]

[Thomas Murrills]

(The core version is in Lean.Data.Rat)

[Ruben Van de Velde]

Hm. Does the documentation search not index core?

[Ruben Van de Velde]

Anyway, the question would be whether @Mario Carneiro is interested in more API about it, I suppose

[Junyan Xu]

It's docs#Lean.Rat.isInt in core

[Junyan Xu]

Interesting that Lean core uses == for = while Std uses both.

(Oh == is probably Bool-valued comparison ...)

[Yaël Dillies]

Btw all those should be called IsInt.

[Matthew Pocock]

My motivation was that I'm playing with the collatz conjecture, and wanted to prove to myself that a computation that has to go through Rat is guaranteed to have integer values, despite intermediate values having fractional parts. So I thought I could sprinkle things with some isInt constraints, but then found there did not seem to be any machinery to track these through the calculations.

[Matthew Pocock]

Ruben Van de Velde said:

Looks like it's defined in Std and not used there at all?

Right, but there are a ton of places that test den = 1. So it seems odd there's a def that tests exactly this, and every place I looked at where den = 1 is checked, the intention is to show that the Rat is equivalent to an integer. That got my software engineering spidie senses tingling.

[Thomas Murrills]

Yaël Dillies said:

Btw all those should be called IsInt.

Note that they are both Bools, not Props! :)

[Matthew Pocock]

Thomas Murrills said:

Note that they are both Bools, not Props! :)

Being a bool was a bit annoying, to be honest. Would it be worth refactoring this to an IsInt Prop?

[Thomas Murrills]

IsInt certainly sounds nicer to work with and more canonical! What I’m personally not sure of is if there’s another way to phrase it that might be even better (e.g. that there exists an n : ℤ such that a = (n : ℚ)) or if some equivalent definition exists in mathlib already under a different name. loogle might be helpful!

[Yaël Dillies]

Being in the range of Int.cast has the advantage of generalising to any AddGroupWithOne.

[Jireh Loreaux]

Note: the core rats are just pairs of ints and nats, no proofs in the structure. docs#Lean.Rat

[Matthew Pocock]

So while washing dishes and buying milk, I kept getting nagged at a comment in the Rat file -- it notes that Int is embedded in Rat, by which I take it to mean that there is a function to convert each Int into a corresponding Rat, where a wide range of typeclass behaviours are conserved. But I couldn't see the machinery to check any of this. And I think this is the same issue as I was having with isInt writ-large.

So I got to tinkering, and I'm sure that what I've made is well-trod ground, but it seems to me that with some code generation and a couple of typeclasses, we can put "embeds X into Y" on a rather more sound footing, and get a ton of machinery from it for free. I am hoping that I've reinvented poorly something that is already essentially implemented.

-- Claim a natural embedding of one type into another
class NatEmb (α β : Type*) :=
  (embed : α → β)       -- project every α to a corresponding β that is its natural representation
  (embedding : Set β)   -- the set of embedded values, allowing us to track that calculations in β have an interpretation in α

-- we assume (perhaps hastily) that `Coe` always sanely embeds α into β
instance [c : Coe α β] : NatEmb α β where
  embed := Coe.coe
  embedding := c.coe '' Set.univ

-- an example of claiming that an embedding preserves a particular typeclass
-- I would expect that these could (mostly) be code-generated
class NatEmb_LT (α β : Type*)
    [e : NatEmb α β] [LT α] [LT β] :=
    embeds_lt (a₁ a₂) : LT.lt a₁ a₂ ↔ LT.lt (e.embed a₁) (e.embed a₂)

-- this would be hand-written, as somebody needs to make the claim that the natural embedding
-- of Nat into Int exists
instance NatEmb_LT ℕ ℤ where ...

[Jireh Loreaux]

I would claim this is docs#CharZero

[Jireh Loreaux]

Oh, maybe not with LT, but probably if R is a strict ordered semiring then you get LT too.

[Matthew Pocock]

The NatEmb then gives us things like (not compiled, so may contain errors):

-- test if a value is an embedding
def NatEmb.IsEmbedding {α β : Type*) [e : NatEmbed α β] (b : β) := b ∈ e.embedding

-- test if a value is an embedding of an Int
def Int.IsInt { β : Type }  [e : NatEmbed Int β] (b : β) := b.IsEmbedding

I think this gives us a uniform way to ask questions about embeddings.