Pigeonhole principle for two subsets

Stream: general

[Adam Kurkiewicz]

Hi all, I'm working on Compfiles IMO 1970 P4.

I've been able to make good progres so far; currently I'm trying to show that two subsets of a Finset overalap at least once if their total size exceeds that of the Finset. I belive this would be typically argued by "pigeonhole principle". But I had a look at several pigeonhole lemmas in Mathlib and I couldn't find the right lemma to use.

This is stated formally below:

import Mathlib.Tactic

lemma subsets_must_overlap_pigeonhole (s s_subset_1 s_subset_2 : Finset ℕ) (predicate_s1: ℕ → Prop) (predicate_s2 : ℕ → Prop)
                                      [DecidablePred predicate_s1] [DecidablePred predicate_s2]
                                      (s1_filter : s_subset_1 = (s.filter (λ x => predicate_s1 x)))
                                      (s2_filter : s_subset_2 = (s.filter (λ x => predicate_s2 x)))
                                      (a b c : ℕ) (total_size_exceeds: a + b > c)
                                      (card_s : s.card = c) (card_s1 : s_subset_1.card = a) (card_s2 : s_subset_2.card = b):
                                      ∃ x ∈ s, predicate_s1 x ∧ predicate_s2 x := by
  sorry

Any suggestions on how to make progress?

[Etienne Marion]

I would make a reasoning by contradiction. If this is not true, then your subsets are disjoint and you can apply docs#Finset.card_union_of_disjoint.

[Adam Kurkiewicz]

Thanks, I'll give it a try!

[François G. Dorais]

Try docs#Finset.card_union_add_card_inter

[Adam Kurkiewicz]

Thans all,

I've got it:

import Mathlib.Tactic

lemma subsets_must_overlap_pigeonhole (s s1 s2 : Finset ℕ) (predicate_s1: ℕ → Prop) (predicate_s2 : ℕ → Prop)
                                      [DecidablePred predicate_s1] [DecidablePred predicate_s2]
                                      (s1_filter : s1 = (s.filter (λ x => predicate_s1 x)))
                                      (s2_filter : s2 = (s.filter (λ x => predicate_s2 x)))
                                      (a b c : ℕ) (total_size_exceeds: a + b > c)
                                      (card_s : s.card = c) (card_s1 : s1.card = a) (card_s2 : s2.card = b):
                                      ∃ x ∈ s, predicate_s1 x ∧ predicate_s2 x := by
  have s1_is_subset: s1 ⊆ s := by
    rw[s1_filter]
    apply Finset.filter_subset
  have s2_is_subset: s2 ⊆ s := by
    rw[s2_filter]
    apply Finset.filter_subset
  have lift_x_in_s1 : ∀ x ∈ s, x ∈ s1 ↔ predicate_s1 x := by
    rw[s1_filter]
    intro x _
    subst card_s
    simp_all only [Finset.mem_filter, true_and]
  have lift_x_in_s2 : ∀ x ∈ s, x ∈ s2 ↔ predicate_s2 x := by
    rw[s2_filter]
    intro x _
    subst card_s
    simp_all only [Finset.mem_filter, true_and]
  apply not_forall_not.mp
  intro h
  simp at h
  have step_1 : (∀ x ∈ s, predicate_s1 x → ¬predicate_s2 x) → (∀ x ∈ s, x ∈ s1 → ¬ x ∈ s2) := by
    intro left
    intro x x_in_s
    intro predicate_s1_fulfills
    intro predicate_s2_fulfills
    have part_1 := ((lift_x_in_s1 x x_in_s).mp predicate_s1_fulfills)
    have part_2 := ((lift_x_in_s2 x x_in_s).mp predicate_s2_fulfills)
    exact left x x_in_s part_1 part_2
  have step_2 : (∀ x ∈ s, x ∈ s1 → x ∉ s2) → Disjoint s1 s2 := by
    intro left
    dsimp[Disjoint]
    dsimp[Finset.instHasSubset]
    simp
    intro s3
    intro rel1
    intro rel2
    intro a
    intro a_in_s3
    have a_in_s1 := rel1 a_in_s3
    have a_in_s2 := rel2 a_in_s3
    have a_in_s : a ∈ s := by
      subst card_s card_s1 s1_filter card_s2 s2_filter
      simp_all only [Finset.filter_subset, Finset.mem_filter, true_and, implies_true, and_self]
    exact left a a_in_s a_in_s1 a_in_s2
  have s1_s2_disjoint : Disjoint s1 s2 := by
    apply step_2
    apply step_1
    exact h
  have card_calc := Finset.card_union_of_disjoint s1_s2_disjoint
  rw[card_s1] at card_calc
  rw[card_s2] at card_calc
  rw[← card_calc] at total_size_exceeds
  rw[← card_s] at total_size_exceeds
  have s1_s2_subset : (s1 ∪ s2) ⊆ s := by
    dsimp[Finset.instHasSubset]
    simp
    intro a
    intro s1_or_s2
    cases s1_or_s2
    case inl left =>
      simp_all only [Finset.filter_subset, Finset.mem_filter]
    case inr left =>
      simp_all only [Finset.filter_subset, Finset.mem_filter]
  have : (s1 ∪ s2).card ≤ s.card := by
    apply Finset.card_le_card
    exact s1_s2_subset
  omega

[Yaël Dillies]

I've already added a version of this to mathlib

[Yaël Dillies]

docs#Finset.inter_nonempty_of_card_lt_card_add_card

[Adam Kurkiewicz]

Thanks Yaël! That's exactly what I needed :sweat_smile:

Any tips on how to find those results with moogle or loogle (or maybe there's another tool I'm missing) going forward? I've tried pasting the content of the lemma above in moogle (I think for loogle I generally need to use special syntax), and I couldn't get this as a hit.

I suspect that's because the statements are different on the surface (one is about Finset.filters and the other is about subsets).

I hear about "premise selection" in the literature, it seems like a user-facing tool doing premise selection that could find these kind of statements in Mathlib would be super helpful (maybe it exists and I just don't know about it?).

[Shreyas Srinivas]

Finset filters are also subsets.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

In a sense you are defining s1 and s2 twice. The first time, when what you really just need is the hypotheses that they are both subsets of s

[Shreyas Srinivas]

In a sense you are defining s1 and s2 twice. The first time, when what you really just need is the hypotheses that they are both subsets of s

[Yaël Dillies]

One thing is that you have many substitutable variables in your statement. This is mathematically the same, but very different to our search tools.

[Yaël Dillies]

Once you have substituted s1, s2, a, b, you get something which is much closer to my statement

[Yaël Dillies]

Now, notice that s.filter predicate_s1 and s.filter predicate_2 are just weirdly spelled out subsets of s. So replace them by t, u, hts : t subset s, hus : u subset s. This is syntactically more general (in the sense that there is a substitution of variables that turns the new statement into the old one, but there is no substitution going the other way around). Simplify the return type. Tada! You get exactly my lemma

[Adam Kurkiewicz]

Thanks that's helpful, I'll use this next time I'm searching for these kind of lemmas!