1羽より多く鳩を見つけるアルゴリズム

Coq アルゴリズム

概要

鳩の巣原理(あるいはディリクレの箱入れ原理、部屋割り論法)の構成的な証明は、
1羽より多く鳩が入っている巣を見つけるアルゴリズムである。

動機

ある日鳩の巣原理がアルゴリズムに見えてきたのでCoqで書いてみた。

命題とアルゴリズム

鳩の巣原理（はとのすげんり）またはディリクレの箱入れ原理（はこいれげんり）とは、n 羽の鳩が m 個の巣にいるとき、n > m であれば、少なくとも1個の巣には1羽より多い鳩が中にいる、という原理である。別の言い方をすれば、1つの箱に1つの物を入れるとき、m 個の箱には最大 m 個の物しか入れることができない（もう1つ物を入れたいなら、箱の1つを再利用しないといけないから）、ということである。

http://ja.wikipedia.org/wiki/鳩の巣原理

鳩の巣原理を証明するためには、絶対に鳩が1羽より多い巣が見つかる
アルゴリズムを与えればよい。
アルゴリズムとその正当性はだいたいこんな感じ。

  1. (巣の数 < 鳩の数の合計)が成立している
  2. 先頭の巣を見て、1羽より多かったらその数を出力して終了
  3. 1羽以下だったらその巣および中の鳩を除くと(巣の数 < 鳩の数の合計)が依然として成立するので除いて(1.)に戻る
  4. (3.)で，もし全ての巣を取り除いてしまったら、巣の数 = 0、 鳩の数 = 0なので(1.)に矛盾する。したがって巣がなくなる前にどこかで1羽より多い鳩が見つかっているはず

って、先頭から見ていくだけじゃん。
なお、このアルゴリズムが止まるためには巣の数が有限である必要がある。

実装

以下Coqで。

Definition nest := nat.
Definition pigeons : list nest -> nat := fold_right plus 0.
Definition num_nests : list nest -> nat := @length nest.

巣を中に入っている鳩の数で表現する。
巣の列を、巣のリストで表現する。
鳩の数を、巣のリスト中の鳩の数を全部加えて計算する。
巣の数を、リストの長さだとする。
その上で、以下の型を持つ関数を作る。

Definition somePigeons (ns : list nest) : 
  (num_nests ns < pigeons ns) -> {n : nest | 1 < n /\ In n ns}.

このsomePigeonsは、巣の数よりも鳩の数が多いことの証明を引数にとって、
1よりも多い、いずれかの巣の鳩の数を出力するプログラムである。
以下ソースコード全体。

Require Import Lt Compare_dec List Plus.
Set Implicit Arguments.

Definition nest := nat.
Definition pigeons : list nest -> nat := fold_right plus 0.
Definition num_nests : list nest -> nat := @length nest.

Lemma notlt00 : ~ 0 < 0.
apply lt_irrefl.
Qed.

Lemma plus_le1 : forall l m n : nat,
  n <= 1 -> S l < n + m -> l < m.
intros.
change (1 + l < n + m) in H0.
assert (n + (1 + l) < 1 + (n + m)).
apply plus_le_lt_compat; assumption.
rewrite plus_permute in H1.
repeat rewrite plus_assoc in H1.
apply (plus_lt_reg_l _ _ _ H1).
Qed.

Definition somePigeons (ns : list nest) : 
  (num_nests ns < pigeons ns) -> {n : nest | 1 < n /\ In n ns}.

refine (fix somePigeons' (ns : list nest) : 
  (num_nests ns < pigeons ns) -> {n : nest | 1 < n /\ In n ns} :=
  match ns as ns return
    (num_nests ns < pigeons ns) -> {n : nest | 1 < n /\ In n ns} with
    | nil => fun H => match notlt00 H with end
    | cons n ns' => match le_lt_dec n 1 with
      | left prf => _
      | right prf => fun _ => exist _  n (conj prf (or_introl _ (refl_equal _)))
    end
  end).
intro H.
simpl in H.
assert (num_nests ns' < pigeons ns').
apply (plus_le1 _ prf); assumption.
destruct (somePigeons' ns' H0).
destruct a.
exists x.
split.
assumption.
apply or_intror.
assumption.
Defined.

Definition getPigeons (ns : list nest) (H : num_nests ns < pigeons ns) :=
  proj1_sig (somePigeons ns H).

Ltac lt :=
  match goal with
    | [ |- lt _ _] => repeat (try apply le_n; apply le_S)
  end.

Lemma lt35 : 3 < 5.
lt.
Qed.

(* 4 *)
Eval compute in (getPigeons (4 :: 0 :: 1 :: nil) lt35).
(* 4 *)
Eval compute in (getPigeons (0 :: 4 :: 1 :: nil) lt35).
(* 4 *)
Eval compute in (getPigeons (0 :: 1 :: 4 :: nil) lt35).
(* 3 *)
Eval compute in (getPigeons (3 :: 2 :: 0 :: nil) lt35).
(* 2 *)
Eval compute in (getPigeons (2 :: 3 :: 0 :: nil) lt35).

ltタクティックは改善の余地あり。
なお、plus_le1のような定理を証明するには、omegaタクティックが簡単。