Encodable.decode_ofEquiv
theorem Encodable.decode_ofEquiv :
∀ {α : Type u_3} {β : Type u_4} [inst : Encodable α] (e : β ≃ α) (n : ℕ),
Encodable.decode n = Option.map (⇑e.symm) (Encodable.decode n)
The theorem `Encodable.decode_ofEquiv` states that for any types `α` and `β`, given that `α` is encodable and there is an equivalence `e` between `β` and `α`, for any natural number `n`, decoding `n` as an `α` and then mapping the inverse of `e` over the result is the same as just decoding `n` directly. In other words, it ensures that the decoding process respects the provided equivalence between the two types. This theorem essentially states that the decoding operation is invariant under applying the equivalence.
More concisely: For any encodable types `α` and `β` with an equivalence `e`, decoding a natural number `n` as `α` and applying `e.symm` to the result is equivalent to directly decoding `n` as `β`.
|
Encodable.decode_prod_val
theorem Encodable.decode_prod_val :
∀ {α : Type u_1} {β : Type u_2} [inst : Encodable β] [i : Encodable α] (n : ℕ),
Encodable.decode n =
(Encodable.decode n.unpair.1).bind fun a => Option.map (Prod.mk a) (Encodable.decode n.unpair.2)
The theorem `Encodable.decode_prod_val` states that for any two encodable types `α` and `β`, and for any natural number `n`, the decoding of `n` is equivalent to first unpacking `n` into a pair of natural numbers, then decoding the first element of the pair to get an optional `α` value, and if it exists, mapping it to a pair with the decoding of the second element of the pair, otherwise resulting in `none`. In other words, it is encoding a pair of values in a specific way that involves both elements of the pair.
More concisely: For any encodable types `α` and `β`, the decoding of a natural number `n` for a product type `α × β` is equivalent to optionally decoding an `α` value from the first `n` bits and pairing it with the decoding of the remaining `n` bits as a `β` value.
|
Encodable.axiom_of_choice
theorem Encodable.axiom_of_choice :
∀ {α : Type u_1} {β : α → Type u_2} {R : (x : α) → β x → Prop} [inst : (a : α) → Encodable (β a)]
[inst : (x : α) → (y : β x) → Decidable (R x y)], (∀ (x : α), ∃ y, R x y) → ∃ f, ∀ (x : α), R x (f x)
This theorem is a constructive version of the 'axiom of choice' for types that can be encoded (`Encodable` types) in Lean 4. It states that for any types `α` and `β`, where `β` is a type dependent on `α`, and a rule `R` that takes an element of `α` and an element of `β` related to it, if every element of `α` has an associated element of `β` such that the rule `R` holds, then there exists a function `f` from `α` to `β` such that, for every element of `α`, the rule `R` holds for it and its image under `f`. This theorem is applicable when each `β a` is encodable for any `a` in `α`, and the rule `R` is decidable for any pair of elements from `α` and `β`.
More concisely: If every element of an `Encodable` type `α` has a related element in another type `β` such that a decidable rule `R` holds between them, then there exists a function `f` from `α` to `β` satisfying `R(x, f x)` for all `x` in `α`.
|
nonempty_encodable
theorem nonempty_encodable : ∀ (α : Type u_1) [inst : Countable α], Nonempty (Encodable α)
This theorem, called `nonempty_encodable`, states that for any type `α` that is countable (i.e., there exists a bijection from the set of natural numbers to `α`), there exists an encoding (an explicit, constructive way of representing elements of `α` as natural numbers). In other words, if you can establish a one-to-one correspondence between the set of natural numbers and any type `α`, then you can ensure that the elements of `α` can be represented as natural numbers.
More concisely: If `α` is a countable type, then there exists a function that encodes elements of `α` as natural numbers.
|
Encodable.skolem
theorem Encodable.skolem :
∀ {α : Type u_1} {β : α → Type u_2} {P : (x : α) → β x → Prop} [inst : (a : α) → Encodable (β a)]
[inst : (x : α) → (y : β x) → Decidable (P x y)], (∀ (x : α), ∃ y, P x y) ↔ ∃ f, ∀ (x : α), P x (f x)
This theorem, named `Encodable.skolem`, is a constructive version of Skolem's Theorem for encodable types. Given a type `α`, a dependent type `β` indexed by `α`, and an encoding for each type `β a` for `a : α`, it asserts that for a given property `P` that relates an element of `α` to an element of `β`, the statement "for all `x` in `α`, there exists `y` in `β x` such that `P x y` is true" is equivalent to "there exists a function `f` from `α` to `β` such that for all `x` in `α`, `P x (f x)` is true". This theorem assumes that the truth of `P x y` is decidable for any `x : α` and `y : β x`.
More concisely: Given an encodable type `α` and dependent type `β`, if for all `x : α` and `y : β x`, the predicate `P x y` is decidably propositional, then the existence of a function `f : α -> β` such that `P x (f x)` holds for all `x` is equivalent to the universal quantification of the existence of `y` in `β x` satisfying `P x y`.
|
Encodable.encodek
theorem Encodable.encodek :
∀ {α : Type u_1} [self : Encodable α] (a : α), Encodable.decode (Encodable.encode a) = some a
This theorem, `Encodable.encodek`, states that for every type `α` that has an encoding (`Encodable α`), for any element `a` of that type, if you encode `a` into a natural number using `Encodable.encode` and then decode it back using `Encodable.decode`, you will always retrieve `a` back. In other words, the encoding and decoding processes are inverse operations for any given `a` of type `α`. This ensures that no information is lost during encoding and decoding.
More concisely: For any `Encodable` type `α` and its element `a`, the encoding and decoding functions `Encodable.encode` and `Encodable.decode` form an inverse pair, i.e., `Encodable.decode (Encodable.encode a) = a`.
|
Encodable.mem_decode₂
theorem Encodable.mem_decode₂ :
∀ {α : Type u_1} [inst : Encodable α] {n : ℕ} {a : α}, a ∈ Encodable.decode₂ α n ↔ Encodable.encode a = n := by
sorry
This theorem states that for any type `α` that is encodable, a given natural number `n`, and an element `a` of type `α`, the element `a` is in the result of decoding `n` with the failsafe variant `decode₂` if and only if `n` is the result of encoding `a`. In other words, the encoding of `a` results in `n` if and only if `n` can be safely decoded back into `a`. This forms a kind of "round trip" property for the encoding and failsafe decoding operations: encoding an element and then decoding it returns the original element.
More concisely: For any encodable type `α`, the encoding of `a : α` equals the natural number `n` if and only if `a` is the result of decoding `n` using `decode₂`.
|
Encodable.encode_injective
theorem Encodable.encode_injective : ∀ {α : Type u_1} [inst : Encodable α], Function.Injective Encodable.encode := by
sorry
This theorem, `Encodable.encode_injective`, states that for any type `α` which has an `Encodable` instance, the `encode` function from this `Encodable` instance is injective. In mathematical terms, this means that if we have two elements `x` and `y` of type `α`, and if `Encodable.encode x = Encodable.encode y`, then `x = y`. That is, no two distinct elements of type `α` will be mapped to the same natural number by the `encode` function, ensuring the uniqueness of the encoding for each element.
More concisely: For any type `α` with an `Encodable` instance, the `encode` function is a bijection from `α` to its image under `encode`. (In other words, `encode` is both injective and surjective.)
|
Encodable.encodek₂
theorem Encodable.encodek₂ :
∀ {α : Type u_1} [inst : Encodable α] (a : α), Encodable.decode₂ α (Encodable.encode a) = some a
The theorem `Encodable.encodek₂` states that for any type `α` that has an `Encodable` instance and any element `a` of type `α`, when we encode `a` into a natural number and then decode it back using the failsafe decoding method `decode₂`, we get back the original element `a`. In other words, the encoding and subsequent failsafe decoding of an element from an encodable type `α` form an identity operation, showing that the encoding-decoding process is lossless for given element of `α`.
More concisely: For any encodable type `α` and element `a` of type `α`, the failsafe decoding of the encoding of `a` is equal to `a`.
|