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 β.

Equations

• e.listEquivOfEquiv = { toFun := List.map ⇑e, invFun := List.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

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

Explicit encoding function for List α

Equations

• Encodable.encodeList [] = 0
• Encodable.encodeList (a :: l) = (Nat.pair (Encodable.encode a) (Encodable.encodeList l)).succ

@[irreducible]

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

Explicit decoding function for List α

Equations

• Encodable.decodeList 0 = some []
• Encodable.decodeList v.succ = match Nat.unpair v, ⋯ with | (v₁, v₂), h => have this := ⋯; (fun (x1 : α) (x2 : List α) => x1 :: x2) <$> Encodable.decode v₁ <*> Encodable.decodeList v₂

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.

Equations

• List.encodable = { encode := Encodable.encodeList, decode := Encodable.decodeList, encodek := ⋯ }

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.

Equations

• Encodable.encodableOfList l H = { encode := fun (a : α) => List.idxOf a l, decode := fun (x : ℕ) => l[x]?, encodek := ⋯ }

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Fintype.toEncodable α = (Fintype.truncEncodable α).out

@[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 α.

Equations

• Denumerable.denumerableList = { toEncodable := List.encodable, decode_inv := ⋯ }

@[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.

Equations

• Equiv.listUniqueEquiv α = { toFun := List.length, invFun := fun (n : ℕ) => List.replicate n default, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[deprecated Equiv.listUniqueEquiv (since := "2025-02-17")]

def Equiv.listUnitEquiv : List Unit ≃ ℕ

The type lists on unit is canonically equivalent to the natural numbers.

Equations

• Equiv.listUnitEquiv = Equiv.listUniqueEquiv Unit

def Equiv.listNatEquivNat : List ℕ ≃ ℕ

List ℕ is equivalent to ℕ.

Equations

• Equiv.listNatEquivNat = Denumerable.eqv (List ℕ)

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

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

Equations

• e.listEquivSelfOfEquivNat = Trans.trans (Trans.trans e.listEquivOfEquiv Equiv.listNatEquivNat) e.symm