Equivalences involving List-like types

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

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 => let_fun 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

def Encodable.encodeMultiset {α : Type u_1} [Encodable α] (s : Multiset α) : ℕ

Explicit encoding function for Multiset α

Equations

• Encodable.encodeMultiset s = Encodable.encode (Multiset.sort Encodable.enle✝ s)

def Encodable.decodeMultiset {α : Type u_1} [Encodable α] (n : ℕ) : Option (Multiset α)

Explicit decoding function for Multiset α

Equations

• Encodable.decodeMultiset n = Multiset.ofList <$> Encodable.decode n

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

If α is encodable, then so is Multiset α.

Equations

• Multiset.encodable = { encode := Encodable.encodeMultiset, decode := Encodable.decodeMultiset, encodek := ⋯ }

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

If α is countable, then so is Multiset α.

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 := l.get?, 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

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

If α is encodable, then so is Vector α n.

Equations

• Encodable.List.Vector.encodable = Subtype.encodable

instance Encodable.List.Vector.countable {α : Type u_1} [Countable α] {n : ℕ} : Countable (List.Vector α n)

If α is countable, then so is Vector α n.

instance Encodable.finArrow {α : Type u_1} [Encodable α] {n : ℕ} : Encodable (Fin n → α)

If α is encodable, then so is Fin n → α.

Equations

• Encodable.finArrow = Encodable.ofEquiv (List.Vector α n) (Equiv.vectorEquivFin α n).symm

instance Encodable.finPi (n : ℕ) (π : Fin n → Type u_2) [(i : Fin n) → Encodable (π i)] : Encodable ((i : Fin n) → π i)

Equations

• Encodable.finPi n π = Encodable.ofEquiv { f : Fin n → (i : Fin n) × π i // ∀ (i : Fin n), (f i).fst = i } (Equiv.piEquivSubtypeSigma (Fin n) π)

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

If α is encodable, then so is Finset α.

Equations

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

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

If α is countable, then so is Finset α.

def Encodable.fintypeArrow (α : Type u_2) (β : Type u_3) [DecidableEq α] [Fintype α] [Encodable β] : Trunc (Encodable (α → β))

When α is finite and β is encodable, α → β is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

Equations

• Encodable.fintypeArrow α β = Trunc.map (fun (f : α ≃ Fin (Fintype.card α)) => Encodable.ofEquiv (Fin (Fintype.card α) → β) (f.arrowCongr (Equiv.refl β))) (Fintype.truncEquivFin α)

def Encodable.fintypePi (α : Type u_2) (π : α → Type u_3) [DecidableEq α] [Fintype α] [(a : α) → Encodable (π a)] : Trunc (Encodable ((a : α) → π a))

When α is finite and all π a are encodable, Π a, π a is encodable too. 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.

def Encodable.sortedUniv (α : Type u_2) [Fintype α] [Encodable α] : List α

The elements of a Fintype as a sorted list.

Equations

• Encodable.sortedUniv α = Finset.sort (⇑(Encodable.encode' α) ⁻¹'o fun (x1 x2 : ℕ) => x1 ≤ x2) Finset.univ

@[simp]

theorem Encodable.mem_sortedUniv {α : Type u_2} [Fintype α] [Encodable α] (x : α) : x ∈ sortedUniv α

@[simp]

theorem Encodable.length_sortedUniv (α : Type u_2) [Fintype α] [Encodable α] : (sortedUniv α).length = Fintype.card α

@[simp]

theorem Encodable.sortedUniv_nodup (α : Type u_2) [Fintype α] [Encodable α] : (sortedUniv α).Nodup

@[simp]

theorem Encodable.sortedUniv_toFinset (α : Type u_2) [Fintype α] [Encodable α] [DecidableEq α] : (sortedUniv α).toFinset = Finset.univ

def Encodable.fintypeEquivFin {α : Type u_2} [Fintype α] [Encodable α] : α ≃ Fin (Fintype.card α)

An encodable Fintype is equivalent to the same size Fin.

Equations

• Encodable.fintypeEquivFin = (List.Nodup.getEquivOfForallMemList (Encodable.sortedUniv α) ⋯ ⋯).symm.trans (Equiv.cast ⋯)

instance Encodable.fintypeArrowOfEncodable {α : Type u_2} {β : Type u_3} [Encodable α] [Fintype α] [Encodable β] : Encodable (α → β)

If α and β are encodable and α is a fintype, then α → β is encodable as well.

Equations

• Encodable.fintypeArrowOfEncodable = Encodable.ofEquiv (Fin (Fintype.card α) → β) (Encodable.fintypeEquivFin.arrowCongr (Equiv.refl β))

@[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 = Denumerable.mk ⋯

@[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 Denumerable.lower : List ℕ → ℕ → List ℕ

Outputs the list of differences of the input list, that is lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]

Equations

• Denumerable.lower [] x✝ = []
• Denumerable.lower (m :: l) x✝ = (m - x✝) :: Denumerable.lower l m

def Denumerable.raise : List ℕ → ℕ → List ℕ

Outputs the list of partial sums of the input list, that is raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]

Equations

• Denumerable.raise [] x✝ = []
• Denumerable.raise (m :: l) x✝ = (m + x✝) :: Denumerable.raise l (m + x✝)

theorem Denumerable.lower_raise (l : List ℕ) (n : ℕ) : lower (raise l n) n = l

theorem Denumerable.raise_lower {l : List ℕ} {n : ℕ} : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (n :: l) → raise (lower l n) n = l

theorem Denumerable.raise_chain (l : List ℕ) (n : ℕ) : List.Chain (fun (x1 x2 : ℕ) => x1 ≤ x2) n (raise l n)

theorem Denumerable.raise_sorted (l : List ℕ) (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 ≤ x2) (raise l n)

raise l n is a non-decreasing sequence.

instance Denumerable.multiset {α : Type u_1} [Denumerable α] : Denumerable (Multiset α)

If α is denumerable, then so is Multiset α. Warning: this is not the same encoding as used in Multiset.encodable.

Equations

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

def Denumerable.lower' : List ℕ → ℕ → List ℕ

Outputs the list of differences minus one of the input list, that is lower' [a₁, a₂, a₃, ...] n = [a₁ - n, a₂ - a₁ - 1, a₃ - a₂ - 1, ...].

Equations

• Denumerable.lower' [] x✝ = []
• Denumerable.lower' (m :: l) x✝ = (m - x✝) :: Denumerable.lower' l (m + 1)

def Denumerable.raise' : List ℕ → ℕ → List ℕ

Outputs the list of partial sums plus one of the input list, that is raise [a₁, a₂, a₃, ...] n = [n + a₁, n + a₁ + a₂ + 1, n + a₁ + a₂ + a₃ + 2, ...]. Adding one each time ensures the elements are distinct.

Equations

• Denumerable.raise' [] x✝ = []
• Denumerable.raise' (m :: l) x✝ = (m + x✝) :: Denumerable.raise' l (m + x✝ + 1)

theorem Denumerable.lower_raise' (l : List ℕ) (n : ℕ) : lower' (raise' l n) n = l

theorem Denumerable.raise_lower' {l : List ℕ} {n : ℕ} : (∀ m ∈ l, n ≤ m) → List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) l → raise' (lower' l n) n = l

theorem Denumerable.raise'_chain (l : List ℕ) {m n : ℕ} : m < n → List.Chain (fun (x1 x2 : ℕ) => x1 < x2) m (raise' l n)

theorem Denumerable.raise'_sorted (l : List ℕ) (n : ℕ) : List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) (raise' l n)

raise' l n is a strictly increasing sequence.

def Denumerable.raise'Finset (l : List ℕ) (n : ℕ) : Finset ℕ

Makes raise' l n into a finset. Elements are distinct thanks to raise'_sorted.

Equations

• Denumerable.raise'Finset l n = { val := ↑(Denumerable.raise' l n), nodup := ⋯ }

instance Denumerable.finset {α : Type u_1} [Denumerable α] : Denumerable (Finset α)

If α is denumerable, then so is Finset α. Warning: this is not the same encoding as used in Finset.encodable.

Equations

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

def Equiv.listUnitEquiv : List Unit ≃ ℕ

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

Equations

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

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