30を言ったら負けゲームの勝敗をCoqで証明

# 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`とします。

```coq
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`コマンドを使います。

```coq
Compute nim 29.
```

```coq
     = true
     : bool
```

すると（少し経って）結果が帰ってきて、`true`つまり勝ちであることがわかります。

## 一般的な結果の証明

特定の`n`については全探索により結果を計算できました。
しかし一方で、`n`が大きくなると計算時間が指数的に増加しますし、
一般の`n`についての性質を証明できなければCoqを使う意味がないです。

そこで、実際に`0`から順に計算してみて、法則性を確認してみます。

```coq
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`が勝ち」を証明します。

```coq
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`のような順序を基本にしています。

```coq
Lemma nim_diff_win2 : forall n : nat,
  nim n = false -> nim (2 + n) = true.
Proof.
  intros n H.
  simpl.
  rewrite H.
  simpl.
  reflexivity.
Qed.
```

```coq
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`が負け」を証明します。

```coq
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`で特別に展開式を定義して使っています。

### 負けと勝ちの一般式の証明

これらの補題を利用して一般の値での勝敗を証明します。
まず負けの場合。

```coq
Lemma nim_lose : forall m : nat,
  nim 4 * m = false.
```

`4`周期で結果が変わることを利用して、`n = 4 * m`で`m`に対する帰納法で証明します。

```coq
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`の形にして、これまでに証明した補題を適用します。

次に勝ちの場合。

```coq
Lemma nim_win : forall m k : nat,
  k < 3 -> nim (1 + k + 4 * m) = true.
```

4の倍数ではないことを表現するために新たな変数`k`を導入し、`k<3`という条件の下で勝ちを証明します。

```coq
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`の性質を使って等価な命題に変形します。

```coq
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.
```

`=`の反対は`<>`なので勝ち側は`<>`を使います。

```coq
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.
```

これらを使って、ゲームの勝敗を一つの式にまとめると次の定理が得られます。

```coq
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`で場合分けし、それぞれの場合で`=?`を`=`と`<>`に変換して補題を適用しました。

また、次のように同値`<->`によって逆も成りたつことを主張できます。

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