Gen_J: 帰納法の仮定の一般化

前章ではdouble関数が単射であることの証明をしました。この証明を始める方法は少々デリケートです。
      intros n. induction n.

で始めればうまくいきます。 しかし
      intros n m. induction n.

で始めてしまうと、帰納段階の途中でつまってしまいます...

何がいけなかったのでしょうか?

帰納法の仮定を導入した時点で m をコンテキストに導入してしまっていることが問題です。直感的に言うと、これはCoqに「ある特定の n と m について考えよう」と教えるようなものです。そのため、この特定の n と m について double n = double m ならば n = m を証明しなければなりません。

次のタクティックス induction n はCoqに「このゴールの n に関する帰納法で示します」と伝えます。 なので、命題

• P n = "double n = double m ならば n = m"

がすべてのnについて成り立つことを

• P O
  
  (すなわち、"double O = double m ならば O = m")
  
  
• P n → P (S n)
  
  (すなわち、 "double n = double m ならば n = m" が成り立つならば " double (S n) = double m ならば S n = m").

2つめの文を見ると、これは奇妙なことを言っています。 それによると特定の m について

• "double n = double m ならば n = m"

が成り立つならば

• "double (S n) = double m ならば S n = m".

が証明できることになります。

これがどう奇妙かを説明するために、特定の m 、例えば 5 について考えてみましょう。 するとこの文は

• Q = "double n = 10 ならば n = 5"

が成り立つならば

• R = "double (S n) = 10 ならば S n = 5".

が証明できると言っています。

しかし Q を知っていても、Rを証明するのには何の役にたちません! (もし Q から R を示そうとすると「double (S n) = 10...を仮定すると...」のようなことを言わないといけませんが、これは途中でつまってしまいます。 double (S n) が 10 があることは、 double nが10であるかどうかについては何も教えてくれません。なのでQ はここでは役にたちません。)

まとめると、mがすでにコンテキストにある状態でnに関する帰納法による証明がうまくいかないのは、すべてのnと単一のmの関係を示そうとしてしまうかからです。

double_injective のいい証明では、inductionをnに対して使う時点ではmをゴールに残しています。

帰納法によって証明しようとしていることが、限定的すぎないかに注意する必要があることを学びました。 もしnとmの性質に関する証明をnに関する帰納法で行ないたい場合は、mを一般的なままにしておく必要があるかもしれません。

しかし、この戦略がいつもそのまま使えるわけではありません。ときには、ちょっとした工夫が必要です。 例えば、double_injectiveをnではなくmに関する帰納法で示したいとします。

mに関する帰納法の問題点は、最初にnをintroしなければいけないことです。 (もし何も導入せずにinduction mをしても、Coqは自動的にnをintroします!) どうしたらいいでしょうか?

1つめの方法は、補題の文を書き換えてnより先にmがくるようにします。 これはうまくいきますが、いい方法ではありません。 特定の証明戦略のために補題の文をめちゃくちゃにしたくありません。 補題の文はできるかぎり明確かつ自然な形であるべきです。

その代わりに、いったんすべての限量変数を導入し、そのうちいくつかをコンテキストから取りゴールの先頭に置くことで、再び一般化します。 これはgeneralize dependentタクティックスによって実現できます。

この定理の非形式な証明を見てみましょう。なお nを限量化したまま帰納法によって命題を証明する箇所は、形式的な証明ではgeneralize dependentを使う箇所に対応します。

Theorem: すべての自然数 n と m について、 double n = double m ならば n = m。

Proof: mをnatとする。 mに関する帰納法によって、 すべてのn に対して double n = double m ならば n = m を示す。

• 最初に m = 0 と仮定し、n を double n = double m をみたす数とし、 n = 0 を示す。
  
  m = 0なので、doubleの定義よりdouble n = 0。 n について2つの場合分けが考えれる。 n = 0 ならば、それが示したいことなので、すでに終了している。 そうでなくてn = S n'となるn'が存在する場合、矛盾を導くことで証明する。 doubleの定義によりn = S (S (double n'))だが、これは仮定 dobule n = 0 と矛盾する。
  
  
• そうでない場合、m = S m' と仮定し、nは再び double n = double m をみたす数とする。 n = S m'を示すために、 帰納法の仮定「 すべての数 s に対して double s = double m'ならばs = m'」を用いる。
  
  m = S m'とdoubleの定義により、double n = S (S (double m'))。 nに関して2つの場合分けが考えられる。
  
  n = 0ならば、定義によりdouble n = 0となり、矛盾を導ける。 なので、n = S n'となるn'があると仮定すると、再びdoubleの定義により、 S (S (double n')) = S (S (double m'))。 ここでinversionによりdouble n' = dobule m'。
  
  帰納法の仮定をn'をあてはめることで、n' = m'という結論を導ける。 S n' = nかつS m' = mなので、これにより示せる。 ☐

練習問題: ★★★ (gen_dep_practice)

mに関する帰納法で以下を示しなさい。

lに関する帰納法で示しなさい。

☐

練習問題: ★★★, optional (index_after_last_informal)

index_after_lastのCoqによる証明に対応する非形式的な証明を書きなさい。

Theorem: すべてのSet X, リスト l : list X, 自然数nに対して、length l = n ならば index (S n) l = None。

Proof: ☐

練習問題: ★★★, optional (gen_dep_practice_opt)

lに関する帰納法で示しなさい。

☐

練習問題: ★★★, optional (app_length_cons)

app_lengthを使わずにl1に関する帰納法で示しなさい。

☐

練習問題: ★★★★, optional (app_length_twice)

app_lengthを使わずにl1に関する帰納法で示しなさい。

☐