Zulip Chat Archive

Stream: new members

Topic: pigeonhole lemma


view this post on Zulip 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,
        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

view this post on Zulip 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!

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip Alexandre Rademaker (Sep 09 2020 at 23:50):

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

view this post on Zulip 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.

view this post on Zulip 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"!

view this post on Zulip 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:

view this post on Zulip 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,
      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

view this post on Zulip Scott Morrison (Sep 10 2020 at 00:15):

obtain is pretty awesome. :-)

view this post on Zulip David Renshaw (Sep 10 2020 at 00:15):

how would you use an existential without obtain?

view this post on Zulip Scott Morrison (Sep 10 2020 at 00:16):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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})

view this post on Zulip David Renshaw (Sep 10 2020 at 00:37):

cool!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip David Renshaw (Sep 10 2020 at 00:45):

ah... push_neg is quite convenient

view this post on Zulip 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:ABf : A \to B with BB a finite set, then the maximum cardinality of a preimage is at least A/B\lvert A\rvert / \lvert B\rvert. So, for f:NBf : \mathbb{N} \to B, I'd like bB,f1(b)=\exists b \in B, \lvert f^{-1}(b)\rvert = \infty.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 01:06):

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

view this post on Zulip Kyle Miller (Sep 10 2020 at 01:10):

(Ah, found it: #2272)

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip David Renshaw (Sep 10 2020 at 01:42):

One thing you can do is set_option pp.notation false

view this post on Zulip 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 }.

view this post on Zulip David Renshaw (Sep 10 2020 at 01:45):

(in emacs)

view this post on Zulip Julian Berman (Sep 10 2020 at 01:46):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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