萩原、アフェルト 著 「Coq/SSReflect/MathCompによる定理証明」森北出版　の4章を読んでいきます。

ただし、今回はテキストから離れて 自然数の除算のライブラリ div.v を勉強します。

参加をご希望のかたは、管理者までお問い合わせください。

Coq/MathComp をセットアップしたのち、

https://github.com/suharahiromichi/coq/blob/master/csm/csm_4_a_div.v

をダウンロードしておいてください。 資料は改訂していますから、申し訳ありませんが、開始直前に再度ダウンロードしなおしてください。

また、https://github.com/suharahiromichi/coq/blob/master/common/ssromega.v　もダウンロードして同じディレクトリに置き coqc ssromega.v を実行して、ssromega.vo ができていることを確認してください。

問題 1.

整数除算の問題です。10➗3の答えは、3あまり1ですが、(-10)➗3は答えは何でしょうか。 また、10➗(-3) と (-10)➗(-3) の答えはなんでしょうか。

問題 2.

中国人の剰余定理の（比較的易しい）特殊なかたちを証明してください。変数はすべて自然数とします。
d1 と d2 が違いに素のとき、 m と n がd1*d2を法として合同であことと、mとnが法d1で合同かつmとnが法d2で合同であること、は同値である。
coprime d1 d2 -> ( (m == n [mod d1 * d2]) <-> (m == n [mod d1]) /\ (m == n [mod d2]))

次の補題を使ってください：
m と n の積と、最大公約数と最小公倍数の積は同じ。
muln_lcm_gcd : forall m n : nat, lcmn m n * gcdn m n = m * n.

m と n が違いに素なら、m と n の積は最小公倍数と同じ。
coprime_lcm m n : coprime m n -> lcmn m n = m * n.

以上