"a/b の切り上げ" がプログラム上で "(a+b-1)/b" と書けることの証明

# 本記事の概要
本記事は、"$a/b$ の切り上げ" がプログラム上で "$(a+b-1)/b$" と書けることを、数学的に証明した記事です。ネット上に証明が見当たらなかったので、自分の証明を投稿し、もし間違いがあったら指摘してもらおうという魂胆です。私のための備忘録でもあります。というわけで、何か間違いがありましたらご連絡ください。

# 修正履歴
2023年7月3日：$a$ の範囲を整数から非負整数に制限しました。理由は後述します。
2023年7月3日：$\textrm{ceil}(\ (\textrm{double})a/b\ )$ と $(a+b-1)/b$ の書き換えについて、アンダー/オーバーフローに関する注釈を加えました。

# (a+b-1)/b
プログラミングにおける分数の切り上げ処理として、次のようなテクニックが知られています。

「$a$ が非負整数 ( int型など ) かつ $b$ が自然数の時、$a/b$ の切り上げ $\textrm{ceil}(\ (\textrm{double})a/b\ )$ を、$(a+b-1)/b$ と書いてしまうことができる (注[^1])。」

この記法は、double型などによる誤差の心配をする必要が無く、その意味で魅力的です。私もよく使います。

(※) この $(a+b-1)/b$ は整数型同士の演算なので、~~もちろん値は "通常の割り算 $\frac{a+b-1}{b}$" の切り捨てとなります。~~ <font color="red">(2023年7月3日追記) $(a+b-1)/b$ は小数点以下をカットする処理になりますので、これが切り捨て処理となるのは $\frac{a+b-1}{b} \geq 0$ のとき、つまり $a \geq -b+1$ の時になります。$b \geq 1$ ですので、実用上は $a \geq 0$ の時に切り捨て処理となると考えると良いでしょう。本記事でもそのようにしています。</font>これを式に起こすと次の通りです。(右辺の記号については次項で定義します。要するに切り捨てのことです)
```math

    (a+b-1)/b\ =\ \left\lfloor \frac{a+b-1}{b} \right\rfloor

```
(※: 終わり)

しかし、この $\textrm{ceil}$ の書き換えを証明なしで用いるのはちょっと怖いです。一見なぜ成り立つか分からない見た目をしています。ということで、これを証明していきましょう。
といっても、ある定理を認めてしまえば、証明はすぐに終わります。

# 記号の定義
この先用いる記号の定義を示します。すでに理解している人や厳密な定義がいらない人は、読み飛ばしていただいて構いません。

・整数全体の集合として、記号 $\mathbb{Z}$ を用います。( $\mathbb{Z}= \lbrace \ldots , -2, -1, 0, 1, 2, \ldots \rbrace $ )
また、$n$ が整数であることを、集合の記号を用いて $n \in \mathbb{Z}$ と書きます。

・床関数、天井関数の定義を示します。(要するに切り捨てと切り上げのことです)
    
$x$を実数とする。この時、床関数 $\left\lfloor x \right\rfloor$ と天井関数 $\left\lceil x \right\rceil$ はそれぞれ次のように定義される。
```math
\displaylines{
    \left\lfloor x \right\rfloor := n \in \mathbb{Z}\ \ \mathrm{s.t.}\ \ n \leq x < n+1 \\

    \left\lceil x \right\rceil := n \in \mathbb{Z}\ \ \mathrm{s.t.}\ \ n-1 < x \leq n
}
```
上2つの定義式は証明に直接登場するわけではないので、理解せずとも「切り捨てと切り上げ」のイメージだけで証明は追えます。しかし、より厳密な議論が行いたいという方は参考にしてください。

# 命題の整理と、その証明
これまでの話を整理すると、この記事で証明したい命題は次のように書くことができます。<font color="red">(2023年7月3日追記) 書き換えの件は $a$ が非負整数の範囲に限定しましたが、以下の命題は (私の証明が間違いでなければ) $a, b$ が整数 $(b>0)$ の範囲で成り立ちます。</font>
```math

    \forall a, b\in \mathbb{Z}\ (b > 0)\ \left[\ \left\lceil \frac{a}{b} \right\rceil = \left\lfloor \frac{a+b-1}{b} \right\rfloor\ \right]

```
(任意の整数 $a, b\ (b > 0)$ に対し、( [ ] の中身の式 )が成り立つ。)

では、証明しましょう。
#### 証明の前に
証明には、以下の定理を用います。難しく見えますが、要するに「割り算をすると商と余りが1つに決まる」という意味の定理です。$k$ が商、$l$ が余りに対応します。
```math

    \forall a, b\in \mathbb{Z}\ (b > 0)\ \exists! (k, l) \in \mathbb{Z}^2 \ \ \mathrm{s.t.}\ \ a=kb+l\ \ (0 \leq l < b)

```
(任意の整数 $a, b\ (b > 0)$ に対し、$a=kb+l\ \ (0 \leq l < b)$ と書けるような整数 $k, l$ の組がただ一つ存在する。)

これは「除数定理」や「除法の原理」と呼ばれる定理です。証明は他の文献に譲りますが (注[^2])、私たちが小学生の頃から当たり前のように使用している定理ですので、今回はこれを仮定して証明します。

#### 証明
左辺と右辺の値をそれぞれ導き、それらが一致することを示す。
整数 $a$ と自然数 $b$ をとる。この時、除数定理によって $a$ は整数 $k, l\ (0 \leq l < b)$ を用いて次のように書ける。
```math

    a=kb+l

```
これを用いて、左辺を
```math

    \left\lceil \frac{a}{b} \right\rceil = \left\lceil \frac{kb+l}{b} \right\rceil = \left\lceil k + \frac{l}{b} \right\rceil

```
と表す。
$\textrm{(i)}\ l = 0$ のとき
```math

    \left\lceil \frac{a}{b} \right\rceil = \left\lceil k \right\rceil = k

```
である。
$\textrm{(ii)}\ 1 \leq l \leq b-1$ のとき
$0 < \frac{l}{b} < 1$ なので
```math

    \left\lceil \frac{a}{b} \right\rceil = \left\lceil k + \frac{l}{b} \right\rceil = k+1

```
である。

$\textrm{(i)}$, $\textrm{(ii)}$ より、
```math

    \left\lceil \frac{a}{b} \right\rceil =
    \begin{cases}
        k & (l=0) \\
        k+1 & (1 \leq l < b)
    \end{cases}\ \ \cdots (\textrm{A})

```
である。

また、左辺と同様に右辺を
```math

    \left\lfloor \frac{a+b-1}{b} \right\rfloor = \left\lfloor \frac{(kb+l)+b-1}{b} \right\rfloor = \left\lfloor k+1 +\frac{l-1}{b} \right\rfloor

```
と表す。
$\textrm{(a)}\ l = 0$ のとき
```math

    \left\lfloor \frac{a+b-1}{b} \right\rfloor = \left\lfloor k+1 -\frac{1}{b} \right\rfloor

```
であるが、ここで $0 < \frac{1}{b} \leq 1$ なので
```math

    \left\lfloor \frac{a+b-1}{b} \right\rfloor = \left\lfloor k+1 -\frac{1}{b} \right\rfloor = k

```
である。
$\textrm{(b)}\ 1 \leq l \leq b-1$ のとき
$0 \leq \frac{l-1}{b} < 1$ なので
```math

    \left\lfloor \frac{a+b-1}{b} \right\rfloor = \left\lfloor k+1 +\frac{l-1}{b} \right\rfloor = k+1

```
である。

$\textrm{(a)}$, $\textrm{(b)}$ より、
```math

    \left\lfloor \frac{a+b-1}{b} \right\rfloor =
    \begin{cases}
        k & (l=0) \\
        k+1 & (1 \leq l < b)
    \end{cases}\ \ \cdots (\textrm{B})

```
である。

$(\textrm{A})$, $(\textrm{B})$ により、
```math

    \forall a, b\in \mathbb{Z}\ (b > 0)\ \left[\ \left\lceil \frac{a}{b} \right\rceil = \left\lfloor \frac{a+b-1}{b} \right\rfloor\ \right]

```
が示された。$\square$

# 余談
初めての記事なので、いろいろと苦戦しました。Qiita の式番号ってどうやって振るんですかね？

[^1]: ただし、この書き換えは互いに両者がアンダー/オーバーフローしない範囲に限ります。例えば、$a, b$ を int 型範囲内の非負整数 $(b>0)$ とし、$\textrm{INT_MAX}$ を int 型の最大値とします。このとき、$a+b > \textrm{INT_MAX}$ となる場合、$(a+b-1)/b$ は計算過程でオーバーフローします。結果として両者は異なる値を取り、書き換えは成立しなくなります。
プログラムで数値計算を組む場合、受け取る値や、計算途中に登場する値の最大[小]値を考慮して型や演算を設計することは重要です。必要に応じて、より大きな値を扱える型や、多倍長整数などの利用を検討しましょう。
また、$\textrm{ceil}(\ (\textrm{double})a/b\ )$ では double 型へのキャストで情報を失い、切り上げが正しく行われない可能性があるというご指摘を頂きましたが、むしろそれを解消するのが本書き換えの主題です。「～と書いてしまうことができる」という文は、両者が CPU 演算によっていつ何時も同じ値を返す事を主張しているのではなく、概念としての「切り上げ」という演算を、ライブラリ中の関数である $\textrm{ceil}(\ (\textrm{double})a/b\ )$ だけでなく、$(a+b-1)/b$ でも書き表せるという事を主張しています。(以上、2023年7月3日追記)

[^2]: 除数定理の証明については、 https://examist.jp/mathematics/integer/jyohou/ さん (2023年7月2日最終閲覧) が分かりやすいかもしれません。