finset to vector?

Stream: new members

[Andrew Souther]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

there's S.val.to_list

[Mario Carneiro]

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]

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]

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]

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

[Andrew Souther]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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