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

Require Export Poly_J.

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

intros n. induction n.

で始めればうまくいきます。しかし

intros n m. induction n.

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

Theorem double_injective_FAILED : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n m. induction n as [| n'].
  Case "n = O". simpl. intros eq. destruct m as [| m'].
    SCase "m = O". reflexivity.
    SCase "m = S m'". inversion eq.
  Case "n = S n'". intros eq. destruct m as [| m'].
    SCase "m = O". inversion eq.
    SCase "m = S m'".
      assert (n' = m') as H.
      SSCase "Proof of assertion".

      Admitted.

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

帰納法の仮定を導入した時点で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をゴールに残しています。

Theorem double_injective' : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n. induction n as [| n'].
  Case "n = O". simpl. intros m eq. destruct m as [| m'].
    SCase "m = O". reflexivity.
    SCase "m = S m'". inversion eq.
  Case "n = S n'".

    intros m eq.

    destruct m as [| m'].
    SCase "m = O". inversion eq.
    SCase "m = S m'".

      assert (n' = m') as H.
      SSCase "Proof of assertion". apply IHn'.
        inversion eq. reflexivity.
      rewrite -> H. reflexivity.  Qed.

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

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

Theorem double_injective_take2_FAILED : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n m. induction m as [| m'].
  Case "m = O". simpl. intros eq. destruct n as [| n'].
    SCase "n = O". reflexivity.
    SCase "n = S n'". inversion eq.
  Case "m = S m'". intros eq. destruct n as [| n'].
    SCase "n = O". inversion eq.
    SCase "n = S n'".
      assert (n' = m') as H.
      SSCase "Proof of assertion".

Admitted.

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

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

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

Theorem double_injective_take2 : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n m.

  generalize dependent n.

  induction m as [| m'].
  Case "m = O". simpl. intros n eq. destruct n as [| n'].
    SCase "n = O". reflexivity.
    SCase "n = S n'". inversion eq.
  Case "m = S m'". intros n eq. destruct n as [| n'].
    SCase "n = O". inversion eq.
    SCase "n = S n'".
      assert (n' = m') as H.
      SSCase "Proof of assertion".
        apply IHm'. inversion eq. reflexivity.
      rewrite -> H. reflexivity.  Qed.

この定理の非形式な証明を見てみましょう。なお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に関する帰納法で以下を示しなさい。

Theorem plus_n_n_injective_take2 : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  (* FILL IN HERE *) Admitted.

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

Theorem index_after_last: forall (n : nat) (X : Type) (l : list X),
     length l = n ->
     index (S n) l = None.
Proof.
  (* FILL IN HERE *) Admitted.

FILL IN HERE ☐

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

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

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

Proof:(* FILL IN HERE *)☐

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