Encodable types #
This file defines encodable (constructively countable) types as a typeclass.
This is used to provide explicit encode/decode functions from and to ℕ
, with the information that
those functions are inverses of each other.
The difference with Denumerable
is that finite types are encodable. For infinite types,
Encodable
and Denumerable
agree.
Main declarations #
Encodable α
: States that there exists an explicit encoding functionencode : α → ℕ
with a partial inversedecode : ℕ → Option α
.decode₂
: Version ofdecode
that is equal tonone
outside of the range ofencode
. Useful as we do not require this in the definition ofdecode
.ULower α
: Any encodable type has an equivalent type living in the lowest universe, namely a subtype ofℕ
.ULower α
finds it.
Implementation notes #
The point of asking for an explicit partial inverse decode : ℕ → Option α
to encode : α → ℕ
is
to make the range of encode
decidable even when the finiteness of α
is not.
- encode : α → ℕ
Encoding from Type α to ℕ
Decoding from ℕ to Option α
- encodek : ∀ (a : α), Encodable.decode (Encodable.encode a) = some a
Invariant relationship between encoding and decoding
Constructively countable type. Made from an explicit injection encode : α → ℕ
and a partial
inverse decode : ℕ → Option α
. Note that finite types are countable. See Denumerable
if you
wish to enforce infiniteness.
Instances
An encodable type has decidable equality. Not set as an instance because this is usually not the best way to infer decidability.
Instances For
The encoding function has decidable range.
Instances For
A type with unique element is encodable. This is not an instance to avoid diamonds.
Instances For
Explicit decoding function for a decidable subtype of an encodable type
Instances For
A decidable subtype of an encodable type is encodable.
The lift of an encodable type is encodable
If β
is encodable and there is an injection f : α → β
, then α
is encodable as well.
Instances For
Constructive choice function for a decidable subtype of an encodable type.
Instances For
Constructive choice function for a decidable predicate over an encodable type.
Instances For
A constructive version of Classical.axiom_of_choice
for Encodable
types.
A constructive version of Classical.skolem
for Encodable
types.
Given a Directed r
function f : α → β
defined on an encodable inhabited type,
construct a noncomputable sequence such that r (f (x n)) (f (x (n + 1)))
and r (f a) (f (x (encode a + 1))
.
Equations
- Directed.sequence f hf 0 = default
- Directed.sequence f hf (Nat.succ n) = let p := Directed.sequence f hf n; match Encodable.decode n with | none => Classical.choose (hf p p) | some a => Classical.choose (hf p a)
Instances For
Representative of an equivalence class. This is a computable version of Quot.out
for a setoid
on an encodable type.
Instances For
The quotient of an encodable space by a decidable equivalence relation is encodable.