Documentation

Mathlib.Logic.Equiv.List

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} [inst : Encodable α] :
List α

Explicit encoding function for List α

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

Explicit decoding function for List α

Equations
instance List.encodable {α : Type u_1} [inst : Encodable α] :

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

Equations
@[simp]
theorem Encodable.encode_list_nil {α : Type u_1} [inst : Encodable α] :
@[simp]
theorem Encodable.encode_list_cons {α : Type u_1} [inst : Encodable α] (a : α) (l : List α) :
@[simp]
theorem Encodable.decode_list_zero {α : Type u_1} [inst : Encodable α] :
@[simp]
theorem Encodable.decode_list_succ {α : Type u_1} [inst : Encodable α] (v : ) :
Encodable.decode (Nat.succ v) = Seq.seq ((fun x x_1 => x :: x_1) <$> Encodable.decode (Nat.unpair v).fst) fun x => Encodable.decode (Nat.unpair v).snd
def Encodable.encodeMultiset {α : Type u_1} [inst : Encodable α] (s : Multiset α) :

Explicit encoding function for Multiset α

Equations
def Encodable.decodeMultiset {α : Type u_1} [inst : Encodable α] (n : ) :

Explicit decoding function for Multiset α

Equations
instance Multiset.encodable {α : Type u_1} [inst : Encodable α] :

If α is encodable, then so is Multiset α.

Equations
  • One or more equations did not get rendered due to their size.
instance Multiset.countable {α : Type u_1} [inst : Countable α] :

If α is countable, then so is Multiset α.

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

A listable type with decidable equality is encodable.

Equations
def Fintype.truncEncodable (α : Type u_1) [inst : DecidableEq α] [inst : Fintype α] :

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_1) [inst : 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.toEncodable.

Equations
instance Vector.encodable {α : Type u_1} [inst : Encodable α] {n : } :

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

Equations
  • Vector.encodable = Encodable.Subtype.encodable
instance Vector.countable {α : Type u_1} [inst : Countable α] {n : } :

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

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

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

Equations
instance Encodable.finPi (n : ) (π : Fin nType u_1) [inst : (i : Fin n) → Encodable (π i)] :
Encodable ((i : Fin n) → π i)
Equations
instance Finset.encodable {α : Type u_1} [inst : Encodable α] :

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} [inst : Countable α] :

If α is countable, then so is Finset α.

Equations
def Encodable.fintypeArrow (α : Type u_1) (β : Type u_2) [inst : DecidableEq α] [inst : Fintype α] [inst : 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.fintypePi (α : Type u_1) (π : αType u_2) [inst : DecidableEq α] [inst : Fintype α] [inst : (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_1) [inst : Fintype α] [inst : Encodable α] :
List α

The elements of a Fintype as a sorted list.

Equations
@[simp]
theorem Encodable.mem_sortedUniv {α : Type u_1} [inst : Fintype α] [inst : Encodable α] (x : α) :
@[simp]
@[simp]
theorem Encodable.sortedUniv_nodup (α : Type u_1) [inst : Fintype α] [inst : Encodable α] :
@[simp]
theorem Encodable.sortedUniv_toFinset (α : Type u_1) [inst : Fintype α] [inst : Encodable α] [inst : DecidableEq α] :
def Encodable.fintypeEquivFin {α : Type u_1} [inst : Fintype α] [inst : Encodable α] :

An encodable Fintype is equivalent to the same size fin.

Equations
  • One or more equations did not get rendered due to their size.
instance Encodable.fintypeArrowOfEncodable {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst : Fintype α] [inst : Encodable β] :
Encodable (αβ)

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

Equations
instance Denumerable.denumerableList {α : Type u_1} [inst : Denumerable α] :

If α is denumerable, then so is List α.

Equations
@[simp]
theorem Denumerable.list_ofNat_zero {α : Type u_1} [inst : Denumerable α] :

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.raise_lower {l : List } {n : } :
List.Sorted (fun x x_1 => x x_1) (n :: l)Denumerable.raise (Denumerable.lower l n) n = l
theorem Denumerable.raise_chain (l : List ) (n : ) :
List.Chain (fun x x_1 => x x_1) n (Denumerable.raise l n)
theorem Denumerable.raise_sorted (l : List ) (n : ) :
List.Sorted (fun x x_1 => x x_1) (Denumerable.raise l n)

raise l n is an non-decreasing sequence.

instance Denumerable.multiset {α : Type u_1} [inst : Denumerable α] :

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.

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.raise_lower' {l : List } {n : } :
(∀ (m : ), m ln m) → List.Sorted (fun x x_1 => x < x_1) lDenumerable.raise' (Denumerable.lower' l n) n = l
theorem Denumerable.raise'_chain (l : List ) {m : } {n : } :
m < nList.Chain (fun x x_1 => x < x_1) m (Denumerable.raise' l n)
theorem Denumerable.raise'_sorted (l : List ) (n : ) :
List.Sorted (fun x x_1 => x < x_1) (Denumerable.raise' l n)

raise' l n is a strictly increasing sequence.

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

Equations
instance Denumerable.finset {α : Type u_1} [inst : Denumerable α] :

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.

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

Equations
def Equiv.listEquivSelfOfEquivNat {α : Type} (e : α ) :
List α α

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

Equations