doc-next-gen

Mathlib.Logic.Encodable.Basic

Module docstring

{"# 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 function encode : α → ℕ with a partial inverse decode : ℕ → Option α.
  • decode₂: Version of decode that is equal to none outside of the range of encode. Useful as we do not require this in the definition of decode.
  • 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. "}

Encodable structure
(α : Type*)
Full source 
/-- 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. -/
class Encodable (α : Type*) where
  /-- Encoding from Type α to ℕ -/
  encode : α → ℕ
  /-- Decoding from ℕ to Option α -/
  decode : ℕ → Option α
  /-- Invariant relationship between encoding and decoding -/
  encodek : ∀ a, decode (encode a) = some a
Encodable Type
Informal description
An encodable (constructively countable) type is a type $\alpha$ equipped with an explicit encoding function $\text{encode} : \alpha \to \mathbb{N}$ and a partial inverse $\text{decode} : \mathbb{N} \to \text{Option } \alpha$, such that $\text{decode}$ is a partial inverse of $\text{encode}$. This structure allows finite types to be encodable, distinguishing it from `Denumerable` which requires infinite types. The encoding provides a decidable range for $\text{encode}$ even when the finiteness of $\alpha$ is unknown.
Encodable.encode_injective theorem
[Encodable α] : Function.Injective (@encode α _)
Full source 
theorem encode_injective [Encodable α] : Function.Injective (@encode α _)
  | x, y, e => Option.some.inj <| by rw [← encodek, e, encodek]
Injectivity of the Encoding Function for Encodable Types
Informal description
For any encodable type $\alpha$, the encoding function $\text{encode} : \alpha \to \mathbb{N}$ is injective. That is, for any $a, b \in \alpha$, if $\text{encode}(a) = \text{encode}(b)$, then $a = b$.
Encodable.encode_inj theorem
[Encodable α] {a b : α} : encode a = encode b ↔ a = b
Full source 
@[simp]
theorem encode_inj [Encodable α] {a b : α} : encodeencode a = encode b ↔ a = b :=
  encode_injective.eq_iff
Encoding Function is Injective for Encodable Types
Informal description
For any encodable type $\alpha$ and elements $a, b \in \alpha$, the encoding function $\text{encode}$ satisfies $\text{encode}(a) = \text{encode}(b)$ if and only if $a = b$.
Encodable.countable instance
[Encodable α] : Countable α
Full source 
instance (priority := 400) countable [Encodable α] : Countable α where
  exists_injective_nat' := ⟨_,encode_injective⟩
Encodable Types are Countable
Informal description
Every encodable type $\alpha$ is countable.
Encodable.surjective_decode_iget theorem
(α : Type*) [Encodable α] [Inhabited α] : Surjective fun n => ((Encodable.decode n).iget : α)
Full source 
theorem surjective_decode_iget (α : Type*) [Encodable α] [Inhabited α] :
    Surjective fun n => ((Encodable.decode n).iget : α) := fun x =>
  ⟨Encodable.encode x, by simp_rw [Encodable.encodek]⟩
Surjectivity of Decoding with Default Extraction for Encodable Types
Informal description
For any encodable and inhabited type $\alpha$, the function $n \mapsto \text{decode}(n).\text{iget}$ (where $\text{decode} : \mathbb{N} \to \text{Option } \alpha$ is the decoding function and $\text{iget}$ extracts a default value from $\text{Option } \alpha$) is surjective. That is, for every $a \in \alpha$, there exists an $n \in \mathbb{N}$ such that $\text{decode}(n).\text{iget} = a$.
Encodable.decidableEqOfEncodable definition
(α) [Encodable α] : DecidableEq α
Full source 
/-- An encodable type has decidable equality. Not set as an instance because this is usually not the
best way to infer decidability. -/
def decidableEqOfEncodable (α) [Encodable α] : DecidableEq α
  | _, _ => decidable_of_iff _ encode_inj
Decidable equality for encodable types
Informal description
For any encodable type $\alpha$, the equality relation on $\alpha$ is decidable. That is, there exists an algorithm that, given any two elements $a, b \in \alpha$, can determine whether $a = b$ holds or not.
Encodable.ofLeftInjection definition
[Encodable α] (f : β → α) (finv : α → Option β) (linv : ∀ b, finv (f b) = some b) : Encodable β
Full source 
/-- If `α` is encodable and there is an injection `f : β → α`, then `β` is encodable as well. -/
def ofLeftInjection [Encodable α] (f : β → α) (finv : α → Option β)
    (linv : ∀ b, finv (f b) = some b) : Encodable β :=
  ⟨fun b => encode (f b), fun n => (decode n).bind finv, fun b => by
    simp [Encodable.encodek, linv]⟩
Encodability via Injection
Informal description
Given an encodable type $\alpha$, an injection $f : \beta \to \alpha$, and a partial left inverse $\text{finv} : \alpha \to \text{Option } \beta$ satisfying $\text{finv}(f(b)) = \text{some } b$ for all $b \in \beta$, then $\beta$ is also encodable. The encoding function for $\beta$ is defined as $\text{encode}(b) = \text{encode}(f(b))$, and the decoding function is $\text{decode}(n) = \text{decode}(n) \mathbin{\text{bind}} \text{finv}$.
Encodable.ofLeftInverse definition
[Encodable α] (f : β → α) (finv : α → β) (linv : ∀ b, finv (f b) = b) : Encodable β
Full source 
/-- If `α` is encodable and `f : β → α` is invertible, then `β` is encodable as well. -/
def ofLeftInverse [Encodable α] (f : β → α) (finv : α → β) (linv : ∀ b, finv (f b) = b) :
    Encodable β :=
  ofLeftInjection f (somesome ∘ finv) fun b => congr_arg some (linv b)
Encodability via Left Inverse
Informal description
Given an encodable type $\alpha$, a function $f : \beta \to \alpha$, and a left inverse $\text{finv} : \alpha \to \beta$ satisfying $\text{finv}(f(b)) = b$ for all $b \in \beta$, then $\beta$ is also encodable. The encoding function for $\beta$ is defined as $\text{encode}(b) = \text{encode}(f(b))$, and the decoding function is $\text{decode}(n) = \text{finv} <$> \text{decode}(n)$ (where `<$>` is the `Option.map` operation).
Encodable.ofEquiv definition
(α) [Encodable α] (e : β ≃ α) : Encodable β
Full source 
/-- Encodability is preserved by equivalence. -/
def ofEquiv (α) [Encodable α] (e : β ≃ α) : Encodable β :=
  ofLeftInverse e e.symm e.left_inv
Encodability via Equivalence
Informal description
Given an encodable type $\alpha$ and an equivalence $e : \beta \simeq \alpha$, the type $\beta$ is also encodable. The encoding function for $\beta$ is defined as $\text{encode}(b) = \text{encode}(e(b))$, and the decoding function is $\text{decode}(n) = \text{decode}(n) \mathbin{\text{map}} e^{-1}$ (where $\text{map}$ is the `Option.map` operation and $e^{-1}$ is the inverse of $e$).
Encodable.encode_ofEquiv theorem
{α β} [Encodable α] (e : β ≃ α) (b : β) : @encode _ (ofEquiv _ e) b = encode (e b)
Full source 
theorem encode_ofEquiv {α β} [Encodable α] (e : β ≃ α) (b : β) :
    @encode _ (ofEquiv _ e) b = encode (e b) :=
  rfl
Encoding Preservation under Equivalence
Informal description
Let $\alpha$ and $\beta$ be types with $\alpha$ encodable, and let $e : \beta \simeq \alpha$ be an equivalence. For any $b \in \beta$, the encoding of $b$ under the encodable structure induced by $e$ is equal to the encoding of $e(b)$ under the original encodable structure on $\alpha$. That is, $\text{encode}(b) = \text{encode}(e(b))$.
Encodable.decode_ofEquiv theorem
{α β} [Encodable α] (e : β ≃ α) (n : ℕ) : @decode _ (ofEquiv _ e) n = (decode n).map e.symm
Full source 
theorem decode_ofEquiv {α β} [Encodable α] (e : β ≃ α) (n : ℕ) :
    @decode _ (ofEquiv _ e) n = (decode n).map e.symm :=
  show Option.bind _ _ = Option.map _ _
  by rw [Option.map_eq_bind]
Decoding via Equivalence for Encodable Types
Informal description
For any encodable type $\alpha$ and an equivalence $e : \beta \simeq \alpha$, the decoding function for $\beta$ satisfies $\text{decode}(n) = \text{decode}(n) \mathbin{\text{map}} e^{-1}$ for any natural number $n$, where $e^{-1}$ is the inverse of $e$ and $\text{map}$ is the `Option.map` operation.
Nat.encodable instance
: Encodable ℕ
Full source 
instance _root_.Nat.encodable : Encodable ℕ :=
  ⟨id, some, fun _ => rfl⟩
Encodable Structure on Natural Numbers
Informal description
The natural numbers $\mathbb{N}$ form an encodable type, where the encoding function $\text{encode} : \mathbb{N} \to \mathbb{N}$ is the identity function and the decoding function $\text{decode} : \mathbb{N} \to \text{Option } \mathbb{N}$ maps each natural number to itself.
Encodable.encode_nat theorem
(n : ℕ) : encode n = n
Full source 
@[simp]
theorem encode_nat (n : ℕ) : encode n = n :=
  rfl
Identity Encoding for Natural Numbers
Informal description
For any natural number $n$, the encoding function $\text{encode}$ satisfies $\text{encode}(n) = n$.
Encodable.decode_nat theorem
(n : ℕ) : decode n = some n
Full source 
@[simp 1100]
theorem decode_nat (n : ℕ) : decode n = some n :=
  rfl
Identity Decoding for Natural Numbers
Informal description
For any natural number $n$, the decoding function $\text{decode}$ satisfies $\text{decode}(n) = \text{some } n$.
Encodable.encode_star theorem
: encode PUnit.unit = 0
Full source 
@[simp]
theorem encode_star : encode PUnit.unit = 0 :=
  rfl
Encoding of Unit Element Yields Zero
Informal description
The encoding function applied to the single element `PUnit.unit` of the unit type returns the natural number `0`, i.e., $\text{encode}(\text{PUnit.unit}) = 0$.
Encodable.decode_unit_zero theorem
: decode 0 = some PUnit.unit
Full source 
@[simp]
theorem decode_unit_zero : decode 0 = some PUnit.unit :=
  rfl
Decoding Zero Yields Unit Element
Informal description
The decoding function applied to the natural number $0$ returns the unit element of the unit type, i.e., $\text{decode}(0) = \text{some}(\text{PUnit.unit})$.
Encodable.decode_unit_succ theorem
(n) : decode (succ n) = (none : Option PUnit)
Full source 
@[simp]
theorem decode_unit_succ (n) : decode (succ n) = (none : Option PUnit) :=
  rfl
Decoding Successor Yields None for Unit Type
Informal description
For any natural number $n$, the decoding function applied to the successor of $n$ returns `none` when decoding into the unit type, i.e., $\text{decode}(n+1) = \text{none}$.
Option.encodable instance
{α : Type*} [h : Encodable α] : Encodable (Option α)
Full source 
/-- If `α` is encodable, then so is `Option α`. -/
instance _root_.Option.encodable {α : Type*} [h : Encodable α] : Encodable (Option α) :=
  ⟨fun o => Option.casesOn o Nat.zero fun a => succ (encode a), fun n =>
    Nat.casesOn n (some none) fun m => (decode m).map some, fun o => by
    cases o <;> dsimp; simp [encodek, Nat.succ_ne_zero]⟩
Encodability of Option Types
Informal description
For any encodable type $\alpha$, the type $\text{Option } \alpha$ is also encodable. The encoding function maps $\text{none}$ to $0$ and $\text{some } a$ to $\text{encode}(a) + 1$.
Encodable.encode_none theorem
[Encodable α] : encode (@none α) = 0
Full source 
@[simp]
theorem encode_none [Encodable α] : encode (@none α) = 0 :=
  rfl
Encoding of None is Zero
Informal description
For any encodable type $\alpha$, the encoding function maps the `none` value of type $\text{Option } \alpha$ to $0$, i.e., $\text{encode}(\text{none}) = 0$.
Encodable.encode_some theorem
[Encodable α] (a : α) : encode (some a) = succ (encode a)
Full source 
@[simp]
theorem encode_some [Encodable α] (a : α) : encode (some a) = succ (encode a) :=
  rfl
Encoding of Some Element in Option Type
Informal description
For any encodable type $\alpha$ and element $a \in \alpha$, the encoding of $\text{some } a$ in $\text{Option } \alpha$ is equal to the successor of the encoding of $a$, i.e., $\text{encode}(\text{some } a) = \text{encode}(a) + 1$.
Encodable.decode_option_zero theorem
[Encodable α] : (decode 0 : Option (Option α)) = some none
Full source 
@[simp]
theorem decode_option_zero [Encodable α] : (decode 0 : Option (Option α))= some none :=
  rfl
Decoding Zero for Option Types Yields None
Informal description
For any encodable type $\alpha$, the decoding function applied to $0$ for the type $\text{Option } \alpha$ returns $\text{some none}$.
Encodable.decode_option_succ theorem
[Encodable α] (n) : (decode (succ n) : Option (Option α)) = (decode n).map some
Full source 
@[simp]
theorem decode_option_succ [Encodable α] (n) :
    (decode (succ n) : Option (Option α)) = (decode n).map some :=
  rfl
Successor Decoding for Option Types
Informal description
For any encodable type $\alpha$ and natural number $n$, the decoding function applied to $n+1$ for the type $\text{Option } \alpha$ equals the result of applying the `some` constructor to the decoded value of $n$ (if it exists). That is, $\text{decode}_{\text{Option } \alpha}(n+1) = \text{some} \circ \text{decode}_\alpha(n)$.
Encodable.decode₂ definition
(α) [Encodable α] (n : ℕ) : Option α
Full source 
/-- 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. -/
def decode₂ (α) [Encodable α] (n : ℕ) : Option α :=
  (decode n).bind (Option.guard fun a => encode a = n)
Failsafe decoding function for encodable types
Informal description
The function `decode₂` is a failsafe variant of `decode` for an encodable type $\alpha$. Given a natural number $n$, it returns the preimage of $n$ under the encoding function $\text{encode}$ if it exists (i.e., returns $\text{some } a$ where $\text{encode } a = n$), and returns $\text{none}$ otherwise. This ensures that $\text{decode₂}$ is always $\text{none}$ outside the range of $\text{encode}$, a property not necessarily enforced by $\text{decode}$ itself.
Encodable.mem_decode₂' theorem
[Encodable α] {n : ℕ} {a : α} : a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n
Full source 
theorem mem_decode₂' [Encodable α] {n : ℕ} {a : α} :
    a ∈ decode₂ α na ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n := by
  simp [decode₂, Option.bind_eq_some_iff]
Characterization of Failsafe Decoding via Standard Decoding and Encoding
Informal description
For an encodable type $\alpha$, a natural number $n$, and an element $a \in \alpha$, the element $a$ is in the result of the failsafe decoding function $\text{decode₂}$ applied to $n$ if and only if $a$ is in the result of the standard decoding function $\text{decode}$ applied to $n$ and the encoding of $a$ equals $n$. That is, $a \in \text{decode₂}_\alpha(n) \leftrightarrow (a \in \text{decode}(n) \land \text{encode}(a) = n)$.
Encodable.mem_decode₂ theorem
[Encodable α] {n : ℕ} {a : α} : a ∈ decode₂ α n ↔ encode a = n
Full source 
theorem mem_decode₂ [Encodable α] {n : ℕ} {a : α} : a ∈ decode₂ α na ∈ decode₂ α n ↔ encode a = n :=
  mem_decode₂'.trans (and_iff_right_of_imp fun e => e ▸ encodek _)
Characterization of Failsafe Decoding via Encoding
Informal description
For an encodable type $\alpha$, a natural number $n$, and an element $a \in \alpha$, the element $a$ is in the result of the failsafe decoding function $\text{decode₂}_\alpha(n)$ if and only if the encoding of $a$ equals $n$, i.e., $a \in \text{decode₂}_\alpha(n) \leftrightarrow \text{encode}(a) = n$.
Encodable.decode₂_eq_some theorem
[Encodable α] {n : ℕ} {a : α} : decode₂ α n = some a ↔ encode a = n
Full source 
theorem decode₂_eq_some [Encodable α] {n : ℕ} {a : α} : decode₂decode₂ α n = some a ↔ encode a = n :=
  mem_decode₂
Failsafe Decoding Yields Some Element iff Encoding Matches
Informal description
For any encodable type $\alpha$, natural number $n$, and element $a \in \alpha$, the failsafe decoding function $\text{decode}_\alpha(n)$ returns $\text{some } a$ if and only if the encoding of $a$ equals $n$, i.e., $\text{encode}(a) = n$.
Encodable.decode₂_encode theorem
[Encodable α] (a : α) : decode₂ α (encode a) = some a
Full source 
@[simp]
theorem decode₂_encode [Encodable α] (a : α) : decode₂ α (encode a) = some a := by
  ext
  simp [mem_decode₂, eq_comm, decode₂_eq_some]
Failsafe Decoding of Encoded Element Returns Original Element
Informal description
For any encodable type $\alpha$ and any element $a \in \alpha$, the failsafe decoding function $\text{decode}_\alpha$ applied to the encoding $\text{encode}(a)$ returns $\text{some } a$.
Encodable.decode₂_ne_none_iff theorem
[Encodable α] {n : ℕ} : decode₂ α n ≠ none ↔ n ∈ Set.range (encode : α → ℕ)
Full source 
theorem decode₂_ne_none_iff [Encodable α] {n : ℕ} :
    decode₂decode₂ α n ≠ nonedecode₂ α n ≠ none ↔ n ∈ Set.range (encode : α → ℕ) := by
  simp_rw [Set.range, Set.mem_setOf_eq, Ne, Option.eq_none_iff_forall_not_mem,
    Encodable.mem_decode₂, not_forall, not_not]
Failsafe Decoding Non-None iff in Encoding Range
Informal description
For any encodable type $\alpha$ and natural number $n$, the failsafe decoding function $\text{decode}_\alpha(n)$ returns a non-none value if and only if $n$ is in the range of the encoding function $\text{encode} : \alpha \to \mathbb{N}$.
Encodable.decode₂_is_partial_inv theorem
[Encodable α] : IsPartialInv encode (decode₂ α)
Full source 
theorem decode₂_is_partial_inv [Encodable α] : IsPartialInv encode (decode₂ α) := fun _ _ =>
  mem_decode₂
Partial Inverse Property of Failsafe Decoding Function
Informal description
For any encodable type $\alpha$, the function $\text{decode}_\alpha$ is a partial inverse of the encoding function $\text{encode} : \alpha \to \mathbb{N}$. This means that for any $a \in \alpha$, $\text{decode}_\alpha(\text{encode}(a)) = \text{some } a$, and for any $n \in \mathbb{N}$ in the range of $\text{encode}$, $\text{encode}(\text{decode}_\alpha(n)) = n$.
Encodable.decode₂_inj theorem
[Encodable α] {n : ℕ} {a₁ a₂ : α} (h₁ : a₁ ∈ decode₂ α n) (h₂ : a₂ ∈ decode₂ α n) : a₁ = a₂
Full source 
theorem decode₂_inj [Encodable α] {n : ℕ} {a₁ a₂ : α} (h₁ : a₁ ∈ decode₂ α n)
    (h₂ : a₂ ∈ decode₂ α n) : a₁ = a₂ :=
  encode_injective <| (mem_decode₂.1 h₁).trans (mem_decode₂.1 h₂).symm
Injectivity of Failsafe Decoding for Encodable Types
Informal description
For any encodable type $\alpha$ and natural number $n$, if two elements $a_1, a_2 \in \alpha$ are both decoded from $n$ via the failsafe decoding function $\text{decode}_\alpha(n)$, then $a_1 = a_2$. In other words, $\text{decode}_\alpha(n)$ contains at most one element of $\alpha$.
Encodable.encodek₂ theorem
[Encodable α] (a : α) : decode₂ α (encode a) = some a
Full source 
theorem encodek₂ [Encodable α] (a : α) : decode₂ α (encode a) = some a :=
  mem_decode₂.2 rfl
Failsafe Decoding Recovers Original Element: $\text{decode₂}_\alpha(\text{encode}(a)) = \text{some } a$
Informal description
For any encodable type $\alpha$ and any element $a \in \alpha$, the failsafe decoding function $\text{decode₂}_\alpha$ applied to the encoding $\text{encode}(a)$ returns $\text{some } a$. In other words, $\text{decode₂}_\alpha(\text{encode}(a)) = \text{some } a$.
Encodable.decidableRangeEncode definition
(α : Type*) [Encodable α] : DecidablePred (· ∈ Set.range (@encode α _))
Full source 
/-- The encoding function has decidable range. -/
def decidableRangeEncode (α : Type*) [Encodable α] : DecidablePred (· ∈ Set.range (@encode α _)) :=
  fun x =>
  decidable_of_iff (Option.isSome (decode₂ α x))
    ⟨fun h => ⟨Option.get _ h, by rw [← decode₂_is_partial_inv (Option.get _ h), Option.some_get]⟩,
      fun ⟨n, hn⟩ => by rw [← hn, encodek₂]; exact rfl⟩
Decidability of the range of an encoding function
Informal description
For any encodable type $\alpha$, the predicate determining whether a natural number is in the range of the encoding function $\text{encode} : \alpha \to \mathbb{N}$ is decidable. Specifically, given $x \in \mathbb{N}$, one can decide whether there exists an element $a \in \alpha$ such that $\text{encode } a = x$.
Encodable.equivRangeEncode definition
(α : Type*) [Encodable α] : α ≃ Set.range (@encode α _)
Full source 
/-- An encodable type is equivalent to the range of its encoding function. -/
def equivRangeEncode (α : Type*) [Encodable α] : α ≃ Set.range (@encode α _) where
  toFun := fun a : α => ⟨encode a, Set.mem_range_self _⟩
  invFun n :=
    Option.get _
      (show isSome (decode₂ α n.1) by obtain ⟨x, hx⟩ := n.2; rw [← hx, encodek₂]; exact rfl)
  left_inv a := by dsimp; rw [← Option.some_inj, Option.some_get, encodek₂]
  right_inv := fun ⟨n, x, hx⟩ => by
    apply Subtype.eq
    dsimp
    conv =>
      rhs
      rw [← hx]
    rw [encode_injective.eq_iff, ← Option.some_inj, Option.some_get, ← hx, encodek₂]
Equivalence between an encodable type and its encoded range
Informal description
For any encodable type $\alpha$, there exists an equivalence between $\alpha$ and the range of its encoding function $\text{encode} : \alpha \to \mathbb{N}$. Specifically: - The forward map sends an element $a \in \alpha$ to $\langle \text{encode}(a), \text{mem\_range\_self } a \rangle$. - The inverse map takes a pair $\langle n, h_n \rangle$ where $h_n$ proves $n \in \text{range encode}$, and returns the unique $a \in \alpha$ such that $\text{encode}(a) = n$ (using $\text{decode}_2$ to guarantee existence and uniqueness). This equivalence satisfies: 1. Applying the inverse to the forward map of any $a \in \alpha$ returns $a$. 2. Applying the forward map to any $\langle n, h_n \rangle$ in the range of $\text{encode}$ reconstructs the original pair.
Unique.encodable definition
[Unique α] : Encodable α
Full source 
/-- A type with unique element is encodable. This is not an instance to avoid diamonds. -/
def _root_.Unique.encodable [Unique α] : Encodable α :=
  ⟨fun _ => 0, fun _ => some default, Unique.forall_iff.2 rfl⟩
Encodable structure for unique types
Informal description
For any type $\alpha$ with a unique element, there exists an encoding function that maps the unique element to $0$ and a decoding function that maps any natural number to the unique element (wrapped in `some`). The encoding and decoding functions satisfy the property that decoding the encoded unique element returns the original element.
Encodable.encodeSum definition
: α ⊕ β → ℕ
Full source 
/-- Explicit encoding function for the sum of two encodable types. -/
def encodeSum : α ⊕ β → ℕ
  | Sum.inl a => 2 * encode a
  | Sum.inr b => 2 * encode b + 1
Encoding function for sum type
Informal description
The encoding function for the sum type $\alpha \oplus \beta$ maps: - $\text{Sum.inl } a$ to $2 \cdot \text{encode}(a)$ - $\text{Sum.inr } b$ to $2 \cdot \text{encode}(b) + 1$ where $\text{encode}$ is the encoding function for the respective types $\alpha$ and $\beta$.
Encodable.decodeSum definition
(n : ℕ) : Option (α ⊕ β)
Full source 
/-- Explicit decoding function for the sum of two encodable types. -/
def decodeSum (n : ℕ) : Option (α ⊕ β) :=
  match boddDiv2 n with
  | (false, m) => (decode m : Option α).map Sum.inl
  | (_, m) => (decode m : Option β).map Sum.inr
Decoding function for sum of encodable types
Informal description
The decoding function for the sum type $\alpha \oplus \beta$ takes a natural number $n$ and returns an element of $\alpha \oplus \beta$ wrapped in `Option`. It first checks the parity of $n$ using `boddDiv2`: - If $n$ is even (i.e., the first component of `boddDiv2 n` is `false`), it decodes the remaining part $m$ as an element of $\alpha$ and wraps it in `Sum.inl`. - Otherwise, it decodes the remaining part $m$ as an element of $\beta$ and wraps it in `Sum.inr`.
Sum.encodable instance
: Encodable (α ⊕ β)
Full source 
/-- If `α` and `β` are encodable, then so is their sum. -/
instance _root_.Sum.encodable : Encodable (α ⊕ β) :=
  ⟨encodeSum, decodeSum, fun s => by cases s <;> simp [encodeSum, div2_val, decodeSum, encodek]⟩
Encodability of Sum Types
Informal description
For any two encodable types $\alpha$ and $\beta$, their sum type $\alpha \oplus \beta$ is also encodable. The encoding function maps $\text{Sum.inl } a$ to $2 \cdot \text{encode}(a)$ and $\text{Sum.inr } b$ to $2 \cdot \text{encode}(b) + 1$, where $\text{encode}$ is the encoding function for $\alpha$ and $\beta$ respectively. The decoding function checks the parity of the input natural number $n$ and decodes it accordingly as either an element of $\alpha$ or $\beta$.
Encodable.encode_inl theorem
(a : α) : @encode (α ⊕ β) _ (Sum.inl a) = 2 * (encode a)
Full source 
@[simp]
theorem encode_inl (a : α) : @encode (α ⊕ β) _ (Sum.inl a) = 2 * (encode a) :=
  rfl
Encoding of Left Injection in Sum Type: $\text{encode}(\text{inl } a) = 2 \cdot \text{encode}(a)$
Informal description
For any encodable type $\alpha$ and element $a \in \alpha$, the encoding of the left injection $\text{Sum.inl } a$ in the sum type $\alpha \oplus \beta$ is given by $2 \cdot \text{encode}(a)$, where $\text{encode}$ is the encoding function for $\alpha$.
Encodable.encode_inr theorem
(b : β) : @encode (α ⊕ β) _ (Sum.inr b) = 2 * (encode b) + 1
Full source 
@[simp]
theorem encode_inr (b : β) : @encode (α ⊕ β) _ (Sum.inr b) = 2 * (encode b) + 1 :=
  rfl
Encoding of Right Injection in Sum Type: $\text{encode}(\text{inr } b) = 2 \cdot \text{encode}(b) + 1$
Informal description
For any encodable type $\beta$ and element $b \in \beta$, the encoding of the right injection $\text{Sum.inr } b$ in the sum type $\alpha \oplus \beta$ is given by $2 \cdot \text{encode}(b) + 1$, where $\text{encode}$ is the encoding function for $\beta$.
Encodable.decode_sum_val theorem
(n : ℕ) : (decode n : Option (α ⊕ β)) = decodeSum n
Full source 
@[simp]
theorem decode_sum_val (n : ℕ) : (decode n : Option (α ⊕ β)) = decodeSum n :=
  rfl
Decoding Consistency for Sum Types
Informal description
For any natural number $n$, the decoding function for the sum type $\alpha \oplus \beta$ satisfies $\text{decode}(n) = \text{decodeSum}(n)$, where $\text{decodeSum}$ is the specific decoding function defined for sum types.
Encodable.encode_true theorem
: encode true = 1
Full source 
@[simp]
theorem encode_true : encode true = 1 :=
  rfl
Encoding of True: $\text{encode}(\text{true}) = 1$
Informal description
The encoding function for the boolean type maps `true` to the natural number $1$, i.e., $\text{encode}(\text{true}) = 1$.
Encodable.encode_false theorem
: encode false = 0
Full source 
@[simp]
theorem encode_false : encode false = 0 :=
  rfl
Encoding of False as Zero
Informal description
The encoding function applied to the boolean value `false` yields the natural number `0`, i.e., $\text{encode}(\text{false}) = 0$.
Encodable.decode_zero theorem
: (decode 0 : Option Bool) = some false
Full source 
@[simp]
theorem decode_zero : (decode 0 : Option Bool) = some false :=
  rfl
Decoding Zero Yields False in Boolean Encodable Type
Informal description
The decoding function for the encodable type `Bool` maps the natural number `0` to `some false`, i.e., $\text{decode}(0) = \text{some}(\text{false})$.
Encodable.decode_one theorem
: (decode 1 : Option Bool) = some true
Full source 
@[simp]
theorem decode_one : (decode 1 : Option Bool) = some true :=
  rfl
Decoding of One in Boolean Type Yields True
Informal description
The decoding function for the encodable type `Bool` maps the natural number `1` to `some true`, i.e., $\text{decode}(1) = \text{some}(\text{true})$.
Encodable.decode_ge_two theorem
(n) (h : 2 ≤ n) : (decode n : Option Bool) = none
Full source 
theorem decode_ge_two (n) (h : 2 ≤ n) : (decode n : Option Bool) = none := by
  suffices decodeSum n = none by
    change (decodeSum n).bind _ = none
    rw [this]
    rfl
  have : 1 ≤ n / 2 := by
    rw [Nat.le_div_iff_mul_le]
    exacts [h, by decide]
  obtain ⟨m, e⟩ := exists_eq_succ_of_ne_zero (_root_.ne_of_gt this)
  simp only [decodeSum, boddDiv2_eq, div2_val]; cases bodd n <;> simp [e]
Decoding of Large Natural Numbers for Boolean Type Yields None
Informal description
For any natural number $n \geq 2$, the decoding function for the boolean type `Bool` returns `none`, i.e., $\text{decode}(n) = \text{none}$.
Prop.encodable instance
: Encodable Prop
Full source 
noncomputable instance _root_.Prop.encodable : Encodable Prop :=
  ofEquiv Bool Equiv.propEquivBool
Encodability of Propositions
Informal description
The type of propositions `Prop` is encodable, meaning there exists an explicit encoding function `encode : Prop → ℕ` with a partial inverse `decode : ℕ → Option Prop`.
Encodable.encodeSigma definition
: Sigma γ → ℕ
Full source 
/-- Explicit encoding function for `Sigma γ` -/
def encodeSigma : Sigma γ → ℕ
  | ⟨a, b⟩ => pair (encode a) (encode b)
Encoding function for dependent pairs
Informal description
The encoding function for a dependent pair type $\Sigma \gamma$ maps a pair $\langle a, b \rangle$ to a natural number by pairing the encodings of $a$ and $b$ using a pairing function on natural numbers.
Encodable.decodeSigma definition
(n : ℕ) : Option (Sigma γ)
Full source 
/-- Explicit decoding function for `Sigma γ` -/
def decodeSigma (n : ℕ) : Option (Sigma γ) :=
  let (n₁, n₂) := unpair n
  (decode n₁).bind fun a => (decode n₂).map <| Sigma.mk a
Decoding function for dependent pairs
Informal description
The decoding function for a dependent pair type $\Sigma \gamma$ takes a natural number $n$, unpairs it into two natural numbers $n_1$ and $n_2$, then attempts to decode $n_1$ into an element $a$ of the first component type. If successful, it attempts to decode $n_2$ into an element of the second component type (which may depend on $a$), and if both decodings succeed, it returns the pair $\langle a, b \rangle$ wrapped in `Some`; otherwise, it returns `None`.
Sigma.encodable instance
: Encodable (Sigma γ)
Full source 
instance _root_.Sigma.encodable : Encodable (Sigma γ) :=
  ⟨encodeSigma, decodeSigma, fun ⟨a, b⟩ => by
    simp [encodeSigma, decodeSigma, unpair_pair, encodek]⟩
Encodability of Dependent Pair Types
Informal description
For any family of encodable types $\gamma$, the dependent pair type $\Sigma \gamma$ is also encodable. This means there exists an encoding function $\text{encode} : \Sigma \gamma \to \mathbb{N}$ and a decoding function $\text{decode} : \mathbb{N} \to \text{Option } (\Sigma \gamma)$ that are partial inverses of each other.
Encodable.decode_sigma_val theorem
(n : ℕ) : (decode n : Option (Sigma γ)) = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Sigma.mk a
Full source 
@[simp]
theorem decode_sigma_val (n : ℕ) :
    (decode n : Option (Sigma γ)) =
      (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Sigma.mk a :=
  rfl
Decoding Property for Dependent Pairs
Informal description
For any natural number $n$, the decoding function for the dependent pair type $\Sigma \gamma$ satisfies $\text{decode}(n) = \text{decode}(n_1) \text{.bind } \lambda a, \text{decode}(n_2) \text{.map } \langle a, \cdot \rangle$, where $(n_1, n_2) = \text{unpair}(n)$.
Encodable.encode_sigma_val theorem
(a b) : @encode (Sigma γ) _ ⟨a, b⟩ = pair (encode a) (encode b)
Full source 
@[simp]
theorem encode_sigma_val (a b) : @encode (Sigma γ) _ ⟨a, b⟩ = pair (encode a) (encode b) :=
  rfl
Encoding of Dependent Pairs via Pairing Function
Informal description
For any elements $a$ and $b$ of encodable types, the encoding of the dependent pair $\langle a, b \rangle$ in $\Sigma \gamma$ is given by $\text{encode}(\langle a, b \rangle) = \text{pair}(\text{encode}(a), \text{encode}(b))$, where $\text{pair}$ is a pairing function on natural numbers.
Encodable.Prod.encodable instance
: Encodable (α × β)
Full source 
/-- If `α` and `β` are encodable, then so is their product. -/
instance Prod.encodable : Encodable (α × β) :=
  ofEquiv _ (Equiv.sigmaEquivProd α β).symm
Encodability of Product Types
Informal description
For any two encodable types $\alpha$ and $\beta$, their product $\alpha \times \beta$ is also encodable. The encoding function for the product is given by pairing the encodings of the components, and the decoding function unpairs the natural number and decodes each component separately.
Encodable.decode_prod_val theorem
(n : ℕ) : (@decode (α × β) _ n : Option (α × β)) = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Prod.mk a
Full source 
@[simp]
theorem decode_prod_val (n : ℕ) :
    (@decode (α × β) _ n : Option (α × β))
      = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Prod.mk a := by
  simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
  cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
  <;> rfl
Decoding of Product Types via Unpairing
Informal description
For any natural number $n$, the decoding function for the product type $\alpha \times \beta$ satisfies \[ \text{decode}(n) = \text{bind}\ (\text{decode}\ (\text{unpair}_1\ n))\ \left(\lambda a,\ \text{map}\ (\text{Prod.mk}\ a)\ (\text{decode}\ (\text{unpair}_2\ n))\right), \] where: - $\text{unpair}_1$ and $\text{unpair}_2$ are the first and second projections of the unpairing function on natural numbers, - $\text{bind}$ is the monadic bind operation for the `Option` type, and - $\text{map}$ is the `Option.map` operation.
Encodable.encode_prod_val theorem
(a b) : @encode (α × β) _ (a, b) = pair (encode a) (encode b)
Full source 
@[simp]
theorem encode_prod_val (a b) : @encode (α × β) _ (a, b) = pair (encode a) (encode b) :=
  rfl
Encoding of Product Elements via Pairing Function
Informal description
For any encodable types $\alpha$ and $\beta$, and any elements $a \in \alpha$ and $b \in \beta$, the encoding of the pair $(a, b)$ in the product type $\alpha \times \beta$ is given by $\text{pair}(\text{encode}(a), \text{encode}(b))$, where $\text{pair}$ is a pairing function on natural numbers.
Encodable.encodeSubtype definition
: { a : α // P a } → ℕ
Full source 
/-- Explicit encoding function for a decidable subtype of an encodable type -/
def encodeSubtype : { a : α // P a } → ℕ
  | ⟨v,_⟩ => encode v
Encoding function for decidable subtypes
Informal description
The encoding function for a decidable subtype $\{a : \alpha \mid P a\}$ of an encodable type $\alpha$ maps each element $\langle v, \_ \rangle$ of the subtype to the natural number obtained by applying the encoding function of $\alpha$ to $v$.
Encodable.decodeSubtype definition
(v : ℕ) : Option { a : α // P a }
Full source 
/-- Explicit decoding function for a decidable subtype of an encodable type -/
def decodeSubtype (v : ℕ) : Option { a : α // P a } :=
  (decode v).bind fun a => if h : P a then some ⟨a, h⟩ else none
Decoding function for decidable subtypes
Informal description
The decoding function for a decidable subtype $\{a : \alpha \mid P a\}$ of an encodable type $\alpha$ takes a natural number $v$ and returns an optional element of the subtype. It first decodes $v$ to an optional element of $\alpha$, then checks if the decoded element satisfies the predicate $P$. If it does, it returns the element as a term of the subtype; otherwise, it returns `none`.
Subtype.encodable instance
: Encodable { a : α // P a }
Full source 
/-- A decidable subtype of an encodable type is encodable. -/
instance _root_.Subtype.encodable : Encodable { a : α // P a } :=
  ⟨encodeSubtype, decodeSubtype, fun ⟨v, h⟩ => by simp [encodeSubtype, decodeSubtype, encodek, h]⟩
Encodability of Decidable Subtypes
Informal description
For any encodable type $\alpha$ and decidable predicate $P$ on $\alpha$, the subtype $\{a : \alpha \mid P a\}$ is also encodable. The encoding function for the subtype is inherited from $\alpha$, and the decoding function checks whether the decoded element satisfies $P$ before returning it.
Encodable.Subtype.encode_eq theorem
(a : Subtype P) : encode a = encode a.val
Full source 
theorem Subtype.encode_eq (a : Subtype P) : encode a = encode a.val := by cases a; rfl
Encoding Equality for Subtype Elements: $\text{encode}(a) = \text{encode}(a.\text{val})$
Informal description
For any element $a$ of a decidable subtype $\{x : \alpha \mid P x\}$ of an encodable type $\alpha$, the encoding of $a$ is equal to the encoding of its underlying value $a.val$ in $\alpha$.
Fin.encodable instance
(n) : Encodable (Fin n)
Full source 
instance _root_.Fin.encodable (n) : Encodable (Fin n) :=
  ofEquiv _ Fin.equivSubtype
Encodability of Finite Ordinals
Informal description
For any natural number $n$, the type $\mathrm{Fin}(n)$ of finite ordinals less than $n$ is encodable. The encoding function maps each element of $\mathrm{Fin}(n)$ to its underlying natural number representation, and the decoding function checks that the decoded number is less than $n$ before returning it.
Int.encodable instance
: Encodable ℤ
Full source 
instance _root_.Int.encodable : Encodable ℤ :=
  ofEquiv _ Equiv.intEquivNat
Encodable Structure on Integers
Informal description
The integers $\mathbb{Z}$ form an encodable type, where there exists an explicit encoding function $\text{encode} : \mathbb{Z} \to \mathbb{N}$ with a partial inverse $\text{decode} : \mathbb{N} \to \text{Option } \mathbb{Z}$.
PNat.encodable instance
: Encodable ℕ+
Full source 
instance _root_.PNat.encodable : Encodable ℕ+ :=
  ofEquiv _ Equiv.pnatEquivNat
Encodable Structure on Positive Natural Numbers
Informal description
The type of positive natural numbers $\mathbb{N}^+$ is encodable, with the encoding function $\text{encode} : \mathbb{N}^+ \to \mathbb{N}$ defined as the inclusion map and the decoding function $\text{decode} : \mathbb{N} \to \text{Option } \mathbb{N}^+$ mapping each natural number $n$ to $\text{some}(n)$ if $n \geq 1$ and $\text{none}$ otherwise.
ULift.encodable instance
[Encodable α] : Encodable (ULift α)
Full source 
/-- The lift of an encodable type is encodable -/
instance _root_.ULift.encodable [Encodable α] : Encodable (ULift α) :=
  ofEquiv _ Equiv.ulift
Encodability of Universe-Lifted Types
Informal description
For any encodable type $\alpha$, the lifted type $\text{ULift}\,\alpha$ (which lives in a higher universe) is also encodable. The encoding and decoding functions for $\text{ULift}\,\alpha$ are naturally induced from those of $\alpha$.
PLift.encodable instance
[Encodable α] : Encodable (PLift α)
Full source 
/-- The lift of an encodable type is encodable. -/
instance _root_.PLift.encodable [Encodable α] : Encodable (PLift α) :=
  ofEquiv _ Equiv.plift
Encodability of Universe-Lifted Types
Informal description
For any encodable type $\alpha$, the lifted type $\text{PLift}\,\alpha$ is also encodable. Here, $\text{PLift}\,\alpha$ is a type in a lower universe that is equivalent to $\alpha$.
Encodable.ofInj definition
[Encodable β] (f : α → β) (hf : Injective f) : Encodable α
Full source 
/-- If `β` is encodable and there is an injection `f : α → β`, then `α` is encodable as well. -/
noncomputable def ofInj [Encodable β] (f : α → β) (hf : Injective f) : Encodable α :=
  ofLeftInjection f (partialInv f) fun _ => (partialInv_of_injective hf _ _).2 rfl
Encodability via injective function
Informal description
Given an encodable type $\beta$ and an injective function $f : \alpha \to \beta$, the type $\alpha$ is also encodable. The encoding function for $\alpha$ is defined as $\text{encode}(a) = \text{encode}(f(a))$, and the decoding function is obtained by composing the decoding function of $\beta$ with a partial inverse of $f$.
Encodable.ofCountable definition
(α : Type*) [Countable α] : Encodable α
Full source 
/-- If `α` is countable, then it has a (non-canonical) `Encodable` structure. -/
noncomputable def ofCountable (α : Type*) [Countable α] : Encodable α :=
  Nonempty.some <|
    let ⟨f, hf⟩ := exists_injective_nat α
    ⟨ofInj f hf⟩
Encodable structure from countability
Informal description
Given a countable type $\alpha$, there exists an encodable structure on $\alpha$. This is constructed by using an injective function from $\alpha$ to $\mathbb{N}$ to define the encoding and decoding functions.
nonempty_encodable theorem
(α : Type*) [Countable α] : Nonempty (Encodable α)
Full source 
/-- See also `nonempty_fintype`, `nonempty_denumerable`. -/
theorem nonempty_encodable (α : Type*) [Countable α] : Nonempty (Encodable α) :=
  ⟨Encodable.ofCountable _⟩
Existence of Encodable Structure for Countable Types
Informal description
For any countable type $\alpha$, there exists an encodable structure on $\alpha$.
instCountablePNat instance
: Countable ℕ+
Full source 
instance : Countable ℕ+ := by delta PNat; infer_instance
Countability of Positive Natural Numbers
Informal description
The type of positive natural numbers $\mathbb{N}^+$ is countable.
ULower definition
(α : Type*) [Encodable α] : Type
Full source 
/-- `ULower α : Type` is an equivalent type in the lowest universe, given `Encodable α`. -/
def ULower (α : Type*) [Encodable α] : Type :=
  Set.range (Encodable.encode : α → ℕ)
Lowest universe equivalent of an encodable type
Informal description
Given an encodable type $\alpha$, the type `ULower α` is an equivalent type living in the lowest universe, represented as a subtype of $\mathbb{N}$ consisting of the range of the encoding function $\text{encode} : \alpha \to \mathbb{N}$.
instDecidableEqULower instance
{α : Type*} [Encodable α] : DecidableEq (ULower α)
Full source 
instance {α : Type*} [Encodable α] : DecidableEq (ULower α) := by
  delta ULower; exact Encodable.decidableEqOfEncodable _
Decidable Equality for the Lowest Universe Equivalent of an Encodable Type
Informal description
For any encodable type $\alpha$, the equality relation on its lowest universe equivalent `ULower α` is decidable. That is, there exists an algorithm that, given any two elements $a, b \in \text{ULower } \alpha$, can determine whether $a = b$ holds or not.
instEncodableULower instance
{α : Type*} [Encodable α] : Encodable (ULower α)
Full source 
instance {α : Type*} [Encodable α] : Encodable (ULower α) := by
  delta ULower; infer_instance
Encodability of the Lowest Universe Equivalent Type
Informal description
For any encodable type $\alpha$, its lowest universe equivalent `ULower α` is also encodable. The encoding function for `ULower α` is inherited from the encoding function of $\alpha$, and the decoding function checks whether the decoded element belongs to the range of the encoding function before returning it.
ULower.equiv definition
: α ≃ ULower α
Full source 
/-- The equivalence between the encodable type `α` and `ULower α : Type`. -/
def equiv : α ≃ ULower α :=
  Encodable.equivRangeEncode α
Equivalence between an encodable type and its lowest universe equivalent
Informal description
The equivalence between an encodable type $\alpha$ and its lowest universe equivalent `ULower α`, which is a subtype of $\mathbb{N}$ representing the range of the encoding function $\text{encode} : \alpha \to \mathbb{N}$. Specifically: - The forward map sends an element $a \in \alpha$ to its encoded form in `ULower α`. - The inverse map reconstructs the original element from its encoded form in `ULower α$. This equivalence ensures that $\alpha$ and `ULower α$ are in bijection, with the encoding and decoding functions preserving this correspondence.
ULower.down definition
(a : α) : ULower α
Full source 
/-- Lowers an `a : α` into `ULower α`. -/
def down (a : α) : ULower α :=
  equiv α a
Lowering an element to its lowest universe equivalent
Informal description
The function maps an element $a$ of an encodable type $\alpha$ to its corresponding element in the lowest universe equivalent `ULower α`, which is a subtype of $\mathbb{N}$ representing the range of the encoding function $\text{encode} : \alpha \to \mathbb{N}$.
ULower.instInhabited instance
[Inhabited α] : Inhabited (ULower α)
Full source 
instance [Inhabited α] : Inhabited (ULower α) :=
  ⟨down default⟩
Inhabitedness of the Lowest Universe Equivalent of an Encodable Type
Informal description
For any inhabited encodable type $\alpha$, its lowest universe equivalent `ULower α` is also inhabited.
ULower.up definition
(a : ULower α) : α
Full source 
/-- Lifts an `a : ULower α` into `α`. -/
def up (a : ULower α) : α :=
  (equiv α).symm a
Lift from `ULower α` to $\alpha$
Informal description
The function maps an element $a$ of the type `ULower α` (the lowest universe equivalent of an encodable type $\alpha$) back to its original form in $\alpha$ using the inverse of the equivalence between $\alpha$ and `ULower α`.
ULower.down_up theorem
{a : ULower α} : down a.up = a
Full source 
@[simp]
theorem down_up {a : ULower α} : down a.up = a :=
  Equiv.right_inv _ _
Identity Property of Lowering after Lifting in `ULower α`
Informal description
For any element $a$ of the type `ULower α` (the lowest universe equivalent of an encodable type $\alpha$), applying the lowering function `down` to the lifted element `a.up` returns $a$ itself. In other words, the composition of lifting and lowering is the identity on `ULower α`.
ULower.up_down theorem
{a : α} : (down a).up = a
Full source 
@[simp]
theorem up_down {a : α} : (down a).up = a := by
  simp [up, down,Equiv.left_inv _ _, Equiv.symm_apply_apply]
Lifting after lowering recovers the original element
Informal description
For any element $a$ of an encodable type $\alpha$, the composition of the lowering and lifting operations returns the original element, i.e., $\text{up}(\text{down}(a)) = a$.
ULower.up_eq_up theorem
{a b : ULower α} : a.up = b.up ↔ a = b
Full source 
@[simp]
theorem up_eq_up {a b : ULower α} : a.up = b.up ↔ a = b :=
  Equiv.apply_eq_iff_eq _
Equality in `ULower α` via Lift to $\alpha$
Informal description
For any two elements $a$ and $b$ of the type `ULower α`, the equality $a.\text{up} = b.\text{up}$ holds if and only if $a = b$.
ULower.down_eq_down theorem
{a b : α} : down a = down b ↔ a = b
Full source 
@[simp]
theorem down_eq_down {a b : α} : downdown a = down b ↔ a = b :=
  Equiv.apply_eq_iff_eq _
Equality Preservation in Lower Universe Encoding
Informal description
For any two elements $a$ and $b$ of an encodable type $\alpha$, the equality of their encodings in `ULower α$ is equivalent to the equality of the original elements, i.e., $\text{down}(a) = \text{down}(b) \leftrightarrow a = b$.
ULower.ext theorem
{a b : ULower α} : a.up = b.up → a = b
Full source 
@[ext]
protected theorem ext {a b : ULower α} : a.up = b.up → a = b :=
  up_eq_up.1
Injectivity of Lift from `ULower α` to $\alpha$
Informal description
For any two elements $a$ and $b$ of the type `ULower α` (the lowest universe equivalent of an encodable type $\alpha$), if their lifts to $\alpha$ are equal ($a.\text{up} = b.\text{up}$), then $a = b$.
Encodable.chooseX definition
(h : ∃ x, p x) : { a : α // p a }
Full source 
/-- Constructive choice function for a decidable subtype of an encodable type. -/
def chooseX (h : ∃ x, p x) : { a : α // p a } :=
  have : ∃ n, good p (decode n) :=
    let ⟨w, pw⟩ := h
    ⟨encode w, by simp [good, encodek, pw]⟩
  match (motive := ∀ o, good p o → { a // p a }) _, Nat.find_spec this with
  | some a, h => ⟨a, h⟩
Constructive choice for decidable predicates on encodable types
Informal description
Given an encodable type $\alpha$ and a decidable predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ such that $p(x)$ holds, then $\text{Encodable.chooseX}$ constructs a specific element $a$ of $\alpha$ along with a proof that $p(a)$ holds. This is achieved by leveraging the encoding and decoding functions of the encodable type to find a suitable element.
Encodable.choose definition
(h : ∃ x, p x) : α
Full source 
/-- Constructive choice function for a decidable predicate over an encodable type. -/
def choose (h : ∃ x, p x) : α :=
  (chooseX h).1
Constructive choice function for encodable types
Informal description
Given an encodable type $\alpha$ and a decidable predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ such that $p(x)$ holds, then $\text{Encodable.choose}$ constructs a specific element $a$ of $\alpha$ satisfying $p(a)$. This is the value component of $\text{Encodable.chooseX}$, without the accompanying proof.
Encodable.choose_spec theorem
(h : ∃ x, p x) : p (choose h)
Full source 
theorem choose_spec (h : ∃ x, p x) : p (choose h) :=
  (chooseX h).2
Constructive Choice Yields Satisfying Element
Informal description
For any encodable type $\alpha$ and decidable predicate $p$ on $\alpha$, if there exists an element $x \in \alpha$ such that $p(x)$ holds, then the element $\text{choose}(h)$ selected by the constructive choice function satisfies $p(\text{choose}(h))$.
Encodable.axiom_of_choice theorem
{α : Type*} {β : α → Type*} {R : ∀ x, β x → Prop} [∀ a, Encodable (β a)] [∀ x y, Decidable (R x y)] (H : ∀ x, ∃ y, R x y) : ∃ f : ∀ a, β a, ∀ x, R x (f x)
Full source 
/-- A constructive version of `Classical.axiom_of_choice` for `Encodable` types. -/
theorem axiom_of_choice {α : Type*} {β : α → Type*} {R : ∀ x, β x → Prop} [∀ a, Encodable (β a)]
    [∀ x y, Decidable (R x y)] (H : ∀ x, ∃ y, R x y) : ∃ f : ∀ a, β a, ∀ x, R x (f x) :=
  ⟨fun x => choose (H x), fun x => choose_spec (H x)⟩
Constructive Axiom of Choice for Encodable Types
Informal description
Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types indexed by $\alpha$. Suppose that for each $a \in \alpha$, the type $\beta(a)$ is encodable, and the relation $R : \forall x, \beta(x) \to \text{Prop}$ is decidable. If for every $x \in \alpha$ there exists $y \in \beta(x)$ such that $R(x, y)$ holds, then there exists a function $f : \forall a, \beta(a)$ such that for every $x \in \alpha$, $R(x, f(x))$ holds.
Encodable.skolem theorem
{α : Type*} {β : α → Type*} {P : ∀ x, β x → Prop} [∀ a, Encodable (β a)] [∀ x y, Decidable (P x y)] : (∀ x, ∃ y, P x y) ↔ ∃ f : ∀ a, β a, ∀ x, P x (f x)
Full source 
/-- A constructive version of `Classical.skolem` for `Encodable` types. -/
theorem skolem {α : Type*} {β : α → Type*} {P : ∀ x, β x → Prop} [∀ a, Encodable (β a)]
    [∀ x y, Decidable (P x y)] : (∀ x, ∃ y, P x y) ↔ ∃ f : ∀ a, β a, ∀ x, P x (f x) :=
  ⟨axiom_of_choice, fun ⟨_, H⟩ x => ⟨_, H x⟩⟩
Constructive Skolem Theorem for Encodable Types
Informal description
Let $\alpha$ be a type and $\beta : \alpha \to \text{Type}$ be a family of types indexed by $\alpha$. Suppose that for each $a \in \alpha$, the type $\beta(a)$ is encodable, and the relation $P : \forall x, \beta(x) \to \text{Prop}$ is decidable. Then the following equivalence holds: for every $x \in \alpha$ there exists $y \in \beta(x)$ such that $P(x, y)$ holds if and only if there exists a function $f : \forall a, \beta(a)$ such that for every $x \in \alpha$, $P(x, f(x))$ holds.
Encodable.encode' definition
(α) [Encodable α] : α ↪ ℕ
Full source 
/-- The `encode` function, viewed as an embedding. -/
def encode' (α) [Encodable α] : α ↪ ℕ :=
  ⟨Encodable.encode, Encodable.encode_injective⟩
Encoding embedding of an encodable type
Informal description
The embedding of an encodable type $\alpha$ into the natural numbers $\mathbb{N}$, given by the encoding function $\text{encode} : \alpha \to \mathbb{N}$, which is injective.
Encodable.instIsAntisymmPreimageNatCoeEmbeddingEncode'Le instance
{α} [Encodable α] : IsAntisymm _ (Encodable.encode' α ⁻¹'o (· ≤ ·))
Full source 
instance {α} [Encodable α] : IsAntisymm _ (Encodable.encode'Encodable.encode' α ⁻¹'o (· ≤ ·)) :=
  (RelEmbedding.preimage _ _).isAntisymm
Antisymmetry of the Preimage Ordering via Encoding
Informal description
For any encodable type $\alpha$, the preimage of the natural number ordering relation $\leq$ under the encoding function $\text{encode} : \alpha \to \mathbb{N}$ is an antisymmetric relation on $\alpha$. That is, for any $x, y \in \alpha$, if $\text{encode}(x) \leq \text{encode}(y)$ and $\text{encode}(y) \leq \text{encode}(x)$, then $x = y$.
Encodable.instIsTotalPreimageNatCoeEmbeddingEncode'Le instance
{α} [Encodable α] : IsTotal _ (Encodable.encode' α ⁻¹'o (· ≤ ·))
Full source 
instance {α} [Encodable α] : IsTotal _ (Encodable.encode'Encodable.encode' α ⁻¹'o (· ≤ ·)) :=
  (RelEmbedding.preimage _ _).isTotal
Total Order Induced by Encoding on an Encodable Type
Informal description
For any encodable type $\alpha$, the preimage of the natural order $\leq$ on $\mathbb{N}$ under the encoding function $\text{encode} : \alpha \to \mathbb{N}$ is a total relation on $\alpha$. That is, for any two elements $x, y \in \alpha$, either $\text{encode}(x) \leq \text{encode}(y)$ or $\text{encode}(y) \leq \text{encode}(x)$ holds.
Directed.sequence definition
{r : β → β → Prop} (f : α → β) (hf : Directed r f) : ℕ → α
Full source 
/-- 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))`. -/
protected noncomputable def sequence {r : β → β → Prop} (f : α → β) (hf : Directed r f) : ℕ → α
  | 0 => default
  | n + 1 =>
    let p := Directed.sequence f hf n
    match (decode n : Option α) with
    | none => Classical.choose (hf p p)
    | some a => Classical.choose (hf p a)
Directed sequence construction for encodable types
Informal description
Given a directed relation $r$ on $\beta$ and a function $f : \alpha \to \beta$ defined on an encodable inhabited type $\alpha$, the sequence $x : \mathbb{N} \to \alpha$ is constructed such that: 1. For any natural number $n$, $r(f(x_n), f(x_{n+1}))$ holds. 2. For any element $a \in \alpha$, $r(f(a), f(x_{\text{encode}(a) + 1}))$ holds. Here, $\text{encode} : \alpha \to \mathbb{N}$ is the encoding function associated with the encodable type $\alpha$, and $\text{decode} : \mathbb{N} \to \text{Option } \alpha$ is its partial inverse.
Directed.sequence_mono_nat theorem
{r : β → β → Prop} {f : α → β} (hf : Directed r f) (n : ℕ) : r (f (hf.sequence f n)) (f (hf.sequence f (n + 1)))
Full source 
theorem sequence_mono_nat {r : β → β → Prop} {f : α → β} (hf : Directed r f) (n : ℕ) :
    r (f (hf.sequence f n)) (f (hf.sequence f (n + 1))) := by
  dsimp [Directed.sequence]
  generalize hf.sequence f n = p
  rcases (decode n : Option α) with - | a
  · exact (Classical.choose_spec (hf p p)).1
  · exact (Classical.choose_spec (hf p a)).1
Monotonicity of Directed Sequence for Encodable Types
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $r$, and $f : \alpha \to \beta$ a function such that $r$ is directed with respect to $f$. For any natural number $n$, the relation $r(f(x_n), f(x_{n+1}))$ holds, where $x_n$ is the $n$-th term of the sequence constructed from $f$ and the encoding of $\alpha$.
Directed.rel_sequence theorem
{r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) : r (f a) (f (hf.sequence f (encode a + 1)))
Full source 
theorem rel_sequence {r : β → β → Prop} {f : α → β} (hf : Directed r f) (a : α) :
    r (f a) (f (hf.sequence f (encode a + 1))) := by
  simp only [Directed.sequence, add_eq, Nat.add_zero, encodek, and_self]
  exact (Classical.choose_spec (hf _ a)).2
Directed Sequence Relation for Encodable Types
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $r$, and $f : \alpha \to \beta$ a function such that $r$ is directed with respect to $f$. For any element $a \in \alpha$, the relation $r(f(a), f(x_{\text{encode}(a) + 1}))$ holds, where $x_n$ is the sequence constructed from $f$ and the encoding of $\alpha$.
Directed.sequence_mono theorem
: Monotone (f ∘ hf.sequence f)
Full source 
theorem sequence_mono : Monotone (f ∘ hf.sequence f) :=
  monotone_nat_of_le_succ <| hf.sequence_mono_nat
Monotonicity of the Directed Sequence Composition
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $r$, and $f : \alpha \to \beta$ a function such that $r$ is directed with respect to $f$. The composition $f \circ x$ is monotone, where $x : \mathbb{N} \to \alpha$ is the sequence constructed from $f$ and the encoding of $\alpha$.
Directed.le_sequence theorem
(a : α) : f a ≤ f (hf.sequence f (encode a + 1))
Full source 
theorem le_sequence (a : α) : f a ≤ f (hf.sequence f (encode a + 1)) :=
  hf.rel_sequence a
Directed sequence lower bound property for encodable types
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $\leq$, and $f : \alpha \to \beta$ a function such that $\leq$ is directed with respect to $f$. For any element $a \in \alpha$, we have $f(a) \leq f(x_{\text{encode}(a) + 1})$, where $x_n$ is the sequence constructed from $f$ and the encoding of $\alpha$.
Directed.sequence_anti theorem
: Antitone (f ∘ hf.sequence f)
Full source 
theorem sequence_anti : Antitone (f ∘ hf.sequence f) :=
  antitone_nat_of_succ_le <| hf.sequence_mono_nat
Antitonicity of the Directed Sequence Composition for Encodable Types
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $\leq$, and $f : \alpha \to \beta$ a function such that $\leq$ is directed with respect to $f$. The composition $f \circ x$ is antitone, where $x : \mathbb{N} \to \alpha$ is the sequence constructed from $f$ and the encoding of $\alpha$.
Directed.sequence_le theorem
(a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a
Full source 
theorem sequence_le (a : α) : f (hf.sequence f (Encodable.encode a + 1)) ≤ f a :=
  hf.rel_sequence a
Directed sequence upper bound property for encodable types
Informal description
Let $\alpha$ be an encodable inhabited type, $\beta$ a type with a relation $\leq$, and $f : \alpha \to \beta$ a function such that $\leq$ is directed with respect to $f$. For any element $a \in \alpha$, we have $f(x_{\text{encode}(a) + 1}) \leq f(a)$, where $x_n$ is the sequence constructed from $f$ and the encoding of $\alpha$.
Quotient.rep definition
(q : Quotient s) : α
Full source 
/-- Representative of an equivalence class. This is a computable version of `Quot.out` for a setoid
on an encodable type. -/
def Quotient.rep (q : Quotient s) : α :=
  choose (exists_rep q)
Representative of a quotient class
Informal description
For a given equivalence class $q$ in the quotient type $\text{Quotient } s$ of an encodable type $\alpha$, the function $\text{Quotient.rep}$ selects a representative element from $\alpha$ that belongs to the equivalence class $q$. This is a computable version of selecting a representative from the quotient, leveraging the encodability of $\alpha$.
Quotient.rep_spec theorem
(q : Quotient s) : ⟦q.rep⟧ = q
Full source 
theorem Quotient.rep_spec (q : Quotient s) : ⟦q.rep⟧ = q :=
  choose_spec (exists_rep q)
Quotient Representative Property: $\llbracket \text{rep}(q) \rrbracket = q$
Informal description
For any equivalence class $q$ in the quotient type $\text{Quotient } s$ of an encodable type $\alpha$, the equivalence class of the representative element $\text{Quotient.rep}(q)$ is equal to $q$ itself, i.e., $\llbracket \text{rep}(q) \rrbracket = q$.
encodableQuotient definition
: Encodable (Quotient s)
Full source 
/-- The quotient of an encodable space by a decidable equivalence relation is encodable. -/
def encodableQuotient : Encodable (Quotient s) :=
  ⟨fun q => encode q.rep, fun n => Quotient.mk'' <$> decode n, by
    rintro ⟨l⟩; dsimp; rw [encodek]; exact congr_arg some ⟦l⟧.rep_spec⟩
Encodable Quotient of an Encodable Type
Informal description
The quotient of an encodable type $\alpha$ by a decidable equivalence relation is itself encodable. Specifically, there exists an encoding function $\text{encode} : \text{Quotient } s \to \mathbb{N}$ defined by encoding a representative of each equivalence class, and a decoding function $\text{decode} : \mathbb{N} \to \text{Option } (\text{Quotient } s)$ that attempts to decode a natural number into an equivalence class via a representative. The encoding and decoding functions are partial inverses of each other.