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