Think Stitch
PRINCIPIA  最近の更新


有界な自然数からなるリストの自然数へのエンコーディング 2

前回は, ある上限 M > 0 未満の自然数からなるリストを1つの自然数にエンコードする関数 enc と それを元に戻す関数 dec を定義して,dec M (enc M cs) = cs であることを証明しました.

今回は逆に enc M (dec M x) = x であることを証明したいと思います.

関数 enc と dec の定義を再掲しておきます.

fun enc :: "nat => nat list => nat" where
  "enc M [] = 0" |
  "enc M (c#cs) = 1 + c + M * (enc M cs)"
fun dec :: "nat => nat => nat list" where
  "dec M 0 = []" |
  "dec M (Suc x) = (x mod M) # (dec M (x div M))"

二重帰納法

証明したい命題はこれです:

lemma enc_dec: "M > 0 ==> enc M (dec M x) = x"

これが任意の x について成り立つはずです. そこで数学的帰納法を使いたいわけですが,x に対して単純に適用しただけではうまくできそうにありません. なぜかというと,x の値の範囲はリストの長さで区分されていて,いわば2次元的な構造を持っているので, 1つ小さい x についての情報だけでは x の場合がいえそうにないからです.

x の値はリストの長さ L に対して次のように分けられていました:

L値の範囲
0F(0) <= x < F(1)
1F(1) <= x < F(2)
2F(2) <= x < F(3)
3F(3) <= x < F(4)
......
LF(L) <= x < F(L + 1)
......

ここで関数 F(L) は次のようなものでした: \[ F(L) = 1 + M + M^2 + \ldots + M^{L-1} = \sum_{0 \le i < L} M^i \]

そこでひと工夫します. x をリストの長さ n とそれに対応する値の範囲の中での位置 k に分解して,二重帰納法を使うことにします. そうすれば1つ短いリストすべてについての情報と,1つ小さい k についての情報を使うことができます.

まず関数 F(L) を定義します.上限 M も引数としてとることにします:

fun F :: "nat => nat => nat" where
  "F M 0 = 0" |
  "F M (Suc k) = F M k + M ^ k"

次に式を二重帰納法が適用できる形に変換するための規則を作ります.欲しい規則は次のようなものです: \[ \frac {\quad \forall n. \forall k. k < M^n \rightarrow P(F(n) + k) \quad} {\forall x. P(x)} \] かんたんにいえば,n と k を動かすと F(n) + k が自然数全体を動くということです. n はリストの長さなのですべての値をとります. リストの長さが n のときの値の範囲は F(n) <= x < F(n + 1) ですから,変数 k の範囲は 0 <= k < F(n + 1) - F(n) です. 関数 F(n) の定義から F(n + 1) - F(n) = M ^ n となります.

この規則を作るために,まず F(n) + k が自然数全体を網羅するという補題を作ります. これはふつうの数学的帰納法と場合分けを使ってかんたんに証明できます.

lemma F_exh:
  "ALL M x. M > 0 --> (EX n k. k < M ^ n & x = F M n + k)"
apply(rule allI)
apply(rule allI)
apply(rule impI)
apply(induct_tac x)
apply(auto)
apply(rule_tac x="0" in exI)
apply(simp)
apply(case_tac "k = M^na - 1")
apply(rule_tac x="Suc na" in exI)
apply(rule_tac x="0" in exI)
apply(simp)
apply(rule_tac x="na" in exI)
apply(rule_tac x="Suc k" in exI)
apply(auto)
done

これを使って変換規則を証明します:

lemma F_ind [rule_format]:
  "M > 0 ==>
    (ALL n k. k < M ^ n --> P(F M n + k)) --> (ALL x. P x)"
apply(clarsimp)
apply(insert F_exh)
apply(rotate_tac -1)
apply(drule_tac x="M" in spec)
apply(rotate_tac -1)
apply(drule_tac x="x" in spec)
apply(drule mp)
apply(auto)
done

rule_format によって次のように推論規則の形になりました.

F_ind:
  [| 0 < ?M; !!n k. k < ?M ^ n ==> ?P (F ?M n + k) |]
    ==> ?P ?x

これで準備完了です.

enc M (dec M x) = x の証明

では証明を始めます.すこし長くて全体を見失う可能性があるので,概要を書いておきます.

  1. enc_dec に変換規則 F_ind を適用して,二重帰納法が使える形にする.
  2. 二重帰納法の処方にしたがい,enc_dec のゴールを対象レベルに変換する.これを ind_n とする.
  3. ind_n において n に対し帰納法を適用する.
  4. このゴールを再び対象レベルに変換する.これを ind_k とする.
  5. ind_k において k に対し帰納法を適用する.
  6. ind_k をがんばって証明する.
  7. ind_k を使って ind_n を証明する.
  8. ind_n を使って enc_dec を証明しておわり.

二重帰納法の形への変換

では始めます.まず変換規則 F_ind を適用します.

lemma enc_dec: "M > 0 ==> enc M (dec M x) = x"
apply(rule F_ind)
apply(auto)
------------------------------
goal (1 subgoal):
 1. !!n k.
       [| 0 < M; k < M ^ n |]
       ==> enc M (dec M (F M n + k)) = F M n + k

n についての帰納法 (1/2)

この命題に対して二重帰納法を適用します. そのために,この証明自体はいったん置いて,二重帰納法の処方にしたがい,式を対象レベルに変換します.これを ind_n とします.

lemma ind_n [rule_format]:
  "M > 0 ==>
   ALL k. k < M ^ n --> enc M (dec M (F M n + k)) = F M n + k"

まず n に対して帰納法を適用します. その後 auto をかけると帰納ケースだけが残ります.

lemma ind_n [rule_format]:
  "M > 0 ==>
   ALL k. k < M ^ n --> enc M (dec M (F M n + k)) = F M n + k"
apply(induct_tac n)
apply(auto)
------------------------------
goal (1 subgoal):
 1. !!n k.
       [| 0 < M;
          ALL k<M ^ n. enc M (dec M (F M n + k)) = F M n + k;
          k < M * M ^ n |]
       ==> enc M (dec M (F M n + M ^ n + k)) =
           F M n + M ^ n + k

k についての帰納法

次に k について帰納法を適用するために,このゴールを再び対象レベルに変換します. これを ind_k とします.

lemma ind_k [rule_format]:
  "M > 0 ==>
     (ALL k. k < M ^ n --> enc M (dec M (F M n + k)) = F M n + k) &
      k < M * M ^ n
    --> enc M (dec M (F M n + M ^ n + k)) = F M n + M ^ n + k"
apply(induct_tac k)
apply(auto)
------------------------------
goal (2 subgoals):
 1. [| 0 < M;
       ALL k<M ^ n. enc M (dec M (F M n + k)) = F M n + k |]
    ==> enc M (dec M (F M n + M ^ n)) = F M n + M ^ n
 2. !!na. [| 0 < M;
             ALL k<M ^ n.
                enc M (dec M (F M n + k)) = F M n + k;
             Suc na < M * M ^ n;
             enc M (dec M (F M n + M ^ n + na)) =
             F M n + M ^ n + na |]
          ==> (F M n + M ^ n + na) mod M +
              M *
              enc M (dec M ((F M n + M ^ n + na) div M)) =
              F M n + M ^ n + na

基底ケース,帰納ケースともに残りました. ここから先はがんばって証明します:P. まず基底ケースから攻めます. dec の引数は F M n + M ^ n です. M ^ n は k の範囲をはみ出していますからそのままでは帰納法の仮定を使うことはできません. そこで定義を目指します.そのためには引数は Suc ... という形にする必要があります. そこで F M n + M ^ n = Suc (F M n + M ^ n - 1) と考えます.

apply(subgoal_tac "Suc (M ^ n - Suc 0) = M ^ n")
apply(erule_tac t="M^n" in subst)
apply(subgoal_tac
  "Suc (F M n + M ^ n - Suc 0) = F M n + Suc (M ^ n - Suc 0)")
apply(erule_tac t="F M n + Suc (M ^ n - Suc 0)" in subst)
apply(subst dec.simps)
------------------------------
goal (4 subgoals):
 1. [| 0 < M;
       ALL k<M ^ n. enc M (dec M (F M n + k)) = F M n + k |]
    ==> enc M
         ((F M n + M ^ n - Suc 0) mod M #
          dec M ((F M n + M ^ n - Suc 0) div M)) =
        Suc (F M n + M ^ n - Suc 0)

定義を使って展開するとこのようになりました. 置き換えた F M n + M ^ n - Suc 0 という式が3箇所にあります. これは定義に返って考えてみると M * (F M n) です. したがって

(F M n + M ^ n - Suc 0) mod M = 0
(F M n + M ^ n - Suc 0) div M = F M n

となるはずです.そこでこれらの補題を作りましょう.

lemma M_dvd_F: "M > 0 ==> F M n + M ^ n - Suc 0 = M * (F M n)"
apply(induct_tac n)
apply(auto)
apply(subst diff_add_assoc2)
apply(induct_tac n)
apply(auto)
apply(subst add_mult_distrib2)
apply(auto)
done
lemma F_mod_0: "M > 0 ==> (F M n + M ^ n - Suc 0) mod M = 0"
apply(subst M_dvd_F)
apply(auto)
done
lemma F_div: "M > 0 ==> (F M n + M ^ n - Suc 0) div M = F M n"
apply(subst M_dvd_F)
apply(auto)
done

元の証明に戻って補題を適用します.

apply(subst F_mod_0)
apply(simp)
apply(subst F_div)
apply(auto)
------------------------------
goal (2 subgoals):
 1. [| 0 < M;
       ALL k<M ^ n. enc M (dec M (F M n + k)) = F M n + k |]
    ==> Suc (M * enc M (dec M (F M n))) = F M n + M ^ n

これで dec の引数が F M n になりました. これは k = 0 の場合に対応しますから帰納法の仮定を使うことができます.

apply(drule_tac x="0" in spec)
apply(simp)
------------------------------
goal (2 subgoals):
 1. [| 0 < M; enc M (dec M (F M n)) = F M n |]
    ==> Suc (M * F M n) = F M n + M ^ n

これについては前に作った補題が使えます.基底ケースはこれで証明完了です.

apply(subst M_dvd_F[symmetric])
apply(auto)

続いて帰納ケースの証明に移ります.

goal (1 subgoal):
 1. !!k. [| 0 < M;
            ALL k<M ^ n.
               enc M (dec M (F M n + k)) = F M n + k;
            Suc k < M * M ^ n;
            enc M (dec M (F M n + M ^ n + k)) =
            F M n + M ^ n + k |]
         ==> (F M n + M ^ n + k) mod M +
             M * enc M (dec M ((F M n + M ^ n + k) div M)) =
             F M n + M ^ n + k

F M n + M ^ n について先程と同じように処理すると

  F M n + M ^ n + k
= F M n + M ^ n - 1 + k + 1
= M * (F M n) + (k + 1)

となります.したがって

(F M n + M ^ n + k) mod M = (k + 1) mod M
(F M n + M ^ n + k) div M = F M n + (k + 1) div M

となります.補題を作って,まずはここまで進めます.

lemma dvd_mod_elim [rule_format]:
  "M > (0::nat) ==> M dvd a --> (a + b) mod M = b mod M"
apply(unfold dvd_def, auto simp add: algebra_simps)
done
lemma dvd_mod_elim [rule_format]:
  "M > (0::nat) ==> M dvd a --> (a + b) mod M = b mod M"
apply(unfold dvd_def, auto simp add: algebra_simps)
done
lemma ind_k [rule_format]:
  "0 < M ==>
     (ALL k. k < M ^ n --> enc M (dec M (F M n + k)) = F M n + k) &
      k < M * M ^ n
    --> enc M (dec M (F M n + M ^ n + k)) = F M n + M ^ n + k"
apply(induct_tac k)
...
apply(subgoal_tac "F M n + M ^ n - Suc 0 + Suc k = F M n + M ^ n + k")
apply(rotate_tac -1)
apply(erule_tac t="F M n + M ^ n + k" in subst)
apply(subst dvd_mod_elim)
apply(simp)
apply(subst dvd_eq_mod_eq_0)
apply(rule F_mod_0)
apply(simp)
apply(subst dvd_div_distrib)
apply(auto)
apply(subst dvd_eq_mod_eq_0)
apply(rule F_mod_0)
apply(simp)
apply(subst F_div)
apply(simp)
apply(subst M_dvd_F)
apply(simp)
------------------------------
goal (1 subgoal):
 1. !!k. [| 0 < M;
            ALL k<M ^ n.
               enc M (dec M (F M n + k)) = F M n + k;
            Suc k < M * M ^ n;
            enc M (dec M (F M n + M ^ n + k)) =
            F M n + M ^ n + k |]
         ==> Suc k mod M +
             M * enc M (dec M (F M n + Suc k div M)) =
             Suc (M * F M n + k)

Suc k div M < M ですから帰納法の仮定が使えます.

apply(drule_tac x="Suc k div M" in spec)
apply(drule mp)
------------------------------
goal (2 subgoals):
 1. !!k. [| 0 < M; Suc k < M * M ^ n;
            enc M (dec M (F M n + M ^ n + k)) =
            F M n + M ^ n + k |]
         ==> Suc k div M < M ^ n
 2. !!k. [| 0 < M; Suc k < M * M ^ n;
            enc M (dec M (F M n + M ^ n + k)) =
            F M n + M ^ n + k;
            enc M (dec M (F M n + Suc k div M)) =
            F M n + Suc k div M |]
         ==> Suc k mod M +
             M * enc M (dec M (F M n + Suc k div M)) =
             Suc (M * F M n + k)

このゴールの1番目はほぼ自明ですが,div, mod の証明はいつも面倒になります. しかたがないので補題を作ります.

lemma div_0:
  "[| x div M = c; (0::nat) < M |] ==> x >= M * c"
apply(subst mod_div_equality[symmetric, of x M])
apply(simp)
done
lemma less_div_M: "(0::nat) < M ==>
  x < M * M ^ n ==> x div M < M ^ n"
apply(subst less_le) (* (?x < ?y) = (?x <= ?y & ?x ~= ?y) *)
apply(rule conjI)
apply(subgoal_tac "(M * M ^ n) div M = M ^ n")
apply(erule subst)
apply(rule div_le_mono)  (* ?m <= ?n ==> ?m div ?k <= ?n div ?k *)
apply(auto)
apply(drule div_0)
apply(auto)
done

ind_k の証明に戻って補題を適用します.そうすると ind_k の証明はおわりです.

apply(erule less_div_M)
apply(auto)
apply(subst add_mult_distrib2) (* ?k * (?m + ?n) = ?k * ?m + ?k * ?n *)
apply(auto)
done

n についての帰納法 (2/2)

k についての帰納法が完了したので,n についての帰納法 ind_n の証明に戻ります. ind_k を使っておわりです.

lemma ind_n [rule_format]:
  "M > 0 ==>
   ALL k. k < M ^ n --> enc M (dec M (F M n + k)) = F M n + k"
apply(induct_tac n)
apply(auto)
apply(erule ind_k)
apply(auto)
done

enc_dec の証明

最後まで戻ってきました.enc_dec も完成した ind_n を使うだけです.

lemma enc_dec: "M > 0 ==> enc M (dec M x) = x"
apply(rule F_ind)
apply(simp)
apply(erule ind_n)
apply(simp)
done

つづく

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