logic.equiv.list

# Equivalences involving list-like types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Explicit encoding function for list α

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

Explicit decoding function for list α

Equations
• = encodable.decode_list._match_1 v (λ (v₁ v₂ : ) (h : (v₁, v₂).snd v) (this : v₂ < v.succ), (nat.unpair v) _
• 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 @[protected, instance] def list.encodable {α : Type u_1} [encodable α] : If α is encodable, then so is list α. This uses the mkpair and unpair functions from data.nat.pairing. Equations @[protected, instance] def list.countable {α : Type u_1} [countable α] : @[simp] theorem encodable.encode_list_nil {α : Type u_1} [encodable α] : @[simp] theorem encodable.encode_list_cons {α : Type u_1} [encodable α] (a : α) (l : list α) : @[simp] theorem encodable.decode_list_zero {α : Type u_1} [encodable α] : @[simp] theorem encodable.decode_list_succ {α : Type u_1} [encodable α] (v : ) : v.succ = (λ (_x : α) (_y : list α), _x :: _y) <$> <*> (nat.unpair v).snd
theorem encodable.length_le_encode {α : Type u_1} [encodable α] (l : list α) :
def encodable.encode_multiset {α : Type u_1} [encodable α] (s : multiset α) :

Explicit encoding function for multiset α

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

Explicit decoding function for multiset α

Equations
@[protected, instance]
def multiset.encodable {α : Type u_1} [encodable α] :

If α is encodable, then so is multiset α.

Equations
@[protected, instance]
def multiset.countable {α : Type u_1} [countable α] :

If α is countable, then so is multiset α.

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

A listable type with decidable equality is encodable.

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

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

Equations
noncomputable def fintype.to_encodable (α : Type u_1) [fintype α] :

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
@[protected, instance]
def vector.encodable {α : Type u_1} [encodable α] {n : } :

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

Equations
@[protected, instance]
def vector.countable {α : Type u_1} [countable α] {n : } :

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

@[protected, instance]
def encodable.fin_arrow {α : Type u_1} [encodable α] {n : } :

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

Equations
@[protected, instance]
def encodable.fin_pi (n : ) (π : fin n Type u_1) [Π (i : fin n), encodable (π i)] :
encodable (Π (i : fin n), π i)
Equations
@[protected, instance]
def finset.encodable {α : Type u_1} [encodable α] :

If α is encodable, then so is finset α.

Equations
@[protected, instance]
def finset.countable {α : Type u_1} [countable α] :

If α is countable, then so is finset α.

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
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
def encodable.sorted_univ (α : Type u_1) [fintype α] [encodable α] :
list α

The elements of a fintype as a sorted list.

Equations
@[simp]
theorem encodable.mem_sorted_univ {α : Type u_1} [fintype α] [encodable α] (x : α) :
@[simp]
theorem encodable.length_sorted_univ (α : Type u_1) [fintype α] [encodable α] :
@[simp]
theorem encodable.sorted_univ_nodup (α : Type u_1) [fintype α] [encodable α] :
@[simp]
theorem encodable.sorted_univ_to_finset (α : Type u_1) [fintype α] [encodable α] [decidable_eq α] :
def encodable.fintype_equiv_fin {α : Type u_1} [fintype α] [encodable α] :

An encodable fintype is equivalent to the same size fin.

Equations
@[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
theorem denumerable.denumerable_list_aux {α : Type u_1} [denumerable α] (n : ) :
(a : list α) (H : ,
@[protected, instance]

If α is denumerable, then so is list α.

Equations
@[simp]
theorem denumerable.list_of_nat_zero {α : Type u_1} [denumerable α] :
@[simp]
theorem denumerable.list_of_nat_succ {α : Type u_1} [denumerable α] (v : ) :

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

Equations

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

Equations
theorem denumerable.lower_raise (l : list ) (n : ) :
= l
theorem denumerable.raise_lower {l : list } {n : } :
(n :: l) = l
theorem denumerable.raise_chain (l : list ) (n : ) :
n)
theorem denumerable.raise_sorted (l : list ) (n : ) :

raise l n is an non-decreasing sequence.

@[protected, instance]
def denumerable.multiset {α : Type u_1} [denumerable α] :

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

Equations

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

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
theorem denumerable.lower_raise' (l : list ) (n : ) :
= l
theorem denumerable.raise_lower' {l : list } {n : } :
( (m : ), m l n m) = l
theorem denumerable.raise'_chain (l : list ) {m n : } :
m < n
theorem denumerable.raise'_sorted (l : list ) (n : ) :

raise' l n is a strictly increasing sequence.

def denumerable.raise'_finset (l : list ) (n : ) :

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

Equations
@[protected, instance]
def denumerable.finset {α : Type u_1} [denumerable α] :

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

Equations

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

Equations

list ℕ is equivalent to ℕ.

Equations
def equiv.list_equiv_self_of_equiv_nat {α : Type u_1} (e : α ) :
list α α

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

Equations