a / b の時点で float になって誤差が出てしまうので、$\floor{a/b}$ になってくれるとは限りません。というのがよくある説明です。
「誤差が出てしまう」と言われると、「では実際にそういうケースを構築してください」「誤差が出ない範囲を教えてください」と言いたくなってしまうのが人情というものです。 なので、それに答えましょう。
導入
まず、int / int についてですが、「両方のオペランドを float に変換してから除算し、float / float と同様の値を得る」演算ではありません。
いわゆる correctly-rounded な演算です。すなわち、除算を無限精度で行い、それを丸めモード（ここでは tiesToEven）に従って正確に丸めたものです。
なお、片方が float のときは float / float になってしまうようです。
>>> a, b = 2**53+1, 3 >>> a / b 3002399751580331.0 >>> float(a) / float(b) 3002399751580330.5 >>> a / float(b) 3002399751580330.5
note: int() は $0$ 方向への丸め、// は $-\infty$ 方向への丸めです。
a や b がどのくらいの大きさであれば int(a / b) == a // b となってくれるのか？というのが、今回知りたいことです。
上界
さて、自明な反例を挙げておきましょう。
>>> a, b = 2**53+1, 1 >>> int(a / b) 9007199254740992 >>> a // b 9007199254740993
float(a) != a となりうる範囲ではどうしようもないということですね。
以降は、float(a) == a であるところの $1\le a\le 2^{53}$ であればどうか？ということについて考えます。
spoiler: $1\le a\le 2^{53}$ であれば、常に等しくなることが示せます。
証明
いつものように、実数 $x$ を浮動小数点数に丸めたものを $\roundp x$ と書き、浮動小数点数 $a$, $b$ に対して $\roundp{\tfrac ab} = a\oslash b$ と書きます。 前提知識などについて、必要なら下記の記事を見てください。
まず、$a, b \in [1\lldot 2^{53}]\cap\Z$ とし、$a=bq+r$ ($q\in\Z$, $r\in [0\lldot b-1]\cap\Z$) とします。 また、$q\ge 1$ のとき、整数 $k$ は $2^k\le q\lt 2^{k+1}$ を満たすとします。すなわち、$\hfloor q=2^k$ です。
この範囲において $\roundp a=a$, $\roundp b=b$ であることに注意しましょう。
Lemma 1: $\tfrac1b \ge q\cdot2^{-53}$ が成り立つ。
Proof
$$ \begin{aligned} \tfrac1b-q\cdot2^{-53} &\ge \tfrac1b-(q+\tfrac rb)\cdot2^{-53} \\ &= \tfrac1b-\tfrac ab\cdot2^{-53} \\ &= \tfrac1b\cdot2^{-53}\cdot(2^{53}-a) \\ &\ge 0. \qquad\qed \end{aligned} $$
Claim 2: $a\lt b$ のとき、$\floor{a\oslash b} = \floor{\tfrac ab} = 0$ が成り立つ。
Proof
$\tfrac ab\gt 0$ より $a\oslash b\ge 0$ は明らかなので、$a\oslash b\lt 1$ を示せばよい。 $1$ 未満で最大の浮動小数点数は $1-2^{-53}$ であり、$\tfrac ab\lt1-2^{-54} \implies a\oslash b\lt 1$ となる。
整数性より、$a\le b-1$ であることに注意する。 $$ \begin{aligned} \tfrac ab - (1-2^{-54}) &\le \tfrac{b-1}b - (1-2^{-54}) \\ &= -\tfrac1b+2^{-54} \\ &\le -2^{-53}+2^{-54} \\ &\lt 0. \qquad\qed \end{aligned} $$
Claim 3: $a\ge b$ かつ $\hfloor q=q$ のとき、$\floor{a\oslash b} = \floor{\tfrac ab}$ が成り立つ。
Proof
丸めの範囲から、$\floor{a\oslash b} = q$ となる十分条件は次のように書ける。 $$ q-2^{k-54} \le \tfrac ab \le q+1-2^{k-53}. $$
まず、左側の不等式を示す。 $$ \begin{aligned} q-2^{k-54} - \tfrac ab &= q-q\cdot2^{-54} - (q+\tfrac rb) \\ &= -q\cdot 2^{-54} - \tfrac rb \\ &\le 0. \end{aligned} $$ （追記：$q\le\tfrac ab$ から明らかでした）
次に、右側の不等式を示す。最後の不等号は Lemma 1 による。 $$ \begin{aligned} q+1-2^{k-53}-\tfrac ab &= q+1-q\cdot 2^{-53} - (q+\tfrac rb) \\ &= 1-q\cdot 2^{-53} - \tfrac rb \\ &\ge 1-q\cdot 2^{-53} - \tfrac{b-1}b \\ &= \tfrac1b - q\cdot 2^{-53} \\ &\ge 0. \qquad \qed \end{aligned} $$
Claim 4: $a\ge b$ かつ $\hfloor q\lt q$ のとき、$\floor{a\oslash b} = \floor{\tfrac ab}$ が成り立つ。
Proof
丸めの範囲から、$\floor{a\oslash b} = q$ となる十分条件は次のように書ける*1。 $$ q-2^{k-53} \lt \tfrac ab \lt q+1-2^{k-53}. $$
まず、左側の不等式を示す。 $$ \begin{aligned} q-2^{k-53} - \tfrac ab &= q-2^{k-53} - (q+\tfrac rb) \\ &= -2^{k-53} - \tfrac rb \\ &\lt 0. \end{aligned} $$
次に、右側の不等式を示す。最後の不等号は Lemma 1 による。 $$ \begin{aligned} q+1-2^{k-53} - \tfrac ab &= q+1-2^{k-53} - (q+\tfrac rb) \\ &= 1-2^{k-53} - \tfrac rb \\ &\ge 1-2^{k-53} - \tfrac{b-1}b \\ &= \tfrac1b - 2^{k-53} \\ &\gt \tfrac1b - q\cdot 2^{-53} \\ &\ge 0. \qquad\qed \end{aligned} $$
Corollary 5: $\floor{a\oslash b} = \floor{\tfrac ab}$ が成り立つ。
Proof: Claims 2–4 より従う。
所感
これは結構うれしい結果なのではないでしょうか？ たとえば JavaScript のようにデフォルトの数値型が binary64 な言語においても、$2^{53}$ 以下の非負整数であれば、誤差なしで切り捨て除算ができることが保証されるわけですからね*2。
また、扱いたい整数の範囲が $2^{53}$ 以下に収まっているのであれば、（クロック数などによるところの）double を使う高速化が正当化されますね。
$a\gt 2^{53}$ の範囲では、$\floor{a\oslash b} = \floor{\tfrac ab}$ となるのはどういうときでしょうか？ すぐに見つかった反例としては $(a, b) = (2^{54}-2, 3)$ がありました。冷静になるとそれはそうという感じですね。
簡単な不等式評価で済んだとはいえ、もやもや〜っとしたお祈りではなく確信を持って扱えるようになるのはうれしいことです。
おわり
おわりです。
