- 01/26 [Schedule/ProofCafe_27]()
- 時間: 14:30 - 17:30
- 場所: 名古屋大学　東山キャンパス　多元数理科学棟　309号室
- 参加登録: [PARTAKE: ProofCafe](http://partake.in/events/eac9889a-ac54-4cca-99e8-a26c0883ceb0)
- ソフトウェアの基礎
- ドキュメントは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]()

# 鳩の巣原理の証明

~~~
Lemma app_nil:forall{X:Type}(l: list X) ,
l ++ [] = l.
Proof. induction l.
  reflexivity.
  simpl. rewrite IHl. reflexivity.
Qed.


Lemma ai_comm : forall{X:Type} (l1 l2:list X) (x:X),
appears_in x(l1++l2)->appears_in x(l2++l1).
Proof.
 intros. SearchAbout appears_in. apply app_appears_in.
 apply or_commut. apply appears_in_app. apply H.
Qed.

Lemma  ai_later' : forall {X:Type} (l:list X) (x x0 :X),
x<>x0 -> appears_in x0 (x::l) -> appears_in x0 l.
Proof. intros.
 inversion H0. 

  rewrite H2 in H. destruct H. reflexivity.
  apply H2.
Qed.


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. generalize dependent l2. induction l1.
(* l1=[] のとき*) intros. inversion H0.

(* l1=x::l1 のとき*) intros. 
  destruct(EM(appears_in x l1)).

  (*appears_in x l1 のとき*)
   apply RP_hd. apply H1.

  (*~ appears_in x l1 のとき*)
   apply RP_tl. 
   destruct (appears_in_app_split x l2).
      (*appears_in_app_split x l2 の証明*)
      apply H.
      apply ai_here.
   destruct H2.
   apply IHl1 with (witness++witness0).
      (*forall x0 : X, appears_in x0 l1 
          -> appears_in x0 (witness ++ witness0)の証明*)
      intros. 
      assert(appears_in x0 l2).
         apply H. apply ai_later. apply H3.
      rewrite H2 in H4. apply ai_comm in H4.
      simpl in H4. apply ai_later' in H4.
         apply ai_comm. apply H4.
         intro. apply H1. rewrite H5. apply H3.
      (*length (witness ++ witness0) < length l1 の証明*)
      rewrite H2 in H0. rewrite app_length.
      rewrite app_length in H0. simpl in H0. rewrite <- plus_n_Sm in H0. 
      unfold lt. unfold lt in H0.
      apply Sn_le_Sm__n_le_m . apply H0.
Qed.
~~~