## Stream: general

### Topic: encodable fintypes

#### Jeremy Avigad (Jan 16 2020 at 03:20):

Given [fintype α] and [encodable α], we should have α ≃ fin (card α). Does anyone see a nice way to prove that?

#### Yury G. Kudryashov (Jan 16 2020 at 03:42):

You probably want to_fun x = ⟨card {y : α | encode y < encode x}, _⟩. This function is injective, hence bijective. Then it should be possible to use nat.find to build an inverse.

#### Yury G. Kudryashov (Jan 16 2020 at 04:00):

Probably we can use fintype.bij_inv and fintype.injective_iff_surjective_of_equiv.

#### Yury G. Kudryashov (Jan 16 2020 at 04:31):

This works:

import data.fintype data.equiv.encodable tactic.wlog

open fintype encodable function

variables (α : Type*) [fintype α] [encodable α] [decidable_eq α]

theorem fintype.card_subtype_strict_mono [fintype α] {p q : α → Prop} [decidable_pred p]
[decidable_pred q] (hpq : {x | p x} ⊂ {x | q x}) :
card {x // p x} < card {x // q x} :=
begin
rw [subtype_card, subtype_card],
apply finset.card_lt_card,
simp only [finset.coe_ssubset.symm, set.ssubset_def, set.subset_def,
finset.mem_coe, finset.mem_filter, finset.mem_univ, true_and],
exact hpq
end

def equiv_fin_card_of_encodable : α ≃ fin (card α) :=
begin
set f : α → fin (card α) :=
λ x, ⟨card {y : α | encode y < encode x}, card_subtype_lt $lt_irrefl$ encode x⟩,
suffices : bijective f,
from ⟨f, bij_inv this, left_inverse_bij_inv this, right_inverse_bij_inv this⟩,
suffices : injective f,
{ rcases equiv_fin α with ⟨e⟩,
exact ⟨this, (injective_iff_surjective_of_equiv e).1 this⟩ },
assume x y hxy,
apply encode_injective,
wlog H : encode x < encode y := lt_or_gt_of_ne h using [x y, y x],
suffices : f x < f y,
from ne_of_lt this hxy,
refine fintype.card_subtype_strict_mono _ ⟨λ z hz, _,
λ h, absurd (h H) $by simp only [set.mem_set_of_eq, lt_irrefl, not_false_iff]⟩, simp only [set.mem_set_of_eq] at hz ⊢, exact lt_trans hz H end  #### Yury G. Kudryashov (Jan 16 2020 at 04:34): (deleted) #### Mario Carneiro (Jan 16 2020 at 07:01): I think this is in mathlib #### Mario Carneiro (Jan 16 2020 at 07:02): fintype.equiv_fin #### Jeremy Avigad (Jan 16 2020 at 12:21): @Mario Carneiro: def equiv_fin (α) [fintype α] [decidable_eq α] : trunc (α ≃ fin (card α)). There's a trunc there. @Yury G. Kudryashov: Thanks! Do you mind if I add it to the library? I need it to revise a PR. #### Mario Carneiro (Jan 16 2020 at 12:29): @Jeremy Avigad Use trunc.out to get rid of it #### Mario Carneiro (Jan 16 2020 at 12:30): It's not computable without the trunc, because there is no canonical ordering of the type #### Jeremy Avigad (Jan 16 2020 at 12:34): Is it an advantage that Yuri's version is computable? (Also, for the record, Yuri, decidable_eq α follows from encodable α.) #### Jeremy Avigad (Jan 16 2020 at 12:41): Background: I need encodable (α → β) where α is an encodable fintype and β is encodable. Right now we only have that when α is fin. #### Mario Carneiro (Jan 16 2020 at 12:41): does it have to be computable? #### Jeremy Avigad (Jan 16 2020 at 12:43): You tell me. It is towards a proof that finitely branching W types are encodable, which can be used e.g. to show that syntactic definitions are encodable. My guess is that yes, we want that to be computable. #### Mario Carneiro (Jan 16 2020 at 13:11): Here's a nicer approach IMO: (The first lemma is a fragment of the proof of fintype.equiv_fin) def list.equiv_fin {α} [decidable_eq α] {l : list α} (h : ∀ x:α, x ∈ l) (nd : l.nodup) : α ≃ fin (l.length) := ⟨λ a, ⟨_, list.index_of_lt_length.2 (h a)⟩, λ i, l.nth_le i.1 i.2, λ a, by simp, λ ⟨i, h⟩, fin.eq_of_veq$ list.nodup_iff_nth_le_inj.1 nd _ _
(list.index_of_lt_length.2 (list.nth_le_mem _ _ _)) h \$ by simp⟩

instance order.preimage.decidable {α β} (f : α → β) (s : β → β → Prop)
[H : decidable_rel s] : decidable_rel (f ⁻¹'o s) := λ x y, H _ _

def encodable.encode' (α) [encodable α] : α ↪ nat :=
⟨encodable.encode, encodable.encode_injective⟩

instance {α} [encodable α] : is_trans _ (encodable.encode' α ⁻¹'o (≤)) :=
(order_embedding.preimage _ _).is_trans
instance {α} [encodable α] : is_antisymm _ (encodable.encode' α ⁻¹'o (≤)) :=
(order_embedding.preimage _ _).is_antisymm
instance {α} [encodable α] : is_total _ (encodable.encode' α ⁻¹'o (≤)) :=
(order_embedding.preimage _ _).is_total

def sorted_univ (α) [fintype α] [encodable α] : list α :=
finset.univ.sort (encodable.encode' α ⁻¹'o (≤))

theorem mem_sorted_univ {α} [fintype α] [encodable α] (x : α) : x ∈ sorted_univ α :=
(finset.mem_sort _).2 (finset.mem_univ _)

theorem length_sorted_univ {α} [fintype α] [encodable α] : (sorted_univ α).length = fintype.card α :=
finset.length_sort _

theorem sorted_univ_nodup {α} [fintype α] [encodable α] : (sorted_univ α).nodup :=
finset.sort_nodup _ _

def encodable_fintype.equiv_fin {α} [fintype α] [encodable α] [decidable_eq α] :
α ≃ fin (fintype.card α) :=
by rw ← @length_sorted_univ α; exact
list.equiv_fin mem_sorted_univ sorted_univ_nodup


#### Jeremy Avigad (Jan 16 2020 at 15:17):

Looks good. I am leaving for Zurich in a couple of hours but I'll get this in while traveling. (And, to repeat, we can drop [decidable_eq α].)

Last updated: May 13 2021 at 00:41 UTC