# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Indexing with multiset

#### Peter Nelson (Jan 20 2021 at 18:08):

I have a problem which I believe is essentially captured by the following question.

How would one define a function `foo : multiset (set int) → int → Prop`

so that `foo S x`

holds iff `x`

is the sum of a transversal of `S`

? (That is, for some ordering A_1, A_2, ... A_k of the sets in `S`

, we have x = a_1 + ... + a_k with a_i \in A_i). This is of course easy if we replace `multiset (set int)`

with `list (set int)`

as we have a way to index `S`

, but this approach breaks a symmetry in the definition. I can't see how to do this `multiset.map`

, because this requires a function term `f : set int → int`

, which doesn't really exist here.

#### Bryan Gin-ge Chen (Jan 20 2021 at 20:50):

This is probably cheating since I'm using `multiset.to_list`

and then just working with lists, and I suspect it'd be a gigantic pain to prove anything about this:

```
import data.multiset.basic
def foo (S : multiset (set ℤ)) (x : ℤ) : Prop :=
∃ (l : list ℤ) (hl : (l.zip_with (∈) S.to_list).foldl (and) true),
l.sum = x
```

`multiset.to_list`

is also `noncomputable`

, though I'm not sure if that matters to you.

I think we are missing a convenient API for this sort of thing but I'm not sure what it should look like.

#### Kyle Miller (Jan 20 2021 at 21:04):

Another would be to define all this for lists, show it's invariant under permutation of the lists, and then descend to the quotient:

```
import data.multiset.basic
import data.fintype.basic
import algebra.big_operators.basic
open_locale big_operators
def is_traversal₀ (L : list (set ℤ)) (f : fin L.length → ℤ) : Prop :=
∀ (i : fin L.length), f i ∈ L.nth_le i.1 i.2
def foo₀ (L : list (set ℤ)) (n : ℤ) : Prop :=
∃ (f : fin L.length → ℤ), is_traversal₀ L f ∧ (∑ i, f i) = n
def foo (S : multiset (set ℤ)) (n : ℤ) : Prop :=
quotient.rec_on S (λ L, foo₀ L n) begin
intros L₁ L₂ h,
simp only [eq_rec_constant, eq_iff_iff],
sorry,
end
```

#### Kyle Miller (Jan 20 2021 at 21:06):

(this could be mixed with @Bryan Gin-ge Chen's better definition for traversals of lists)

#### Yakov Pechersky (Jan 20 2021 at 21:11):

Why `multiset`

as opposed to `finset`

? In your ordering of A_1, ..., A_k, do you have indices that reoccur?

#### Peter Nelson (Jan 20 2021 at 21:43):

I don't have recurring indices, but the same set might occur more than once (for instance, some ordering might have A_1 = A_3). Insisting that the sets are distinct seems artificial given that the definition makes perfect sense without this stipulation.

Thanks Bryan and Kyle; your solutions look good. The way I stated things is a toy example; what I actually have is a `multiset T`

for some type `T`

, a term `X : set T' `

, and I want to assert the existence of a family of terms of type `set T'`

, indexed by the elements of the multiset, each of which must satisfy some predicate depending on the multiset element, whose union is `X`

. And here, union could be any associative, commutative operation. Could there be a place for a 'dependent multiset folding' at this level of generality in mathlib?

#### Bryan Gin-ge Chen (Jan 20 2021 at 23:07):

Could there be a place for a 'dependent multiset folding' at this level of generality in mathlib?

Generally, if something makes part of mathlib easier to use, it belongs in mathlib. I think we definitely need something like what you're suggesting, but I don't have the experience to comment on whether what you've proposed is the right abstraction without seeing more code.

#### Yakov Pechersky (Jan 20 2021 at 23:24):

What's the way to express the `sum`

of a `set ℤ`

? Doesn't that require some more constraints, like decidability or `finset`

?

#### Bhavik Mehta (Jan 20 2021 at 23:34):

Looking at the type `multiset (set int) → int → Prop`

, this is the same as `multiset (set int) → set int`

, and the binary version of your construction would be `set int → set int → set int`

given by `liftA2 (+)`

(which probably has a different name in Lean which I don't recall right now), so my guess is that you could just use `multiset.fold`

to make the set you'd like

#### Bhavik Mehta (Jan 20 2021 at 23:37):

More concretely, if I'm reading your question correctly, your `foo`

is

```
def foo : multiset (set ℤ) → set ℤ := multiset.fold (set.image2 (+)) {0}
```

#### Yakov Pechersky (Jan 20 2021 at 23:41):

Isn't `set.image2 (+) s t`

the set of all possible values `a + b | a ∈ s ∧ b ∈ t`

?

#### Bhavik Mehta (Jan 20 2021 at 23:42):

It is

#### Yakov Pechersky (Jan 20 2021 at 23:45):

And if the question was about a `set.sum`

? The multiset symmetry comes from the fact that addition is associative and commutative. Correct?

#### Bhavik Mehta (Jan 20 2021 at 23:46):

I'm not sure what you're asking - are you saying my implementation is different from what Peter was looking for?

#### Yakov Pechersky (Jan 20 2021 at 23:50):

Two separate questions;

- If the interpretation that the sum over all the sets, where each set is summed, must equal to
`x`

, is that expressible with`set`

? - The "breaks a symmetry in the definition" comes from the commutativity and associativity of
`(+)`

, which imply that the order of the sets shouldn't matter, correct?

#### Bhavik Mehta (Jan 20 2021 at 23:54):

- There is no sum over sets happening (since of course there's no guarantee each set is finite), and this isn't what Peter was asking to express in the first place.
- Correct, the order of the sets doesn't matter.

#### Bhavik Mehta (Jan 20 2021 at 23:54):

An alternate way to express the function is:

```
def foo (x : multiset (set int)) : set int :=
set.image multiset.sum (multiset.traverse id x)
```

#### Bhavik Mehta (Jan 20 2021 at 23:55):

I'm a little surprised there's no instance `traversable multiset`

so I can just use `sequence`

to express this

#### Bhavik Mehta (Jan 21 2021 at 00:28):

To try to be more clear:

```
def foo' : multiset (set ℤ) → set (multiset ℤ) := multiset.traverse id
example : foo' {{0,2,6}, {1,3}, {5}} = {{0,1,5}, {0,3,5}, {2,1,5}, {2,3,5}, {6,1,5}, {6,3,5}} :=
```

This function constructs all the transversals of the given multiset of sets, in particular the resulting sets are those containing one element of each set in the original multiset. Then you can just `set.image multiset.sum`

on this to get the desired function

Last updated: May 17 2021 at 15:13 UTC