# 掛け算のオーバーフローを割り算で検知するやつの証明 `if (a * b <= c)`の代わりに`if (a <= c / b)`とするやつです. 次の2つを証明します. * $ab \le c$と$a \le \lfloor{\frac{c}{b}}\rfloor$は同値である * $ab \lt c$と$a \lt \lfloor{\frac{c}{b}}\rfloor$は同値でない ただし,$a, b, c$は非負整数,$b \gt 0$とします. ## 1. $ab \le c$と$a \le \lfloor{\frac{c}{b}}\rfloor$は同値である * $ab \le c \Rightarrow a \le \lfloor{\frac{c}{b}}\rfloor$ $$ ab \le c \\ a \le \frac{c}{b} $$ $a \le \frac{c}{b} \Rightarrow a$の整数部分 $\le \frac{c}{b}$の整数部分であり,$a$は整数だから, $$a \le \lfloor{\frac{c}{b}}\rfloor$$ よって, $$ab \le c \Rightarrow a \le \lfloor{\frac{c}{b}}\rfloor$$ * $a \le \lfloor{\frac{c}{b}}\rfloor \Rightarrow ab \le c$ $$\lfloor{\frac{c}{b}}\rfloor b \le c$$ だから, $$ a \le \lfloor{\frac{c}{b}}\rfloor \\ ab \le \lfloor{\frac{c}{b}}\rfloor b \le c \\ ab \le c $$ よって, $$a \le \lfloor{\frac{c}{b}}\rfloor \Rightarrow ab \le c$$ ## 2. $ab \lt c$と$a \lt \lfloor{\frac{c}{b}}\rfloor$は同値でない 反例: $a = 1, b = 2, c = 3$ $1 \cdot 2 \lt 3$ですが,$1 \lt \lfloor{\frac{3}{2}}\rfloor$ではありません.($\lfloor{\frac{3}{2}}\rfloor = 1$) ちなみに,$ab \lt c \Rightarrow a \lt \lfloor{\frac{c}{b}}\rfloor$は偽ですが,$a \lt \lfloor{\frac{c}{b}}\rfloor \Rightarrow ab \lt c$は1の場合と同様にして示せます.