## Stream: new members

### Topic: finset to vector?

#### Andrew Souther (Dec 21 2020 at 23:43):

I am working with a finset, and I want to put all of the elements into a finite sequence. It doesn't really matter how the elements are arranged in the sequence. But every element of the sequence should be in the finset, and every element of the finset should be in the sequence only once.

I'm thinking about trying to build a vector, like this:

import data.set.finite
import data.finset.basic

example {α : Type} {n : ℕ} (S : finset α) (h : finset.card S = n) :
∃ v : (vector α n), ∀ a : α, ∃ k : fin n, vector.nth v k = a := sorry


Is there any easy lemma like finset.to_vector that could help me with this? Is there a better way to accomplish this goal ?

#### Thomas Browning (Dec 22 2020 at 00:07):

list.to_finset_surjective proves that one exists, I think (edit: it doesn't guarantee that the length is right)

#### Mario Carneiro (Dec 22 2020 at 00:09):

the theorem statement is false, S doesn't appear in the consequent

#### Mario Carneiro (Dec 22 2020 at 00:11):

I think the easiest way to do this kind of thing is to do rcases on the finset to extract the list, at which point h will be defeq to list.length l = n and then you can build a vector A n from that

#### Thomas Browning (Dec 22 2020 at 00:11):

there's S.val.to_list

#### Mario Carneiro (Dec 22 2020 at 00:12):

You will end up with the side condition l.nodup as well, which you probably want to hold on to if you want to know the list has no duplicates

#### Andrew Souther (Dec 22 2020 at 00:13):

Whoops haha. I guess this is what I meant, just to be extra clear:

import data.set.finite
import data.finset.basic

example2 {α : Type} {n : ℕ} (S : finset α) (h : finset.card S = n) :
∃ v : (vector α n), ∀ a : S, ∃ k : fin n, vector.nth v k = a := sorry


#### Mario Carneiro (Dec 22 2020 at 00:17):

import data.set.finite
import data.finset.basic

example {α : Type} {n : ℕ} (S : finset α) (h : finset.card S = n) :
∃ v : vector α n, ∀ a ∈ S, ∃ k : fin n, vector.nth v k = a :=
begin
rcases S with ⟨⟨l⟩, (hl : l.nodup)⟩,
change l.length = n at h,
refine ⟨⟨l, h⟩, λ a ha, _⟩,
rcases list.nth_le_of_mem ha with ⟨k, hk, e⟩,
refine ⟨⟨k, by rwa ← h⟩, e⟩,
end


#### Mario Carneiro (Dec 22 2020 at 00:18):

Probably you don't need anything other than the first two lines for whatever you were doing

#### Andrew Souther (Dec 22 2020 at 00:33):

Yeah, I think you're right about that, thanks Mario! Just curious:

What's going on in that first line with rcases S? I've only ever used rcases to break up elaborate 'and' statements. Does that just mean S is an elaborate 'and' statement under the hood?

#### Andrew Souther (Dec 22 2020 at 00:36):

Also, S.val.to_listlooks helpful too, thanks Thomas. I will look at that more on mathlib, play around with both of these routes, and see if they work for my purposes.

#### Bryan Gin-ge Chen (Dec 22 2020 at 00:37):

rcases can be used to break up any inductive data type, and S, being a finset, is an inductive datatype composed of a multiset (1st component) and a proof that the elements in the multiset are distinct (hl). Multisets are quotients of lists by permutations, and the inner pair of angle brackets is able to pull out a list representative l in its equivalence class.

#### Andrew Souther (Dec 22 2020 at 00:59):

I think I roughly understand up until the last sentence, Bryan.
If I replace ⟨l⟩ with l in Mario's first line, I see that l turns out to be a multiset. But how does that 'second layer' of angle brackets pull out a representative list from there? I've never used the angle brackets around a single term before, and I'm just curious about its general use.

#### Mario Carneiro (Dec 22 2020 at 01:06):

You can use angle brackets also on single-member inductives, like inhabited , in which case you get something like ⟨l⟩

#### Mario Carneiro (Dec 22 2020 at 01:07):

Technically a quotient is not an inductive type, but rcases supports pattern matching on it anyway, by invoking quotient.ind as appropriate

#### Mario Carneiro (Dec 22 2020 at 01:09):

Unlike matching on inductives, when you match on a quotient there is a side condition that the proof term you are constructing does not depend on the witness; but if you are proving a theorem then this side goal is trivial because of proof irrelevance, so it ends up looking exactly like you pattern matched on a single-member inductive

Last updated: May 13 2021 at 20:13 UTC