Hoare論理をCoqでやってみたかったのでソフトウェアの基礎を読んでいた。何かしら書いておかないと自分のなかで記憶がまたゼロに戻ってしまうので何かしら書いておく。当たり前のことをたくさん書く。あと、答えをそのまま書くのはよくないらしいので、Coqの証明を書きたい場面では自然言語での証明を書くに留める。
ソフトウェア的なところ(数学的でないところ)
環境構築
シンタックスハイライティング
コンパイルについて
Lists_Jからは
Require Export Basics_J.
しろというのが出てくるが、その前にBasics_J.vをコンパイルしなければいけない。(自分でBasics_J.vを使ってもよいが、
http://proofcafe.org/sf/sfja.tar.gz
からダウンロードするのが簡単だと思う。)このとき、Basics_J.vを開いた上でメニューの「Compile > Compile buffer」をするのだが、このときBasics_J.vの入っているディレクトリをカレントディレクトリにしておかないとコンパイルが通らなかった。したがって、コンパイルしたいときはcoqideコマンドをそのディレクトリで叩く必要があるっぽい。
コピペについて
ウェブサイトからCoqのコードをコピペしたくなることがあるが、∀はforallに直すなどしないとcoqide上で動いてくれない(本当は何か設定があるのかもしれない)。
そういうわけで、とりあえず次のようなコマンドを作ってxselと一緒に使っていた。
#!/bin/bash sed -r 's/→/->/g' | sed -r 's/∀/forall/g' | sed -r 's/∧/\/\\/g' | sed -r 's/∨/\\\//g' | sed -r 's/∃/exists/g'
自然数の和の可換性(basic_induction)
Basics_Jの演習のbasic_inductionのplus_commについて。
教訓としては、「とりあえずでintrosするのをやめろ」ということになる。
まず日本語で証明を書いてみるとこうなる*1
- nについての帰納法で示す。自然数の帰納法の原理は「P(n)を示すには、(a)P(0)を示し、(b)P(n)が成り立っているという仮定のもとでP(S n)を示せばよい。」であるから、P(n)を「任意のmについて『n+m=m+n』となる」として示す。
- P(0)を示す。0+m=m+0を示せばよいが、これはm=m+0と同じである。
- mについての帰納法でm=m+0を示す。Q(m)を「m=m+0」とする。
- P(n)を仮定し、P(S n)を示す。P(n)、すなわち「任意のmについて、n+m=m+n」を用いてよい。
- mについての帰納法でP(S n)、すなわち「S n+m=m+S n」を示す。Q(m)を新たに「S n+m=m+S n」とする。
- Q(0)、すなわち「S n+0=0+S n」を示す。S n+0=S (n+0)=S(0+n)=S n=0+ S nなので、示された。ここで、1つ目の等式は足し算の定義、2つ目は帰納法の仮定であるP(n)で、∀mでm=0としたもの。3つめは足し算の定義、4つ目も帰納法の定義。
- Q(m)を仮定し、Q(S m)を示す。Q(m)、すなわち「S n+m=m+S n」を用いて、Q(S m)、すなわち「S n+S m = S m + S n」を示す。S n + S m=S (n + S m)=S(Sm + n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はP帰納法の仮定であるP(n)で、∀mでm=S mとしたもの。3つ目は足し算の定義。一方、S m+S n=S(m+S n)=S(Sm+n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はplus_n_Smとしてすでに示されている。3つ目は足し算の定義。
というわけで、まず帰納法を「任意のmについて『n+m=m+n』となる」としてスタートさせなくてはいけないので、
induction n.
と始めなくてはいけない。ここで
intros. induction n.
とすると、固定したmについて証明が始まってしまってうまく行かない。
普段の手書きの証明だと、∀の外に出たり入ったりを無意識にやってしまうが、その辺をちゃんと意識してやらないとなあと思った。
ちなみに、この命題の証明をぼくはAMSから出ているSaunders MacLane, Garrett Birkhoffの「Algebra」でしか見たことがないんですが他に何かありますか。
リストの2回反転(list_exercisesでのrev_involute)
実は何回かソフトウェアの基礎に挑戦していて、何度もLists_Jのlist_exercisesのrev_involuteで苦戦しているので、手書き証明をここに置いておく。4つ目の等式は帰納法の仮定で、5つ目の等式のために補題を置くのがポイントになる。
条件式が常にtrueと等価なWHILE文が停止しないこと
Equiv_JのWHILE_true_nontermの証明が何やってるかよくわからなくなって、段々帰納法ってなんだっけってなったので思い出した話。簡単なところなら帰納法のことが分かっていたつもりになっていたのだが、WHILE言語ぐらい複雑になると落ち着いて振り返らないとよく分からなくなっていた。
示したいのは、
Lemma WHILE_true_nonterm : ∀ b c st st',
bequiv b BTrue →
~( (WHILE b DO c END) / st ⇓ st' ).である。やりたいことは、「bが式BTrueと等価なら、WHILE b DO c END/st⇓st'がcevalの規則によって導かれるわけはない」ということなので、
cevalの規則から導かれる帰納法の原理ceval_indを上手く使って証明しなくてはいけない。
帰納法の原理ceval_indは、3つ組「c/ st ⇓ st'」についての述語「P(c/st ⇓ st')」を示すには、次のことを示せばいいことを教えてくれる。
- ベースケース(前提に3つ組が出ない)
- E_Skip: 任意のstについて、P(SKIP/st⇓st)が成り立つ。
- E_Ass: 任意のst,a,l,nについて、整数式aがstのもとでnに評価されるなら、P(l::=a/st⇓(stのlをnで置換したもの)が成り立つ。
- E_WhileEnd: 任意のb,st,cについて、bがstのもとでfalseに評価されるなら、P(WHILE b DO c END/st⇓st)が成り立つ。
- ステップケース(前提に3つ組が出る)
- E_Seq: 任意のc1,st,st',st'',c2について、P(c1/st⇓st')とP(c2/st'⇓st'')が成り立つなら、P(c1;c2/st⇓st'')が成り立つ。
- E_IfTrue: 任意のb,st,st',c,c'について、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c ELSE c'/st⇓st')が成り立つ。
- E_IfFalse: 任意のb,st,st',c,c'について、bがstのもとでfalseに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c' ELSE c/st⇓st')が成り立つ。
- E_WhileLoop: 任意のb,st,st',st'',cについて、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立ち、P(WHILE b DO c END/st'⇓st'')が成り立つなら、P(WHILE b DO c END/st⇓st'')が成り立つ。
帰納法の原理はP(c/st ⇓ st')の形をしているので、これを示したいことである「任意のc,st,st'について、~( (WHILE b DO c END) / st ⇓ st' )」に合わせるには、P(c0/st0⇓st0')をcを固定した上で
「c0=(WHILE b DO c END)ならば、false」*2と、命題中でならばを使う。
これで示してみる。
- Boolean式bはBTrueと等価とする。c,st,st'は固定する。
- Pを上のように定義し、Pをcevalのの帰納法(この3つ組の導出についての帰納法)で示す。
- E_Skipについて。P(SKIP/st0⇓st0)を示す。これは、「SKIP=(WHILE b DO c END)ならば、false」だが、「SKIP=(WHILE b DO c END)」というのは構文的におかしい。前提が偽なので、全体は真。
- E_Assについて。これも同様に前提が「(l::=a)=(WHILE b DO c END)」となってしまって構文的におかしい。
- E_WhlieEndについて。「bがstのもとでfalseに評価されるならば、P(WHILE b DO c0 END/st⇓st)」を示す。ところが、式bはBTrueと等価なので、前提の「bがstのもとでfalseに評価されるならば」が常に偽になり、全体が真になる。
- E_Seqについて。「(c1;c2)=(WHILE b DO c END)」となり構文的におかしい。
- E_IfTrueについて。やっぱり構文的におかしい。
- E_IfFalseについて。やっぱり構文的におかしい。
- E_WhileLoopについて。「bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b DO c0 END/st0'⇓st0'')が成り立つなら、false」を示す。
- bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b0 DO c0 END/st0'⇓st0'')が成り立つとする。
- 「P(c0/st0⇓st0')」は「c0=(WHILE b DO c END)ならば、false」である。
- 「P(WHILE b DO c0 END/st0'⇓st0'')」は「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。
- 示したいのは「P(WHILE b DO c0 END/st0⇓st0'')」だったが、これは「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。なので、「(WHILE b DO c0 END)=(WHILE b DO c END)」を仮定しよう。ここから、c0=cがわかる。このもとでfalseを導く。
- 「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」と「(WHILE b DO c0 END)=(WHILE b DO c END)」があるので、falseが得られる。示された。
多分、証明を思い付くには、「( (WHILE b DO c END) / st ⇓ st' )」が導出されたとして証明木の一番下がどう導出されたかを見ればよいんだろうなあと思う(？)
