自然数とリスト: rewriteなど (3.2)

x=0の場合は終わったので、残ったゴールはこれです。

-------------------------
S x < S x + S x

これを証明するには…なにか、このくらいはさっきImportしたArith標準ライブラリで証明されていないでしょうか。CoqIDEでは

SearchAbout (_ < _ + _).

と打ち込むか、F2キーを押して (_ < _ + _) を検索すると…

「(_ < _ + _) という形のゴールに apply できそうなライブラリ定理の一覧」が表示できます。便利です。

表示された一覧の中に、わたしが見た限りでは直接使えそうなものはなかったのですが、近い物がありました。

plus_lt_compat_l : forall n m p: nat, n<m -> p+n < p+m

これ。p+n < p+m というのは S x < S x + S x の形にはなっていませんが、これを使えば "S x + 0 < S x + S x" なら証明できそう。"S x" と "S x + 0" は等しいので、これが示せれば十分ですよね。

十分ではありません。まず「"S x" と "S x + 0" は等しい」から証明してあげないとCoqさんは納得してくれません。納得させます。

 assert (S x = S x + 0).

初回にやった assert (X:=t) というtacticは、tという証明を書いて、その型の命題を仮定に追加するものでした。今回の assert (命題) は、「(命題)が成り立つので仮定に足してくれ！証明は今からやる！」とCoqさんに伝えるものです。

assertすると、メインの証明はいったん脇に置いておいて、assertされた命題の証明モードに入ります。ゼロを足しても値は等しい、というのは流石に標準の定理にあって、SearchAbout (_ = _ + 0). するとすぐ見つかりますので、それをapplyすれば証明完了。

 apply plus_n_O.

証明が１行で書ける場合は

 assert (S x = S x + 0) by apply plus_n_O.

と assert 〜 by でまとめて書いちゃうこともできます。

assertで脇道にそれましたが、無事に仮定が増えて、こうなっているはずです。

H0: S x = S x + 0
-------------------------
S x < S x + S x

ここで、「"S x" は "S x + 0" に等しいとわかっているんだから、ゴールにある "S x" は "S x + 0" に書き換えてよ！」とCoqさんに伝えるtacticが、rewrite。

 rewrite H0 at 1.

"at 1" は"１個目の" S xを書き換えてね、の意味です。これを指定しないとゴールが(S x + 0) < (S x + 0) + (S x + 0) に全部変わってしまって困ります。"at 1" なら

-------------------------
S x + 0 < S x + S x

狙い通りにこの形になってくれるので、使いたかったライブラリ定理 plus_lt_compat_l : forall n m p: nat, n p+n < p+m が使えます。

 apply plus_lt_compat_l.

ゴールが 0 < S x に変わりますが、SearchAbout (0 < S _). で、ピッタリの定理が見つかります。

 apply lt_O_Sn.
Qed.

まとめ。

rewrite H (at p1 p2 ....): e1 = e2 の形の仮定 H があるときに、ゴールの中のe1をe2に書き換え。at ... があるときは、指定した番号のe1のみを書き換え。
rewrite <-H.: e1 = e2 の仮定 H を使って、逆向きに、e2をe1に書き換え
rewrite (<-)H in H1.: ゴールじゃなくて別の仮定H1の中を書き換え

今回は使いませんでしたが、assert + rewrite は非常によく使うので、replace、という複合tacticも用意されています。