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つまで進められる方の一般化もぜひチャレンジしてみてください！