## 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?

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

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

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