golfing challenge!

Stream: general

[Hanting Zhang]

I'm currently fighting supr/bsupr and finsupp.sum/finset.sum and struggling. Is there any way to shorten these lemmas?

import data.finsupp.basic
import data.finset.basic
import linear_algebra.basic

open finset
open_locale big_operators classical
universes u v w

theorem bsupr_eq_supr {α : Type u} [complete_lattice α] {ι : Type v} {s : ι → α}
  {p : ι → Prop} : (⨆ i (H : p i), s i) = ⨆ (i : subtype p), s i :=
begin
  sorry,
end

lemma finsupp.sum_add_add {α : Type u} {M : Type v}
  [add_comm_monoid M] (f g : α →₀ M) :
  ∑ a in (f + g).support, (f a + g a) = ∑ a in f.support, f a + ∑ a in g.support, g a :=
begin
  change (f + g).sum (λ _ a, a) = f.sum (λ _ a, a) + g.sum (λ _ a, a),
  rw finsupp.sum_add_index _ _,
  exact λ a, rfl, exact λ a b₁ b₂, rfl,
end

-- pretty atrocious but hey it works
lemma mem_supr' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} (p : ι → submodule R M) {x : M} :
  x ∈ supr p ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ p i) ∧ ∑ i in v.support, v i = x :=
begin
  classical,
  rw submodule.supr_eq_span,
  refine ⟨λ h, _, λ h, _⟩,
  refine submodule.span_induction h _ _ _ _,
  { intros y hy,
    rw set.mem_Union at hy,
    cases hy with i hy,
    use finsupp.single i y,
    split,
    { intro j, by_cases h : j = i,
      simp only [h, finsupp.single_eq_same], exact hy,
      rw ← ne.def at h,
      simp only [finsupp.single_eq_of_ne h.symm, submodule.zero_mem], },
    by_cases hy : y = 0, rw hy,
    simp only [finsupp.coe_zero, pi.zero_apply, finsupp.single_zero, finset.sum_const_zero],
    rw [finsupp.support_single_ne_zero hy, finset.sum_singleton],
    exact finsupp.single_eq_same, },
  { use 0,
    simp only [finsupp.coe_zero, pi.zero_apply, implies_true_iff, eq_self_iff_true, and_self,
      finset.sum_const_zero, submodule.zero_mem], },
  { intros x y hx hy,
    rcases hx with ⟨v, hv, hvs⟩,
    rcases hy with ⟨w, hw, hws⟩,
    use v + w,
    refine ⟨λ i, submodule.add_mem _ (hv i) (hw i), _⟩,
    rw [← hvs, ← hws],
    simp only [finsupp.add_apply],
    convert finsupp.sum_add_add v w, },
  { intros r x hx,
    rcases hx with ⟨v, hv, hvs⟩,
    use r • v,
    refine ⟨λ i, submodule.smul_mem _ _ (hv i), _⟩,
    rw [← hvs, finset.smul_sum],
    simp only [finsupp.smul_apply],
    refine finset.sum_subset finsupp.support_smul
      (λ a ha han, finsupp.not_mem_support_iff.mp han) },
  rcases h with ⟨v, hv, hvs⟩,
  have := submodule.sum_mem (supr p) (λ i _, (le_supr p i : p i ≤ supr p) (hv i)),
  rw ← submodule.supr_eq_span,
  rwa hvs at this,
end

-- **definitely** atrocious but hey it works
lemma mem_bsupr {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} {p : ι → Prop} (f : ι → submodule R M) (x : M) :
  x ∈ (⨆ i (H : p i), f i) ↔
  ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ ∑ i in v.support, v i = x ∧ (∀ i, ¬ p i → v i = 0) :=
begin
  classical,
  change set ι at p,
  refine ⟨λ h, _, λ h, _⟩,
  { rw bsupr_eq_supr at h,
    rcases (mem_supr' _).mp h with ⟨v', hv', hsum⟩,
    change p →₀ M at v',
    -- define `v = v'` where `p i` is true and zero otherwise
    let v : ι →₀ M :=
      ⟨v'.support.map (function.embedding.subtype p),
       λ (i : ι), dite (p i) (λ hi, v' ⟨i, hi⟩) (λ _, 0), _⟩,
    refine ⟨v, _, _, _⟩,
    { intros i,
      simp only [finsupp.coe_mk],
      split_ifs with hi,
      { exact hv' ⟨i, hi⟩ },
      exact submodule.zero_mem _ },
    { simp only [finsupp.coe_mk, dite_eq_ite, function.embedding.coe_subtype, finset.sum_map,
        subtype.coe_eta],
      convert hsum,
      ext i, split_ifs with hi, refl,
      exfalso, apply hi, exact i.2 },
    { intros i hi,
      simp only [finsupp.coe_mk, dif_neg hi], },
    intros i,
    simp only [exists_prop, function.embedding.coe_subtype, set_coe.exists, finset.mem_map,
      exists_and_distrib_right, exists_eq_right, finsupp.mem_support_iff, ne.def, subtype.coe_mk],
    split_ifs with hi,
    { refine ⟨λ hh, _, λ hh, ⟨hi, hh⟩⟩,
      cases hh with _ key, exact key },
    refine ⟨λ hh _, _, λ hh, _⟩,
    { cases hh with key _,
      exact hi key },
    exfalso, exact hh rfl },
  rcases h with ⟨v, hv, hsum, hzero⟩,
  have hle: (⨆ i ∈ v.support, f i) ≤ ⨆ (i : ι) (H : p i), f i,
  { refine bsupr_le_bsupr' (λ i hi, _),
    revert hi, contrapose!,
    refine λ h, finsupp.not_mem_support_iff.mpr (hzero i h), },
  have key: x ∈ ⨆ i ∈ v.support, f i,
  { rw ← hsum, exact submodule.sum_mem_bsupr (λ i hi, hv i), },
  exact hle key,
end

[Hanting Zhang]

In particular, I feel like bsupr_eq_supr and finsupp.sum_add_add both are supposed to be one line proofs, but I'm not abusing definitional equality hard enough.

mem_supr' and mem_bsupr have some actual content, but the current proofs seem far too awkward. I'm not sure how to make them better.

Thanks in advance for any help!

[Eric Wieser]

I think the first one is docs#finsupp.sum_add_index nevermind, you already prove it with that. It golfs to a single invocation of that lemma though.

[Eric Wieser]

bsupr_eq_supr is docs#supr_subtype (or the primed version)

[Heather Macbeth]

Can you use docs#submodule.exists_finset_of_mem_supr? (For the main result.)

[Eric Wieser]

I just PR'd #8268 which adds an iff version of that lemma, mem_supr_iff_exists_finset, on the off-chance it helps

[Heather Macbeth]

@Kevin Buzzard apparently asked the same question three months ago!
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/submonoid.2Emem_supr

[Eric Wieser]

I also wonder whether there's a nice variant of docs#submodule.coe_sup which could be stated for supr. I don't have a good understanding of the cases when the index set isn't finite though.

[Eric Wieser]

Here's a golf of mem_supr' that follows the same strategy as your proof:

lemma add_submonoid.finsupp_sum_mem {M : Type*} [add_comm_monoid M] (S : add_submonoid M)
  {ι₁ ι₂ : Type*} [has_zero ι₂]
  (f : ι₁ →₀ ι₂) (g : ι₁ → ι₂ → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
S.sum_mem $ λ i hi, h _ (finsupp.mem_support_iff.mp hi)

lemma submodule.finsupp_sum_mem {R M : Type*} [semiring R] [add_comm_monoid M] [module R M]
  (S : submodule R M) {ι₁ ι₂ : Type*} [has_zero ι₂]
  (f : ι₁ →₀ ι₂) (g : ι₁ → ι₂ → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
S.to_add_submonoid.finsupp_sum_mem f g h

-- pretty atrocious but hey it works
lemma mem_supr' {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} (p : ι → submodule R M) {x : M} :
  x ∈ supr p ↔ ∃ v : ι →₀ M, (∀ i, v i ∈ p i) ∧ v.sum (λ i vi, vi) = x :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { rw submodule.supr_eq_span at h,
    refine submodule.span_induction h _ _ _ _,
    { intros y hy,
      obtain ⟨i, hy⟩ := set.mem_Union.mp hy,
      refine ⟨finsupp.single i y, λ j, _, finsupp.sum_single_index rfl⟩,
      cases eq_or_ne j i with h h,
      { simp only [h, finsupp.single_eq_same], exact hy, },
      { simp only [finsupp.single_eq_of_ne h.symm, submodule.zero_mem], }, },
    { exact ⟨0, λ i, submodule.zero_mem _, finsupp.sum_zero_index⟩, },
    { rintros x y ⟨v, hv, rfl⟩ ⟨w, hw, rfl⟩,
      refine ⟨v + w, λ i, submodule.add_mem _ (hv i) (hw i),
                    finsupp.sum_add_index (λ _, rfl) (λ _ _ _, rfl)⟩ },
    { rintros r x ⟨v, hv, rfl⟩,
      refine ⟨r • v, λ i, submodule.smul_mem _ _ (hv i), _⟩,
      rw [finsupp.sum_smul_index' (λ _, _), finsupp.smul_sum],
      refl }, },
  { rcases h with ⟨v, hv, rfl⟩,
    exact submodule.finsupp_sum_mem _ v _ (λ i _, (le_supr p i : p i ≤ supr p) (hv i)),}
end

[Eric Wieser]

mem_bsupr is much easier, and most of the proof is just pushing binders around:

lemma mem_bsupr {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} {p : ι → Prop} (f : ι → submodule R M) (x : M) :
  x ∈ (⨆ i (H : p i), f i) ↔
  ∃ v : ι →₀ M, (∀ i, v i ∈ f i) ∧ v.sum (λ i vi, vi) = x ∧ (∀ i, ¬ p i → v i = 0) :=
begin
  rw mem_supr',
  apply exists_congr,
  intro a,
  conv_rhs { rw [←and_assoc, and_comm, ←and_assoc]},
  apply and_congr_left',
  rw ←forall_and_distrib,
  apply forall_congr,
  intro i,
  by_cases hp : p i,
  simp [hp],
  simp [hp] {contextual := tt},
end

[Eric Wieser]

If you tweak the statement it gets shorter:

lemma mem_bsupr {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} {p : ι → Prop} (f : ι → submodule R M) (x : M) :
  x ∈ (⨆ i (H : p i), f i) ↔
  ∃ v : ι →₀ M, (∀ i, (¬ p i → v i = 0) ∧ v i ∈ f i) ∧ v.sum (λ i vi, vi) = x :=
begin
  rw mem_supr',
  apply exists_congr,
  intro v,
  apply and_congr_left',
  apply forall_congr,
  intro i,
  by_cases hp : p i,
  simp [hp],
  simp [hp] {contextual := tt},
end

[Eric Wieser]

I think this lemma is the one we really want:

/-- Note that `dfinsupp.lsum ℕ f` is precisely `direct_sum.to_module f` -/
lemma supr_eq_dfinsupp_lsum_range
  {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [module R M]
  {ι : Type w} [decidable_eq ι] (p : ι → submodule R M) :
  supr p = (dfinsupp.lsum ℕ (λ i, (p i).subtype)).range :=
begin
  apply le_antisymm,
  { apply supr_le _,
    intros i y hy,
    exact ⟨dfinsupp.single i ⟨y, hy⟩, dfinsupp.sum_add_hom_single _ _ _⟩, },
  { rintros x ⟨v, rfl⟩,
    exact dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr p i : p i ≤ _) (v i).prop) }
end

[Hanting Zhang]

Thanks @Eric Wieser! You're too fast for me though with #8274; I'll be moving stuff around in #8246 to readjust my approach