Theorem Proving Advent Calendar 6日目
超現実数というものがあります。それをネタにKnuthが小説を書きました(日本語訳)。ConwayのOn Numbers and Gamesという本もむかし読みました。これをCoqで実装して修論を書いたMamameさんという人がいる(TYPESのMamameさん論文)のは知っていたけれども、中身はまだ見てなくて、で、見ないまま自分でやってみると、少し違うものができました(github)。
まずゲームを定義してから、数は特殊なゲームだと言います。
ここでいうゲームは二人ゲームです。左の人と右の人が勝負します。なにもできなくなったほうがまけ。ゲームを決めるには、左の人が先手で何かした結果どういうゲームにできるかと、右の人が先手で何かした結果どういうゲームにできるかとが決まればよいです。ここで問題はゲームを定義するためにゲームを使っていることですが、なんとかなります。残り何手以内のゲームかでもって話を切れば、残り0手のゲームを定義するためにゲームを使う必要がないので、めでたくゲームを定義していくことができる(ちなみにMamameさんはもっとエレガントなことをしています)。
それで残りn+1手以内のゲームとは何か。まず、残りn手以内のゲームは、残りn+1手以内のゲームでもありますね。めでたい。それから、左の人が移れる行けるゲームと右の人が移れるゲームを決めてもいいですね。この、nからn+1にうつるところを、ゲームどもからゲームどもを決めるしかけとして実装してみましょう。
Inductive step (orig: Type): Type :=
| inherit: orig -> step orig (* もともとゲームだったものはゲームのまま *)
| compose: (orig -> Prop) -> (orig -> Prop) -> step orig
(* 左が動ける先のゲームを定義する述語と、右が動ける先のゲームを定義する述語があればよい *)
.
あとは、空の型から始めて、順々につくっていけばいいです。証明をCoqに通したい人はgithubから持っていってください。
Fixpoint game (m: nat): Type :=
match m with
| O => empty
| S m' => step (game m')
end.
game 0という型のものはないはずなので、game 0という型のものについての述語は簡単に定義できます。どんなgame 0のものを持ってこられても「にゃー」とか言っておけばいいのです。どうせ何も持ってこられないはずなので。
Definition charm: game 0 -> Prop.
intro.
destruct X.
Defined.
ひとたび「にゃー」と言えればゲームを作るのは簡単です。
Definition zero: game 1 := compose _ charm charm.
Definition one : game 2 := compose _ (fun _ => True) (fun _ => False).
Definition half: game 3 := compose _ (fun x => x = inherit _ zero) (fun y => y = one).
ついでにゲーム同士を比べるgleという関係を定義してみます。どっちのほうが左に有利、というのを比べます。擬順序になるつもりです。
Inductive gle: forall m n, game m -> game n -> bool -> Prop (* 定義は略 *)
これを使うと、さっき定義した3つのゲーム同士を比較できます。
Lemma zero_one: gle _ _ zero one true.
Lemma one_zero: gle _ _ one zero false.
Lemma zero_half: gle _ _ zero half true.
擬順序のつもりですから、たとえばreflexivityが成り立ちます。
refl : forall (m : nat) (g : game m), gle m m g g true (* 証明は略 *)
推移律も成り立つはずです、えーと、まだ証明していません。次回以降にやります。反射律と推移律があるなら、すくなくともpreorderとして圏になりますね。でも、ゲームがゲーム以下というのは、あっちのゲームの勝ち方がわかればこっちのゲームの勝ち方もわかるということで、戦略から戦略を計算する仕掛けと捉えることもできますから、もっと豊かな構造を持っていてもいいはずです…ということを考えている先人はたくさんいます。Joyal (1997)の英訳
いまのところ、m手以下のゲームというのを考えてきました。しかし、一手進めると、残り何手なのか決まるゲームというのを考えてもいいでしょう。どうせ終わるのですから。残りω手のゲームと言えるでしょう。残りn手のnのところに、自然数に限らず順序数を許しておけば、最初からこの手のゲームも扱えて幸せになれそうですね。いまは、ωのところだけ、書いておきましょう。
Inductive ogame : Type :=
| o_inherit: forall m, game m -> ogame
| o_compose: (forall m, game m -> Prop) -> (forall m, game m -> Prop) -> ogame
.
