Generate Finset-indexed function given a Multiset.

Stream: Is there code for X?

[Artie Khovanov]

Is there a way, given M : Multiset A, to generate the "function indexing M": that is, an index set I : Finset B and a map f: B -> A such that map f I.val = A?

I imagine you would take B = Fin (M.card) and I = Finset.univ, and build up f inductively.

The context is that I am trying to prove certain objects can be written as finite sums. For example, I am trying to prove the lemma

theorem AddSubmonoid.closure_iff_finsum [AddCommMonoid R] {S : Set R} (a : R) :
    a ∈ closure S ↔ (∃ (α : Type) (I : Finset α) (x : α → R) (x_cl : ∀ i ∈ I, x i ∈ S), a = ∑ i ∈ I, x i)

Now, the library has the following theorem:

theorem AddSubmonoid.exists_multiset_of_mem_closure {M : Type u_4} [AddCommMonoid M] {s : Set M} {x : M} (hx : x ∈ AddSubmonoid.closure s) :
∃ (l : Multiset M), (∀ y ∈ l, y ∈ s) ∧ l.sum = x

This is very close to what I want, but I want to use Finset.sum (i.e. $\Sigma$ notation) rather than Multiset.sum, hence my question.

Further context: it's not enough for me to just use multisets, since the theorem I am actually trying to get to is

theorem isSumSq_iff_finsum [AddCommMonoid R] [Mul R] (a : R) :
    IsSumSq a ↔ (∃ (α : Type) (I : Finset α) (x : α → R), a = ∑ i ∈ I, x i * x i)

I know this, too, could be stated using Multiset and map, but ultimately I'm trying to use the natural notation. This is especially important since down the line I am defining formally real rings, which have the property that $\sum_i x_i^2=0$ implies $x_i=0$ for all $i$ --- writing this using Multiset and map would be pretty strange.

[Ruben Van de Velde]

Maybe you can work with Finsupp?

[Ruben Van de Velde]

docs#Multiset.toFinsupp

[Yaël Dillies]

There are ways of doing what you want, but really the better thing to do is to make this AddSubmonoid lemma return a finset

[Yaël Dillies]

Namely it should be easier to fix the existing proof rather than bootstrapping after the fact

[Artie Khovanov]

This doesn't do the right thing -- I want to index a Multiset by a Finset, not turn a Multiset into a Finset (possibly with extra data).

[Artie Khovanov]

Yaël Dillies said:

There are ways of doing what you want, but really the better thing to do is to make this AddSubmonoid lemma return a finset

Well, this is what I'm trying to do. Making this lemma return a Finset.sum is the same thing as providing this transformation, right? The existing lemma is proved by transforming a List into a Multiset, this is just the next step along if you unpack what Finset.sum is defined as.

[Artie Khovanov]

Here is a snippet from Submonoid.membership:

/-- Product of a list of elements in a submonoid is in the submonoid. -/
@[to_additive "Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`."]
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S := by
  lift l to List S using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid. -/
@[to_additive
      "Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
      in the `AddSubmonoid`."]
theorem multiset_prod_mem {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M)
    (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S := by
  lift m to Multiset S using hm
  rw [← coe_multiset_prod]
  exact m.prod.coe_prop

/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
    submonoid. -/
@[to_additive
      "Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
      is in the `AddSubmonoid`."]
theorem prod_mem {M : Type*} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type*}
    {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S :=
  multiset_prod_mem (t.1.map f) fun _x hx =>
    let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
    hix ▸ h i hi

I'm just trying to go the other way basically. The first two lemmas are there:

@[to_additive]
theorem exists_list_of_mem_closure {s : Set M} {x : M} (hx : x ∈ closure s) :
    ∃ l : List M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x := by
  rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

@[to_additive]
theorem exists_multiset_of_mem_closure {M : Type*} [CommMonoid M] {s : Set M} {x : M}
    (hx : x ∈ closure s) : ∃ l : Multiset M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x := by
  obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
  exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

and I want to provide the third.

[Yaël Dillies]

Artie Khovanov said:

Making this lemma return a Finset.sum is the same thing as providing this transformation, right?

No it's not, because you can directly change the proof instead

[Artie Khovanov]

Anyway I was told the answer elsewhere:
it's List.get.

[Artie Khovanov]

Yaël Dillies said:

Artie Khovanov said:

Making this lemma return a Finset.sum is the same thing as providing this transformation, right?

No it's not, because you can directly change the proof instead

I'm not sure what you mean -- do you mean to go back to the original place where they do the induction on List or whatever and repeat it with Finset.sum instead?

[Yaël Dillies]

Yes, exactly

[Artie Khovanov]

Oh right -- that seems much harder to me?

[Artie Khovanov]

For starters I'm not even sure where they do this induction

[Yaël Dillies]

No, it should be really easy. Every time you add an element, you change the type ι by Option ι and extend the function using docs#Option.elim

[Yaël Dillies]

Where this induction is proved doesn't really matter. The proof you now need to provide should be quite straightforward

[Artie Khovanov]

I'll have a go (I already did it the other way) and compare, probably a good exercise

[Artie Khovanov]

I think I'm just not that good at coming up with "new" stuff yet, I mostly do better at modifying existing stuff.