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.