Basic lemma about Schnirelmann density

Stream: new members

[Stepan Nesterov]

I found an elementary lemma missing from ## Mathlib.Combinatorics.Schnirelmann, and I thought it could be a nice exercise to fill it in:

open Pointwise in
theorem sumset_univ_of_schirelmannDensity_ge_one {A B : Set ℕ} [DecidablePred (· ∈ A)]
    [DecidablePred (· ∈ B)] (h : schnirelmannDensity A + schnirelmannDensity B ≥ 1) :
    ({0} ∪ A) + ({0} ∪ B) = Set.univ := by
  rw [Set.eq_univ_iff_forall]
  intro n
  cases n with
    | zero => exact ⟨0, Set.mem_union_left A rfl, 0, Set.mem_union_left B rfl, rfl⟩
    | succ m =>
      set n := m + 1
      by_cases hnA : n ∈ A
      · exact ⟨n, Set.mem_union_right {0} hnA, 0, Set.mem_union_left B rfl, rfl⟩
      · by_cases hnB : n ∈ B
        · refine ⟨0, Set.mem_union_left A rfl, n, Set.mem_union_right {0} hnB, ?_⟩
          dsimp
          exact zero_add n
        let f : ℕ ⊕ ℕ → ℕ := fun z => match z with
          | Sum.inl x => x
          | Sum.inr y => n - y
        have hc : (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card <
          (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card
          := by
          calc
          (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card ≤
            (Ioo 0 n).card := by
            apply card_le_card
            intro k hk
            rw [mem_image] at hk
            obtain ⟨z, hz, hz'⟩ := hk
            simp only [mem_disjSum, mem_filter, mem_Ioc] at hz
            obtain ⟨a, ⟨⟨⟨a_pos, a_le_n⟩, a_in_A⟩, hz⟩⟩ | ⟨b, ⟨⟨⟨b_pos, b_le_n⟩, b_in_B⟩, hz⟩⟩ := hz
            · rw [← hz] at hz'
              dsimp [f] at hz'
              rw [← hz']
              rw [mem_Ioo]
              refine ⟨a_pos, ?_⟩
              rw [lt_iff_le_and_ne]
              refine ⟨a_le_n, ?_⟩
              intro a_eq_n
              rw [← a_eq_n] at hnA
              contradiction
            · rw [← hz] at hz'
              dsimp [f] at hz'
              rw [← hz', mem_Ioo]
              refine ⟨?_, Nat.sub_lt (Nat.zero_lt_succ m) b_pos⟩
              apply Nat.zero_lt_sub_of_lt
              rw [lt_iff_le_and_ne]
              refine ⟨b_le_n, ?_⟩
              intro b_eq_n
              rw [← b_eq_n] at hnB
              contradiction
          _ = n - 1 := by rw [Nat.card_Ioo, Nat.sub_zero]
          _ < n := lt_add_one (n - 1)
          _ ≤ {a ∈ Ioc 0 n | a ∈ A}.card + {b ∈ Ioc 0 n | b ∈ B}.card := by
            have hA : schnirelmannDensity A * n ≤ #{a ∈ Ioc 0 n | a ∈ A} :=
              schnirelmannDensity_mul_le_card_filter
            have hB : schnirelmannDensity B * n ≤ #{b ∈ Ioc 0 n | b ∈ B} :=
              schnirelmannDensity_mul_le_card_filter
            rify
            nlinarith
          _ = (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card :=
            Eq.symm (card_disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))
        obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
        match x, y with
        | Sum.inl a, Sum.inl a' =>
          dsimp [f] at hxy
          rw [hxy] at x_ne_y
          contradiction
        | Sum.inl a, Sum.inr b =>
          dsimp [f] at hxy
          simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
          rw [← Nat.Simproc.eq_add_le a hy.1.2] at hxy
          exact ⟨a, Set.mem_union_right {0} hx.2, b, Set.mem_union_right {0} hy.2, Eq.symm hxy⟩
        | Sum.inr b, Sum.inl a =>
          dsimp [f] at hxy
          simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
          rw [Nat.sub_eq_iff_eq_add hx.1.2] at hxy
          exact ⟨a, Set.mem_union_right {0} hy.2, b, Set.mem_union_right {0} hx.2, Eq.symm hxy⟩
        | Sum.inr b, Sum.inr b' =>
          dsimp [f] at hxy
          simp only [inr_mem_disjSum, mem_filter, mem_Ioc] at hx hy
          rw [tsub_right_inj hx.1.2 hy.1.2] at hxy
          rw [hxy] at x_ne_y
          contradiction

Would this code be suitable for a mathlib PR, and if not, how do I rewrite it in a more mathlib way?

[Yaël Dillies]

There are a lot intro foo; cases foo and fun foo => match foo that you can cancel with each other

[Michael Rothgang]

Please make a #mwe (that's a link you can click on): right now, your code doesn't compile on the playground, making it harder to help you.

[Michael Rothgang]

Three more style comments:

• you can remove the dsimp on line 19 (and then combine the exact with the preceding refine)
• you can combine two subsequent rewrites into one line
• in general, using tactics can be more readable than constructing proof terms by hand: line 12 can use by simp twice, for example

[Michael Rothgang]

This list is not exhaustive. Let me link to this file with some advice on how to golf code: this will be shorter than me repeating everything in there, and I'm sure you'll find another trick or two in there!

[Damiano Testa]

Here is a very simple-minded shortening, where I simply tried to use grind more.

import Mathlib

open Finset Pointwise in
theorem sumset_univ_of_schirelmannDensity_ge_one {A B : Set ℕ} [DecidablePred (· ∈ A)]
    [DecidablePred (· ∈ B)] (h : schnirelmannDensity A + schnirelmannDensity B ≥ 1) :
    ({0} ∪ A) + ({0} ∪ B) = Set.univ := by
  rw [Set.eq_univ_iff_forall]
  rintro (_ | m)
  · exact ⟨0, Set.mem_union_left A rfl, 0, Set.mem_union_left B rfl, rfl⟩
  ·   set n := m + 1
      by_cases hnA : n ∈ A
      · exact ⟨n, Set.mem_union_right {0} hnA, 0, Set.mem_union_left B rfl, rfl⟩
      · by_cases hnB : n ∈ B
        · refine ⟨0, Set.mem_union_left A rfl, n, Set.mem_union_right {0} hnB, ?_⟩
          simp
        let f : ℕ ⊕ ℕ → ℕ := fun z => match z with
          | Sum.inl x => x
          | Sum.inr y => n - y
        have hc : (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card <
          (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card
          := by
          calc
          (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card ≤
            (Ioo 0 n).card := card_le_card (by grind [mem_disjSum])
          _ < n := by grind [Nat.card_Ioo]
          _ ≤ {a ∈ Ioc 0 n | a ∈ A}.card + {b ∈ Ioc 0 n | b ∈ B}.card := by
            have hA : schnirelmannDensity A * n ≤ #{a ∈ Ioc 0 n | a ∈ A} :=
              schnirelmannDensity_mul_le_card_filter
            have hB : schnirelmannDensity B * n ≤ #{b ∈ Ioc 0 n | b ∈ B} :=
              schnirelmannDensity_mul_le_card_filter
            rify
            nlinarith
          _ = (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card :=
            Eq.symm (card_disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))
        obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
        match x, y with
        | Sum.inl a, Sum.inl a' => solve_by_elim
        | Sum.inl a, Sum.inr b =>
          dsimp [f] at hxy
          simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
          rw [← Nat.Simproc.eq_add_le a hy.1.2] at hxy
          exact ⟨a, Set.mem_union_right {0} hx.2, b, Set.mem_union_right {0} hy.2, Eq.symm hxy⟩
        | Sum.inr b, Sum.inl a =>
          dsimp [f] at hxy
          simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
          rw [Nat.sub_eq_iff_eq_add hx.1.2] at hxy
          exact ⟨a, Set.mem_union_right {0} hy.2, b, Set.mem_union_right {0} hx.2, Eq.symm hxy⟩
        | Sum.inr b, Sum.inr b' =>
          grind [inr_mem_disjSum]

[Stepan Nesterov]

Ok I was able to shave a few more lines off @Damiano Testa suggestion, and I believe this should now be an mwe:

import Mathlib

open Finset Pointwise

theorem sumset_univ_of_schirelmannDensity_ge_one {A B : Set ℕ} [DecidablePred (· ∈ A)]
    [DecidablePred (· ∈ B)] (h : schnirelmannDensity A + schnirelmannDensity B ≥ 1) :
    ({0} ∪ A) + ({0} ∪ B) = Set.univ := by
  rw [Set.eq_univ_iff_forall]
  rintro (_ | m)
  · exact ⟨0, Set.mem_union_left A rfl, 0, Set.mem_union_left B rfl, rfl⟩
  · set n := m + 1
    by_cases hnA : n ∈ A
    · exact ⟨n, Set.mem_union_right {0} hnA, 0, Set.mem_union_left B rfl, rfl⟩
    · by_cases hnB : n ∈ B
      · exact ⟨0, Set.mem_union_left A rfl, n, Set.mem_union_right {0} hnB, zero_add n⟩
      let f : ℕ ⊕ ℕ → ℕ
        | Sum.inl x => x
        | Sum.inr y => n - y
      have hc : (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card <
        (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card
        := calc
        (image f (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))).card ≤
          (Ioo 0 n).card := card_le_card (by grind [mem_disjSum])
        _ < n := by rw [Nat.card_Ioo, Nat.sub_zero]; exact lt_add_one (n - 1)
        _ ≤ {a ∈ Ioc 0 n | a ∈ A}.card + {b ∈ Ioc 0 n | b ∈ B}.card := by
          rify
          nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
            @schnirelmannDensity_mul_le_card_filter B _ n]
        _ = (disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})).card :=
          Eq.symm (card_disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B}))
      obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
      match x, y with
      | Sum.inl a, Sum.inl a' => grind
      | Sum.inl a, Sum.inr b =>
        dsimp [f] at hxy
        simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
        rw [← Nat.Simproc.eq_add_le a hy.1.2] at hxy
        exact ⟨a, Set.mem_union_right {0} hx.2, b, Set.mem_union_right {0} hy.2, Eq.symm hxy⟩
      | Sum.inr b, Sum.inl a =>
        dsimp [f] at hxy
        simp only [inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
        rw [Nat.sub_eq_iff_eq_add hx.1.2] at hxy
        exact ⟨a, Set.mem_union_right {0} hy.2, b, Set.mem_union_right {0} hx.2, Eq.symm hxy⟩
      | Sum.inr b, Sum.inr b' => grind [inr_mem_disjSum]

[Stepan Nesterov]

In general, is there a rule of thumb for when the proof is too long for Mathlib?

[Ruben Van de Velde]

Not as such, no

[Vlad Tsyrklevich]

Eq.symm (card_disjSum ({a ∈ Ioc 0 n | a ∈ A}) ({b ∈ Ioc 0 n | b ∈ B})) could just be (card_disjSum _ _).symm. Eq.symm hxy could be hxy.symm. There's a lot of long types that make this quite dense, here's a golf for the hc hypothesis that is not that much shorter in terms of lines but I think is more readable

  let sA := {a ∈ Ioc 0 n | a ∈ A}
  let sB := {b ∈ Ioc 0 n | b ∈ B}
  have hc : (image f (disjSum sA sB)).card < (disjSum sA sB).card := by
    grw [card_le_card (t := Ioo 0 n) (by grind [mem_disjSum]), Nat.card_Ioo, Nat.sub_zero]
    refine Nat.sub_one_lt_of_le (by lia) ?_
    suffices n ≤ sA.card + sB.card by grw [this, ← card_disjSum]
    rify
    nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
      @schnirelmannDensity_mul_le_card_filter B _ n]

[Vlad Tsyrklevich]

Have not looked at or thought about if it's possible to reduce those case checks early on

import Mathlib

open Finset Pointwise

theorem sumset_univ_of_schirelmannDensity_ge_one {A B : Set ℕ} [DecidablePred (· ∈ A)]
    [DecidablePred (· ∈ B)] (h : schnirelmannDensity A + schnirelmannDensity B ≥ 1) :
    ({0} ∪ A) + ({0} ∪ B) = Set.univ := by
  refine Set.eq_univ_iff_forall.mpr ?_
  rintro (_ | m)
  · exact ⟨0, by grind⟩
  set n := m + 1
  by_cases hnA : n ∈ A
  · exact ⟨n, by grind⟩
  by_cases hnA : n ∈ B
  · exact ⟨0, by grind⟩
  let f : ℕ ⊕ ℕ → ℕ
    | Sum.inl x => x
    | Sum.inr y => n - y
  let sA := {a ∈ Ioc 0 n | a ∈ A}
  let sB := {b ∈ Ioc 0 n | b ∈ B}
  have hc : (image f (disjSum sA sB)).card < (disjSum sA sB).card := by
    grw [card_le_card (t := Ioo 0 n) (by grind [mem_disjSum]), Nat.card_Ioo, Nat.sub_zero]
    refine Nat.sub_one_lt_of_le (by lia) ?_
    suffices n ≤ sA.card + sB.card by grw [this, ← card_disjSum]
    rify
    nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
      @schnirelmannDensity_mul_le_card_filter B _ n]
  obtain ⟨x, hx, y, hy, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
  match x, y with
  | Sum.inl a, Sum.inl a' => grind
  | Sum.inl a, Sum.inr b =>
    simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
    exact ⟨a, by simp [hx], b, by simp [hy], by lia⟩
  | Sum.inr b, Sum.inl a =>
    simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at hx hy
    exact ⟨a, by simp [hy], b, by simp [hx], by lia⟩
  | Sum.inr b, Sum.inr b' => grind [inr_mem_disjSum]

[Vlad Tsyrklevich]

Also mathlib prefers 1 \le x to x \ge 1 so the h hypothesis should be updated.

[Stepan Nesterov]

What is the difference between rw [Set.eq_univ_iff_forall] and refine Set.eq_univ_iff_forall.mpr ?_?

[Vlad Tsyrklevich]

Ah in this case there is none. I was trying to do something earlier that didn't work out and just forgot to change it back.

[Stepan Nesterov]

Ok thank you all for the helpful suggestions, this now feels short enough for Mathlib. I've made a PR of this proof here: https://github.com/leanprover-community/mathlib4/pull/34227

[Kevin Buzzard]

Pop a newline after your PR description before the --- to stop yourself from shouting.