[English](/en/Front Page)

# 至急解決求む。 or_commが適用できない(8.4pl1)

Theorem pigeonhole_principle: forall {X:Type} (l1 l2:list X),
  excluded_middle ->
  (forall x, appears_in x l1 -> appears_in x l2) ->
  length l2 < length l1 ->
  repeats l1.
Proof.
intros X l1 l2 EM.
unfold excluded_middle in EM.
assert (forall P, ~~P -> P) as NNPP.
  intros.
  destruct (EM P); [assumption | ].
  elimtype False; exact (H H0).
revert l2.
induction l1.

  simpl; intros.
  inversion H0.

  simpl.
  intros.
  apply NNPP; intro L1; apply L1.
  destruct (EM (appears_in x l1)).

    apply RP_hd.
    assumption.

    apply RP_tl.
    destruct (appears_in_app_split x l2).

      apply H.
      apply ai_here.

      destruct H2.
      apply (IHl1 (witness++witness0)).
      intros.
      rewrite H2 in *; clear H2.
      cut (appears_in x0 (witness ++ x :: witness0)).

        intro.
        apply app_appears_in.
        destruct (EM (appears_in x0 witness)).

          left; assumption.

          apply NNPP.
          intro L2.
          apply L2.
          generalize (or_comm (appears_in x0 witness) (appears_in x0 witness0)); intro.
          destruct H5.
          set (M := appears_in x0 witness) in *.
          set (N := appears_in x0 witness0) in *.
          apply H6.


# ProofCafe

ProofCafeは名古屋でプログラムの証明について勉強する勉強会です。現在は[ソフトウェアの基礎](http://proofcafe.org/sf/)というドキュメントを読んでいます。コーヒーを飲みながら楽しく証明しましょう。

- 日時 : 毎月第4土曜 14:30〜17:00ごろまで。 
- ハッシュタグ: [#proofcafe](http://twitter.com/#!/search/realtime/%23proofcafe)

## 次回勉強会とこれまでの活動
[スケジュール](Schedule)

## 過去読んでいた文書
- [CPDT]()

![勉強会の様子](http://s1-02.twitpicproxy.com/photos/large/429834625.jpg)

## ProofCafeのメンバーが作ったもの作っているもの
### Coqで実装
- [マーク&スイープGC](http://github.com/mzp/gc)
- [ocamltter](): ターミナルで動作する対話的twitterクライアント
- [MessagePackライブラリ](http://github.com/mzp/msgpack-ocaml)

### Coqの拡張
- [Coq2Ruby](http://github.com/mzp/coq-ruby)
- [Coq2Clojure](http://patch-tag.com/r/leque/coq-clojure-ext/home)
- [Coq2Scala]()
- [Coq2Javascript](http://bitbucket.org/yoshihiro503/coq2javascript)

## Coqの応用
- [cochin](http://proofcafe.org/cochin/)
- [Coq for iPad](https://github.com/mzp/coq-for-ipad)

## 勉強したことしてること
- [Coq]()
- [ProofGeneral]()
- [coq_makefile]()

## リンク
- [ocaml-nagoya](http://www.itpl.co.jp/ocaml-nagoya/)