## Stream: new members

### Topic: pigeonhole lemma

#### David Renshaw (Sep 09 2020 at 23:38):

Can anyone help me to simplify my proof of this pigeonhole lemma?

import data.finset.basic
import data.nat.basic
import tactic

lemma pidgeonhole :
∀ s: finset ℕ, ∀ f : ℕ → {x : ℕ // x ∈ s}, ∃ a b : ℕ, (a ≠ b ∧ f a = f b) :=
begin
apply @finset.induction ℕ (λ s: finset ℕ, ∀ f : ℕ → {x : ℕ // x ∈ s}, ∃ a b : ℕ, (a ≠ b ∧ f a = f b)),
{
intro,
exfalso,
exact (finset.not_mem_empty (f 0).val) (f 0).property,
},
intros n s hn hip f,
cases classical.em (∃k:ℕ, (∀ m:ℕ, k ≤ m → (f m).val ≠ n)) with hbounded hinf,
{
obtain ⟨k0, hk0⟩ := hbounded,
let fk: ℕ → {x // x ∈ s} := (λn:ℕ, ⟨(f (n + k0)).val, _⟩),
{
obtain ⟨a, ha⟩ := hip fk,
obtain ⟨b, hb⟩ := ha,
use (a + k0),
use (b + k0),
cases hb,
split,
{
intro heq,
apply hb_left,
},
simp at hb_right,
exact subtype.ext hb_right,
},
have hk0a := (hk0 (n + k0)) (nat.le_add_left _ _),
exact finset.mem_of_mem_insert_of_ne (f (n + k0)).property hk0a,
},
{
have hall : ∀k:ℕ, ¬(∀ m:ℕ, k ≤ m → (f m).val ≠ n) := not_exists.mp hinf,
let hk0 := hall 0,
have : (∃ m:ℕ, ¬(0 ≤ m → (f m).val ≠ n)) := not_forall.mp hk0,
obtain ⟨m0, hm0⟩ := this,
have hnn : 0 ≤ m0 ∧ ¬ (f m0).val ≠ n := not_imp.mp hm0,
have hfm0 : (f m0).val = n := not_not.mp hnn.2,

let hk1 := hall (m0 + 1),
have : (∃ m:ℕ, ¬(m0 + 1 ≤ m → (f m).val ≠ n)) := not_forall.mp hk1,
obtain ⟨m1, hm1⟩ := this,
have hnn1 : m0 + 1 ≤ m1 ∧ ¬ (f m1).val ≠ n := not_imp.mp hm1,
have hfm1 : (f m1).val = n := not_not.mp hnn1.2,
use m0,
use m1,
split,
{
cases hnn1,
linarith,
},
have : (f m0).val = (f m1).val := by rw [hfm0, hfm1],
exact subtype.eq this,
}
end


#### Scott Morrison (Sep 09 2020 at 23:44):

Very mathlib style would be to deduce this from src#infinite_pigeonhole. :-) I appreciate that's not what you're asking for!

#### Scott Morrison (Sep 09 2020 at 23:47):

By "simplify" do you mean "but still using induction on finset"? Because my first suggest would be to not do that. :-)

#### Scott Morrison (Sep 09 2020 at 23:49):

Given the result you're after, you could just intro s, say its card is n, and restrict f to range (n+1), and use a finite pigeonhole principle.

#### Alexandre Rademaker (Sep 09 2020 at 23:50):

That on the same formulation of the lemma ? Or are you proposing another formulation ?

#### Scott Morrison (Sep 09 2020 at 23:51):

I was suggesting to either use from a mathlib, or prove from scratch if that's the exercise, the usual finite pigeonhole principle for maps between finsets. Then reduce what @David Renshaw wants to prove to that.

#### Scott Morrison (Sep 09 2020 at 23:53):

There is src#finset.card_image_of_injective. Someone should PR the easy consequence that actually looks like the finite pigeonhole principle, and make sure to add a doc-string with the word "pigeonhole"!

#### David Renshaw (Sep 10 2020 at 00:02):

thanks! I tried searching mathlib for "pidgeonhole" but that was before I figured out that I was spelling it wrong. :face_palm:

#### Kyle Miller (Sep 10 2020 at 00:08):

I simplified your proof using some tricks I know. I didn't know about obtain!

import data.finset.basic
import data.nat.basic
import tactic

lemma pidgeonhole (s : finset ℕ) (f : ℕ → {x : ℕ // x ∈ s}) :
∃ a b : ℕ, (a ≠ b ∧ f a = f b) :=
begin
refine finset.induction (λ f, _) (λ n s hn hip f, _) s f,
{ exfalso,
exact (finset.not_mem_empty (f 0).val) (f 0).property, },
by_cases h : ∃ k : ℕ, ∀ m : ℕ, k ≤ m → (f m).val ≠ n,
{ obtain ⟨k0, hk0⟩ := h,
let fk: ℕ → {x // x ∈ s} := λ n : ℕ, ⟨(f (n + k0)).val, begin
have hk0a := hk0 (n + k0) (nat.le_add_left _ _),
exact finset.mem_of_mem_insert_of_ne (f (n + k0)).property hk0a,
end⟩,
obtain ⟨a, b, hne, hfk⟩ := hip fk,
use [a + k0, b + k0],
split,
{ revert hne,
contrapose, push_neg,
{ simp only [subtype.mk_eq_mk, subtype.val_eq_coe] at hfk,
exact subtype.ext hfk, } },
{ push_neg at h,
obtain ⟨m0, _, hk0⟩ := h 0,
obtain ⟨m1, hne, hk1⟩ := h (m0 + 1),
use [m0, m1],
split,
{ linarith [hne], },
{ apply subtype.eq,
rw [hk0, hk1], }, },
end


#### Scott Morrison (Sep 10 2020 at 00:15):

obtain is pretty awesome. :-)

#### David Renshaw (Sep 10 2020 at 00:15):

how would you use an existential without obtain?

#### Scott Morrison (Sep 10 2020 at 00:16):

some combination of have and Exists.some, I guess?

#### Kyle Miller (Sep 10 2020 at 00:16):

I always would do rcases hip fk with ⟨a, b, hne, hfk⟩ rather than obtain ⟨a, b, hne, hfk⟩ := hip fk.

#### Kyle Miller (Sep 10 2020 at 00:18):

It's pretty much the same, but I like how with obtain the expression is at the end, since it opens up having a larger expression being decomposed while still having somewhat readable code.

#### Bryan Gin-ge Chen (Sep 10 2020 at 00:20):

Before I learned to use rcases, I would write horrible terms starting with exists.elim. I still need to get in the habit of using obtain though.

#### Kyle Miller (Sep 10 2020 at 00:36):

@David Renshaw Found a way to simplify it even more:

lemma pigeonhole (s : finset ℕ) (f : ℕ → (↑s : set ℕ)) :
∃ a b : ℕ, a ≠ b ∧ f a = f b :=
begin
classical,
by_contra hc,
push_neg at hc,
have hinj : function.injective f,
{ intros a b,
contrapose,
exact hc a b, },
apply not_injective_infinite_fintype f hinj,
end


(The (↑s : set ℕ) is another way to write {x : ℕ // x ∈ s})

cool!

#### Scott Morrison (Sep 10 2020 at 00:39):

At this point, you're essentially relying on an existing proof of the pigeonhole principle, and this proof is just providing the glue.

#### David Renshaw (Sep 10 2020 at 00:41):

That's good enough for me! Working through the induction was a fun exercise, but I'm mostly concerned with learning how to do things idiomatically.

#### David Renshaw (Sep 10 2020 at 00:45):

ah... push_neg is quite convenient

#### Kyle Miller (Sep 10 2020 at 00:48):

I wouldn't really call these the pigeonhole principle, but maybe I've been too influenced by a Dijkstra essay. His formulation was, essentially, that if you have a function $f : A \to B$ with $B$ a finite set, then the maximum cardinality of a preimage is at least $\lvert A\rvert / \lvert B\rvert$. So, for $f : \mathbb{N} \to B$, I'd like $\exists b \in B, \lvert f^{-1}(b)\rvert = \infty$.

#### David Renshaw (Sep 10 2020 at 00:51):

You're saying that there's a stronger lemma that better deserves the name pigeonhole? That sounds like a reasonable stance to me.

#### Kyle Miller (Sep 10 2020 at 01:01):

You can say that there's a hole that contains at least the average number of pigeons per hole. I'm not sure the best way to formalize that in Lean, though.

Following @Scott Morrison's suggestion, it seems like it might be worth creating an analogue of not_injective_infinite_fintype for fintype.card_le_of_injective and adding documentation comments that these are the classic pigeonhole principles for finitely many and infinitely many pigeons. All I really did with my last simplification was using push_neg to recover the hidden function.injective.

#### Bryan Gin-ge Chen (Sep 10 2020 at 01:06):

(Issue #2772 is also about the pigeonhole principle.)

#### Kyle Miller (Sep 10 2020 at 01:10):

(Ah, found it: #2272)

#### Julian Berman (Sep 10 2020 at 01:39):

Kyle Miller said:

(The (↑s : set ℕ) is another way to write {x : ℕ // x ∈ s})

what do these notations mean?

#### Julian Berman (Sep 10 2020 at 01:40):

(or how would I look up // other than grepping around mathlib which takes me to some pretty low-level files)

#### David Renshaw (Sep 10 2020 at 01:42):

One thing you can do is set_option pp.notation false

#### David Renshaw (Sep 10 2020 at 01:45):

I find that when I jump-to-definition on the opening { of {x : ℕ // x ∈ s}, I get properly taken the definition of subtype. It does not work on the // or the closing }.

(in emacs)

#### Julian Berman (Sep 10 2020 at 01:46):

aha cool, that helps, thanks (pp.notation works here), lemme try jump to definition

#### Julian Berman (Sep 10 2020 at 01:47):

@David Renshaw awesome, that works too as long as yeah I do it on the { and not // which is what I tried before. Appreciated!

#### Kyle Miller (Sep 10 2020 at 04:01):

Bryan Gin-ge Chen said:

(Issue #2272 is also about the pigeonhole principle.)

Ok, here they are! #4096

#### Kevin Buzzard (Sep 10 2020 at 06:11):

Adrian Mathias told me that the pigeonhole principle was that if there were two pigeons in one hole, then one hole contained two pigeons. He then remarked that this idea could be generalized

Last updated: May 14 2021 at 00:42 UTC