- 01/26 [Schedule/ProofCafe_27]()
- 時間: 14:30 - 17:30
- 場所: 名古屋大学　東山キャンパス　多元数理科学棟　309号室
- 参加登録: PARTAKE: ProofCafe
- ソフトウェアの基礎
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: http://proofcafe.org/sf/sfja.tar.gz
- ハッシュタグ: #proofcafe
- 参加人数: 6人

### nostutterの定義

- [https://twitter.com/t6s/status/295051241258639361]()
- [https://twitter.com/maeda_/status/295051256102277121]()
- [https://twitter.com/yoshihiro503/status/295051547941928960]()
- [https://twitter.com/suharahiromichi/status/295052180631744514]()

### repeatsの定義
- [https://twitter.com/yoshihiro503/status/295059014348308481]()


# or_commが適用できない
~~~
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.
~~~