ここでは、+ の交換律、すなわち任意の i、j について、i + j = j + i が成立することを示す。
交換律も結合律と同様に i に関する帰納法で証明する。まず最初に基底を証明する証明譜を示す:
open NAT+ + EQL . -- arbitarily choosen two naturals: ops i j : -> Nat . -- base step: red 0 + j = j + 0 . --> should be true. close
この証明譜を CafeOBJ に読み込ませると、以下に示すように期待しない結果 (j = j + 0) が返ってきてしまった:
-- reduce in %NAT+ + EQL : 0 + j = j + 0 j = j + 0 : Bool (0.002 sec for parse, 1 rewrites(0.001 sec), 6 matches) --> should be true. CafeOBJ>
CafeOBJ の推論エンジンは健全ではあるが完全ではない。従って、true 以外の簡約結果が返ってきたからと言って、すぐにがっかりすることはない。返ってきた項をよく観察すると、左辺は j が得られているが、右辺は j + 0 で書き換えが停止している。もし、j + 0 を j に書き換えることができれば、言い換えると、j + 0 と j が等しいことが言えれば、基底に関する証明は完了する。そこで、次の補題を証明する:
i について、i + 0 = i .この補題を証明する証明譜は、次のようになる:
-- LEMMA1: \forall i \in Nat: i + 0 = i . -- PROOF: open NAT+ + EQL . ops i : -> Nat . -- base step: red 0 + 0 = 0 . --> should be true. -- induction hypothesis: eq i + 0 = i . -- inductive step: red s(i) + 0 = s(i) . --> should be true. close -- Q.E.D.
補題1 を証明する証明譜を CafeOBJ に読み込ませると、以下のような結果が得られる:
-- opening module NAT+ + EQL.. done. -- reduce in %NAT+ + EQL : 0 + 0 = 0 true : Bool (0.001 sec for parse, 2 rewrites(0.000 sec), 2 matches) --> should be true.* -- reduce in %NAT+ + EQL : s(i) + 0 = s(i) true : Bool (0.001 sec for parse, 3 rewrites(0.001 sec), 5 matches) --> should be true.
基底、帰納段階ともに期待した結果が得られたので、補題1 は証明できた。
ここで、交換律を証明する基底の議論に戻る。基底を証明する証明譜に、補題1 を加える:
open NAT+ + EQL . -- arbitarily choosen two naturals: ops i j : -> Nat . -- base step: eq N:Nat + 0 = N . -- use LEMMA1. red 0 + j = j + 0 . --> should be true. close
補題1 を加えた証明譜を CafeOBJ に読み込ませると、以下のような結果が得られる。
-- opening module NAT+ + EQL.. done._* -- reduce in %NAT+ + EQL : 0 + j = j + 0 true : Bool (0.001 sec for parse, 3 rewrites(0.000 sec), 4 matches) --> should be true.
以上で、基底に関する証明が完了した。次に帰納段階の証明を行う。帰納段階では、さらに別の補題を必要とする。帰納段階の証明と、もう一つの補題は練習問題として残す。
Original Copyright © Takahiro Seino, all rights reserved.