# Zulip Chat Archive

## Stream: new members

### Topic: working with sets of vectors

#### Koundinya Vajjha (Jun 05 2019 at 14:41):

Is there any function which transforms a `vector (set A) n`

into `set(vector A n)`

in mathlib?

#### Reid Barton (Jun 05 2019 at 14:42):

Transforms how? The cartesian product?

#### Reid Barton (Jun 05 2019 at 14:42):

Is `set`

a monad?

#### Reid Barton (Jun 05 2019 at 14:42):

If so it looks like `traverse`

#### Koundinya Vajjha (Jun 05 2019 at 14:44):

Yes I want the cartesian product.

#### Koundinya Vajjha (Jun 05 2019 at 14:44):

`set`

is a functor..

#### Chris Hughes (Jun 05 2019 at 14:46):

`set`

is a monad, but I don't think it's been proved yet.

#### Reid Barton (Jun 05 2019 at 14:46):

Yeah, I should have said a `monad`

#### Koundinya Vajjha (Jun 05 2019 at 14:49):

@Reid Barton could you explain how `traverse`

gives the cartesian product?

#### Reid Barton (Jun 05 2019 at 14:53):

Basically `set`

models a nondeterministic computation. `do a <- s, b <- t, ...`

corresponds to taking any combination of `a`

in `s`

and `b`

in `t`

.

#### Reid Barton (Jun 05 2019 at 14:54):

The monad instance has `return : t -> set t`

given by singleton and `join : set (set t) -> set t`

given by union

#### Reid Barton (Jun 05 2019 at 14:55):

`list`

is another instance of the same idea that you can actually compute with, and `sequence : list (list a) -> list (list a)`

being the cartesian product is a classic example in Haskell

#### Koundinya Vajjha (Jun 05 2019 at 14:58):

I'm finding it hard to convince lean that `vector A n`

is the same thing as the `n`

-fold cartesian product of elements of A.

#### Reid Barton (Jun 05 2019 at 15:02):

Is there a `traversable`

instance for `\lam A, vector A n`

? (Does that even work, with a lambda?)

#### Koundinya Vajjha (Jun 05 2019 at 15:03):

`vector`

is defined as a subtype of `list`

. I assume `list`

is `traversable`

, so does `vector`

inherit that?

#### Mario Carneiro (Jun 05 2019 at 15:04):

no, that doesn't work in general

#### Reid Barton (Jun 05 2019 at 15:05):

Not automatically, and in fact there is something to prove--that the length of the list doesn't change

#### Reid Barton (Jun 05 2019 at 15:05):

It should be free by parametricity, but Lean doesn't know that

#### Mario Carneiro (Jun 05 2019 at 15:06):

actually parametricity doesn't tell you the length doesn't change; it could drop the first element without violating parametricity

#### Koundinya Vajjha (Jun 05 2019 at 15:06):

If `vector`

does have a `traversable`

instance, how would that help me define cartesian products?

#### Reid Barton (Jun 05 2019 at 15:06):

I guess you need the traversable laws as well then

#### Reid Barton (Jun 05 2019 at 15:06):

`traverse`

would exactly be the cartesian product

#### Reid Barton (Jun 05 2019 at 15:08):

Of course if the traversable instance doesn't already exist then in some sense it doesn't help you.

#### Koundinya Vajjha (Jun 05 2019 at 15:08):

Isn't there a simpler way to do this?

#### Mario Carneiro (Jun 05 2019 at 15:08):

do it directly

#### Chris Hughes (Jun 05 2019 at 15:08):

example (n : ℕ) {M : Type → Type} {α : Type} [monad M] : (M (fin n → α)) → fin n → M α := λ x i, do y ← x, return (y i)

#### Mario Carneiro (Jun 05 2019 at 15:09):

that's the wrong way around, I think

#### Chris Hughes (Jun 05 2019 at 15:09):

So it is.

#### Chris Hughes (Jun 05 2019 at 15:10):

The other way is harder.

#### Mario Carneiro (Jun 05 2019 at 15:12):

@Koundinya Vajjha is this an XY problem?

#### Mario Carneiro (Jun 05 2019 at 15:12):

I suspect you don't want this

#### Koundinya Vajjha (Jun 05 2019 at 15:12):

An XY problem?

#### Reid Barton (Jun 05 2019 at 15:12):

It would be easy on the inductive family version of vector (like https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr#L11 )--I forget whether this is also in mathlib. The "subtype of list" definition seems a bit more inconvenient here

#### Mario Carneiro (Jun 05 2019 at 15:13):

the subtype of list definition is very rarely the convenient one

#### Koundinya Vajjha (Jun 05 2019 at 15:13):

I just want to define the product measure and pass a vector of sets and not have it complain that it's not the right type.

#### Mario Carneiro (Jun 05 2019 at 15:13):

what do you want to actually say?

#### Koundinya Vajjha (Jun 05 2019 at 15:14):

I want to prove that the `n`

-fold product measure has it's defining property.

#### Mario Carneiro (Jun 05 2019 at 15:14):

if you are giving something of the wrong type then "making it not complain" is the wrong way to approach the problem

#### Mario Carneiro (Jun 05 2019 at 15:21):

Given `s : ∀ i, set (A i)`

, the set of elements of `∀ i:I, A i`

in the s's is `Prod s : set (∀ i, A i) := { f | ∀ i, f i ∈ s i }`

#### Koundinya Vajjha (Jun 05 2019 at 15:27):

Here is what I am working with:

def collapse_in (S: set α) {n: ℕ} (Es: set (vector α n)): set (vector α (n+1)) := set.sUnion (set.image (λ x: α, set.image (λ v: _, vector.cons x v) Es) S) def collapse: Π n, vector (set α) n → set (vector α n) | 0 _ := ∅ | (nat.succ n) v := collapse_in (vector.head v) n (collapse n (vector.tail v))

#### Reid Barton (Jun 05 2019 at 15:29):

Do you already have the product of two measure spaces?

#### Koundinya Vajjha (Jun 05 2019 at 15:31):

Yes, most of the definitions for the product construction were available in mathlib

#### Simon Hudon (Jun 05 2019 at 18:01):

I'm pretty sure I wrote traversable instance for vector and array

#### Simon Hudon (Jun 05 2019 at 18:02):

`traversable (flip vector n)`

to be exact

#### Simon Hudon (Jun 05 2019 at 18:02):

Just import `data.vector2`

#### Koundinya Vajjha (Jun 05 2019 at 18:35):

@Simon Hudon thank you! Can you please tell me how I can use this? I have a bunch of lemmas proven for binary cartesian products. Can I use this to extend to `n`

tuples (vectors)?

#### Simon Hudon (Jun 05 2019 at 18:37):

Probably. It depends on the lemmas. What do you have in mind?

#### Koundinya Vajjha (Jun 05 2019 at 18:43):

At the most basic level, given a set `(A : set α)`

and `(B : set (vector α n))`

I want to construct `A.prod B`

which lives in `set(vector α (succ n))`

.

#### Simon Hudon (Jun 05 2019 at 18:46):

yes, that works. You can work by induction on `n`

#### Simon Hudon (Jun 05 2019 at 18:53):

Proving this lemma might make things more straightforward:

lemma traverse_cons {n α β F} [applicative F] (f : α → F β) (v : α) (vs : flip vector n α) : (traverse f (vector.cons v vs) : F (flip vector _ β)) = vector.cons <$> f v <*> traverse f vs := sorry

Last updated: May 16 2021 at 21:11 UTC