encodable fintypes

Stream: general

[Jeremy Avigad]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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,
  by_contradiction h,
  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]

(deleted)

[Mario Carneiro]

I think this is in mathlib

[Mario Carneiro]

fintype.equiv_fin

[Jeremy Avigad]

@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]

@Jeremy Avigad Use trunc.out to get rid of it

[Mario Carneiro]

It's not computable without the trunc, because there is no canonical ordering of the type

[Jeremy Avigad]

Is it an advantage that Yuri's version is computable?
(Also, for the record, Yuri, decidable_eq α follows from encodable α.)

[Jeremy Avigad]

Background: I need encodable (α → β) where α is an encodable fintype and β is encodable. Right now we only have that when α is fin.

[Mario Carneiro]

does it have to be computable?

[Jeremy Avigad]

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]

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]

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 α].)