Equivalences involving List-like types #
This file defines some additional constructive equivalences using Encodable and the pairing
function on ℕ.
Explicit encoding function for List α
Equations
- Encodable.encodeList [] = 0
- Encodable.encodeList (a :: l) = Nat.succ (Nat.mkpair (Encodable.encode a) (Encodable.encodeList l))
If α is encodable, then so is List α. This uses the mkpair and unpair functions from
Data.Nat.Pairing.
Equations
- List.encodable = { encode := Encodable.encodeList, decode := Encodable.decodeList, encodek := (_ : ∀ (l : List α), Encodable.decodeList (Encodable.encodeList l) = some l) }
Equations
Explicit encoding function for Multiset α
Equations
- Encodable.encodeMultiset s = Encodable.encode (Multiset.sort Encodable.enle s)
Explicit decoding function for Multiset α
Equations
- Encodable.decodeMultiset n = Multiset.ofList <$> Encodable.decode n
If α is countable, then so is Multiset α.
A listable type with decidable equality is encodable.
Equations
- Encodable.encodableOfList l H = { encode := fun a => List.indexOf a l, decode := List.get? l, encodek := (_ : ∀ (x : α), List.get? l (List.indexOf x l) = some x) }
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.
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
If α is countable, then so is Vector α n.
Equations
If α is encodable, then so is Fin n → α→ α.
Equations
- Encodable.finArrow = Encodable.ofEquiv (Vector α n) (Equiv.symm (Equiv.vectorEquivFin α n))
Equations
- Encodable.finPi n π = Encodable.ofEquiv { f // ∀ (i : Fin n), (f i).fst = i } (Equiv.piEquivSubtypeSigma (Fin n) π)
If α is countable, then so is Finset α.
Equations
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 => Encodable.ofEquiv (Fin (Fintype.card α) → β) (Equiv.arrowCongr f (Equiv.refl β))) (Fintype.truncEquivFin α)
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.
The elements of a Fintype as a sorted list.
Equations
- Encodable.sortedUniv α = Finset.sort (↑(Encodable.encode' α) ⁻¹'o fun x x_1 => x ≤ x_1) Finset.univ
An encodable Fintype is equivalent to the same size fin.
Equations
- One or more equations did not get rendered due to their size.
If α and β are encodable and α is a fintype, then α → β→ β is encodable as well.
Equations
- Encodable.fintypeArrowOfEncodable = Encodable.ofEquiv (Fin (Fintype.card α) → β) (Equiv.arrowCongr Encodable.fintypeEquivFin (Equiv.refl β))
If α is denumerable, then so is List α.
Equations
- Denumerable.denumerableList = Denumerable.mk (_ : ∀ (n : ℕ), ∃ a, a ∈ Encodable.decodeList n ∧ Encodable.encodeList a = n)
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
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)
raise l n is an non-decreasing sequence.
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
- Denumerable.lower' [] x = []
- Denumerable.lower' (m :: l) x = (m - x) :: Denumerable.lower' l (m + 1)
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)
raise' l n is a strictly increasing sequence.
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 := (_ : List.Pairwise (fun a b => a ≠ b) (Denumerable.raise' l n)) }
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
- Equiv.listUnitEquiv = { toFun := List.length, invFun := fun n => List.replicate n (), left_inv := Equiv.listUnitEquiv.proof_1, right_inv := Equiv.listUnitEquiv.proof_2 }
List ℕ is equivalent to ℕ.
Equations
If α is equivalent to ℕ, then List α is equivalent to α.