この記事は Theorem Prover Advent Calendar 2017 の12/18(月)の記事です。

職場でIsabelle勉強会をやっていて、Concrete Semanticsを読んでいます。本記事では、その中から面白かった演習問題3.11を解説します。3章はケーススタディで簡単なプログラム言語IMPの構文と意味論を定義します。意味論はavalという関数で与えられます。その後3.3節でスタックマシンで動作する命令instrの定義および実行関数execを定義します。加えてIMPをコンパイルしてinstrに変換する関数compを定義します。演習問題3.11は、コンパイルした結果が正しいことを示す、以下の命題を証明することです。

exec (comp a r) s rs r = aval a s

これを命題(1)とします。aはIMPで書かれたプログラム、rはレジスタ、sはプログラムの中の変数がどの値を持つかを表す状態、rsはレジスターの状態です。よって、左辺の(comp a r)は、プログラムaをコンパイルして得られる命令列です（結果を格納するレジスタrに引数にとります）。命令列をisとすると、exec is s rs rは、命令列isを状態s、レジスタの状態rsの状態からですべて実行した後のレジスタrの値です。一方、右辺のaval a sは、プログラムaを状態sで評価した値になります。

まずは、exec, compの定義を与えます。それぞれ以下のようになります。

fun exec :: "instr list ⇒ state ⇒ rstate ⇒ reg ⇒ val" where
"exec [] s rs r = rs(r)" |
"exec (i#is) s rs r = exec is s (exec1 i s rs) r"

fun comp :: "aexp ⇒ reg ⇒ instr list" where
"comp (N n) r = [LDI n r]" |
"comp (V v) r = [LD v r]" |
"comp (Plus a1 a2) r = (comp a1 r) @ (comp a2 (r + 1)) @ [ADD r (r + 1)]"

では、さっそく命題の証明にとりかかりましょう。まずはプログラムaの構造に観する帰納法を用いてaのパターンごとにわけます。

theorem "exec (comp a r) s rs r = aval a s"
apply(induction a)

帰納法でパターンごとにわけたら、とりあえず自動証明autoを試します。運がよければこれで最後まで証明してくれます。

theorem "exec (comp a r) s rs r = aval a s"
apply(induction a)
apply(auto)

ひとつだけ証明できずに残りました。

proof (prove)
goal (1 subgoal):
 1. ⋀a1 a2.
       exec (comp a1 r) s rs r = aval a1 s ⟹
       exec (comp a2 r) s rs r = aval a2 s ⟹
       exec (comp a1 r @ comp a2 (Suc r) @ [ADD r (Suc r)])
        s rs r =
       aval a1 s + aval a2 s

これは、a1, a2のそれぞれについて(1)が成り立つときに、a1をコンパイルした命令列にa2をコンパイルした命令列を連結して、さらに最後にそれぞれのレジスタの値を足す命令を追加して実行した結果が、a1を評価した値とa2を評価した値の和に一致すると言ってます。

まずは

exec (comp a1 r @ comp a2 (Suc r) @ [ADD r (Suc r)]) s rs r

に注目します。@は列の連結演算子です。命令列が連結の形になっているものについてのexecについて定理が何もないので補題で追加する必要があります。このとき、execで最後の引数を渡さずレジスタの状態を返すものを定義しておくと便利なので別途関数execnを定義します。

fun execn :: "instr list ⇒ state ⇒ rstate ⇒ rstate" where
"execn [] s rs = rs" |
"execn (i#is) s rs = execn is s (exec1 i s rs)"

exec is s rs rは、execn is s rsが返す結果にレジスタrを適用した結果と一致するはずなのでこれも補題にして証明します。

lemma exec_execn:"exec is1 s rs r = (execn is1 s rs) r"
apply(induction is1 arbitrary: rs)
apply(auto)  
done

命令列の連結に関する補題を定義する準備ができたので定義します。

lemma execn_comp_append:"(execn ((comp a r) @ is2) s rs) = (execn is2 s (execn (comp a r) s rs))"

この補題は、命令列が comp a r @ is2 になっているものは、comp a rをじっこうした結果のレジスタの状態からis2を実行した結果に等しいというものです。残念ながらこの補題はそのままでは証明できません。execnから一度compの部分を除いて命令列がis1 @ is2という連結になっている補題を先に証明します。

lemma execn_dist_append:"(execn (is1 @ is2) s rs) = (execn is2 s (execn is1 s rs))"
apply(induction is1 arbitrary: rs)
apply(auto)
done

これで、先ほどの補題が証明できます。

lemma execn_comp_append:"(execn ((comp a r) @ is2) s rs) = (execn is2 s (execn (comp a r) s rs))"
apply(auto simp add:execn_dist_append)
done

いま証明した補題をautoに与えてもう一度自動証明を試みてみましょう。

theorem "exec (comp a r) s rs r = aval a s"
apply(induction a)
apply(auto simp add:exec_execn execn_comp_append)

残念ながらまだ証明できません。今度は次のようなゴールが残りました。

proof (prove)
goal (1 subgoal):
 1. ⋀a1 a2.
       execn (comp a1 r) s rs r = aval a1 s ⟹
       execn (comp a2 r) s rs r = aval a2 s ⟹
       execn (comp a2 (Suc r)) s (execn (comp a1 r) s rs) r +
       execn (comp a2 (Suc r)) s (execn (comp a1 r) s rs) (Suc r) =
       aval a1 s + aval a2 s

ここでは、帰結の左辺の2項目

execn (comp a2 (Suc r)) s (execn (comp a1 r) s rs) (Suc r)

に注目してみましょう。これは、a1を実行したあとにa2をコンパイルした結果の命令列をレジスタr + 1 (Suc rは、r + 1を表す）に格納した値を表しますが、よく考えるとそれは仮定にある

execn (comp a2 r) s rs r

と一致するはずです。これが一致すれば、どちらもaval a2 sに等しいので、a2に関する項を消すことができるはずです。これが一致していないとIsabelleが判定しているのは、仮定にある rs や r を任意の値としていないからです。そのため帰納法の仮定が使えません。こういうときは帰納法を適用するときにarbitraryをオプションで渡します。すると仮定のrs, rは任意となるので帰結にある命題に適用できます。

theorem "exec (comp a r) s rs r = aval a s"
apply(induction a arbitrary: r rs)
apply(auto simp add:exec_execn execn_comp_append)

すると、以下のようにa2に関する項が消えました。あとはa1に関するものだけです。

proof (prove)
goal (1 subgoal):
 1. ⋀a1 a2 r rs.
       (⋀r rs. execn (comp a1 r) s rs r = aval a1 s) ⟹
       (⋀r rs. execn (comp a2 r) s rs r = aval a2 s) ⟹
       execn (comp a2 (Suc r)) s (execn (comp a1 r) s rs) r = aval a1 s

最後の帰結の左辺をよく見ると、a1をコンパイルしてレジスタrに格納してから、a2をレジスタr + 1に格納するようにコンパイルして実行したレジスタrの値が、aval a1 sと一致すると言っています。a1を実行した結果をrに入れたあとに、それより大きいアドレスを使う命令を実行してもrの値は残るはずなので、それを補題にすれば良さそうです。そこで再び補題を定義して証明します。

lemma comp_left_rs_not_changed:"r1 > r ⟹ execn (comp a r1) s rs r = rs(r)"
apply(induction a arbitrary: r r1 rs)
apply(auto simp add:execn_dist_append)
done

もう一度いま証明した補題をautoに渡して証明します。

theorem "exec (comp a r) s rs r = aval a s"
apply(induction a arbitrary: r rs)
apply(auto simp add:exec_execn execn_comp_append comp_left_rs_not_changed)

すると、

proof (prove)
goal:
No subgoals!

となって証明ができました。

見たようにIsabelleの証明の仕方というのはとりあえずautoで試してみてダメなら残った命題をよく見て次の戦略を考えます。このとき残った命題が証明できそうなら補題を与え、証明できない命題が残っていたら関数の定義か命題が誤っている可能性が高いのでもう一度見直すということになります。

証明を通して今まで気づかなった性質に気づかされることが多くそこから対象への理解がぐっと深まることがあります。証明の一番のメリットとしてはテストにはない網羅性が挙げられますが、実はその途中で得られる深い理解も見逃すことはできません。