結合律の証明

ここでは、+ の結合律、すなわち任意の i、j、k について、(i + j) + k = i + (j + k) が成立することを示す。

これまでモジュールの選択には select コマンドを用いていたが、証明を行う際には open コマンドを用いる:

open NAT+ + EQL .

open コマンドを使うと、証明に用いる定数や等式をモジュールに追加できるようになる。

次に定数を宣言する:

-- declaring three arbitrary numbers i,j and k on the sort Nat:
ops i j k : -> Nat .

基底 (i = 0) の推論を行う。

-- base step:
red (0 + j) + k = 0 + (j + k) .
--> should be true.

帰納段階の推論を行う。つまり任意の i について (i + j) + k = i + (j + k) が成立することを仮定したとき、i が 1 増えたとき (すなわち s(i)) のときも表明が保存されることを示す:

-- induction hypothesis:
eq (i + j) + k = i + (j + k) .
-- inductive step:
red (s(i) + j) + k = s(i) + (j + k) .
--> should be true.

オープンしたモジュールは、close コマンドでクローズできる。クローズすると、追加した定数や等式は破棄される:

close

オープンしたまま何度も定数や等式の追加を繰り返すと、これらの宣言が互いに干渉することがある。例えば、次のように奇数か偶数かで場合分けを要するため、以下のような等式を追加したときである:

...
-- case: n is an arbitrary odd number.
eq odd(n) = true .
...
-- case: n is an arbitrary even number.
eq odd(n) = false .
...

このようなトラブルを避けるため、以下のようにこまめにオープン・クローズを行うべきである:

open NAT-EVENODD .
...
-- case: n is an arbitrary odd number.
eq odd(n) = true .
...
close

open NAT-EVENODD .
...
-- case: n is an arbitrary even number.
eq odd(n) = false .
...
close

[Next] 交換律の証明

Original Copyright © Takahiro Seino, all rights reserved.