この記事は株式会社 proof ninja の助成を受けて書いています．
研究室の輪読で Benjamin Pierce, Types and Programming Languages (通称TAPL) の3章を読んでいるときに，証明が厄介な部分があったので，Rocq (Coq) をうまく使うと証明が楽になるぞという例として書いてみました．
今回は3章の真偽値と if 式のみがあるシンプルな型なし言語が対象です．言語と簡約規則を以下で定めます．
Inductive term :=
Tru
| Fls
| IfThenElse : term -> term -> term -> term.
Notation "'If' c1 'Then' c2 'Else' c3" := (IfThenElse c1 c2 c3)
(at level 200, right associativity, format
"'[v ' 'If' c1 '/' '[' 'Then' c2 ']' '/' '[' 'Else' c3 ']' ']'").
Reserved Notation "x --> y" (at level 60).
Inductive step : term -> term -> Prop :=
EIfTrue : forall t2 t3, (If Tru Then t2 Else t3) --> t2
| EIfFalse : forall t2 t3, (If Fls Then t2 Else t3) --> t3
| EIf : forall t1 t1' t2 t3, t1 --> t1' -> (If t1 Then t2 Else t3) --> (If t1' Then t2 Else t3)
where "x --> y" := (step x y).
term が今回扱う項を定め，step x y は項 x が項 y に簡約されることを意味します．
x --> y で step x y を表すように notation を作っています．
では，この簡約の行き先が一意であること，すなわち deterministic であることを示します．
Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
教科書では t --> t' の帰納法と場合分けを駆使した証明が書いてあるのですが，この手の場合分けは機械的にできるので機械的にやりましょう．
まず，Tru や Fls はこれ以上簡約されないので Tru --> t や Fls --> t といった場合はありえません．また，(If t1 Then t2 Else t3) --> t は EIf よりさらに場合分けができます．
Tru --> t や (If t1 Then t2 Else t3) --> t の型を持った仮定 H があるときは inversion H で証明を進められます．この処理を Ltac で書きます．
Ltac auto_inversion0 :=
match goal with
H : step Tru _ |- _ => inversion H
| H : step Fls _ |- _ => inversion H
| H : step (IfThenElse _ _ _) _ |- _ => inversion H
end.
一旦この auto_inversion0 を使って証明を進めてみます．
Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
Proof.
intros t t' H.
induction H; intros; auto_inversion0.
t2, t3, t'' : term
H : (If Tru
Then t2
Else t3) --> t''
t0, t1 : term
H1 : t0 = t2
H2 : t1 = t3
H0 : t2 = t''
============================
t'' = t''
goal 2 (ID 147) is:
t2 = (If t1'
Then t2
Else t3)
goal 3 (ID 195) is:
t'' = t''
goal 4 (ID 244) is:
t3 = (If t1'
Then t2
Else t3)
goal 5 (ID 292) is:
(If t1'
Then t''
Else t3) = t''
goal 6 (ID 334) is:
(If t1'
Then t2
Else t'') = t''
goal 7 (ID 383) is:
(If t1'
Then t2
Else t3) = (If t1'0
Then t2
Else t3)
一個目のサブゴールは自明な等式です．
二個目のサブゴールの仮定を見ると Tru --> t1' のような仮定があり，これも auto_inversion0 で処理できることがわかります．
ここで，auto_inversion0 のパターンマッチに当てはまるような仮定がなくなるまで inversion を繰替えすように Ltac を書き換えてみます．
Ltac auto_inversion1 :=
repeat match goal with
H : step Tru _ |- _ => inversion H
| H : step Fls _ |- _ => inversion H
| H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; auto
end.
match の前に repeat を追加し，さらに三つ目の分岐のときに clear H; auto を追加しています．
clear H を追加しないと H : step (IfThenElse _ _ _) _ の形の仮定を無限に inversion してしまい，repeat が停止しなくなってしまいます．
auto は自明なサブゴールを消すためについでに入れてみました．
auto_inversion1 を使って証明をやり直してみましょう．
Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
Proof.
intros t t' H.
induction H; intros; auto_inversion1.
3 goals (ID 466)
t1, t1', t2, t3 : term
H : t1 --> t1'
IHstep : forall t'' : term, t1 --> t'' -> t1' = t''
t'', t0, t4 : term
H2 : Tru = t1
H3 : t0 = t2
H4 : t4 = t3
H1 : t2 = t''
============================
(If t1'
Then t''
Else t3) = t''
goal 2 (ID 467) is:
(If t1'
Then t2
Else t'') = t''
goal 3 (ID 468) is:
(If t1'
Then t2
Else t3) = (If t1'0
Then t2
Else t3)
一個目のサブゴールは何が起きているでしょうか．仮定の H2 の行から等式が続いており，見にくいので，こういうときは私は subst タクティクで一旦整理します．
subst した後のサブゴールは以下です．
3 goals (ID 482)
t1', t3 : term
IHstep : forall t'' : term, Tru --> t'' -> t1' = t''
H : Tru --> t1'
t'' : term
============================
(If t1'
Then t''
Else t3) = t''
goal 2 (ID 467) is:
(If t1'
Then t2
Else t'') = t''
goal 3 (ID 468) is:
(If t1'
Then t2
Else t3) = (If t1'0
Then t2
Else t3)
subst した後は Tru --> t1' が仮定に現れました．これも自動で処理したいところです．
そのために auto_inversion1 の中に subst も追加します．
Ltac auto_inversion2 :=
repeat match goal with
H : step Tru _ |- _ => inversion H
| H : step Fls _ |- _ => inversion H
| H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; auto; subst
end.
Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
Proof.
intros t t' H.
induction H; intros; auto_inversion2.
1 goal (ID 505)
t1, t1', t2, t3 : term
H : t1 --> t1'
IHstep : forall t'' : term, t1 --> t'' -> t1' = t''
t1'0 : term
H5 : t1 --> t1'0
============================
(If t1'
Then t2
Else t3) = (If t1'0
Then t2
Else t3)
サブゴールが一個だけになりました．この結論の両辺は t1' と t1'0 の違い除いて等しいです．このサブゴールを t1' = t1'0 に帰着させるには f_equal タクティクが便利です．
以下が f_equal 適用後です．
t1, t1', t2, t3 : term
H : t1 --> t1'
IHstep : forall t'' : term, t1 --> t'' -> t1' = t''
t1'0 : term
H5 : t1 --> t1'0
============================
t1' = t1'0
このサブゴールは帰納法の仮定である IHstep で証明できます．普通に証明を書いて終わらせてもいいですが，折角なので auto_inversion を最後のステップも証明できるように少し改造します．
Ltac auto_inversion3 :=
repeat match goal with
H : step Tru _ |- _ => inversion H
| H : step Fls _ |- _ => inversion H
| H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; subst; try f_equal; auto
end.
subst の後に try f_equal を追加し，さらに元々あった auto の位置を変えて最後に持ってきました．try tac はゴールにタクティク tac が適用できるならば適用し，できないなら何もしないという意味です．
これを使うと，以下のようになります．
Theorem step_deterministic : forall t t', t --> t' -> forall t'', t --> t'' -> t' = t''.
Proof.
intros t t' H.
induction H; intros; auto_inversion3.
Qed.
すべて証明が終わりました．
このような半自動の証明方法では「この場合がまだ残っていて…」「この場合は示すべきことがこういう形になって…」というようなことを一切考えておらず，とっても楽です．
次に，Exercise 3.5.13 (2)を考えていきます．この問題では E-Funny2 という新しい規則を追加した簡約を考えるので，Rocq でも書いてみます．
Reserved Notation "x -->' y" (at level 60).
Inductive step' : term -> term -> Prop :=
EIfTrue' : forall t2 t3, (If Tru Then t2 Else t3) -->' t2
| EIfFalse' : forall t2 t3, (If Fls Then t2 Else t3) -->' t3
| EIf' : forall t1 t1' t2 t3, t1 -->' t1' -> (If t1 Then t2 Else t3) -->' (If t1' Then t2 Else t3)
| EFunny2 : forall t1 t2 t2' t3,
t2 -->' t2' -> (If t1 Then t2 Else t3) -->' (If t1 Then t2' Else t3)
where "x -->' y" := (step' x y).
今回はこの step' が局所合流性をみたすことを示します．実際には局所合流性より少し強い以下を示します．
Lemma step'_loc_conf : forall t s s',
t -->' s -> t -->' s' ->
exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u)
\/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
この証明はまず t -->' sに関する帰納法を命題
forall s', t -->' s' ->
exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u)
\/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
に適用します．やってみれば分かるのですが，示す命題を forall s' で s' を全称量化しないと失敗します．
また，先ほどの auto_inversion3 を，step ではなく新しい step' にも適用できるように少しタクティクを書き換えます．
Ltac auto_inversion step :=
repeat match goal with
H : step Tru _ |- _ => inversion H
| H : step Fls _ |- _ => inversion H
| H : step (IfThenElse _ _ _) _ |- _ => inversion H; clear H; subst; try f_equal; auto
end.
auto_inversion の引数として step を渡すようにしました．これで step' に対応させるには auto_inversion step' のようにしてやればよいです．
Lemma step'_loc_conf : forall t s s',
t -->' s -> t -->' s' ->
exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u)
\/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
Proof.
intros t s s' H.
revert s'.
induction H; intros; auto_inversion step'.
revert s' で s' を全称量化してから帰納法をし，auto_inversion step' をしました．
サブゴールは以下のようになります．
10 goals (ID 247)
t3, s' : term
============================
exists u : term,
s' = u /\ s' = u \/ s' = u /\ s' -->' u \/ s' -->' u /\ s' = u \/ s' -->' u /\ s' -->' u
goal 2 (ID 255) is:
exists u : term,
t2 = u /\ (If Tru
Then t2'
Else t3) = u \/
t2 = u /\ (If Tru
Then t2'
Else t3) -->' u \/
t2 -->' u /\ (If Tru
Then t2'
Else t3) = u \/ t2 -->' u /\ (If Tru
Then t2'
Else t3) -->' u
(* 省略するけどサブゴールが全部で10個出てくる! *)
たくさんサブゴールが出てくるので，なるべく自動で処理したいです．
まず，存在量化された命題を証明するときは eexists タクティクが便利です．eexists タクティクは existential variable, evar と呼ばれるメタ変数を作り，その変数を使って exists タクティクを適用します．つまり，一個目と二個目のサブゴールに eexists タクティクを適用した結果を見てみると
t3, s' : term
============================
s' = ?u /\ s' = ?u \/
s' = ?u /\ s' -->' ?u \/ s' -->' ?u /\ s' = ?u \/ s' -->' ?u /\ s' -->' ?u
goal 2 (ID 1073) is:
t2 = ?u0 /\ (If Tru
Then t2'
Else t3) = ?u0 \/
t2 = ?u0 /\ (If Tru
Then t2'
Else t3) -->' ?u0 \/
t2 -->' ?u0 /\ (If Tru
Then t2'
Else t3) = ?u0 \/ t2 -->' ?u0 /\ (If Tru
Then t2'
Else t3) -->' ?u0
となっています．? から始まる識別子が evar です．
一個目は \/ でつながれた条件の一つ目である s' = ?u /\ s' = ?u が，?u と s' を単一化すれば自明に成り立つことがわかります．このように evar に単一化を施した上で auto で解けるような命題は eauto タクティクで証明できます．
二個目は \/ でつながれた最後の条件である
t2 -->' ?u0 /\ (If Tru
Then t2'
Else t3) -->' ?u0
が ?u0 と t2' を単一化すれば成り立ちます．/\ の二個目の条件は constructor タクティクで証明できます．タクティク tac で証明できる命題が /\ や \/ などの論理結合子の中にあるような命題は firstorder tac で証明できます．
つまり，今回は constructor と eauto を組み合わせて firstorder (try constructor; eauto を試します．
Lemma step'_loc_conf : forall t s s',
t -->' s -> t -->' s' ->
exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u)
\/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
Proof.
intros t s s' H.
revert s'.
induction H; intros; auto_inversion step';
try solve [eexists; firstorder (try constructor; eauto)].
solve [tac] はタクティク tac でサブゴールを証明できれば証明し，できなければ失敗する，というタクティクです．たとえば eexists や firstorder はサブゴールの状態を変えますが，solve [ ... ] の中に入れてやることで，証明が完了しないサブゴールには何も適用しないでおく，ということができます．
上の証明スクリプトで証明の状態は以下のようになります．
2 goals (ID 741)
t1, t1', t2, t3 : term
H : t1 -->' t1'
IHstep' : forall s' : term,
t1 -->' s' ->
exists u : term,
t1' = u /\ s' = u \/
t1' = u /\ s' -->' u \/ t1' -->' u /\ s' = u \/ t1' -->' u /\ s' -->' u
t1'0 : term
H5 : t1 -->' t1'0
============================
exists u : term,
(If t1'
Then t2
Else t3) = u /\ (If t1'0
Then t2
Else t3) = u \/
(If t1'
Then t2
Else t3) = u /\ (If t1'0
Then t2
Else t3) -->' u \/
(If t1'
Then t2
Else t3) -->' u /\ (If t1'0
Then t2
Else t3) = u \/
(If t1'
Then t2
Else t3) -->' u /\ (If t1'0
Then t2
Else t3) -->' u
goal 2 (ID 1067) is:
exists u : term,
(If t1
Then t2'
Else t3) = u /\ (If t1
Then t2'0
Else t3) = u \/
(If t1
Then t2'
Else t3) = u /\ (If t1
Then t2'0
Else t3) -->' u \/
(If t1
Then t2'
Else t3) -->' u /\ (If t1
Then t2'0
Else t3) = u \/
(If t1
Then t2'
Else t3) -->' u /\ (If t1
Then t2'0
Else t3) -->' u
サブゴールが残り二個になりました．この二つは手動で証明します．solve [ ... ] の中で使った eexists; firstorder (try constructor; eauto) は残りの証明でも有用だったのでこれも Ltac にしておきました．
Ltac fo := eexists; firstorder (try constructor; eauto).
Lemma step'_loc_conf : forall t s s',
t -->' s -> t -->' s' ->
exists u, (s = u /\ s' = u) \/ (s = u /\ s' -->' u)
\/ (s -->' u /\ s' = u) \/ (s -->' u /\ s' -->' u).
Proof.
intros t s s' H.
revert s'.
induction H; intros; auto_inversion step'; try solve [fo].
- destruct (IHstep' _ H5).
destruct H0 as [|[|[]]]; destruct H0; subst; fo.
- destruct (IHstep' _ H5).
destruct H0 as [|[|[]]]; destruct H0; subst; fo.
Qed.
ということで，真面目にやると場合分けがたくさんあって大変な証明ですが，ほとんど自動で，かつ命題の中身について真面目に考えることなく証明できました．
TAPLのこの辺の証明を見る度に「Rocqでやったほうが早くない？？」と思っていたので，その実証でした．
また，TAPLの模範解答には「二つの導出のペアの帰納法を使う」と書いてあるのですが，実際には普通の(導出一個の)帰納法でよいことが実証されています．
最後に，証明全体のコードをは以下に置きます．
https://gist.github.com/mir-ikbch/0152f50c37c14caac7687242c85f011b