何度目か分からないが、 $\mathbb{X}$ で、小学の算数テストで0で割った答えがどうこうのという話題を見て、思い出したので書いておく。
言うまでもないが、Coqと小学生の算数テストの間には特に関係がない。
Vanilla Coqでのnatの除算
divの定義 を見ると、 0 で割ると 0 になることは定義から分かる。 (y が 0 のとき、 y を返すのだからそう)
Definition div x y :=
match y with
| 0 => y
| S y' => fst (divmod x y' 0 y')
end.
そうすると、気になるのが、矛盾とかが出てきて困らないの?ということだが、特に矛盾は出てきていないっぽい。
x / y = z のとき x = y * z になるはずだけど、 y = 0 だとそれが成り立たない、という話は真っ先に思いつくはずだ。それはその通りである。
Goal ~(forall x y z, (Nat.div x y) = z -> x = y * z).
intro H.
assert (1 = 0 * 0) as C.
apply H; easy.
discriminate C.
Qed.
しかし、Coqの div は割り算の余りは無視する定義になっているので、y = 0 でなくても x / y = z -> x = y * z は成り立たない。
Goal ~(forall x y z, y <> 0 /\ (Nat.div x y) = z -> x = y * z).
intro H.
assert (3 = 2 * 1) as C.
apply H; easy.
discriminate C.
Qed.
なお、 y = 0 以外での除算に関しては、除算と剰余のペアを返す関数 divmod を通じて定義されている。少し変更すれば、ここでの場合分けは不要となるはずである(もちろん、 divmod では場合分けは発生する。次に見るMathComp/ssreflectでは現にそのように定義されている)。
MathComp/ssreflectでのssrnatの除算
ssrnatでは、除算(divn)は、
Definition edivn_rec d :=
fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
Definition divn m d := (edivn m d).1.
と定義されている。記法が独特で慣れないが、除算と剰余のペアを返す関数 edivn の1つ目の要素を返す形で divn が定義されている。
edivn の定義より、 edivn x 0 は (0, x) となることが分かるので、 divn x 0 = 0 となる。
これは divn0 という名前のLemmaが示されている。
ssrnatには、これらを利用したLemmaがたくさん示されている。これらは、0除算を避けられているものもあれば、0より大きいことを明示的に条件に入れているものもある。
例えば、除算結果の不等号に関する補題を2つ見る。
除算結果の不等号に関する補題 leq_div2r
leq_div2r は、 $m \le n$ ならば $m / d \le m / n$ が成り立つ、という補題である。
Lemma leq_div2r d m n : m <= n -> m %/ d <= n %/ d.
$d = 0$ のとき、今回の定義では、 $m / d$ も $n / d$ も共に 0 になるので、この補題は $d = 0$ においても成り立つ。
除算結果の不等号に関する補題 leq_div2l
leq_div2l は、 $0 < d$ かつ $d \le e$ ならば、 $m / e \le m / d$ が成り立つという補題である。
Lemma leq_div2l m d e : 0 < d -> d <= e -> m %/ e <= m %/ d.
これは、 $d = 0$ は条件により明示的に避けられている。もしこの条件がなければ、$d = 0, m / e > 0$ のときに補題が成り立たない(たとえば$m = 1, d = 0, e = 1$のとき)。