Equivalences involving List-like types

This file defines some additional constructive equivalences using Encodable and the pairing function on ℕ.

def Equiv.listEquivOfEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) : List α ≃ List β

An equivalence between α and β generates an equivalence between List α and List β.

def Encodable.encodeList {α : Type u_1} [Encodable α] : List α → ℕ

Explicit encoding function for List α

@[irreducible]

def Encodable.decodeList {α : Type u_1} [Encodable α] : ℕ → Option (List α)

Explicit decoding function for List α

@[simp]

theorem Encodable.decodeList_encodeList_eq_self {α : Type u_1} [Encodable α] (l : List α) : decodeList (encodeList l) = some l

instance List.encodable {α : Type u_1} [Encodable α] : Encodable (List α)

If α is encodable, then so is List α. This uses the pair and unpair functions from Data.Nat.Pairing.

instance List.countable {α : Type u_2} [Countable α] : Countable (List α)

@[simp]

theorem Encodable.encode_list_nil {α : Type u_1} [Encodable α] : encode [] = 0

@[simp]

theorem Encodable.encode_list_cons {α : Type u_1} [Encodable α] (a : α) (l : List α) : encode (a :: l) = (Nat.pair (encode a) (encode l)).succ

@[simp]

theorem Encodable.decode_list_zero {α : Type u_1} [Encodable α] : decode 0 = some []

@[simp]

theorem Encodable.decode_list_succ {α : Type u_1} [Encodable α] (v : ℕ) : decode v.succ = (fun (x1 : α) (x2 : List α) => x1 :: x2) <$> decode (Nat.unpair v).1 <*> decode (Nat.unpair v).2

theorem Encodable.length_le_encode {α : Type u_1} [Encodable α] (l : List α) : l.length ≤ encode l

These two lemmas are not about lists, but are convenient to keep here and don't require Finset.sort.

instance Multiset.countable {α : Type u_1} [Countable α] : Countable (Multiset α)

If α is countable, then so is Multiset α.

instance Finset.countable {α : Type u_1} [Countable α] : Countable (Finset α)

If α is countable, then so is Finset α.

def Encodable.encodableOfList {α : Type u_1} [DecidableEq α] (l : List α) (H : ∀ (x : α), x ∈ l) : Encodable α

A listable type with decidable equality is encodable.

def Fintype.truncEncodable (α : Type u_2) [DecidableEq α] [Fintype α] : Trunc (Encodable α)

A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

noncomputable def Fintype.toEncodable (α : Type u_2) [Fintype α] : Encodable α

A noncomputable way to arbitrarily choose an ordering on a finite type. It is not made into a global instance, since it involves an arbitrary choice. This can be locally made into an instance with attribute [local instance] Fintype.toEncodable.

@[irreducible]

theorem Denumerable.denumerable_list_aux {α : Type u_1} [Denumerable α] (n : ℕ) : ∃ a ∈ Encodable.decodeList n, Encodable.encodeList a = n

instance Denumerable.denumerableList {α : Type u_1} [Denumerable α] : Denumerable (List α)

If α is denumerable, then so is List α.

@[simp]

theorem Denumerable.list_ofNat_zero {α : Type u_1} [Denumerable α] : ofNat (List α) 0 = []

@[simp]

theorem Denumerable.list_ofNat_succ {α : Type u_1} [Denumerable α] (v : ℕ) : ofNat (List α) v.succ = ofNat α (Nat.unpair v).1 :: ofNat (List α) (Nat.unpair v).2

def Equiv.listUniqueEquiv (α : Type u_1) [Unique α] : List α ≃ ℕ

A list on a unique type is equivalent to ℕ by sending each list to its length.

@[simp]

theorem Equiv.listUniqueEquiv_symm_apply (α : Type u_1) [Unique α] (n : ℕ) : (listUniqueEquiv α).symm n = List.replicate n default

@[simp]

theorem Equiv.listUniqueEquiv_apply (α : Type u_1) [Unique α] (a✝ : List α) : (listUniqueEquiv α) a✝ = a✝.length

def Equiv.listNatEquivNat : List ℕ ≃ ℕ

List ℕ is equivalent to ℕ.

def Equiv.listEquivSelfOfEquivNat {α : Type u_1} (e : α ≃ ℕ) : List α ≃ α

If α is equivalent to ℕ, then List α is equivalent to α.