Revision e9524431f0bff944250edbc169e3131fb0effabb

Schedule/ProofCafe_27

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

nostutterの定義

repeatsの定義

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.