Anarchy Proof - PHP
テスト前なので、逃避にCoPL(http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi)やら、Anarchy Proofやらばっかりやってます。
今回の問題は、いわゆる鳩ノ巣原理ですね。
自然数のリストxsがあって、length xs < sum xs ならxsのなかに1より大きい要素があるというのを示せばよい問題です。
xsについて帰納法+ xsがnilでないなら先頭の要素が0か1かそれ以上で場合わけしました。
例によって、autoとか使ってないので、長い……
あと、手元(Coq8.3だったかな?)にはlt_z_Snに相当する命題がlt_0_Snっていう名前であるんですけど、サブミットするとそんな命題ねーよって言われたので、自分で証明してます、なんで……
Require Import Definitions. Require Import Lists.List. Require Import Arith. Lemma lt_z_Sn : forall n : nat, 0 < S n. Proof. induction n. apply lt_n_Sn. assert (S n < S (S n)). apply lt_n_Sn. apply lt_trans with (m := S n); assumption. Qed. Theorem Pigeon_Hole_Principle : forall (xs : list nat), length xs < sum xs -> (exists x, 1<x /\ In x xs). Proof. intros. induction xs. contradict H. simpl; exact (lt_irrefl 0). destruct a. assert (S (length xs) < sum xs). simpl in H; assumption. assert (exists x : nat , 1 < x /\ In x xs). apply IHxs. assert (length xs < S (length xs)). apply lt_n_Sn. apply lt_trans with (m := S (length xs)); assumption. simpl. destruct H1. exists x. split. exact (proj1 H1). right; exact (proj2 H1). destruct a. simpl in H. assert (length xs < sum xs). apply lt_S_n; assumption. assert (exists x : nat , 1 < x /\ In x xs). apply IHxs; assumption. destruct H1. simpl. exists x. split. exact (proj1 H1). right; exact (proj2 H1). exists (S (S a)). split. apply lt_n_S; apply lt_z_Sn. simpl. left. reflexivity. Qed.