Think Stitch
PRINCIPIA  最近の更新


Isabelle:二重帰納法の処方と二項係数の性質証明例

定理証明支援系 Isabelle で二重帰納法を使う場合の処方について整理しておきます. まずふつうの数学的帰納法の使い方を復習します. 次に二重帰納法の処方について説明します. 最後に例として二項係数のある性質を証明してみます.

数学的帰納法 induct_tac

すべての自然数 n について P(n) が成り立つことを数学的帰納法を用いて示すには induct_tac を使います. 引数として対象とする変数を指定します.

lemma "P(n::nat)"
apply(induct_tac n)
------------------------------
goal (2 subgoals):
 1. P 0
 2. !!n. P n ==> P (Suc n)

単に n とだけ書くと Isabelle には型が分からないので,::nat と書いて自然数であることを教えて上げています. ごらんのとおり基底ケースと帰納ケースの2つのゴールが出てきます.これらを証明すればいいわけです.

二重帰納法

二重帰納法とは,すべての自然数 n と k について P(n, k) が成り立つことを証明したいとき,それぞれの変数について順番に2回数学的帰納法を適用するというものです.

まず n に対して数学的帰納法を適用します.n を自由変数にした式を用意して induct_tac を適用します.

lemma "ALL k::nat. P (n::nat) k"
apply(induct_tac n)
------------------------------
goal (2 subgoals):
 1. ALL k. P 0 k
 2. !!n. ALL k. P n k ==> ALL k. P (Suc n) k

この2つのゴールそれぞれについて,k を対象に数学的帰納法を適用します. ゴールの 1 は n も仮定もありませんから,素直に数学的帰納法を適用すれば済みます.

lemma base: "P (0::nat) (k::nat)"
apply(induct_tac k)
------------------------------
goal (2 subgoals):
 1. P 0 0
 2. !!n. P 0 n ==> P 0 (Suc n)

一方,ゴールの 2 では仮定がメタ含意に移ってしまっているので,このままでは induct_tac を適用できません. ここがポイントで,含意を対象レベルに戻して次のような式を作ってから induct_tac を適用します.

lemma ind: "(ALL k::nat. P n k) --> P (Suc n) k"
apply(induct_tac k)
------------------------------
goal (2 subgoals):
 1. (ALL k. P n k) --> P (Suc n) 0
 2. !!na. (ALL k. P n k) --> P (Suc n) na
          ==> (ALL k. P n k) --> P (Suc n) (Suc na)

Isabelle が用意した変数名 nat はちょっと見にくいので,rename_tac を使って j に改名し整理すると次のようになります.

goal (2 subgoals):
 1. ALL k. P n k ==> P (Suc n) 0
 2. !!j. [| ALL k. P n k; P (Suc n) j |] ==> P (Suc n) (Suc j)

まとめると次のようになります:

合計で4つのサブゴールを証明することになります.

例:二項係数のある性質の証明

二重帰納法の適用例として,二項係数に関する次の有名な性質を証明してみます.

\[ \binom{n}{r} = \binom{n}{n - r} \qquad (0 \le r \le n) \]

二項係数の定義としては,次のものを採用することにします.

\[ \binom{n}{0} = 1 \qquad (n \ge 0) \] \[ \binom{0}{r} = 0 \qquad (r > 0) \] \[ \binom{n + 1}{r + 1} = \binom{n}{r + 1} + \binom{n}{r} \qquad (n \ge 0, r \ge 0) \]

Isabelle では次のように定義できます.

fun comb :: "nat => nat => nat" where
  "comb n 0 = 1" |
  "comb 0 (Suc r) = 0" |
  "comb (Suc n) (Suc r) = comb n (Suc r) + comb n r"

ではさっそく証明に挑戦します.まず n だけを自由にした式を作って induct_tac を適用します. apply(auto) を実行すると基底ケースは自動で証明され,帰納ケースだけが残ります.

lemma "ALL r. r <= n --> comb n r = comb n (n - r)"
apply(induct_tac n)
apply(auto)
------------------------------
goal (1 subgoal):
 1. !!n r.
       [| ALL r<=n. comb n r = comb n (n - r); r <= Suc n |]
       ==> comb (Suc n) r = comb (Suc n) (Suc n - r)

次に r について数学的帰納法を適用します. まず仮定を対象レベルの含意に書き直してから induct_tac を適用します.

lemma ind_n: 
  "(ALL r<=n. comb n r = comb n (n - r)) & r <= Suc n
      --> comb (Suc n) r = comb (Suc n) (Suc n - r)"
apply(induct_tac r)
apply(clarsimp)
------------------------------
goal (2 subgoals):
 1. ALL r<=n. comb n r = comb n (n - r) ==> comb n (Suc n) = 0
 2. !!na. (ALL r<=n. comb n r = comb n (n - r)) &
          na <= Suc n -->
          comb (Suc n) na = comb (Suc n) (Suc n - na)
          ==> (ALL r<=n. comb n r = comb n (n - r)) &
              Suc na <= Suc n -->
              comb (Suc n) (Suc na) =
              comb (Suc n) (Suc n - Suc na)

ここからはゴールを見て攻めどころを考えます.まず comb n (Suc n) は 0 であるはずです. そこで補題を作ることにします. ちょっと一般化して r > n のときは comb n r = 0 であることを示しましょう.

lemma n_gt_r [rule_format]: "ALL r. r > n --> comb n r = 0"
apply(induct_tac n)
apply(auto)
------------------------------
goal (2 subgoals):
 1. !!r. 0 < r ==> comb 0 r = 0
 2. !!n r.
       [| ALL r>n. comb n r = 0; Suc n < r |]
       ==> comb (Suc n) r = 0

これはよくあるパターンで,case_tac を使って r = 0 と r > 0 に場合分けをするように指示してあげるとうまくいきます. 2番目のゴールも同様です.

lemma n_gt_r [rule_format]: "ALL r. r > n --> comb n r = 0"
apply(induct_tac n)
apply(auto)
apply(case_tac r)
apply(auto)
apply(case_tac r)
apply(auto)
done

これで補題ができました.元の証明に戻って適用するとゴールの1番目は消えます.

lemma ind_n: 
  "(ALL r<=n. comb n r = comb n (n - r)) & r <= Suc n
      --> comb (Suc n) r = comb (Suc n) (Suc n - r)"
apply(induct_tac r)
apply(clarsimp)
apply(rule n_gt_r)
apply(simp)
(**)
apply(clarify)
apply(rename_tac r)
------------------------------
goal (1 subgoal):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n |]
         ==> comb (Suc n) (Suc r) =
             comb (Suc n) (Suc n - Suc r)

次は2番目のゴールです.まず帰結の最初の項は定義の形なので展開します. 定義または仮定の形を目指すのは基本的な戦略です.

apply(subst comb.simps)
------------------------------
goal (1 subgoal):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n |]
         ==> comb n (Suc r) + comb n r =
             comb (Suc n) (Suc n - Suc r)

次に Suc n - Suc r = n - r と簡約します.

apply(subgoal_tac "n - r = Suc n - Suc r")
apply(rotate_tac -1)
apply(erule_tac t="Suc n - Suc r" in subst)
------------------------------
goal (2 subgoals):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n |]
         ==> comb n (Suc r) + comb n r = comb (Suc n) (n - r)
...

仮定を目指すには Suc n がじゃまなので,定義を目指します.そのためには n - r が Suc p の形 なる必要があるので,再び case_tac で場合分けをします.

apply(case_tac "n - r")
------------------------------
goal (3 subgoals):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n;
            n - r = 0 |]
         ==> comb n (Suc r) + comb n r = comb (Suc n) (n - r)
 2. !!r nat.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc nat |]
       ==> comb n (Suc r) + comb n r = comb (Suc n) (n - r)
...

まず n - r = 0 つまり n = r の方から片付けましょう. 先頭の項は補題により 0 です.

apply(subst n_gt_r)
apply(arith)
------------------------------
goal (3 subgoals):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n;
            n - r = 0 |]
         ==> 0 + comb n r = comb (Suc n) (n - r)
...

最後の項は定義により 1 です.

apply(rule_tac s="0" and t="n - r" in ssubst)
apply(assumption)
apply(subst comb.simps)
------------------------------
goal (3 subgoals):
 1. !!r. [| (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            ALL r<=n. comb n r = comb n (n - r); r <= n;
            n - r = 0 |]
         ==> 0 + comb n r = 1
...

残った comb n r は comb n n ということですから,ここで帰納法の仮定が使えます. これでゴールの1番目は証明できました.

apply(rotate_tac 1)
apply(drule_tac x="n" in spec)
------------------------------
goal (3 subgoals):
 1. !!r. [| r <= n; n - r = 0;
            (ALL r<=n. comb n r = comb n (n - r)) &
            r <= Suc n -->
            comb (Suc n) r = comb (Suc n) (Suc n - r);
            n <= n --> comb n n = comb n (n - n) |]
         ==> 0 + comb n r = 1
...

つづいて2番目のゴールです. 定義の形を目指して n - r を Suc p で置き換えます.

apply(rename_tac p)
------------------------------
goal (2 subgoals):
 1. !!r p.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc p |]
       ==> comb n (Suc r) + comb n r = comb (Suc n) (n - r)
...
apply(rule_tac s="Suc p" and t="n - r" in ssubst)
apply(assumption)
------------------------------
goal (2 subgoals):
 1. !!r p.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc p |]
       ==> comb n (Suc r) + comb n r = comb (Suc n) (Suc p)
...

定義を使って展開します.

apply(subst comb.simps)
------------------------------
goal (2 subgoals):
 1. !!r p.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc p |]
       ==> comb n (Suc r) + comb n r =
           comb n (Suc p) + comb n p
...

これで n についての Suc がすべて消えましたから,だいぶ仮定の形に近づきました. 次は Suc p ですが,これは n - r ですから置き換えれば仮定の形になります.

apply(rule_tac s="n - r" and t="Suc p" in subst)
apply(assumption)
------------------------------
goal (2 subgoals):
 1. !!r p.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc p |]
       ==> comb n (Suc r) + comb n r =
           comb n (n - r) + comb n p
...

最後は Suc r です.n - r = Suc p ですから n = r + Suc p = Suc r + p.よって Suc r = n - p です.

apply(subgoal_tac "n - p = Suc r")
apply(rule_tac s="n - p" and t="Suc r" in subst)
apply(assumption)
------------------------------
goal (3 subgoals):
 1. !!r p.
       [| (ALL r<=n. comb n r = comb n (n - r)) &
          r <= Suc n -->
          comb (Suc n) r = comb (Suc n) (Suc n - r);
          ALL r<=n. comb n r = comb n (n - r); r <= n;
          n - r = Suc p; n - p = Suc r |]
       ==> comb n (n - p) + comb n r =
           comb n (n - r) + comb n p
...

ここで仮定を2回使えば終わりです.

apply(frule_tac x="p" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(arith)
apply(rule_tac s="comb n p" and t="comb n (n - p)" in subst)
apply(assumption)
apply(frule_tac x="r" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(arith)
apply(rule_tac s="comb n r" and t="comb n (n - r)" in subst)
apply(assumption)
apply(rule add_commute)
apply(arith)
apply(arith)
done

一番始めの証明に戻り,いまの補題を使います.

lemma "ALL r. r <= n --> comb n r = comb n (n - r)"
apply(induct_tac n)
apply(auto)
apply(subst ind_n)
------------------------------
goal (2 subgoals):
 1. !!n r.
       [| ALL r<=n. comb n r = comb n (n - r); r <= Suc n |]
       ==> (ALL r<=n. comb n r = comb n (n - r)) & r <= Suc n
 2. !!n r.
       [| ALL r<=n. comb n r = comb n (n - r); r <= Suc n |]
       ==> comb (Suc n) (Suc n - r) = comb (Suc n) (Suc n - r)

残りはほぼ自明です.これで証明できました.

apply(rule conjI)
apply(assumption)
apply(assumption)
apply(rule refl)
done

コメント

数学的帰納法を見ると「お,なんか証明できそうだ」と思うのですけど... \[ P(0) \land (\forall n. P(n) \rightarrow P(n+1)) \rightarrow (\forall n. P(n)) \] これを次のように書き換えると,ありがたみが減ったような感じがします :P \[ P(0) \land (\forall n. \neg P(n) \lor P(n+1)) \rightarrow (\forall n. P(n)) \]

2015/01/27
© 2013,2014,2015 PRINCIPIA Limited