logic.equiv.list - mathlib docs

source

def encodable.encode_list {α : Type u_1} [encodable α] :

list α → ℕ

Explicit encoding function for list α

Equations

encodable.encode_list (a :: l) = (nat.mkpair (encodable.encode a) (encodable.encode_list l)).succ
encodable.encode_list list.nil = 0

source

def encodable.decode_list {α : Type u_1} [encodable α] :

ℕ → option (list α)

Explicit decoding function for list α

Equations

encodable.decode_list v.succ = encodable.decode_list._match_1 v (λ (v₁ v₂ : ℕ) (h : (v₁, v₂).snd ≤ v) (this : v₂ < v.succ), encodable.decode_list v₂) (nat.unpair v) _
encodable.decode_list 0 = some list.nil
encodable.decode_list._match_1 v _f_1 (v₁, v₂) h = have this : v₂ < v.succ, from _, (λ (_x : α) (_y : list α), _x :: _y) <$> encodable.decode α v₁ <*> _f_1 v₁ v₂ h this

source

@[protected, instance]

def list.encodable {α : Type u_1} [encodable α] :

encodable (list α)

If α is encodable, then so is list α. This uses the mkpair and unpair functions from data.nat.pairing.

Equations

list.encodable = {encode := encodable.encode_list _inst_1, decode := encodable.decode_list _inst_1, encodek := _}

source

@[simp]

theorem encodable.encode_list_nil {α : Type u_1} [encodable α] :

encodable.encode list.nil = 0

source

@[simp]

theorem encodable.encode_list_cons {α : Type u_1} [encodable α] (a : α) (l : list α) :

encodable.encode (a :: l) = (nat.mkpair (encodable.encode a) (encodable.encode l)).succ

source

@[simp]

theorem encodable.decode_list_zero {α : Type u_1} [encodable α] :

encodable.decode (list α) 0 = some list.nil

source

@[simp]

theorem encodable.decode_list_succ {α : Type u_1} [encodable α] (v : ℕ) :

encodable.decode (list α) v.succ = (λ (_x : α) (_y : list α), _x :: _y) <$> encodable.decode α (nat.unpair v).fst <*> encodable.decode (list α) (nat.unpair v).snd

source

theorem encodable.length_le_encode {α : Type u_1} [encodable α] (l : list α) :

l.length ≤ encodable.encode l

source

def encodable.encode_multiset {α : Type u_1} [encodable α] (s : multiset α) :

ℕ

Explicit encoding function for multiset α

Equations

encodable.encode_multiset s = encodable.encode (multiset.sort enle s)

source

def encodable.decode_multiset {α : Type u_1} [encodable α] (n : ℕ) :

option (multiset α)

Explicit decoding function for multiset α

Equations

encodable.decode_multiset n = coe <$> encodable.decode (list α) n

source

@[protected, instance]

def multiset.encodable {α : Type u_1} [encodable α] :

encodable (multiset α)

If α is encodable, then so is multiset α.

Equations

multiset.encodable = {encode := encodable.encode_multiset _inst_1, decode := encodable.decode_multiset _inst_1, encodek := _}

source

def encodable.encodable_of_list {α : Type u_1} [decidable_eq α] (l : list α) (H : ∀ (x : α), x ∈ l) :

encodable α

A listable type with decidable equality is encodable.

Equations

encodable.encodable_of_list l H = {encode := λ (a : α), list.index_of a l, decode := l.nth, encodek := _}

source

def fintype.trunc_encodable (α : Type u_1) [decidable_eq α] [fintype α] :

trunc (encodable α)

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

Equations

fintype.trunc_encodable α = quot.rec_on_subsingleton finset.univ.val (λ (l : list α) (H : ∀ (x : α), x ∈ quot.mk setoid.r l), trunc.mk (encodable.encodable_of_list l H)) finset.mem_univ

source

noncomputable def fintype.to_encodable (α : Type u_1) [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 local attribute [instance] fintype.to_encodable.

Equations

fintype.to_encodable α = (fintype.trunc_encodable α).out

source

@[protected, instance]

def vector.encodable {α : Type u_1} [encodable α] {n : ℕ} :

encodable (vector α n)

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

Equations

vector.encodable = subtype.encodable

source

@[protected, instance]

def encodable.fin_arrow {α : Type u_1} [encodable α] {n : ℕ} :

encodable (fin n → α)

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

Equations

encodable.fin_arrow = encodable.of_equiv (vector α n) (equiv.vector_equiv_fin α n).symm

source

@[protected, instance]

def encodable.fin_pi (n : ℕ) (π : fin n → Type u_1) [Π (i : fin n), encodable (π i)] :

encodable (Π (i : fin n), π i)

Equations

encodable.fin_pi n π = encodable.of_equiv {f // ∀ (i : fin n), (f i).fst = i} (equiv.pi_equiv_subtype_sigma (fin n) π)

source

@[protected, instance]

def array.encodable {α : Type u_1} [encodable α] {n : ℕ} :

encodable (array n α)

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

Equations

array.encodable = encodable.of_equiv (fin n → α) (equiv.array_equiv_fin n α)

source

@[protected, instance]

def finset.encodable {α : Type u_1} [encodable α] :

encodable (finset α)

If α is encodable, then so is finset α.

Equations

finset.encodable = encodable.of_equiv {s // s.nodup} {to_fun := λ (_x : finset α), encodable._root_.finset.encodable._match_1 _x, inv_fun := λ (_x : {s // s.nodup}), encodable._root_.finset.encodable._match_2 _x, left_inv := _, right_inv := _}

source

def encodable.fintype_arrow (α : Type u_1) (β : Type u_2) [decidable_eq α] [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.fintype_arrow α β = trunc.map (λ (f : α ≃ fin (fintype.card α)), encodable.of_equiv (fin (fintype.card α) → β) (f.arrow_congr (equiv.refl β))) (fintype.trunc_equiv_fin α)

source

def encodable.fintype_pi (α : Type u_1) (π : α → Type u_2) [decidable_eq α] [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

encodable.fintype_pi α π = (fintype.trunc_encodable α).bind (λ (a : encodable α), (encodable.fintype_arrow α (Σ (a : α), π a)).bind (λ (f : encodable (α → (Σ (a : α), π a))), trunc.mk (encodable.of_equiv {a // ∀ (i : α), (a i).fst = i} (equiv.pi_equiv_subtype_sigma α π))))

source

def encodable.sorted_univ (α : Type u_1) [fintype α] [encodable α] :

list α

The elements of a fintype as a sorted list.

Equations

encodable.sorted_univ α = finset.sort (⇑(encodable.encode' α) ⁻¹'o has_le.le) finset.univ

source

@[simp]

theorem encodable.mem_sorted_univ {α : Type u_1} [fintype α] [encodable α] (x : α) :

x ∈ encodable.sorted_univ α

source

@[simp]

theorem encodable.length_sorted_univ (α : Type u_1) [fintype α] [encodable α] :

(encodable.sorted_univ α).length = fintype.card α

source

@[simp]

theorem encodable.sorted_univ_nodup (α : Type u_1) [fintype α] [encodable α] :

(encodable.sorted_univ α).nodup

source

@[simp]

theorem encodable.sorted_univ_to_finset (α : Type u_1) [fintype α] [encodable α] [decidable_eq α] :

(encodable.sorted_univ α).to_finset = finset.univ

source

def encodable.fintype_equiv_fin {α : Type u_1} [fintype α] [encodable α] :

α ≃ fin (fintype.card α)

An encodable fintype is equivalent to the same size fin.

Equations

encodable.fintype_equiv_fin = (list.nodup.nth_le_equiv_of_forall_mem_list (encodable.sorted_univ α) _ encodable.mem_sorted_univ).symm.trans (equiv.cast encodable.fintype_equiv_fin._proof_1)

source

@[protected, instance]

def encodable.fintype_arrow_of_encodable {α : Type u_1} {β : Type u_2} [encodable α] [fintype α] [encodable β] :

encodable (α → β)

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

Equations

encodable.fintype_arrow_of_encodable = encodable.of_equiv (fin (fintype.card α) → β) (encodable.fintype_equiv_fin.arrow_congr (equiv.refl β))

source

theorem denumerable.denumerable_list_aux {α : Type u_1} [denumerable α] (n : ℕ) :

∃ (a : list α) (H : a ∈ encodable.decode_list n), encodable.encode_list a = n

source

@[protected, instance]

def denumerable.denumerable_list {α : Type u_1} [denumerable α] :

denumerable (list α)

If α is denumerable, then so is list α.

Equations

denumerable.denumerable_list = {to_encodable := list.encodable denumerable.to_encodable, decode_inv := _}

source

@[simp]

theorem denumerable.list_of_nat_zero {α : Type u_1} [denumerable α] :

denumerable.of_nat (list α) 0 = list.nil

source

@[simp]

theorem denumerable.list_of_nat_succ {α : Type u_1} [denumerable α] (v : ℕ) :

denumerable.of_nat (list α) v.succ = denumerable.of_nat α (nat.unpair v).fst :: denumerable.of_nat (list α) (nat.unpair v).snd

source

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 (m :: l) n = (m - n) :: denumerable.lower l m
denumerable.lower list.nil n = list.nil

source

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 (m :: l) n = (m + n) :: denumerable.raise l (m + n)
denumerable.raise list.nil n = list.nil

source

theorem denumerable.lower_raise (l : list ℕ) (n : ℕ) :

denumerable.lower (denumerable.raise l n) n = l

source

theorem denumerable.raise_lower {l : list ℕ} {n : ℕ} :

list.sorted has_le.le (n :: l) → denumerable.raise (denumerable.lower l n) n = l

source

theorem denumerable.raise_chain (l : list ℕ) (n : ℕ) :

list.chain has_le.le n (denumerable.raise l n)

source

theorem denumerable.raise_sorted (l : list ℕ) (n : ℕ) :

list.sorted has_le.le (denumerable.raise l n)

raise l n is an non-decreasing sequence.

source

@[protected, instance]

def 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

denumerable.multiset = denumerable.mk' {to_fun := λ (s : multiset α), encodable.encode (denumerable.lower (multiset.sort has_le.le (multiset.map encodable.encode s)) 0), inv_fun := λ (n : ℕ), multiset.map (denumerable.of_nat α) ↑(denumerable.raise (denumerable.of_nat (list ℕ) n) 0), left_inv := _, right_inv := _}

source

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' (m :: l) n = (m - n) :: denumerable.lower' l (m + 1)
denumerable.lower' list.nil n = list.nil

source

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