logic.encodable.basic - mathlib docs

@[class]

structure encodable (α : Type u_1) :

Type u_1

encode : α → ℕ
decode : ℕ → option α
encodek : ∀ (a : α), encodable.decode α (encodable.encode a) = some a

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

source

theorem encodable.encode_injective {α : Type u_1} [encodable α] :

function.injective encodable.encode

source

@[simp]

theorem encodable.encode_inj {α : Type u_1} [encodable α] {a b : α} :

encodable.encode a = encodable.encode b ↔ a = b

source

theorem encodable.surjective_decode_iget (α : Type u_1) [encodable α] [inhabited α] :

function.surjective (λ (n : ℕ), (encodable.decode α n).iget)

source

def encodable.decidable_eq_of_encodable (α : Type u_1) [encodable α] :

decidable_eq α

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

Equations

encodable.decidable_eq_of_encodable α a b = decidable_of_iff (encodable.encode a = encodable.encode b) encodable.encode_inj

source

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

encodable β

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

Equations

encodable.of_left_injection f finv linv = {encode := λ (b : β), encodable.encode (f b), decode := λ (n : ℕ), (encodable.decode α n).bind finv, encodek := _}

source

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

encodable β

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

Equations

encodable.of_left_inverse f finv linv = encodable.of_left_injection f (some ∘ finv) _

source

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

encodable β

Encodability is preserved by equivalence.

Equations

encodable.of_equiv α e = encodable.of_left_inverse ⇑e ⇑(e.symm) _

source

@[simp]

theorem encodable.encode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β ≃ α) (b : β) :

encodable.encode b = encodable.encode (⇑e b)

source

@[simp]

theorem encodable.decode_of_equiv {α : Type u_1} {β : Type u_2} [encodable α] (e : β ≃ α) (n : ℕ) :

encodable.decode β n = option.map ⇑(e.symm) (encodable.decode α n)

source

@[protected, instance]

def nat.encodable :

encodable ℕ

Equations

nat.encodable = {encode := id ℕ, decode := some ℕ, encodek := nat.encodable._proof_1}

source

@[simp]

theorem encodable.encode_nat (n : ℕ) :

encodable.encode n = n

source

@[simp]

theorem encodable.decode_nat (n : ℕ) :

encodable.decode ℕ n = some n

source

@[protected, instance]

def is_empty.to_encodable {α : Type u_1} [is_empty α] :

encodable α

Equations

is_empty.to_encodable = {encode := is_empty_elim (λ (a : α), ℕ), decode := λ (n : ℕ), none, encodek := _}

source

@[protected, instance]

def punit.encodable :

encodable punit

Equations

punit.encodable = {encode := λ (_x : punit), 0, decode := λ (n : ℕ), n.cases_on (some punit.star) (λ (_x : ℕ), none), encodek := punit.encodable._proof_1}

source

@[simp]

theorem encodable.encode_star :

encodable.encode punit.star = 0

source

@[simp]

theorem encodable.decode_unit_zero :

encodable.decode punit 0 = some punit.star

source

@[simp]

theorem encodable.decode_unit_succ (n : ℕ) :

encodable.decode punit n.succ = none

source

@[protected, instance]

def option.encodable {α : Type u_1} [h : encodable α] :

encodable (option α)

If α is encodable, then so is option α.

Equations

option.encodable = {encode := λ (o : option α), o.cases_on 0 (λ (a : α), (encodable.encode a).succ), decode := λ (n : ℕ), n.cases_on (some none) (λ (m : ℕ), option.map some (encodable.decode α m)), encodek := _}

source

@[simp]

theorem encodable.encode_none {α : Type u_1} [encodable α] :

encodable.encode none = 0

source

@[simp]

theorem encodable.encode_some {α : Type u_1} [encodable α] (a : α) :

encodable.encode (some a) = (encodable.encode a).succ

source

@[simp]

theorem encodable.decode_option_zero {α : Type u_1} [encodable α] :

encodable.decode (option α) 0 = some none

source

@[simp]

theorem encodable.decode_option_succ {α : Type u_1} [encodable α] (n : ℕ) :

encodable.decode (option α) n.succ = option.map some (encodable.decode α n)

source

def encodable.decode₂ (α : Type u_1) [encodable α] (n : ℕ) :

option α

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

encodable.decode₂ α n = (encodable.decode α n).bind (option.guard (λ (a : α), encodable.encode a = n))

source

theorem encodable.mem_decode₂' {α : Type u_1} [encodable α] {n : ℕ} {a : α} :

a ∈ encodable.decode₂ α n ↔ a ∈ encodable.decode α n ∧ encodable.encode a = n

source

theorem encodable.mem_decode₂ {α : Type u_1} [encodable α] {n : ℕ} {a : α} :

a ∈ encodable.decode₂ α n ↔ encodable.encode a = n

source

theorem encodable.decode₂_eq_some {α : Type u_1} [encodable α] {n : ℕ} {a : α} :

encodable.decode₂ α n = some a ↔ encodable.encode a = n

source

@[simp]

theorem encodable.decode₂_encode {α : Type u_1} [encodable α] (a : α) :

encodable.decode₂ α (encodable.encode a) = some a

source

theorem encodable.decode₂_ne_none_iff {α : Type u_1} [encodable α] {n : ℕ} :

encodable.decode₂ α n ≠ none ↔ n ∈ set.range encodable.encode

source

theorem encodable.decode₂_is_partial_inv {α : Type u_1} [encodable α] :

function.is_partial_inv encodable.encode (encodable.decode₂ α)

source

theorem encodable.decode₂_inj {α : Type u_1} [encodable α] {n : ℕ} {a₁ a₂ : α} (h₁ : a₁ ∈ encodable.decode₂ α n) (h₂ : a₂ ∈ encodable.decode₂ α n) :

a₁ = a₂

source

theorem encodable.encodek₂ {α : Type u_1} [encodable α] (a : α) :

encodable.decode₂ α (encodable.encode a) = some a

source

def encodable.decidable_range_encode (α : Type u_1) [encodable α] :

decidable_pred (λ (_x : ℕ), _x ∈ set.range encodable.encode)

The encoding function has decidable range.

Equations

encodable.decidable_range_encode α = λ (x : ℕ), decidable_of_iff ↥((encodable.decode₂ α x).is_some) _

source

def encodable.equiv_range_encode (α : Type u_1) [encodable α] :

α ≃ ↥(set.range encodable.encode)

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

Equations

encodable.equiv_range_encode α = {to_fun := λ (a : α), ⟨encodable.encode a, _⟩, inv_fun := λ (n : ↥(set.range encodable.encode)), option.get _, left_inv := _, right_inv := _}

source

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

encodable α

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

Equations

unique.encodable = {encode := λ (_x : α), 0, decode := λ (_x : ℕ), some default, encodek := _}

source

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

α ⊕ β → ℕ

Explicit encoding function for the sum of two encodable types.

Equations

encodable.encode_sum (sum.inr b) = bit1 (encodable.encode b)
encodable.encode_sum (sum.inl a) = bit0 (encodable.encode a)

source

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

encodable.decode_sum n = encodable.decode_sum._match_1 n.bodd_div2
encodable.decode_sum._match_1 (tt, m) = option.map sum.inr (encodable.decode β m)
encodable.decode_sum._match_1 (ff, m) = option.map sum.inl (encodable.decode α m)

source

@[protected, instance]

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

encodable (α ⊕ β)

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

Equations

sum.encodable = {encode := encodable.encode_sum _inst_2, decode := encodable.decode_sum _inst_2, encodek := _}

source

@[simp]

theorem encodable.encode_inl {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) :

encodable.encode (sum.inl a) = bit0 (encodable.encode a)

source

@[simp]

theorem encodable.encode_inr {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (b : β) :

encodable.encode (sum.inr b) = bit1 (encodable.encode b)

source

@[simp]

theorem encodable.decode_sum_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ℕ) :

encodable.decode (α ⊕ β) n = encodable.decode_sum n

source

@[protected, instance]

def bool.encodable :

encodable bool

Equations

bool.encodable = encodable.of_equiv (unit ⊕ unit) equiv.bool_equiv_punit_sum_punit

source

@[simp]

theorem encodable.encode_tt :

encodable.encode tt = 1

source

@[simp]

theorem encodable.encode_ff :

encodable.encode ff = 0

source

@[simp]

theorem encodable.decode_zero :

encodable.decode bool 0 = some ff

source

@[simp]

theorem encodable.decode_one :

encodable.decode bool 1 = some tt

source

theorem encodable.decode_ge_two (n : ℕ) (h : 2 ≤ n) :

encodable.decode bool n = none

source

@[protected, instance]

noncomputable def Prop.encodable :

encodable Prop

Equations

Prop.encodable = encodable.of_equiv bool equiv.Prop_equiv_bool

source

def encodable.encode_sigma {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :

sigma γ → ℕ

Explicit encoding function for sigma γ

Equations

encodable.encode_sigma ⟨a, b⟩ = nat.mkpair (encodable.encode a) (encodable.encode b)

source

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

option (sigma γ)

Explicit decoding function for sigma γ

Equations

encodable.decode_sigma n = encodable.decode_sigma._match_1 (nat.unpair n)
encodable.decode_sigma._match_1 (n₁, n₂) = (encodable.decode α n₁).bind (λ (a : α), option.map (sigma.mk a) (encodable.decode (γ a) n₂))

source

@[protected, instance]

def sigma.encodable {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] :

encodable (sigma γ)

Equations

sigma.encodable = {encode := encodable.encode_sigma (λ (a : α), _inst_2 a), decode := encodable.decode_sigma (λ (a : α), _inst_2 a), encodek := _}

source

@[simp]

theorem encodable.decode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (n : ℕ) :

encodable.decode (sigma γ) n = (encodable.decode α (nat.unpair n).fst).bind (λ (a : α), option.map (sigma.mk a) (encodable.decode (γ a) (nat.unpair n).snd))

source

@[simp]

theorem encodable.encode_sigma_val {α : Type u_1} {γ : α → Type u_3} [encodable α] [Π (a : α), encodable (γ a)] (a : α) (b : γ a) :

encodable.encode ⟨a, b⟩ = nat.mkpair (encodable.encode a) (encodable.encode b)

source

@[protected, instance]

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

encodable (α × β)

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

Equations

prod.encodable = encodable.of_equiv (Σ (_x : α), β) (equiv.sigma_equiv_prod α β).symm

source

@[simp]

theorem encodable.decode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (n : ℕ) :

encodable.decode (α × β) n = (encodable.decode α (nat.unpair n).fst).bind (λ (a : α), option.map (prod.mk a) (encodable.decode β (nat.unpair n).snd))

source

@[simp]

theorem encodable.encode_prod_val {α : Type u_1} {β : Type u_2} [encodable α] [encodable β] (a : α) (b : β) :

encodable.encode (a, b) = nat.mkpair (encodable.encode a) (encodable.encode b)

source

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

encodable.encode_subtype ⟨v, h⟩ = encodable.encode v

source

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

encodable.decode_subtype v = (encodable.decode α v).bind (λ (a : α), dite (P a) (λ (h : P a), some ⟨a, h⟩) (λ (h : ¬P a), none))

source

@[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

subtype.encodable = {encode := encodable.encode_subtype encA, decode := encodable.decode_subtype (λ (a : α), decP a), encodek := _}

source

theorem encodable.subtype.encode_eq {α : Type u_1} {P : α → Prop} [encA : encodable α] [decP : decidable_pred P] (a : subtype P) :

encodable.encode a = encodable.encode a.val

source

@[protected, instance]

def fin.encodable (n : ℕ) :

encodable (fin n)

Equations

fin.encodable n = encodable.of_equiv {m // m < n} (equiv.fin_equiv_subtype n)

source

@[protected, instance]

def int.encodable :

encodable ℤ

Equations

int.encodable = encodable.of_equiv ℕ equiv.int_equiv_nat

source

@[protected, instance]

def pnat.encodable :

encodable ℕ+

Equations

pnat.encodable = encodable.of_equiv ℕ equiv.pnat_equiv_nat

source

@[protected, instance]

def ulift.encodable {α : Type u_1} [encodable α] :

encodable (ulift α)

The lift of an encodable type is encodable.

Equations

ulift.encodable = encodable.of_equiv α equiv.ulift

source

@[protected, instance]

def plift.encodable {α : Type u_1} [encodable α] :

encodable (plift α)

The lift of an encodable type is encodable.

Equations

plift.encodable = encodable.of_equiv α equiv.plift

source

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

encodable α

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

Equations

encodable.of_inj f hf = encodable.of_left_injection f (function.partial_inv f) _

source

@[protected, instance]

def ulower.decidable_eq (α : Type u_1) [encodable α] :

decidable_eq (ulower α)

source

def ulower (α : Type u_1) [encodable α] :

Type

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

Equations

ulower α = ↥(set.range encodable.encode)

source

@[protected, instance]

def ulower.encodable (α : Type u_1) [encodable α] :

encodable (ulower α)

source

def ulower.equiv (α : Type u_1) [encodable α] :

α ≃ ulower α

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

Equations

ulower.equiv α = encodable.equiv_range_encode α

source

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

ulower α

Lowers an a : α into ulower α.

Equations

ulower.down a = ⇑(ulower.equiv α) a

source

@[protected, instance]

def ulower.inhabited {α : Type u_1} [encodable α] [inhabited α] :

inhabited (ulower α)

Equations

ulower.inhabited = {default := ulower.down default}

source

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

α

Lifts an a : ulower α into α.

Equations

a.up = ⇑((ulower.equiv α).symm) a

source

@[simp]

theorem ulower.down_up {α : Type u_1} [encodable α] {a : ulower α} :

ulower.down a.up = a

source

@[simp]

theorem ulower.up_down {α : Type u_1} [encodable α] {a : α} :

(ulower.down a).up = a

source

@[simp]

theorem ulower.up_eq_up {α : Type u_1} [encodable α] {a b : ulower α} :

a.up = b.up ↔ a = b

source

@[simp]

theorem ulower.down_eq_down {α : Type u_1} [encodable α] {a b : α} :

ulower.down a = ulower.down b ↔ a = b

source

@[protected, ext]

theorem ulower.ext {α : Type u_1} [encodable α] {a b : ulower α} :

a.up = b.up → a = b

source

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

encodable.choose_x h = have this : ∃ (n : ℕ), good p (encodable.decode α n), from _, encodable.choose_x._match_4 (encodable.decode α (nat.find this)) _
encodable.choose_x._match_4 (some a) h = ⟨a, h⟩
_ = _

source

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

encodable.choose h = (encodable.choose_x h).val

source

theorem encodable.choose_spec {α : Type u_1} {p : α → Prop} [encodable α] [decidable_pred p] (h : ∃ (x : α), p x) :

p (encodable.choose h)

source

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.

source

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.

source

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

α ↪ ℕ

The encode function, viewed as an embedding.

Equations

encodable.encode' α = {to_fun := encodable.encode _inst_1, inj' := _}

source

@[protected, instance]

def encodable.order.preimage.is_trans {α : Type u_1} [encodable α] :

is_trans α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

source

@[protected, instance]

def encodable.order.preimage.is_antisymm {α : Type u_1} [encodable α] :

is_antisymm α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

source

@[protected, instance]

def encodable.order.preimage.is_total {α : Type u_1} [encodable α] :

is_total α (⇑(encodable.encode' α) ⁻¹'o has_le.le)

source

@[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

directed.sequence f hf (n + 1) = let p : α := directed.sequence f hf n in directed.sequence._match_1 f hf p (encodable.decode α n)
directed.sequence f hf 0 = default
directed.sequence._match_1 f hf p (some a) = classical.some _
directed.sequence._match_1 f hf p none = classical.some _

source

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)))

source

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)))

source

theorem directed.sequence_mono {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : directed has_le.le f) :

monotone (f ∘ directed.sequence f hf)

source

theorem directed.le_sequence {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α → β} (hf : directed has_le.le f) (a : α) :

f a ≤ f (directed.sequence f hf (encodable.encode a + 1))

source

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

q.rep = encodable.choose _

source

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

⟦q.rep ⟧ = q

source

def encodable_quotient {α : Type u_1} {s : setoid α} [decidable_rel has_equiv.equiv] [encodable α] :

encodable (quotient s)

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

Equations

encodable_quotient = {encode := λ (q : quotient s), encodable.encode q.rep, decode := λ (n : ℕ), quotient.mk <$> encodable.decode α n, encodek := _}

mathlib documentation

Encodable types #

Main declarations #

Implementation notes #