複雑な(?) inductive に対する induction principle

……が,期待通りに生成されないと思ったけどよく考えてみるとどうなるべきなのかわからなかった話。

準備

例として,石取りゲームみたいなのを考えます。いくつかの石があって,一度に三つまで取ってよいということにしましょう。

そうすると,プレイヤーのとりうる手は以下のように形式化できます。mov m n で「自分の番で m 個の石があるとき,n 個に減らしてもよい」の意味です。

Inductive mov : nat -> nat -> Prop :=
| mov_1 : forall m, mov (S m) m
| mov_2 : forall m, mov (S (S m)) m
| mov_3 : forall m, mov (S (S (S m))) m.

勝敗は,最後の石を取ったほうが勝ち,というルールで考えることにしましょう。

そうすると,残り n で手番が回ってきたら勝ち目がないことを表す述語 losing n はこう書けるでしょう。

Inductive losing : nat -> Prop :=
| Losing : forall n,
  (forall m, mov n m -> exists k, mov m k /\ losing k) ->
  losing n.

つまり n から自分がどんな手 m を打っても,それに対する適当な相手の応じ手 k があって k は losing である,というときに n は losing である。

石がもう残っていないときは mov 0 m となる m がないので自明に losing で,これが base case になります。他には,例えば 3 個だったらいきなり全部取れば勝ちなので losing ではなく,4 個ならどうやっても次の相手のターンに全部取られるので losing です。

一応それも証明してみた。(本題には関係ありません)

Hint Constructors mov losing.
Hint Extern 0 => match goal with [H : mov _ _ |- _] => inversion H end.

Lemma zero_losing : losing 0.
  auto.
Qed.

Lemma three_not_losing : ~losing 3.
  unfold not; inversion 1 as [? H0].
  destruct (H0 0); intuition.
Qed.

Lemma four_losing : losing 4.
  eauto 6.
Qed.  

induction on "losing"

それで,いくつかそれらしいことも証明できるしたぶん上の losing の定義は正しそうです。

ところで,この inductive に対する induction principle ってどうなるんでしょう。どうなるか考えてもすぐにはよくわからないのですが,とりあえず losing_ind が生成されてるので使ってみようとします。

例題として,losing というのは結局のところ 4 の倍数であるということになるのであって,つまり以下のことが示せるはずなのでそれを考えてみましょう。

Goal forall n, losing n -> exists m, n = 4 * m.

これは losing に関する帰納法で証明できるんじゃないか,と頭の中では思うのですが,coq 上でやろうとするとうまくいかない。*1

どううまくいかないかというと,

Coq < Goal forall n, losing n -> exists m, n = 4 * m.
1 subgoal
  
  ============================
   forall n : nat, losing n -> exists m : nat, n = 4 * m

Unnamed_thm < induction 1.
1 subgoal
  
  x : nat
  H : forall y : nat, mov x y -> exists z : nat, mov y z /\ losing z
  ============================
   exists m : nat, x = 4 * m

となって,帰納法の仮定がなんかおかしい。本来あるべき姿(が具体的にどうなのかきちんと書けないのですが)より弱い気がする。

induction principle?

帰納法の原理がどうなってるのか確認してみると,

Unnamed_thm < Check losing_ind.
losing_ind
     : forall P : nat -> Prop,
       (forall x : nat,
        (forall y : nat, mov x y -> exists z : nat, mov y z /\ losing z) ->
        P x) -> forall n : nat, losing n -> P n

やっぱり期待してるものと違う気がする。帰納法の仮定の部分に P が出てこないし。

じゃあ帰納法の原理の本来あるべき形はどういうものなのか,という話になるわけで,本当はそれを考えて書こうと思ったのですけど,まだよくわかってません。

たぶん cpdt (http://adam.chlipala.net/cpdt/) の section 3.8 とかに書いてあることが関係あると思います (tree と list の話)。exists とかが mutual induction ではなく既に定義されてるものなのでうまくいかない,とかそんなような。でも結局,こうあるべきだ,という式がなんかうまく書けないのですが,どこを見たらわかるんでしょう。

*1:証明そのものは n に関する累積帰納法でやればできます