Indexing with multiset

Stream: Is there code for X?

[Peter Nelson]

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]

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]

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]

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

[Yakov Pechersky]

Why multiset as opposed to finset? In your ordering of A_1, ..., A_k, do you have indices that reoccur?

[Peter Nelson]

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]

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]

What's the way to express the sum of a set ℤ? Doesn't that require some more constraints, like decidability or finset?

[Bhavik Mehta]

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]

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

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

[Yakov Pechersky]

Isn't set.image2 (+) s t the set of all possible values a + b | a ∈ s ∧ b ∈ t?

[Bhavik Mehta]

It is

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

Two separate questions;

1. If the interpretation that the sum over all the sets, where each set is summed, must equal to x, is that expressible with set?
2. 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]

1. 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.
2. Correct, the order of the sets doesn't matter.

[Bhavik Mehta]

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]

I'm a little surprised there's no instance traversable multiset so I can just use sequence to express this

[Bhavik Mehta]

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