Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC