proposition: Theorem ramsey A (W : set A) n (P : Pinf W) B : forall (C : Pf B) (f : Pcard P (S n) -> elts C), Proper (Pcard_equiv ==> elts_eq) f -> exists c (Q : Pinf P), forall X : Pcard Q (S n), f (Pcard_subset Q X) = c.
proof: Proof. intro C; pattern C; apply card_ind; clear C; induction n0 as [|k IH]; intros C cardC f f_eq. exfalso. apply card_0 in cardC. destruct (f (Pcard_of_inf P n)) as [a aC]. unfold Pf_equiv in cardC. simpl in cardC. rewrite cardC in aC. fo. destruct (card_S cardC) as [c [D [CaD [naD cardD]]]]. assert (cC : mem c C). rewrite CaD. apply mem_add. set (c' := elt cC). destruct k. ex c'. set (Q := Pinf_self P). ex Q. intro X. destruct (f (Pcard_subset Q X)). apply sig_eq; simpl. apply card_0 in cardD. rewrite CaD, cardD in m. simpl in m. fo. destruct (card_S cardD) as [d [E [DdE _]]]. assert (dD : mem d D). rewrite DdE. apply mem_add. clear E DdE. set (g := fun X : Pcard P (S n) => match dec (Pf_val D (elt_val (f X))) with | left fXD => elt fXD | _ => elt dD end). assert (g_eq : Proper (Pcard_equiv ==> elts_eq) g). intros X Y XY. unfold g. apply f_eq in XY. rewrite XY. destruct (dec (Pf_val D (elt_val (f Y)))); refl. destruct (IH _ cardD _ g_eq) as [[e eD] [Q h1]]. destruct (dec (e=d)). subst e. set (j := fun X : Pcard Q (S n) => if eq_dec (elt_val (f (Pcard_subset Q X))) c then true else false). assert (j_eq : Proper (Pcard_equiv ==> eq) j). intros X Y XY. unfold j. case_eq (f (Pcard_subset Q X)); intros b bC fXb. apply sig_eq in fXb. rewrite (f_eq _ (Pcard_subset Q Y)) in fXb. apply sig_eq in fXb. rewrite fXb. refl. apply Pcard_subset_inj. hyp. destruct (ramsey_with_2_colors j_eq) as [b [[R [RQ Rinf]] h2]]. simpl in h2. assert (RP : R [<=] P). trans (Pinf_val Q). hyp. destruct Q as [Q [QP Qinf]]; hyp. set (R' := mk_Pinf RP Rinf). destruct b. ex c' R'. intro X. gen (h2 X). unfold j. destruct (eq_dec (elt_val (f (Pcard_subset Q (Pcard_subset RQ X)))) c). 2: discr. intros _. apply sig_eq. simpl. rewrite <- e. apply f_eq. unfold Pcard_equiv, Pf_equiv; simpl. apply Pcard_subset_inj. sym. apply Pcard_subset_equiv. refl. assert (dC : mem d C). rewrite CaD. simpl. unfold mem, add. auto. set (d' := elt dC). ex d' R'. intro X. gen (h1 (Pcard_subset RQ X)). gen (h2 X). unfold g, j. set (X' := Pcard_subset Q (Pcard_subset RQ X)). destruct (eq_dec (elt_val (f X')) c). discr. intros _. destruct (dec (Pf_val D (elt_val (f X')))). intro e. apply sig_eq in e; simpl in e. apply sig_eq; simpl. rewrite <- e. apply f_eq. apply Pcard_subset_equiv. unfold X'. sym. do 2 apply Pcard_subset_equiv. refl. exfalso. apply n1. revert n0. case_eq (f X'); intros b bC _. gen bC; intro bC'. rewrite CaD in bC. simpl. clear -bC. simpl in bC. fo. assert (eC : mem e C). rewrite CaD. simpl. unfold mem, add. auto. set (e' := elt eC). ex e' Q. intro X. gen (h1 X). unfold g. set (X' := Pcard_subset Q X). destruct (dec (Pf_val D (elt_val (f X')))); intro a; apply sig_eq in a; simpl in a; apply sig_eq; simpl; rewrite <- a. apply f_eq. refl. firstorder auto with exfalso. Qed.
imports: Coq(Morphisms Basics Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil DepChoice LogicUtil SetUtil FinSet InfSet NatUtil)