Zulip Chat Archive

Stream: general

Topic: encodable fintypes


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

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

view this post on Zulip Yury G. Kudryashov (Jan 16 2020 at 04:00):

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

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

view this post on Zulip Yury G. Kudryashov (Jan 16 2020 at 04:34):

(deleted)

view this post on Zulip Mario Carneiro (Jan 16 2020 at 07:01):

I think this is in mathlib

view this post on Zulip Mario Carneiro (Jan 16 2020 at 07:02):

fintype.equiv_fin

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

view this post on Zulip Mario Carneiro (Jan 16 2020 at 12:29):

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

view this post on Zulip Mario Carneiro (Jan 16 2020 at 12:30):

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

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

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

view this post on Zulip Mario Carneiro (Jan 16 2020 at 12:41):

does it have to be computable?

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

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

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