Enumerating a finite subset

Stream: Is there code for X?

[Oliver Nash]

Do we have a convenient way enumerating the elements of a finite subset?

[Oliver Nash]

For example, do we have anything like finset.to_fun below:

import data.set.basic
import set_theory.fincard

namespace finset

variables {α : Type*} (t : finset α)

def to_fun : fin t.card → α := sorry

lemma range_to_fun_eq : set.range t.to_fun = ↑t := sorry

-- Variant of `range_to_fun_eq` that stays in computable `finset` land:
lemma image_to_fun_univ_eq [decidable_eq α] : image t.to_fun univ = t := sorry

end finset

[Oliver Nash]

Or maybe we should ignore finset and just work with finite sets. Do we have anything like this:

import data.set.basic
import set_theory.fincard

namespace set.finite

variables {α : Type*} {s : set α} (h : s.finite)
include h

noncomputable def card : ℕ := nat.card s -- How does this not exist already!?

def to_fun : fin h.card → α := sorry

lemma range_to_fun_eq : set.range h.to_fun = s := sorry

end set.finite

[Eric Rodriguez]

you can presumably get it by toying with fintype.equiv_fin, but that's not ideal

[Kyle Miller]

I started an implementation of to_fun using a to_list function, but I think @Eric Rodriguez's suggestion of fintype.equiv_fun might be less work (depending on how all the coercions look).

import data.set.basic
import set_theory.fincard

namespace finset

variables {α : Type*} (t : finset α)

noncomputable def to_list : list α := t.1.to_list

@[simp]
lemma mem_to_list {a : α} : a ∈ t.to_list ↔ a ∈ t :=
by { rw [to_list, ←multiset.mem_coe, multiset.coe_to_list],
     exact iff.rfl }

lemma to_list_length : t.to_list.length = t.card :=
begin
  rw [to_list, ←multiset.coe_card, multiset.coe_to_list],
  refl,
end

noncomputable def to_fun : fin t.card → α :=
λ i, t.to_list.nth_le i begin
  rw to_list_length,
  exact i.property
end

end finset

[Adam Topaz]

We do have docs#finset.sort

[Adam Topaz]

You can sort with any random relation, for example

[Oliver Nash]

Eric Rodriguez said:

you can presumably get it by toying with fintype.equiv_fin, but that's not ideal

Interesting, I suppose that makes this possible:

noncomputable def to_fun : fin t.card → α :=
λ n, (fintype.equiv_fin t).symm.to_fun $ (congr_arg fin (fintype.card_coe t)).mpr n

[Kyle Miller]

I'm a little surprised that finset.to_list doesn't already exist. finset.sort is finset.to_list the long way ("I'm going to put my arbitrary list into an arbitrary order" rather than "I'm happy with the arbitrary list as-is.")

[Oliver Nash]

Kyle Miller said:

Edit: updated this code block

Oh wow, thanks for this! Superb. I'm being pulled away for dinner but I'm really grateful.

[Adam Topaz]

finset.to_list may as well just be finset.sort with the equality relation

[Kyle Miller]

How do you mean? Doesn't finset.sort need a total order?

[Adam Topaz]

Oh right I missed that assumption

[Adam Topaz]

Well that's silly. We should also have a finest.sort that takes any arbitrary relation

[Adam Topaz]

Maybe it would be noncomputable but :shrug:

[Kyle Miller]

finset.to_list: #8797

[Kyle Miller]

Using that PR, finset.to_fun could look like this

import data.fintype.basic

namespace finset

variables {α : Type*} (t : finset α)

noncomputable def to_fun : fin t.card → α :=
λ i, t.to_list.nth_le i (by { cases i, simp [i_property] })

lemma to_fun_injective : function.injective t.to_fun :=
begin
  rintros ⟨i, hi⟩ ⟨j, hj⟩ h,
  rw ←length_to_list at hi hj,
  simp only [to_fun, fin.coe_mk] at h,
  have := congr_arg some h,
  rw [←list.nth_le_nth hi, ←list.nth_le_nth hj] at this,
  simp [list.nth_injective hi (nodup_to_list t) this],
end

lemma image_to_fun_univ_eq [decidable_eq α] : image t.to_fun univ = t :=
begin
  ext x,
  simp only [to_fun, mem_image, mem_univ, list.nth_le, exists_true_left],
  split,
  { rintro ⟨⟨i, h⟩, -, rfl⟩,
    rw ←mem_to_list,
    apply list.nth_le_mem, },
  { intro h,
    rw [←mem_to_list, list.mem_iff_nth_le] at h,
    obtain ⟨i, hi, h⟩ := h,
    rw length_to_list at hi,
    use [⟨i, hi⟩, finset.mem_univ _, h], },
end

lemma range_to_fun_eq : set.range t.to_fun = ↑t :=
begin
  classical,
  conv_rhs { rw ←image_to_fun_univ_eq t },
  simp,
end

end finset

[Eric Wieser]

docs#finset.order_iso_of_fin?

[Oliver Nash]

Eric Wieser said:

docs#finset.order_iso_of_fin?

This would be what I want except that it requires [linear_order α] (presumably to make things computable).

[Oliver Nash]

Oliver Nash said:

Interesting, I suppose that makes this possible:

noncomputable def to_fun : fin t.card → α :=
λ n, (fintype.equiv_fin t).symm.to_fun $ (congr_arg fin (fintype.card_coe t)).mpr n

I might need this later today so I will lazily record what I think might be the most convenient definition here. Instead of fintype.equiv_fin used above, I now realise it is better to use fintype.equiv_fin_of_card_eq and thus obtain:

noncomputable def to_fun : fin t.card → α :=
↑(fintype.equiv_fin_of_card_eq (fintype.card_coe t)).symm.to_fun

[Eric Rodriguez]

Oliver Nash said:

Eric Wieser said:

docs#finset.order_iso_of_fin?

This would be what I want except that it requires [linear_order α] (presumably to make things computable).

Do we not have the well ordering principle?

[Oliver Nash]

I believe we do so I guess this would also work, at the cost of some @ characters to provide the instance!

[Eric Wieser]

We have an open PR that puts a linear order on any fintype I believe

[Oliver Nash]

Interesting! Looks like it is #7123 I'm juggling a few things but I'll look at it more closely if / when I need this. Thanks for the note.

[Oliver Nash]

For the sake of anyone looking at this thread in the future, I might as well say that I cooked up the following approach to what I was asking about here:

import data.fintype.basic

namespace finset

variables {α : Type*} (t : finset α)

/-- Finite subsets carry an enumeration. -/
noncomputable def enumerate : fin t.card → α :=
coe ∘ (fintype.equiv_fin_of_card_eq (fintype.card_coe t)).symm

/-- We can get the index of an element of a finite subset with respect to its enumeration. -/
noncomputable def denumerate : t → fin t.card :=
fintype.equiv_fin_of_card_eq (fintype.card_coe t)

@[simp] lemma enumerate_mem (i : fin t.card) : t.enumerate i ∈ t :=
by simp only [enumerate, coe_mem]

@[simp] lemma denumerate_enumerate_eq (i : fin t.card) :
  t.denumerate ⟨t.enumerate i, t.enumerate_mem i⟩ = i :=
by simp only [enumerate, denumerate, mk_coe, equiv.apply_symm_apply]

@[simp] lemma enumerate_denumerate_eq (x : t) : t.enumerate (t.denumerate x) = x :=
by simp only [enumerate, denumerate, equiv.symm_apply_apply, function.comp_app]

@[simp] lemma range_enumerate : set.range t.enumerate = ↑t :=
begin
  ext x, split,
  { rintros ⟨y, rfl⟩, simp only [enumerate, coe_mem, mem_coe], },
  { intros h, use t.denumerate ⟨x, mem_coe.mp h⟩, simp, },
end

@[simp] lemma image_enumerate_univ_eq [decidable_eq α] : image t.enumerate univ = t :=
begin
  ext x, split; intros h,
  { simp only [mem_image, mem_univ, exists_true_left] at h,
    obtain ⟨y, -, rfl⟩ := h, simp only [enumerate_mem], },
  { simp only [mem_image, mem_univ, exists_true_left],
    use t.denumerate ⟨x, mem_coe.mp h⟩, simp, },
end

variables {t} {s : finset α} (h : s ⊆ t)

/-- A pair of nested finite subsets `s ⊆ t` yields an embedding of their emumerating types. -/
noncomputable def fin_card_embed_of_subset : fin s.card ↪ fin t.card :=
{ to_fun := t.denumerate ∘ (set.inclusion h) ∘
            (fintype.equiv_fin_of_card_eq (fintype.card_coe s)).symm,
  inj'   := λ i j hij,
    begin
      simp only [denumerate, equiv.apply_eq_iff_eq, function.comp_app] at hij,
      simpa only [equiv.apply_eq_iff_eq] using set.inclusion_injective h hij,
    end, }

@[simp] lemma fin_card_embed_of_subset_enumerate_comp :
  t.enumerate ∘ (fin_card_embed_of_subset h) = s.enumerate :=
by { ext, simpa [fin_card_embed_of_subset], }

end finset

[Oliver Nash]

However I eventually decided that t.enumerate was actually just a less useful version of (coe : t → α).

[Yakov Pechersky]

In fact, your enumerate is an embedding into α, so you can have a lemma about finset.map.

Separately, it will get much clunkier when your t is a non-simple finset, like the union/diff/inter of other finsets.

[Oliver Nash]

Well there are times when one wants an embedding into α. For example, if one wants to speak of linear independence of a finset α.