• 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.

鳩の巣原理の証明

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.
         destruct(EM (x=x0)).
            (*x-x0のとき*) rewrite H5 in H1. elimtype False. apply H1. apply H3.
            (*x<>x0のとき*) apply H5.
   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.