Zulip Chat Archive

Stream: new members

Topic: finset to vector?


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

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

view this post on Zulip Mario Carneiro (Dec 22 2020 at 00:09):

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

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

view this post on Zulip Thomas Browning (Dec 22 2020 at 00:11):

there's S.val.to_list

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

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

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

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

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

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

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

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

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

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

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