Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
1
Help us understand the problem. What is going on with this article?
@41semicolon

# Coq で二人じゃんけん

More than 1 year has passed since last update.

# 1. データ型と各種関数

まず、互いに排他なグー・チョキ・パーという３つの状態をとるモノを `Hand`としましょう。`Inductive` で定義できます:

``````Inductive Hand: Type := | G | C | P.
``````

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

# 2. 定理証明

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

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

``````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. 振り返り

N人ジャンケン: これを拡張してN人ジャンケンを考えるのは面白そうだけれど、根本的に色々変えなければいけないと思います。プレイヤー識別子とハンドのペア `nat*Hand``list`または`Ensemble` に対して、勝負がつくときには、その部分集合のSomeを、あいこの場合は None を返すようにすればよさそうです。定理として「N人全員が勝者(敗者)にならない」とか「勝者が1人だけとは限らない」とかでしょうか。list/Ensemble に対しても制約が必要です。１人ではジャンケンが成立しなさそうなので。また、`induction` を使って上記の定理が任意の人数でのジャンケンでも成立することをしょうめいすることもできそうです。

1
Help us understand the problem. What is going on with this article?
Why not register and get more from Qiita?
1. We will deliver articles that match you
By following users and tags, you can catch up information on technical fields that you are interested in as a whole
2. you can read useful information later efficiently
By "stocking" the articles you like, you can search right away

Comments

No comments
Sign up for free and join this conversation.
Sign Up
If you already have a Qiita account Login
1
Help us understand the problem. What is going on with this article?