infinite Ramsey theorem

Stream: new members

[Jared Corduan]

hello, I've just finished a proof of the infinite Ramsey theorem. I would love feedback on what things I've done poorly, what things are weird, what things are redundant with mathlib, etc. Of course I realize that folks are busy with their own projects!

Would this be an appropriate thing for me create a mathlib PR for? I'm not sure if this is even a theorem that you would want in mathlib. PRs are a nice way, though, to get feedback. I have the code in a fork on github already.

[Kevin Buzzard]

It gets taught in maths departments at UG or MSc level so it passes that test. Can you post a link?

[Jared Corduan]

https://github.com/JaredCorduan/mathlib/blob/infinite_ramsey/src/combinatorics/ramsey/infinite.lean

[Johan Commelin]

@Jared Corduan Nice work! A superficial glance over the code tells me that it looks pretty good.

[Johan Commelin]

I would certainly suggest that you create a PR.

[Johan Commelin]

Probably it will generate a boatload of comments, but you should know in advance that those are meant constructively.

[Johan Commelin]

I also have a maths question (I don't know much about this area): Is there a generalization to more than two colours?

[Jared Corduan]

great, thank you! I'll be grateful for any and all feedback!

[Kevin Buzzard]

line 30 I am a bit muddled -- what is S_x? Is this true if x=0?
line 98 some cut and paste error

But in general -- mathlib has some style conventions which seem to demand that you are as brief as possible. People will suggest much shorter variants for proofs like lines 133 to 136 -- they wouldn't even go into tactic mode usually.

[Kevin Buzzard]

Johan -- "the same proof works" for finitely many colours, as we mathematicians say...

[Johan Commelin]

@Jared Corduan Also, for this to be applicable, you would have to state another version of your theorem that works for arbitrary types of cardinality 2.

[Jared Corduan]

yes, the proof for coloring n-element sets with k-colors is an "easy" generalization. I could describe it in a couple sentences here, but I think the proof in lean would take me a bit of work. :) it's just induction on the number of colors, then induction on the size of the sets.

[Johan Commelin]

So, is this the base case of the induction?

[Kevin Buzzard]

def reds (f : ℕ → color) (H : set ℕ) := (λ n : ℕ, f n = red ∧ n ∈ H ) -- are you better off just using sets here? You could define this as an intersection of sets.

[Johan Commelin]

Or does the general proof avoid this case?

[Jared Corduan]

yes, exactly @Johan Commelin . I thought the red and blue was easy to work with, and easy to read. but maybe it's too cute.

[Johan Commelin]

No, that's fine for the proof.

[Johan Commelin]

But you should afterwards restate your theorem

[Johan Commelin]

With a 2-line proof where you reduce to the case of colors

[Johan Commelin]

I can imagine that the inductive type is quite useful during the proof.

[Kevin Buzzard]

for things like line 102 people will encourage you to move x and y to the left of the colon -- it doesn't change the term but makes the proof shorter (you don't need the lambda). But yeah PR and you'll get a bunch of comments like this.

[Johan Commelin]

Do you (@Jared Corduan or @Kevin Buzzard) know of applications of this theorem?

[Kevin Buzzard]

A logician taught it me, they were interested in fancier statements involving cardinals.

[Jared Corduan]

@Kevin Buzzard sorry if the informal proof in the header is confusing. S_x is one of the sets in the(S_i, x_i) sequence. and yes, that line is true for i = 0., but it should say S_{x_{i+1}}.

[Jared Corduan]

as for applications, yea, Ramsey himself had it as a lemma in a logic paper :)

[Jared Corduan]

and indeed you can generalize it, you can travel to large cardinal land if you want

[Jared Corduan]

there's a finite version too, which follows by compactness. I was considering using @Jesse Michael Han 's compactness proof to show this...

[Jared Corduan]

the finite version probably has more applications, but I'm no expert. I think it is used in termination proofs in CS.

[Jared Corduan]

some of the generalization/related theorems are interesting in themselves, I'd claim. Such as Hindman's theorem.

[Johan Commelin]

Ok, cool. Then we certainly want a version that is "applicable" (in the sense that the user-facing version of this theorem should not mention color).

[Jesse Michael Han]

there's a finite version too, which follows by compactness. I was considering using Jesse Michael Han 's compactness proof to show this...

congrats on finishing! while i doubt Flypitch's FOL library will be PR'd to mathlib anytime soon, it would be exciting to see a "real-world" application of it

[Jared Corduan]

@Kevin Buzzard I like the idea of defining reds better, maybe using intersection. That was just the first thing I thought to use. Indeed there is a silly copy paste. I'm more than happy to move variables to which ever side of the colon folks like! I'd love shorter proofs, I just always can't find them!

[Jesse Michael Han]

also, Ramsey's theorem is # 31 on Freek's list (and it looks like it hasn't been done in Lean yet)

[Jared Corduan]

the base case @Johan Commelin is: for size of sets: base case is n=1, ie the pigeon hole principle. for colors, base case is k=2. fix n, I'll show you the color argument - color the first two colors by a new color. now you have a (k-1) coloring. use RT. if you are in one of the old colors, great, done. otherwise now you have a two coloring. qed. then here's the induction on n: for each natural m, you induce a (n-1) coloring by fixing that number m. so use RT for each number. this gives a coloring of singletons, so use the PHP.

[Jared Corduan]

I wasn't sure if # 31 was the finite or infinite version, or if it mattered :)

[Jared Corduan]

I really just used red and blue, and similarly unordered pairs as I defined, since I was having a lot of trouble using finite sets. but that's probably just my own ignorance.

[Johan Commelin]

Great, I suggest you include the n-colored version. It doesn't seem too hard to prove...

[Johan Commelin]

And maybe you can also generalize nat to arbitrary infinite types?

[Jared Corduan]

it's not hard, it's just work :) and it'll get me up to speed with finite sets.

[Jared Corduan]

I'll have to think about infinite types. there are generalizations to ordinals, where it is only sometimes true.

[Jared Corduan]

it's easy to bump into unsolved problems here

[Jared Corduan]

I think I'd like to put what I have up for a PR now, work through suggestions, and then try for the RT^n_kafterwards, if that's cool.

[Johan Commelin]

This is reasonably sized already, so yes... PR this first

[Jared Corduan]

please let me know if chatting here is fine, or if it would be better to use github for this kind of thing.

I had a few minutes today, so I tried to address one of the review comments on my ramsey theorem PR, namely reconciling my definition of infinite with that in data.set.fintype (namely fintype α → false). One direction was easy for me, but the other I'm having a bit of trouble with.

I named my definition infinite', which isn't a great name. maybe normally you all just use namespaces to handle such separate definitions? anyway, at ITP 2019, @Mario Carneiro showed me some marvelous magic for pushing a negation through quantifiers, which is to use simp [not_forall, not_exists]. I can't get it to work in a different situation now, though, and was wondering what I am doing wrong. (I know how to manually prove the flip-flopping quantifiers, but this seems ugly...)

def infinite' (H : set ℕ) := ∀ x : ℕ, ∃ y : ℕ, x < y ∧ y ∈ H

lemma infinite_equiv (H : set ℕ) (h : ¬ infinite' H) : finite H :=
begin
  have hf : ∃ x, ∀ y, ¬ (x < y ∧ y ∈ H),
    simp [infinite', not_forall, not_exists] at h, -- why does Mario's magic not work here?
    sorry,
  simp at hf,
  cases hf with x hx,
  sorry,  -- is there a matlib theorem that says bounded sets of nats have fintype?
end

[Mario Carneiro]

There is a tactic for this BTW, which others will point out soon enough

[Jared Corduan]

ah, thank you! I just learned about the PR reviews channel and I'm talking with @Johan Commelin there. :)

[Mario Carneiro]

The reason the simp line doesn't work is because you need to use classical reasoning to make the not_forall lemma trigger

[Mario Carneiro]

use classical, at the beginning of the proof

[Jared Corduan]

ah! thank you!