Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC