Zulip Chat Archive

Stream: new members

Topic: working with sets of vectors


view this post on Zulip 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?

view this post on Zulip Reid Barton (Jun 05 2019 at 14:42):

Transforms how? The cartesian product?

view this post on Zulip Reid Barton (Jun 05 2019 at 14:42):

Is set a monad?

view this post on Zulip Reid Barton (Jun 05 2019 at 14:42):

If so it looks like traverse

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 14:44):

Yes I want the cartesian product.

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 14:44):

set is a functor..

view this post on Zulip Chris Hughes (Jun 05 2019 at 14:46):

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

view this post on Zulip Reid Barton (Jun 05 2019 at 14:46):

Yeah, I should have said a monad

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 14:49):

@Reid Barton could you explain how traverse gives the cartesian product?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:04):

no, that doesn't work in general

view this post on Zulip 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

view this post on Zulip Reid Barton (Jun 05 2019 at 15:05):

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

view this post on Zulip 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

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 15:06):

If vector does have a traversable instance, how would that help me define cartesian products?

view this post on Zulip Reid Barton (Jun 05 2019 at 15:06):

I guess you need the traversable laws as well then

view this post on Zulip Reid Barton (Jun 05 2019 at 15:06):

traverse would exactly be the cartesian product

view this post on Zulip 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.

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 15:08):

Isn't there a simpler way to do this?

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:08):

do it directly

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:09):

that's the wrong way around, I think

view this post on Zulip Chris Hughes (Jun 05 2019 at 15:09):

So it is.

view this post on Zulip Chris Hughes (Jun 05 2019 at 15:10):

The other way is harder.

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:12):

@Koundinya Vajjha is this an XY problem?

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:12):

I suspect you don't want this

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 15:12):

An XY problem?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:13):

the subtype of list definition is very rarely the convenient one

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 05 2019 at 15:13):

what do you want to actually say?

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 15:14):

I want to prove that the n-fold product measure has it's defining property.

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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))

view this post on Zulip Reid Barton (Jun 05 2019 at 15:29):

Do you already have the product of two measure spaces?

view this post on Zulip Koundinya Vajjha (Jun 05 2019 at 15:31):

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

view this post on Zulip Simon Hudon (Jun 05 2019 at 18:01):

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

view this post on Zulip Simon Hudon (Jun 05 2019 at 18:02):

traversable (flip vector n) to be exact

view this post on Zulip Simon Hudon (Jun 05 2019 at 18:02):

Just import data.vector2

view this post on Zulip 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)?

view this post on Zulip Simon Hudon (Jun 05 2019 at 18:37):

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

view this post on Zulip 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)).

view this post on Zulip Simon Hudon (Jun 05 2019 at 18:46):

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

view this post on Zulip 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