Rat.floor

Stream: mathlib4

[Heather Macbeth]

@Mario Carneiro you defined Rat.floor last month:

/-- The floor of a rational number `a` is the largest integer less than or equal to `a`. -/
protected def floor (a : Rat) : Int :=
  if a.den = 1 then
    a.num
  else
    let r := a.num / a.den
    if a.num < 0 then r - 1 else r

Is this really correct? It looks like the / means Int.instDivInt_1, i.e. Int.ediv, so this definition is sometimes

Int.ediv a.den a.num

and sometimes not. But in Data.Rat.Floor we need to prove it's always equal to Int.ediv.

[Heather Macbeth]

(I have lost track of what ediv is so will not pronounce on which one is actually correct.)

[Mario Carneiro]

no it's not. That was written for when / meant Int.div

[Mario Carneiro]

with Int.ediv the if a.num < 0 is not necessary, it's just a.num / a.den

[Heather Macbeth]

https://github.com/leanprover/std4/pull/80

[Heather Macbeth]

And mathlib4#1427 to pick up the change from Std.