## Stream: new members

### Topic: infinite Ramsey theorem

#### Jared Corduan (Sep 18 2019 at 16:42):

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 (Sep 18 2019 at 16:43):

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

#### Jared Corduan (Sep 18 2019 at 16:44):

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

#### Johan Commelin (Sep 18 2019 at 16:53):

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

#### Johan Commelin (Sep 18 2019 at 16:53):

I would certainly suggest that you create a PR.

#### Johan Commelin (Sep 18 2019 at 16:54):

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

#### Johan Commelin (Sep 18 2019 at 16:55):

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 (Sep 18 2019 at 16:55):

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

#### Kevin Buzzard (Sep 18 2019 at 16:55):

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 (Sep 18 2019 at 16:56):

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

#### Johan Commelin (Sep 18 2019 at 16:56):

@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 (Sep 18 2019 at 16:56):

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 (Sep 18 2019 at 16:57):

So, is this the base case of the induction?

#### Kevin Buzzard (Sep 18 2019 at 16:57):

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 (Sep 18 2019 at 16:57):

Or does the general proof avoid this case?

#### Jared Corduan (Sep 18 2019 at 16:57):

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 (Sep 18 2019 at 16:57):

No, that's fine for the proof.

#### Johan Commelin (Sep 18 2019 at 16:57):

But you should afterwards restate your theorem

#### Johan Commelin (Sep 18 2019 at 16:58):

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

#### Johan Commelin (Sep 18 2019 at 16:58):

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

#### Kevin Buzzard (Sep 18 2019 at 16:58):

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 (Sep 18 2019 at 16:58):

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

#### Kevin Buzzard (Sep 18 2019 at 16:59):

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

#### Jared Corduan (Sep 18 2019 at 17:01):

@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 (Sep 18 2019 at 17:01):

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

#### Jared Corduan (Sep 18 2019 at 17:01):

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

#### Jared Corduan (Sep 18 2019 at 17:02):

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 (Sep 18 2019 at 17:03):

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

#### Jared Corduan (Sep 18 2019 at 17:04):

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

#### Johan Commelin (Sep 18 2019 at 17:06):

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 (Sep 18 2019 at 17:06):

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 (Sep 18 2019 at 17:06):

@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 (Sep 18 2019 at 17:10):

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

#### Jared Corduan (Sep 18 2019 at 17:11):

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 (Sep 18 2019 at 17:11):

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

#### Jared Corduan (Sep 18 2019 at 17:13):

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 (Sep 18 2019 at 17:16):

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

#### Johan Commelin (Sep 18 2019 at 17:16):

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

#### Jared Corduan (Sep 18 2019 at 17:16):

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

#### Jared Corduan (Sep 18 2019 at 17:17):

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

#### Jared Corduan (Sep 18 2019 at 17:18):

it's easy to bump into unsolved problems here

#### Jared Corduan (Sep 18 2019 at 17:19):

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 (Sep 18 2019 at 17:21):

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

#### Jared Corduan (Oct 03 2019 at 17:20):

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 (Oct 03 2019 at 17:25):

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

#### Jared Corduan (Oct 03 2019 at 17:26):

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

#### Mario Carneiro (Oct 03 2019 at 17:27):

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 (Oct 03 2019 at 17:27):

use classical, at the beginning of the proof

#### Jared Corduan (Oct 03 2019 at 17:27):

ah! thank you!

Last updated: May 08 2021 at 03:17 UTC