proposition: Theorem ramsey_with_2_colors : forall n (P : Pinf W) (f : Pcard P (S n) -> bool), Proper (Pcard_equiv ==> eq) f -> exists b (Q : Pinf P), forall X : Pcard Q (S n), f (Pcard_subset Q X) = b.
proof: Proof. induction n; intros P f f_eq. destruct (IPHP_with_2_holes P (g P f)) as [b [Q h]]. ex b Q. intros [X [XQ cX1]]. destruct (card_S cX1) as [a [Y [XaY [naY cY0]]]]. assert (aQ : mem a Q). apply XQ. change (mem a X); rewrite XaY. simpl. fo. rewrite <- (h _ aQ). unfold g; simpl. apply f_eq. unfold Pcard_equiv; simpl. rewrite Pf_singleton_eq, XaY, (card_0 cY0). refl. revert IHn P f f_eq. generalize (S n); clear n; intros n IH P f f_eq. set (R (Q : Pinf P) c := fun U V : Pinf Q => exists a (aU : mem a U) (VU_a : V [<=] rem a U), forall X : Pcard V n, f (i aU VU_a X) = c). assert (L : forall (Q : Pinf P) c, (forall U, exists V, R Q c U V) -> exists T : Pinf P, forall X : Pcard T (S n), f (Pcard_subset T X) = c). intros Q c RQc_total. destruct (@dep_choice _ (Pinf_self Q) (R Q c) RQc_total) as [V [hV V0]]. assert (VP : forall k, V k [<=] P). intro k. simpl. trans (Pinf_val Q). destruct (V k) as [Vk [VkQ Vkinf]]; hyp. destruct Q as [Q [QP Qinf]]; hyp. assert (b_spec : forall k, exists b (bVk : mem b (V k)) (VSkVk_b : V (S k) [<=] rem b (V k)), forall X : Pcard (V (S k)) n, f (i bVk VSkVk_b X) = c). intro k. destruct (hV k) as [b [bVk [VSkVk_b h]]]. ex b bVk VSkVk_b. hyp. set (b := fun k => proj1_sig (cid (b_spec k))). assert (bV : forall k, mem (b k) (V k)). intro k. unfold b. destruct (cid (b_spec k)) as [a [a1 [a2 a3]]]. hyp. assert (VSV_b : forall k, V (S k) [<=] rem (b k) (V k)). intro k. unfold b. destruct (cid (b_spec k)) as [a [a1 [a2 a3]]]. hyp. assert (Vf : forall k (X : Pcard (V (S k)) n), f (i (bV k) (VSV_b k) X) = c). intros k X. case_eq (cid (b_spec k)); intros a [a1 [a2 a3]] e. rewrite <- (a3 X). apply f_eq. unfold Pcard_equiv, Pf_equiv. rewrite !i_eq. unfold b. rewrite e; simpl. refl. assert (nbVS : forall k, ~mem (b k) (V (S k))). intros k h. rewrite VSV_b in h. revert h. apply notin_rem. assert (Vle : Proper (le --> subset) V). intros l k. unfold flip. revert k l. intro k. induction l; intro hl. assert (k=0). lia. subst. refl. destruct (le_dec k l) as [kl|nkl]. trans (Pinf_val (V l)). 2: apply IHl; hyp. rewrite VSV_b. apply subset_rem. assert (k=S l). lia. subst. refl. assert (VSlt : forall k, V (S k) [<] V k). intro k. rewrite VSV_b. apply strict_subset_rem. apply bV. assert (lt_nbV : forall k l, k < l -> ~mem (b k) (V l)). intros k l kl h. apply Vle in kl. apply kl in h. revert h. apply nbVS. set (B := fun x => exists k, x = b k). assert (bB : forall k, mem (b k) B). intro k. ex k. refl. assert (BP : B [<=] P). intros x [k e]. subst. eapply VP. apply bV. assert (Binf : infinite B). apply infinite_inj. ex (fun k => elt (bB k)). intros k l e. apply sig_eq in e; simpl in e. destruct (lt_dec k l) as [kl|nkl]. apply lt_nbV in kl. rewrite e in kl. gen (bV l). contr. destruct (lt_dec l k) as [lk|nlk]. apply lt_nbV in lk. rewrite <- e in lk. gen (bV k). contr. lia. set (B' := mk_Pinf BP Binf). ex B'. intro X'. case_eq X'; intros [X X_fin] [XB cXSn] Xeq; rewrite <- Xeq. destruct (card_S cXSn) as [a [Y [XaY [naY cYn]]]]. unfold Pf_equiv in XaY; simpl in XaY. assert (aX : mem a X). rewrite XaY. apply mem_add. gen aX; intro aX'. rewrite XB in aX'. destruct aX' as [kd abkd]. subst a. set (D := fun k => mem (b k) X). set (k0 := smallest (dec1 D) kd). gen (smallest_ok (dec1 D) aX). fold k0. intro bk0X. clear Y XaY naY cYn. set (Y := Pf_rem (b k0) X_fin). assert (YVSk0 : Y [<=] V (S k0)). intro x. unfold Y; simpl. unfold rem, mem. intros [nxbk0 xX]. gen xX; intro xX'. apply XB in xX'. destruct xX' as [k xbk]. subst x. assert (k0k : k0 < k). assert (k0k' : k0 <= k). unfold k0. apply smallest_comp; hyp. destruct (eq_nat_dec k0 k). rewrite e in nxbk0. cong. lia. unfold lt in k0k. apply (Vle _ _ k0k). apply bV. assert (cYm : card Y = n). unfold Y. rewrite card_rem. unfold mk_Pf. rewrite cXSn. simpl. destruct (dec (mem (b k0) X)). lia. contr. set (Y' := mk_Pcard YVSk0 cYm). rewrite <- (Vf k0 Y'). apply f_eq. unfold Pcard_equiv, Pf_equiv. rewrite i_eq. apply Pcard_subset_equiv. rewrite Xeq. unfold Y', mk_Pcard; simpl. sym. apply add_rem. apply eq_dec. hyp. set (P' := Pinf_self P). destruct (classic (forall U, exists V, R P' true U V)) as [R_P_true_total|R_P_true_not_total]. ex true. eapply L. apply R_P_true_total. rewrite not_forall_eq in R_P_true_not_total. destruct R_P_true_not_total as [E' hE]. revert hE. rewrite not_exists_eq. case_eq E'; intros E [EP Einf] Eeq; rewrite <- Eeq. intro hE. assert (R_E_false_total : forall U, exists V, R E' false U V). intro U'. case_eq U'; intros U [UE' Uinf] Ueq; rewrite <- Ueq. gen UE'; intro UE. rewrite Eeq in UE. simpl in UE. destruct (infinite_not_empty Uinf) as [a aU]. set (T := rem a U). assert (TW : T [<=] W). unfold T. trans U. apply subset_rem. trans E; auto. trans (Pinf_val P'); auto. unfold P'; simpl. destruct P as [P [PW Pinf]]; hyp. assert (Tinf : infinite T). unfold T. rewrite infinite_rem. hyp. set (T' := mk_Pinf TW Tinf). assert (aP : mem a P). rewrite UE, EP in aU. hyp. assert (naT : ~mem a T'). simpl. unfold T. apply notin_rem. assert (TP : T' [<=] P). simpl. unfold T. rewrite subset_rem. trans E; hyp. set (g := fun X : Pcard T' n => f (j n aP naT TP X)). assert (g_equiv : Proper (Pcard_equiv ==> eq) g). intros X Y. unfold Pcard_equiv, Pf_equiv. intro XY. unfold g. apply f_eq. unfold Pcard_equiv, Pf_equiv. rewrite !j_eq. rewrite XY. refl. destruct (IH _ _ g_equiv) as [b [Q hQ]]. destruct b. exfalso. set (Q' := Pinf_subset TP Q). eapply hE with (x := Q'). unfold R. assert (aE' : mem a E'). apply UE'. hyp. assert (QE'_a : Q' [<=] rem a E'). unfold Q', Pinf_subset. destruct Q as [Q [QT Qinf]]; simpl. trans (Pinf_val T'). hyp. simpl. unfold T. rewrite UE'. refl. ex a aE' QE'_a. intro X. assert (Q'Q : Q' [<=] Q). unfold Q', Pinf_subset. destruct Q as [Q [QT Qinf]]; simpl. refl. rewrite <- (hQ (Pcard_subset Q'Q X)). unfold g. apply f_eq. unfold Pcard_equiv, Pf_equiv. rewrite i_eq, j_eq. apply add_equiv. refl. unfold Pcard_subset. destruct X as [X [XQ' cXn]]; simpl. refl. assert (T'E' : T' [<=] E'). simpl. unfold T. rewrite subset_rem. hyp. set (Q' := Pinf_subset T'E' Q). ex Q'. unfold R. assert (aU' : mem a U'). rewrite Ueq. hyp. assert (Q'U'_a : Q' [<=] rem a U'). unfold Q', Pinf_subset. destruct Q as [Q [QT Qinf]]; simpl. trans (Pinf_val T'). hyp. simpl. unfold T. rewrite Ueq. refl. ex a aU' Q'U'_a. intro X. assert (Q'Q : Q' [<=] Q). unfold Q', Pinf_subset. destruct Q as [Q [QT Qinf]]; simpl. refl. rewrite <- (hQ (Pcard_subset Q'Q X)). unfold g. apply f_eq. unfold Pcard_equiv, Pf_equiv. rewrite i_eq, j_eq. apply add_equiv. refl. unfold Pcard_subset. destruct X as [X [XQ' cXn]]; simpl. refl. ex false. eapply L. apply R_E_false_total. Qed.
imports: Coq(Morphisms Basics Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil DepChoice LogicUtil SetUtil FinSet InfSet NatUtil)