リスト反転関数が単射であることを証明する

久々の記事もまたCoqでソフトウェアの基礎ネタです。今回はList_Jにおける練習問題「rev_injective」について。

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.

以上です。

眠気と戦う日々