Simple combinatorics exercise

Stream: new members

[Giacomo Maletto]

Here's a fun exercise (source):
Prove that if $A_1, \dots, A_n \subseteq \{ 1, \dots, m \}$ are distinct sets such that $\ A_i \cap A_j \neq \empty \$ for all $\ i, j, \$ then $\ n \le 2^{m-1}$.
I'm practicing my Lean skills, so I tried to formalize it:

import tactic

open finset

def sdiff_range (n : ℕ) (A : finset ℕ) : finset ℕ := range n \ A

lemma sdiff_range_inj_on (n : ℕ) : set.inj_on (sdiff_range n) (range n).powerset :=
begin
  intros A hA B hB heq, simp [sdiff_range] at hA hB heq,
  rw sdiff_eq_sdiff_iff_inter_eq_inter at heq,
  rw ←(inter_eq_right_iff_subset A (range n)).mpr hA,
  rw ←(inter_eq_right_iff_subset B (range n)).mpr hB,
  assumption
end


universes u v

lemma inj_on_subset {α : Type u} {β : Type v} {f : α → β} {s t : finset α} (h : t ⊆ s) :
  set.inj_on f s → set.inj_on f t :=
begin
  intros H a ha b hb heq,
  refine H _ _ heq,
  exact h ha, exact h hb
end


theorem katona_exercise (n m : ℕ) (A : ℕ → finset ℕ)
  (h₁ : ∀ i : ℕ, i ∈ range n → A i ⊆ range m.succ)
  (h₂ : ∀ i : ℕ, i ∈ range n → ∀ j : ℕ, j ∈ range n → A i = A j → i = j)
  (h₃ : ∀ i : ℕ, i ∈ range n → ∀ j : ℕ, j ∈ range n → A i ∩ A j ≠ ∅) : n ≤ 2 ^ m :=
begin
  -- If we have more than 2^m distinct subsets of {0,...,m},
  -- at least a couple of them are complementary, and this violates hypothesis h₃.
  -- The subsets are represented by A₁, their complements by A₂,
  -- and we prove that if 2^m < n then their intersection is not empty.
  by_contra h_ctr, push_neg at h_ctr,
  let A₁ := image A (range n),
  let A₂ := image (sdiff_range m.succ) A₁,
  have Hc₁ : A₁.card = n,
    { rw [←card_range n, card_image_eq_iff_inj_on], exact h₂ },
  have Hs₁ : A₁ ⊆ (range m.succ).powerset,
    { intros B hB, rw mem_image at hB, rcases hB with ⟨i, hi₁, hi₂⟩,
      specialize h₁ i hi₁, rw hi₂ at h₁, simp [h₁] },
  have Hc₂ : A₂.card = n,
    { rw [←Hc₁, card_image_eq_iff_inj_on],
      exact inj_on_subset Hs₁ (sdiff_range_inj_on m.succ) },
  have Hs₂ : A₂ ⊆ (range m.succ).powerset,
    { intros B hB, rw mem_image at hB, rcases hB with ⟨i, hi₁, hi₂⟩,
      rw sdiff_range at hi₂, rw [mem_powerset, ←hi₂], simp },
  have Hc₃ : (A₁ ∪ A₂).card ≤ 2 ^ m.succ,
    { rw [←card_range m.succ, ←card_powerset],
      exact card_le_of_subset (union_subset Hs₁ Hs₂) },
  have Hc₄ := card_union_add_card_inter A₁ A₂,
  have H₁ : (A₁ ∩ A₂).nonempty,
    { rw ←card_pos,
      calc 0 < n + n - 2 ^ m.succ : by {rw [pow_succ, two_mul], omega }
         ... ≤ (A₁ ∩ A₂).card     : by omega },
  rcases H₁ with ⟨B, hB⟩,
  simp only [mem_image, exists_prop, exists_exists_and_eq_and, mem_inter, sdiff_range] at hB,
  rcases hB with ⟨⟨i, hi₁, hi₂⟩, ⟨j, hj₁, hj₂⟩⟩,
  have H₂ : A i ∩ A j = ∅, { rw [hi₂, ←hj₂], simp },
  exact h₃ i hi₁ j hj₁ H₂
end

It's a bit awkward that A ranges over all natural numbers, and I wonder if there's a better alternative.
Is this how you would have formalized the statement and the proof? Any comments on style?

[Alex J. Best]

You could use the type fin m (see docs#fin) rather than taking a subset of the naturals

[Alex J. Best]

Likewise for the domain of A, and then your condition h2 could be written as function.injective A

[Kyle Miller]

I might formalize it like this:

lemma card_le_of_pairwise_not_disjoint
  (m : ℕ) (A : finset (finset (fin m)))
  (disj : ∀ (s t ∈ A), ¬disjoint s t) :
  A.card ≤ 2 ^ (m - 1) :=
begin
  sorry
end

Since it's a list of distinct sets, you can instead use a set of sets, and then n can be replaced with the cardinality of that set. I used disjoint rather than saying the intersection isn't empty just because it seems to be the mathlib-canonical way to say that.

Another thing you can do is, rather than use natural numbers for the elements of the sets, use an arbitrary finite type:

lemma card_le_of_pairwise_not_disjoint
  {α : Type*} [decidable_eq α] [fintype α]
  (A : finset (finset α))
  (disj : ∀ (s t ∈ A), ¬disjoint s t) :
  A.card ≤ 2 ^ (fintype.card α - 1) :=
begin
  sorry
end

[Kyle Miller]

(I'm surprised that finset requires decidable_eq for its disjoint. That should only be needed to make it decidable.)

[Giacomo Maletto]

Thank you both, I'll try following these approaches and see where they lead.
In my first attempt I tried using fin m but ran in some troubles - but that might be because I was trying to solve the exercise in another way: I wanted to define a particular function of type finset (fin m.succ) → finset (fin m) in order to use the pigeonhole principle, but defining such a function turned out to be a huge hassle simply because of the choice of domain and codomain.

[Kyle Miller]

@Giacomo Maletto The idea you used about how none of the pairs of sets are complementary made me think that there might be a more direct combinatorial proof. It comes down to the fact that complementation of subsets is an involution, and it carries your set of sets A to a disjoint set of sets, which implies the cardinality of A is at most half of m (the cardinality of the type the sets are drawn from).

import tactic

open finset

lemma card_le_div_two_of_invol {α : Type*} [fintype α]
  {f : α → α} (hf : function.involutive f)
  (s : finset α) (hs : ∀ (x ∈ s), ¬ f x ∈ s) :
  s.card ≤ fintype.card α / 2 :=
begin
  suffices : s.card * 2 ≤ fintype.card α,
  { rw ←nat.mul_div_cancel s.card,
    exact nat.div_le_div_right this,
    simp, },
  classical,
  let f' : α ≃ α := hf.to_equiv _,
  transitivity (s ∪ (s.map f'.to_embedding)).card,
  { rw card_union_eq,
    { simp [mul_two] },
    rw disjoint_left,
    simp only [not_exists, mem_map, exists_prop, not_and],
    rintros a ha x hx rfl,
    exact hs x hx ha, },
  { apply card_le_univ, },
end

lemma card_le_of_pairwise_not_disjoint
  {α : Type*} [decidable_eq α] [fintype α] [nonempty α]
  (A : finset (finset α))
  (disj : ∀ (s t ∈ A), ¬disjoint s t) :
  A.card ≤ 2 ^ (fintype.card α - 1) :=
begin
  convert_to A.card ≤ fintype.card (finset α) / 2,
  { rw fintype.card_finset,
    have : 0 < fintype.card α := fintype.card_pos,
    generalize hn : fintype.card α = n,
    rw hn at this,
    cases n,
    { simpa using this, },
    { simp [nat.succ_eq_add_one, pow_add], }, },
  have : ∀ (s ∈ A), ¬ sᶜ ∈ A,
  { intros s hs hs',
    specialize disj _ _ hs hs',
    rw not_disjoint_iff at disj,
    simpa using disj, },
  exact card_le_div_two_of_invol compl_involutive _ this,
end

[Kyle Miller]

Regarding style:

In begin/end blocks, usually tactics are each supposed to go on their own line. Also, beware non-terminal simps (this page explains the problem and has some pointers on how to eliminate them).

...
  intros A hA B hB heq, simp [sdiff_range] at hA hB heq,
  rw sdiff_eq_sdiff_iff_inter_eq_inter at heq,
...

For tactics that create multiple subgoals, make sure to enclose those goals in curly braces to help keep track of the proof structure. For example, instead of

...
  refine H _ _ heq,
  exact h ha, exact h hb
...

it's better to do

  refine H _ _ heq,
  { exact h ha },
  { exact h hb }

or in this case, this is fine:

  refine H (h ha) (h hb) heq,

Mathlib style for curly brace blocks is to put them at the same indentation rather than indenting them. So instead of

  have Hc₁ : A₁.card = n,
    { rw [←card_range n, card_image_eq_iff_inj_on], exact h₂ },

it'd be this

  have Hc₁ : A₁.card = n,
  { rw [←card_range n, card_image_eq_iff_inj_on],
    exact h₂ },

Other than these small things, the style seemed fine.

[Giacomo Maletto]

I was under the impression that non-terminal simps were only problematic when they acted on the goal. Should they be avoided also when used in hypotheses?

[Patrick Massot]

Yes, for the exact same reasons.

[Yaël Dillies]

(I'm surprised that finset requires decidable_eq for its disjoint. That should only be needed to make it decidable.)

This is because disjointness goes through the semilattice_inf_bot structure, which requires decidable equality.

[Yaël Dillies]

And that's because the inf is defined as a filter. To define it, you must compute it.

[Eric Wieser]

Kyle Miller said:

(I'm surprised that finset requires decidable_eq for its disjoint. That should only be needed to make it decidable.)

I've attempted to follow up on that thought in #16436, with definition

def disjoint (a b : α) : Prop := ∀ ⦃x⦄, x ≤ a → x ≤ b → x ≤ ⊥

[Eric Wieser]

An alternative approach would be to make disjoint be a data field of docs#order_bot satisfying the above, which would let us pick a nice defeq.