Zulip Chat Archive

Stream: general

Topic: golfing challenge!


Hanting Zhang (Jul 11 2021 at 19:50):

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 (Jul 11 2021 at 19:54):

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 (Jul 11 2021 at 19:59):

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 (Jul 11 2021 at 20:02):

bsupr_eq_supr is docs#supr_subtype (or the primed version)

Heather Macbeth (Jul 11 2021 at 20:12):

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

Eric Wieser (Jul 11 2021 at 21:44):

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 (Jul 11 2021 at 22:43):

@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 (Jul 11 2021 at 22:48):

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 (Jul 12 2021 at 07:26):

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 (Jul 12 2021 at 07:36):

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 (Jul 12 2021 at 07:40):

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 (Jul 12 2021 at 10:25):

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 (Jul 13 2021 at 02:54):

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


Last updated: Dec 20 2023 at 11:08 UTC