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

Explicit encoding function for List α

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

Explicit decoding function for List α

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance List.encodable {α : Type u_1} [] :

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} [] :
Equations
• =
@[simp]
theorem Encodable.encode_list_nil {α : Type u_1} [] :
@[simp]
theorem Encodable.encode_list_cons {α : Type u_1} [] (a : α) (l : List α) :
Encodable.encode (a :: l) = (().pair ()).succ
@[simp]
theorem Encodable.decode_list_zero {α : Type u_1} [] :
@[simp]
theorem Encodable.decode_list_succ {α : Type u_1} [] (v : ) :
Encodable.decode v.succ = Seq.seq ((fun (x : α) (x_1 : List α) => x :: x_1) <$> Encodable.decode v.unpair.1) fun (x : Unit) => Encodable.decode v.unpair.2 theorem Encodable.length_le_encode {α : Type u_1} [] (l : List α) : l.length def Encodable.encodeMultiset {α : Type u_1} [] (s : ) : Explicit encoding function for Multiset α Equations Instances For def Encodable.decodeMultiset {α : Type u_1} [] (n : ) : Explicit decoding function for Multiset α Equations • = Multiset.ofList <$>
Instances For
instance Multiset.encodable {α : Type u_1} [] :

If α is encodable, then so is Multiset α.

Equations
• Multiset.encodable = { encode := Encodable.encodeMultiset, decode := Encodable.decodeMultiset, encodek := }
instance Multiset.countable {α : Type u_2} [] :

If α is countable, then so is Multiset α.

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

A listable type with decidable equality is encodable.

Equations
• = { encode := fun (a : α) => , decode := l.get?, encodek := }
Instances For
def Fintype.truncEncodable (α : Type u_2) [] [] :

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.
Instances For
noncomputable def Fintype.toEncodable (α : Type u_2) [] :

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
Instances For
instance Vector.encodable {α : Type u_1} [] {n : } :

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

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

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

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

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

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

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

If α is countable, then so is Finset α.

Equations
• =
def Encodable.fintypeArrow (α : Type u_2) (β : Type u_3) [] [] [] :
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
Instances For
def Encodable.fintypePi (α : Type u_2) (π : αType u_3) [] [] [(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.
Instances For
def Encodable.sortedUniv (α : Type u_2) [] [] :
List α

The elements of a Fintype as a sorted list.

Equations
Instances For
@[simp]
theorem Encodable.mem_sortedUniv {α : Type u_2} [] [] (x : α) :
@[simp]
theorem Encodable.length_sortedUniv (α : Type u_2) [] [] :
.length =
@[simp]
theorem Encodable.sortedUniv_nodup (α : Type u_2) [] [] :
.Nodup
@[simp]
theorem Encodable.sortedUniv_toFinset (α : Type u_2) [] [] [] :
.toFinset = Finset.univ
def Encodable.fintypeEquivFin {α : Type u_2} [] [] :
α Fin ()

An encodable Fintype is equivalent to the same size Fin.

Equations
• Encodable.fintypeEquivFin = .symm.trans ()
Instances For
instance Encodable.fintypeArrowOfEncodable {α : Type u_2} {β : Type u_3} [] [] [] :
Encodable (αβ)

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

Equations
• Encodable.fintypeArrowOfEncodable = Encodable.ofEquiv (Fin ()β) (Encodable.fintypeEquivFin.arrowCongr ())
theorem Denumerable.denumerable_list_aux {α : Type u_1} [] (n : ) :
a,
instance Denumerable.denumerableList {α : Type u_1} [] :

If α is denumerable, then so is List α.

Equations
• Denumerable.denumerableList =
@[simp]
theorem Denumerable.list_ofNat_zero {α : Type u_1} [] :
= []
@[simp]
theorem Denumerable.list_ofNat_succ {α : Type u_1} [] (v : ) :
Denumerable.ofNat (List α) v.succ = Denumerable.ofNat α v.unpair.1 :: Denumerable.ofNat (List α) v.unpair.2
def Denumerable.lower :

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

Equations
Instances For
def Denumerable.raise :

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

Equations
Instances For
theorem Denumerable.lower_raise (l : ) (n : ) :
= l
theorem Denumerable.raise_lower {l : } {n : } :
List.Sorted (fun (x x_1 : ) => x x_1) (n :: l) = l
theorem Denumerable.raise_chain (l : ) (n : ) :
List.Chain (fun (x x_1 : ) => x x_1) n ()
theorem Denumerable.raise_sorted (l : ) (n : ) :
List.Sorted (fun (x x_1 : ) => x x_1) ()

raise l n is a non-decreasing sequence.

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

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' :

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
Instances For
def Denumerable.raise' :

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
Instances For
theorem Denumerable.lower_raise' (l : ) (n : ) :
= l
theorem Denumerable.raise_lower' {l : } {n : } :
(ml, n m)List.Sorted (fun (x x_1 : ) => x < x_1) l = l
theorem Denumerable.raise'_chain (l : ) {m : } {n : } :
m < nList.Chain (fun (x x_1 : ) => x < x_1) m ()
theorem Denumerable.raise'_sorted (l : ) (n : ) :
List.Sorted (fun (x x_1 : ) => x < x_1) ()

raise' l n is a strictly increasing sequence.

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

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

Equations
• = { val := (), nodup := }
Instances For
instance Denumerable.finset {α : Type u_1} [] :

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
Instances For

List ℕ is equivalent to ℕ.

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

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

Equations
Instances For