pigeonhole lemma

Stream: new members

[David Renshaw]

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,
        exact nat.add_right_cancel heq,
      },
      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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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

[Kyle Miller]

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,
      apply nat.add_right_cancel, },
    { 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]

obtain is pretty awesome. :-)

[David Renshaw]

how would you use an existential without obtain?

[Scott Morrison]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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]

@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})

[David Renshaw]

cool!

[Scott Morrison]

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]

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]

ah... push_neg is quite convenient

[Kyle Miller]

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]

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]

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]

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

[Kyle Miller]

(Ah, found it: #2272)

[Julian Berman]

Kyle Miller said:

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

what do these notations mean?

[Julian Berman]

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

[David Renshaw]

One thing you can do is set_option pp.notation false

[David Renshaw]

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 }.

[David Renshaw]

(in emacs)

[Julian Berman]

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

[Julian Berman]

@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]

Bryan Gin-ge Chen said:

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

Ok, here they are! #4096

[Kevin Buzzard]

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