久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。
問題のTheorem
Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2.
ソフトウェアの基礎ではCoqコードではありませんが、型Xの部分をnatとしてCoqコードにするとこんな感じになります。 これについて証明していきましょう。
定理の意味を確認
まずはとにかく定理を見てみましょう。
Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2.
revはリストを反転させる関数です。 つまりこの定理は、
rev関数の結果が一致するならば、引数のリストは一致する
ということになります。
証明開始
まずはとにかくintrosしてみましょう。
l1: natlist l2: natlist H: rev l1 = rev l2 =========================== l1 = l2
定理の中にあった仮定の「反転したリスト同士が一致した時」が前提として用意出来ました。 今回の証明ではこれを使います。
前提を見てみる
それでは重要な前提を確認。
H: rev l1 = rev l2
反転したリストは一致する
です。
ということは、どうやらsubgoalのl1 = l2
をどうにかして反転したリストの形式に変更すれば証明できそうです。
どうすればいいでしょうか。
リストの性質
そこで、リストの性質を見なおしてみましょう。 リストは偶数回反転させることで、元のリストと等しくなるという定理がありました。 つまり、
l1 = rev (rev l1) l1 = rev (rev (rev (rev l1))) l1 = rev (rev (rev (rev (rev (rev ...
rev l1
という形を見つけられました。
これを証明することで利用することが可能になります。
この補題をrev_involutive
として、利用しましょう。
「ソフトウェアの基礎」を最初から順にやっていると、きっとすでに定義されているかと思います。
反転した反転リスト
それではrev_involutiveを使ってみます。 先ほどintrosしたばかりの定理に対して、rewriteしてみましょう。
Proof. intros. rewrite <- rev_involutive.
l1: natlist l2: natlist H: rev l1 = rev l2 =========================== l1 = rev (rev l2)
求めていたものが手に入りました。 あとは作業です。
Proof. intros. rewrite <- rev_involutive. rewrite <- H.
l1: natlist l2: natlist H: rev l1 = rev l2 =========================== l1 = rev (rev l1)
Hによって書き換えると、今度は先程も見た形です。 今度はrev_involutiveを逆向きに適用しましょう。
Proof. intros. rewrite <- rev_involutive, rewrite <- H. rewrite -> rev_involtive
l1: natlist l2: natlist H: rev l1 = rev l2 =========================== l1 = l1
はい、あとはいつもの様にして終わりです。 最終的にはこんな感じ。
Proof. intros. rewrite <- rev_involutive, rewrite <- H. rewrite -> rev_involtive reflexivity. Qed.
以上です。