A Rat is less than or eq to its ceiling

Stream: Is there code for X?

[Caleb Schultz Kisby]

Is there a mathlib or standard lib lemma stating that a Rat q is less than or equal to q.ceil? This seems like it should be there, but I can't find it.

[Ruben Van de Velde]

Hmm, you're using Rat.ceil rather than Int.ceil? Any reason? docs#le_ceil lists likely theorems for the latter

[Ruben Van de Velde]

I don't see anything offhand to relate the two

[Eric Wieser]

Do we have the lemma that says the two ceils are equal?

[Eric Wieser]

docs#Rat.ceil

[Jireh Loreaux]

docs#Rat.ceil_cast

[Jireh Loreaux]

that's not it

[Caleb Schultz Kisby]

Oh I didn't even think about casting from Int. I'll use Int.ceil, it looks more general & supported.

[Jireh Loreaux]

Lol: docs#Lean.Rat.ceil

[Kevin Buzzard]

It's casting to Int!

[Caleb Schultz Kisby]

Kevin Buzzard said:

It's casting to Int!

Both Rat.ceil and Int.ceil seem to cast to Int, but Int.ceil seems to take any member of a LinearOrderedRing as input?

[Ruben Van de Velde]

docs#Rat.instFloorRing

[Kevin Buzzard]

Yes, Rat.ceil is the odd one out; Nat.ceil casts to nat and Int.ceil casts to int, from a general input for which this makes sense. Rat.ceil is in Std and as far as I can see we don't really develop any API for it in mathlib, I would stick to the mathlib choices.

[Caleb Schultz Kisby]

Oh that makes much more sense (as to why there are two different ceiling functions for Rats)

[Jireh Loreaux]

Actually, I think docs#Rat.instFloorRingRatInstLinearOrderedRingRat should be redefined so that the ceil argument is given explicitly as Rat.ceil and then they'll be defeq.

[Kevin Buzzard]

yeah that sounds like the coolest solution :-)

[Kevin Buzzard]

So we have Rat.ceil (in Std) and Lean.Rat.ceil (in core) -- are either of them ever used? And then we have mathlib's ceil with a ton of API.

[Kevin Buzzard]

wait -- core's so-called "rationals" look a bit suspicious to me...

[Jireh Loreaux]

Yes, it's docs#Lean.Rat. I assume they are used for something.

[Kevin Buzzard]

decision procedures, apparently. Maybe they'll help us to decide whether to persevere with Rat.ceil.

[Ruben Van de Velde]

It's true, at least, if someone wants to PR it:

instance : FloorRing ℚ where
  floor := Rat.floor
  ceil := Rat.ceil
  gc_coe_floor a b := Rat.le_floor.symm
  gc_ceil_coe a b := by
    simp only [Rat.ceil]
    split_ifs with h
    · rw [← Int.cast_le (α := ℚ)]
      simp [Rat.coe_int_num_of_den_eq_one h]
    · rw [← Rat.floor_def, ← _root_.le_sub_iff_add_le, Int.floor_le_sub_one_iff, lt_iff_le_and_ne]
      have : a ≠ b := by
        rintro rfl
        simp at h
      simp [this]