いま話題の9÷0=0をCoqで証明

Quotients.v

Require Import Coq.ZArith.ZArith.
Require Import Coq.QArith.QArith.

(* テーマ： Coqで 9÷0=0を証明する *)


(* 整数上の除算 *)

Theorem Quotient_1: (9 / 0 = 0)%Z.
Proof.
compute.
reflexivity.
Qed.

(* 有理数上の除算。 9#1は分数(9/1)を意味する *)

Theorem Quotient_2: ((9 # 1) / 0 = 0)%Q.
Proof.
compute.
reflexivity.
Qed.

(*

解説

Coqは一般的なプログラミング言語と違って
計算不可能な場面(無限ループやランタイムエラー)を含めない。

したがって、部分関数を定義するには一工夫必要である。

具体的には以下の4つの方法が考えられる。(恐らくこれでおよそ網羅されているだろう。)

1. option(HaskellにおけるMaybe)などのモナドで包む。
2. 定義域内であることの証明を引数に含める。
3. 定義域外の場合は適当な値を返すようにする。
4. 定義域外の場合も値を返すが、その値が何であるかについて議論できないようにする。

1や2の方法が面倒くさいのは容易に想像がつくだろう。
この手法は、依存型で定義された関数で戻り値の型が空集合になりうる場合に必要になる可能性が
あるが、その他の場面で使う必要はあまり感じない。

4. は実際にR(実数型)で使われている手法である。
そもそも実数はCoqの直観主義システムでは公理なしには作れない。
そこでCoqのRealsライブラリでは、実数の基本的な演算を、
具体的な計算方法を示すのではなく、公理によって定義している。
このとき、a/bはb=0でも定義されるが、
b=0のときはその値について何ら議論をすることはできない、というような仕組みになっている。

ZやQの除算は、計算手順が具体的に定義されている。
Opaqueコマンドなどで計算手順を封印すれば、4. の方法を使えないこともないが、
ベータ簡約で計算式を直接的に評価できる利点のほうが大きいので、封印は行なっていない。
したがって、定義域外である9/0に対して、もっとも中立的な値である0が割り当てられているのである。

*)