mathlib3 documentation

logic.encodable.basic

Encodable types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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.

@[class]
structure encodable (α : Type u_1) :
Type u_1

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 of this typeclass
Instances of other typeclasses for encodable
  • encodable.has_sizeof_inst
@[simp]
theorem encodable.encode_inj {α : Type u_1} [encodable α] {a b : α} :
@[protected, instance]
def encodable.countable {α : Type u_1} [encodable α] :

An encodable type has decidable equality. Not set as an instance because this is usually not the best way to infer decidability.

Equations
def encodable.of_left_injection {α : Type u_1} {β : Type u_2} [encodable α] (f : β α) (finv : α option β) (linv : (b : β), finv (f b) = option.some b) :

If α is encodable and there is an injection f : β → α, then β is encodable as well.

Equations
def encodable.of_left_inverse {α : Type u_1} {β : Type u_2} [encodable α] (f : β α) (finv : α β) (linv : (b : β), finv (f b) = b) :

If α is encodable and f : β → α is invertible, then β is encodable as well.

Equations
def encodable.of_equiv {β : Type u_2} (α : Type u_1) [encodable α] (e : β α) :

Encodability is preserved by equivalence.

Equations
@[simp]
theorem encodable.encode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β α) (b : β) :
@[simp]
theorem encodable.decode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β α) (n : ) :
@[protected, instance]
Equations
@[simp]
@[protected, instance]
def is_empty.to_encodable {α : Type u_1} [is_empty α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem encodable.encode_star  :
encodable.encode punit.star = 0
@[protected, instance]
def option.encodable {α : Type u_1} [h : encodable α] :

If α is encodable, then so is option α.

Equations
@[simp]
def encodable.decode₂ (α : Type u_1) [encodable α] (n : ) :

Failsafe variant of decode. decode₂ α n returns the preimage of n under encode if it exists, and returns none if it doesn't. This requirement could be imposed directly on decode but is not to help make the definition easier to use.

Equations
theorem encodable.mem_decode₂' {α : Type u_1} [encodable α] {n : } {a : α} :
theorem encodable.mem_decode₂ {α : Type u_1} [encodable α] {n : } {a : α} :
@[simp]
theorem encodable.decode₂_inj {α : Type u_1} [encodable α] {n : } {a₁ a₂ : α} (h₁ : a₁ encodable.decode₂ α n) (h₂ : a₂ encodable.decode₂ α n) :
a₁ = a₂

The encoding function has decidable range.

Equations

An encodable type is equivalent to the range of its encoding function.

Equations
def unique.encodable {α : Type u_1} [unique α] :

A type with unique element is encodable. This is not an instance to avoid diamonds.

Equations
def encodable.encode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
α β

Explicit encoding function for the sum of two encodable types.

Equations
def encodable.decode_sum {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
option β)

Explicit decoding function for the sum of two encodable types.

Equations
@[protected, instance]
def sum.encodable {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
encodable β)

If α and β are encodable, then so is their sum.

Equations
@[simp]
theorem encodable.encode_inl {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) :
@[simp]
theorem encodable.encode_inr {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (b : β) :
@[simp]
theorem encodable.decode_sum_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
@[protected, instance]
noncomputable def Prop.encodable  :
Equations
def encodable.encode_sigma {α : Type u_1} {γ : α Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :

Explicit encoding function for sigma γ

Equations
def encodable.decode_sigma {α : Type u_1} {γ : α Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ) :

Explicit decoding function for sigma γ

Equations
@[protected, instance]
def sigma.encodable {α : Type u_1} {γ : α Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :
Equations
@[simp]
theorem encodable.decode_sigma_val {α : Type u_1} {γ : α Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ) :
@[simp]
theorem encodable.encode_sigma_val {α : Type u_1} {γ : α Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (a : α) (b : γ a) :
@[protected, instance]
def prod.encodable {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] :
encodable × β)

If α and β are encodable, then so is their product.

Equations
@[simp]
theorem encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ) :
@[simp]
theorem encodable.encode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) (b : β) :
def encodable.encode_subtype {α : Type u_1} {P : α Prop} [encA : encodable α] :
{a // P a}

Explicit encoding function for a decidable subtype of an encodable type

Equations
def encodable.decode_subtype {α : Type u_1} {P : α Prop} [encA : encodable α] [decP : decidable_pred P] (v : ) :
option {a // P a}

Explicit decoding function for a decidable subtype of an encodable type

Equations
@[protected, instance]
def subtype.encodable {α : Type u_1} {P : α Prop} [encA : encodable α] [decP : decidable_pred P] :
encodable {a // P a}

A decidable subtype of an encodable type is encodable.

Equations
theorem encodable.subtype.encode_eq {α : Type u_1} {P : α Prop} [encA : encodable α] [decP : decidable_pred P] (a : subtype P) :
@[protected, instance]
def fin.encodable (n : ) :
Equations
@[protected, instance]
def ulift.encodable {α : Type u_1} [encodable α] :

The lift of an encodable type is encodable.

Equations
@[protected, instance]
def plift.encodable {α : Type u_1} [encodable α] :

The lift of an encodable type is encodable.

Equations
noncomputable def encodable.of_inj {α : Type u_1} {β : Type u_2} [encodable β] (f : α β) (hf : function.injective f) :

If β is encodable and there is an injection f : α → β, then α is encodable as well.

Equations
noncomputable def encodable.of_countable (α : Type u_1) [countable α] :

If α is countable, then it has a (non-canonical) encodable structure.

Equations
@[simp]
@[protected, instance]
@[protected, instance]
def ulower.decidable_eq (α : Type u_1) [encodable α] :
def ulower (α : Type u_1) [encodable α] :

ulower α : Type is an equivalent type in the lowest universe, given encodable α.

Equations
Instances for ulower
@[protected, instance]
def ulower.encodable (α : Type u_1) [encodable α] :
def ulower.equiv (α : Type u_1) [encodable α] :
α ulower α

The equivalence between the encodable type α and ulower α : Type.

Equations
def ulower.down {α : Type u_1} [encodable α] (a : α) :

Lowers an a : α into ulower α.

Equations
@[protected, instance]
def ulower.inhabited {α : Type u_1} [encodable α] [inhabited α] :
Equations
def ulower.up {α : Type u_1} [encodable α] (a : ulower α) :
α

Lifts an a : ulower α into α.

Equations
@[simp]
theorem ulower.down_up {α : Type u_1} [encodable α] {a : ulower α} :
@[simp]
theorem ulower.up_down {α : Type u_1} [encodable α] {a : α} :
@[simp]
theorem ulower.up_eq_up {α : Type u_1} [encodable α] {a b : ulower α} :
a.up = b.up a = b
@[simp]
theorem ulower.down_eq_down {α : Type u_1} [encodable α] {a b : α} :
@[protected, ext]
theorem ulower.ext {α : Type u_1} [encodable α] {a b : ulower α} :
a.up = b.up a = b
def encodable.choose_x {α : Type u_1} {p : α Prop} [encodable α] [decidable_pred p] (h : (x : α), p x) :
{a // p a}

Constructive choice function for a decidable subtype of an encodable type.

Equations
def encodable.choose {α : Type u_1} {p : α Prop} [encodable α] [decidable_pred p] (h : (x : α), p x) :
α

Constructive choice function for a decidable predicate over an encodable type.

Equations
theorem encodable.choose_spec {α : Type u_1} {p : α Prop} [encodable α] [decidable_pred p] (h : (x : α), p x) :
theorem encodable.axiom_of_choice {α : Type u_1} {β : α Type u_2} {R : Π (x : α), β x Prop} [Π (a : α), encodable (β a)] [Π (x : α) (y : β x), decidable (R x y)] (H : (x : α), (y : β x), R x y) :
(f : Π (a : α), β a), (x : α), R x (f x)

A constructive version of classical.axiom_of_choice for encodable types.

theorem encodable.skolem {α : Type u_1} {β : α Type u_2} {P : Π (x : α), β x Prop} [c : Π (a : α), encodable (β a)] [d : Π (x : α) (y : β x), decidable (P x y)] :
( (x : α), (y : β x), P x y) (f : Π (a : α), β a), (x : α), P x (f x)

A constructive version of classical.skolem for encodable types.

def encodable.encode' (α : Type u_1) [encodable α] :
α

The encode function, viewed as an embedding.

Equations
@[protected, instance]
@[protected, instance]
@[protected]
noncomputable def directed.sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β β Prop} (f : α β) (hf : directed r f) :
α

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
theorem directed.sequence_mono_nat {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β β Prop} {f : α β} (hf : directed r f) (n : ) :
r (f (directed.sequence f hf n)) (f (directed.sequence f hf (n + 1)))
theorem directed.rel_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] {r : β β Prop} {f : α β} (hf : directed r f) (a : α) :
r (f a) (f (directed.sequence f hf (encodable.encode a + 1)))
theorem directed.sequence_mono {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α β} (hf : directed has_le.le f) :
theorem directed.le_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α β} (hf : directed has_le.le f) (a : α) :
def quotient.rep {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [encodable α] (q : quotient s) :
α

Representative of an equivalence class. This is a computable version of quot.out for a setoid on an encodable type.

Equations
theorem quotient.rep_spec {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [encodable α] (q : quotient s) :

The quotient of an encodable space by a decidable equivalence relation is encodable.

Equations