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.pair (Encodable.encode a) (Encodable.encodeList l))
Instances For
A listable type with decidable equality is encodable.
Instances For
A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc
to
preserve computability.
Instances For
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
.
Instances For
When α
is finite and β
is encodable, α → β
is encodable too. Because the encoding is not
unique, we wrap it in Trunc
to preserve computability.
Instances For
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.
Instances For
If α
is denumerable, then so is List α
.
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
Instances For
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)
Instances For
raise l n
is a non-decreasing sequence.
If α
is denumerable, then so is Multiset α
. Warning: this is not the same encoding as used
in Multiset.encodable
.
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)
Instances For
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)
Instances For
raise' l n
is a strictly increasing sequence.
Makes raise' l n
into a finset. Elements are distinct thanks to raise'_sorted
.
Instances For
If α
is denumerable, then so is Finset α
. Warning: this is not the same encoding as used
in Finset.encodable
.