30を言ったら負け
みなさんは小さい頃、「30を言ったら負け」ゲームで遊んだことがあるでしょうか。
正直このゲームに名前が付いていた記憶は無いのですが、以下のようなゲームです。
- 二人で先攻後攻を決め、１から順に先攻「1、2」後攻「3、4、5」先攻「6」のように相手が言った数の次の数を言い、
30まで進める。 - 一度に
３つまで進めることができる。 -
３０を言った人が負け。
地域差もあるでしょうし、そもそも聞いたことも無い方もいるかもしれませんが、自分は小さい頃遊んだ、というか必勝手順を知っている友達に遊ばれたことがあります。
まずはこのゲームの必勝法を考えていきます。
必勝法
プレイヤーA、Bによるゲームで、Aが必勝手順を知っているプレイヤーとします。ゲーム進行を見ていきます。
A [1]
B [2, 3] A [4, 5]
B [6] A [7, 8, 9]
B [10, 11] A [12, 13]
B [14, 15, 16] A [17]
B [18, 19, 20] A [21]
B [22] A [23, 24, 25]
B [26, 27] A [28, 29]
B [30]
Aの勝ちです。
はい。なかなか悪意のある改行位置ですが（笑）！、つまりは次のような必勝戦略があるようです。
- 先手で[1]を言う。
- 相手が言った数と合わせて４つになるように進めて、[5] [9] [13] [17] [21] [25] [29]を言う。
というわけでこのゲームは先手必勝です。
Coqによる証明
Coqは「定理証明支援系」と言い、証明を書くことのできるプログラミング言語です。
Coqによって、30を言ったら負けゲームを定式化してみます。
定義のしやすさの関係で、以下のようにゲームを変形しています。
- nから順に、数を小さくしながら言っていく。
- 0を言わされたら（0の状態で手番が回ったら）負け。
このときn=29を代入すると、「30を言ったら負け」と等価になります（1ずれる）。
全探索関数による定義
一つの定式化は、ミニマックス探索（いわゆる全探索）により勝敗の計算を定義する方法です。
これはFixpointにより再帰関数を定義することで達成できます。
このゲームは石取りゲーム（ニム）の一種と思われるので関数名はnimとします。
Require Import Coq.Bool.Bool.
Fixpoint nim (n : nat) : bool :=
match n with
| 0 => false
| S n' => negb (nim n') || negb (nim (pred n')) || negb (nim (pred (pred n')))
end.
（手続き型言語に慣れた私たちにとっては）見慣れない書き方ですが、
-
trueを勝ち、falseを負けにしてn = 0のとき負け -
matchで場合分けして、n > 0のときn' <- n - 1を使って計算(S は1を足す演算) - 再帰関数で
n',n' - 1,n' - 2の場合の勝敗を計算（pred は 1を引く演算） - それぞれの勝敗を
negbで反転して||でorを取る
という手順で探索を記述しています。
これは見ての通り再帰関数なので計算することができます。Computeコマンドを使います。
Compute nim 29.
= true
: bool
すると（少し経って）結果が帰ってきて、trueつまり勝ちであることがわかります。
一般的な結果の証明
特定のnについては全探索により結果を計算できました。
しかし一方で、nが大きくなると計算時間が指数的に増加しますし、
一般のnについての性質を証明できなければCoqを使う意味がないです。
そこで、実際に0から順に計算してみて、法則性を確認してみます。
Compute nim 0.
Compute nim 1.
Compute nim 2.
Compute nim 3.
Compute nim 4.
Compute nim 5.
= false
: bool
= true
: bool
= true
: bool
= true
: bool
= false
: bool
= true
: bool
結果は
-
n = 0, 4, ...では負け -
n = 1, 2, 3, 5, ...では勝ち
と、4を周期に結果が変わっていくと予想されます。
これは、必勝手順が足して4になるように言っていくことからも納得できます。
ではこの結果を証明してみます。
証明のやり方は色々ありますが、ここでは細かい補題から順に証明していきます。
差分の証明
まず「nが負けなら、n+1、n+2、n+3が勝ち」を証明します。
Lemma nim_diff_win1 : forall n : nat,
nim n = false -> nim (1 + n) = true.
Proof.
intros n H.
simpl.
rewrite H.
simpl.
reflexivity.
Qed.
補題Lemmaとして、「全てのnに対して、nim n = falseならばnim (1 + n) = true」を定義し、それを証明しています。
途中経過ウインドウの表示がないと状況が見えませんが、nim n = falseをHとおき、nim (1 + n)を展開して代入しています。
なお、Coqの自然数は計算が変数の左側で起こるので1+nのような順序を基本にしています。
Lemma nim_diff_win2 : forall n : nat,
nim n = false -> nim (2 + n) = true.
Proof.
intros n H.
simpl.
rewrite H.
simpl.
reflexivity.
Qed.
Lemma nim_diff_win3 : forall n : nat,
nim n = false -> nim (3 + n) = true.
Proof.
intros n H.
simpl.
rewrite H.
simpl.
reflexivity.
Qed.
次に「n+1、n+2、n+3が勝ちならばn+4が負け」を証明します。
Lemma nim_diff_lose : forall n : nat,
nim (1 + n) = true ->
nim (2 + n) = true ->
nim (3 + n) = true ->
nim (4 + n) = false.
Proof.
intros n H1 H2 H3.
assert (nim (4 + n) = negb (nim (3 + n)) || negb (nim (2 + n)) || negb (nim (1 + n))) as H.
{ simpl.
reflexivity. }
rewrite H.
rewrite H1, H2, H3.
simpl.
reflexivity.
Qed.
こちらもnim (4 + n)を展開して代入しているのですが、直接simplで展開すると暴走して過度な展開が起こったため、assertで特別に展開式を定義して使っています。
負けと勝ちの一般式の証明
これらの補題を利用して一般の値での勝敗を証明します。
まず負けの場合。
Lemma nim_lose : forall m : nat,
nim 4 * m = false.
4周期で結果が変わることを利用して、n = 4 * mでmに対する帰納法で証明します。
Require Import Arith.
Proof.
induction m.
- simpl.
reflexivity.
- rewrite <- Nat.add_1_l with (n:=m).
rewrite Nat.mul_add_distr_l.
rewrite Nat.mul_1_r.
apply nim_diff_lose.
+ apply nim_diff_win1.
apply IHm.
+ apply nim_diff_win2.
apply IHm.
+ apply nim_diff_win3.
apply IHm.
Qed.
inductionでmに対する帰納法を回します。
最初の-以下でm = 0のとき、二つ目の-以下でm+1のときを証明しています。
最初のrewrite三つで4 + 4 * mの形にして、これまでに証明した補題を適用します。
次に勝ちの場合。
Lemma nim_win : forall m k : nat,
k < 3 -> nim (1 + k + 4 * m) = true.
4の倍数ではないことを表現するために新たな変数kを導入し、k<3という条件の下で勝ちを証明します。
Proof.
intros m k H.
remember (4 * m) as n.
simpl.
destruct k.
- rewrite Heqn.
rewrite plus_O_n.
rewrite nim_lose.
reflexivity.
- destruct k.
+ simpl.
rewrite Heqn.
rewrite nim_lose.
reflexivity.
+ destruct k.
* simpl.
rewrite Heqn.
rewrite nim_lose.
reflexivity.
* apply lt_S_n in H.
apply lt_S_n in H.
apply lt_S_n in H.
inversion H.
Qed.
そこそこ長くなりましたが、やっていることはdestructでkを0とそれ以外、1とそれ以外と順に分けていき、最終的にk<3に矛盾するまで増えたら終わりです。
勝敗合わせた条件式の証明
これで無事、全ての自然数nに対してnim nの結果がわかったと言えます。
…ですが、nが命題に入っておらず別の形で表現されており、全てのnに対して本当に勝敗を確定できた（と言って良い）のか不安な人もいるでしょう。
ここからはnが入る命題の形で証明していきます。
nを4で割った余りはn mod 4で表現できるので、modの性質を使って等価な命題に変形します。
Lemma nim_lose_mod : forall n : nat,
n mod 4 = 0 -> nim n = false.
Proof.
intros n H.
apply Nat.mod_divides in H.
- destruct H as [m H].
rewrite H.
apply nim_lose.
- apply Nat.neq_succ_0.
Qed.
=の反対は<>なので勝ち側は<>を使います。
Lemma nim_win_mod : forall n : nat,
n mod 4 <> 0 -> nim n = true.
Proof.
intros n H.
assert (4 <> 0) as Hm.
{ apply Nat.neq_succ_0. }
apply Nat.div_mod with (x:=n) in Hm.
remember (n / 4) as m.
rewrite plus_comm in Hm.
rewrite Hm.
apply not_eq_sym in H.
apply neq_0_lt in H.
apply S_pred_pos in H.
remember (pred (n mod 4)) as k.
rewrite H.
apply nim_win.
apply lt_S_n.
rewrite <- H.
apply Nat.mod_upper_bound.
apply Nat.neq_succ_0.
Qed.
これらを使って、ゲームの勝敗を一つの式にまとめると次の定理が得られます。
Theorem nim_condition : forall n : nat,
nim n = negb (n mod 4 =? 0).
Proof.
intros n.
destruct (n mod 4 =? 0) eqn:E.
- apply nim_lose_mod.
apply Nat.eqb_eq in E.
apply E.
- apply nim_win_mod.
apply Nat.eqb_neq in E.
apply E.
Qed.
=?は比較の演算子で、多くのプログラミング言語における==に相当します。
destructで場合分けし、それぞれの場合で=?を=と<>に変換して補題を適用しました。
また、次のように同値<->によって逆も成りたつことを主張できます。
Theorem nim_win_iff : forall m n : nat,
nim n = true <-> n mod 4 <> 0.
Proof.
split.
- intros H E.
apply eq_true_false_abs in H.
+ apply H.
+ apply nim_lose_mod.
apply E.
- apply nim_win_mod.
Qed.
一つ一つの証明を積み重ねると長くなりましたが、ひとまず30を言ったら負けゲーム「30」の部分を値を変えて一般的な結果を証明することができました！
最後に
30の方は一般化できましたが、一度に3つまで進められる方の一般化もぜひチャレンジしてみてください！