ここでは、+
の結合律、すなわち任意の 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
Original Copyright © Takahiro Seino, all rights reserved.