Library CoLoR.Util.Set.Ramsey

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2014-12-11

Infinite Ramsey theorem

After "On a Problem of Formal Logic", F. P. Ramsey, London Math. Soc. s2-30(1):264-286, 1930, doi:10.1112/plms/s2-30.1.264.

Set Implicit Arguments.

Section S.

  Variables (A : Type) (W : set A).

Infinite pigeon-hole principle with two holes.

  Lemma IPHP_with_2_holes (P : Pinf W) (f : elts P -> bool) :
    exists b (Q : Pinf P), forall x (i : mem x Q), f (elt (Pinf_sub Q _ i)) = b.

Ramsey theorem with 2 colors only.

  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.

End S.

Ramsey theorem with a finite set of colors.

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.