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