習作。ジャンケンに関する定理を証明してみます。
1. データ型と各種関数
まず、互いに排他なグー・チョキ・パーという３つの状態をとるモノを Handとしましょう。Inductive で定義できます:
Inductive Hand: Type := | G | C | P.
二人ジャンケンでは、勝ちの定義を定めれば、負けとあいこは定義できます。つまり、「xがyに勝つ」と「yがxに負ける」が同値であり、「xとyに勝ち負けのどちらも当てはまらない」であいこが定義できます。これらはHand型の二項関係ですが、決定可能な述語（排中律が成立する / 表現可能な述語である）ので Hand->Hand->Prop ではなく Hand->Hand->Bool の方が扱いやすいです:
Require Import Bool.
Definition win h1 h2 := match h1, h2 with
| G, C => true
| C, P => true
| P, G => true
| _, _ => false end.
Definition lose h1 h2 := win h2 h1.
Definition draw h1 h2 := negb (win h1 h2 || lose h1 h2).
以上で、Hand, win, lose, draw が定義できました。これらに関する定理を証明してみます。
2. 定理証明
以下証明の見た目の煩雑さを避けるために以下の Ltac ok を定義します。
Ltac ok:= trivial.
2-1. 勝ちか負けかあいこ
「xがyに勝つ」か「xがyに負ける」か「xとyはあいこ」の三つの内どれかが実現されると期待されます。まずは総調べで証明してみます:
Theorem some_of_three: forall h1 h2,
(win h1 h2) || (lose h1 h2) || (draw h1 h2) = true.
Proof.
intros. destruct h1. destruct h2. ok. ok. ok. destruct h2. ok. ok. ok. destruct h2. ok. ok. ok. Qed.
上述の定義を思い出すと別の方法でも証明できそうです。つまり draw, lose を unfold してあげれば自明なのでは？と気づきます:
Theorem some_of_three': forall h1 h2,
(win h1 h2) || (lose h1 h2) || (draw h1 h2) = true.
Proof.
intros. unfold draw. unfold lose. apply orb_negb_r. Qed.
後は win, lose, draw が互いに排他であることを証明できればよさそうです。
Theorem excl_win_lose: forall h1 h2,
(win h1 h2) && (lose h1 h2) = false.
Proof.
intros. destruct h1. destruct h2. ok. ok. ok. destruct h2. ok. ok. ok. destruct h2. ok. ok. ok. Qed.
Theorem excl_win_draw: forall h1 h2,
(win h1 h2) && (draw h1 h2) = false.
Proof.
intros. unfold draw. unfold lose. rewrite negb_orb. rewrite andb_assoc. rewrite andb_negb_r. ok. Qed.
Theorem excl_lose_draw: forall h1 h2,
(lose h1 h2) && (draw h1 h2) = false.
Proof.
intros. unfold draw. rewrite orb_comm. rewrite negb_orb. rewrite andb_assoc. rewrite andb_negb_r. ok. Qed.
2-2. 勝者は1人
勝負がつくときは、片方が勝者で片方が敗者であるはずです。
(* 補助定理 *)
Lemma implb_id: forall x:bool, implb x x = true.
Proof. intro. case x. ok. ok. Qed.
Theorem one_winner: forall h1 h2,
implb (win h1 h2) (lose h2 h1) = true.
Proof.
intros. unfold lose. apply implb_id. Qed.
Theorem one_loser: forall h1 h2,
implb (lose h1 h2) (win h2 h1) = true.
Proof.
intros. unfold lose. apply one_winner. Qed.
あいこの場合は、勝者も敗者もいません。
Theorem no_winner: forall h1 h2,
implb (draw h1 h2) (negb (win h1 h2 || win h2 h1)) = true.
Proof.
intros. unfold draw. unfold lose. apply implb_id. Qed.
Theorem no_loser: forall h1 h2,
implb (draw h1 h2) (negb (lose h1 h2 || lose h2 h1)) = true.
Proof.
intros. unfold lose. rewrite orb_comm. apply no_winner. Qed.
2-3. 必勝法はない
ジャンケンでは、必ず勝てる手というのは存在しません。三すくみだからです。同様に必ず負ける手というのもありません。証明してみましょう:
Theorem no_strongest: ~exists h1, forall h2, win h1 h2 = true.
Proof. intro. destruct H. destruct x. discriminate (H G). discriminate (H C). discriminate (H P). Qed.
Theorem no_weakest: ~exists h1, forall h2, lose h1 h2 = true.
Proof. intro. destruct H. destruct x. discriminate (H G). discriminate (H C). discriminate (H P). Qed.
3. 振り返り
勝負を別の方向で実装する方法もあった: 勝ち負けを winなどのHand->Hand->Bool という関数で実装したけれど、そうではない方向性もあったと思います。つまり、勝負がつく場合には勝者を x として Some x を返し、あいこの場合は None を返すような Hand->Hand->option Handな関数として実装もできたかもしれない。そっちのほうが各種定理はよりスッキリした形になるかもしれない。
N人ジャンケン: これを拡張してN人ジャンケンを考えるのは面白そうだけれど、根本的に色々変えなければいけないと思います。プレイヤー識別子とハンドのペア nat*Hand の listまたはEnsemble に対して、勝負がつくときには、その部分集合のSomeを、あいこの場合は None を返すようにすればよさそうです。定理として「N人全員が勝者(敗者)にならない」とか「勝者が1人だけとは限らない」とかでしょうか。list/Ensemble に対しても制約が必要です。１人ではジャンケンが成立しなさそうなので。また、induction を使って上記の定理が任意の人数でのジャンケンでも成立することをしょうめいすることもできそうです。